kbuzzard

import data.real.irrational
import tactic

open real

example : irrational (sqrt 2) :=
begin
  rintro ⟨q, hq⟩,
  have hqnum : 0 ≤ q.num,
  { rw rat.num_nonneg_iff_zero_le,

kbuzzard

-- See https://github.com/leanprover-community/mathlib4/blob/489f10454a7ae53fdc6a95d2ac237cbc20e69b36/Mathlib/Algebra/Order/Positive/Field.lean#L42-L46
-- for the actual mathlib problem, which is even slower

universe u

class Preorder (α : Type u) extends LE α, LT α where
  le_refl : ∀ a : α, a ≤ a
  le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c
  lt := λ a b => a ≤ b ∧ ¬ b ≤ a
  lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) := by intros; rfl

kbuzzard

-- see https://github.com/leanprover-community/mathlib4/pull/1099#discussion_r1051747996
import Mathlib.Mathport.Notation -- I don't understand this file well enough to remove it, but it's only notation

set_option autoImplicit false

universe u v

instance {ι : Type u} {α : ι → Type v} [∀ i, LE (α i)] : LE (∀ i, α i) where
  le x y := ∀ i, x i ≤ y i

kbuzzard

import tactic -- a bunch of tactics
import ring_theory.noetherian -- Noetherian rings
/-

# Using ideals in Lean

Throughout, `R` is a commutative ring.

## The type of ideals of a ring

kbuzzard

import geometry.euclidean.monge_point

-- let's look at the definition of the monge point of a simplex.

/-
We don't have an explicit definition of `euler_line`, but 
`affine_span ℝ {s.circumcenter, (univ : finset (fin (n + 1))).centroid ℝ s.points}` 
seems like a reasonable definition to go in `geometry.euclidean.monge_point` 
for the Euler line of a simplex. It should then be straightforward to prove that
 this really is a line (i.e., its `direction` has `finrank` equal to 1) if the 

kbuzzard

@is_scalar_tower 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
  (@smul_with_zero.to_has_scalar 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
     (@mul_zero_class.to_has_zero 𝕜
        (@mul_zero_one_class.to_mul_zero_class 𝕜
           (@monoid_with_zero.to_mul_zero_one_class 𝕜
              (@semiring.to_monoid_with_zero 𝕜
                 (@comm_semiring.to_semiring 𝕜
                    (@comm_ring.to_comm_semiring 𝕜
                       (@semi_normed_comm_ring.to_comm_ring 𝕜
                          (@normed_comm_ring.to_semi_normed_comm_ring 𝕜

kbuzzard

universe u

set_option old_structure_cmd true

/- 0,+ -/
class add_zero_class (M : Type u) extends has_zero M, has_add M :=
(zero_add : ∀ (a : M), 0 + a = a)
(add_zero : ∀ (a : M), a + 0 = a)

class add_semigroup (G : Type u) extends has_add G :=

kbuzzard

universe u

set_option old_structure_cmd true

/- 0,+ -/
class add_zero_class (M : Type u) extends has_zero M, has_add M :=
(zero_add : ∀ (a : M), 0 + a = a)
(add_zero : ∀ (a : M), a + 0 = a)

class add_semigroup (G : Type u) extends has_add G :=

kbuzzard

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_3 : has_coe_to_sort
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))) := @category_theory.induced_category.has_coe_to_sort ?x_4 ?x_5 ?x_6 ?x_7 ?x_8
failed is_def_eq
[class_instances] (0) ?x_3 : has_coe_to_sort
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))) := @wide_subquiver_has_coe_to_sort ?x_9 ?x_10
failed is_def_eq
[class_instances] (0) ?x_3 : has_coe_to_sort
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))) := @set.has_coe_to_sort ?x_11
failed is_def_eq

kbuzzard

import tactic
import data.real.basic
/-

# Some puzzles.

1) (easy logic). If `P`, `Q` and `R` are true-false statements, then show
that `(P → (Q → R)) → ((P → Q) → (P → R))` (where `→` means "implies")

2) (group theory) If `G` is a group such that `∀ g, g^2 = 1`