internlm/Lean-Github huggingface dataset:
Theorem: QuadraticForm.Hasse_Minkowski_of_Equivalent
Proof state before:
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q S : QuadraticForm ℚ V
h : Equivalent Q S
⊢ (¬Anisotropic S ↔
      (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ¬Anisotropic (baseChange ℚ_[p] Q)) ∧ ¬Anisotropic (baseChange ℝ Q)) ↔
    (¬Anisotropic S ↔
      (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ¬Anisotropic (baseChange ℚ_[p] S)) ∧ ¬Anisotropic (baseChange ℝ S))
Tactic:
rw [anisotropic_iff _ _ (baseChange.Equivalent ℝ _ _ h)]
Proof state after:
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q S : QuadraticForm ℚ V
h : Equivalent Q S
⊢ (¬Anisotropic S ↔
      (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ¬Anisotropic (baseChange ℚ_[p] Q)) ∧ ¬Anisotropic (baseChange ℝ S)) ↔
    (¬Anisotropic S ↔
      (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ¬Anisotropic (baseChange ℚ_[p] S)) ∧ ¬Anisotropic (baseChange ℝ S))
Theorem: QuadraticForm.Hasse_Minkowski_of_Equivalent
Proof state before:
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q S : QuadraticForm ℚ V
h : Equivalent Q S
⊢ (¬Anisotropic S ↔
      (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ¬Anisotropic (baseChange ℚ_[p] Q)) ∧ ¬Anisotropic (baseChange ℝ S)) ↔
    (¬Anisotropic S ↔
      (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ¬Anisotropic (baseChange ℚ_[p] S)) ∧ ¬Anisotropic (baseChange ℝ S))
Tactic:
conv in (Anisotropic (baseChange _ Q)) =>
  rw [anisotropic_iff _ _ (baseChange.Equivalent (R := ℚ) ℚ_[p] _ _ h)]
Proof state after:
no goals
Theorem: QuadraticForm.HasseMinkowski_of_degenerate
Proof state before:
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
⊢ Hasse_Minkowski Q
Tactic:
sorry
Proof state after:
no goals
Theorem: QuadraticForm.ex
Proof state before:
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 2
hQ : BilinForm.Nondegenerate (↑associated Q)
⊢ Hasse_Minkowski Q
Tactic:
obtain ⟨w, hw1, hw0, hEQ⟩ := equivalent_weightedSumSquares_units_of_nondegenerate'' Q _ h.symm hQ
Proof state after:
case intro.intro.intro
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 2
hQ : BilinForm.Nondegenerate (↑associated Q)
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEQ : Equivalent Q (weightedSumSquares ℚ w)
⊢ Hasse_Minkowski Q
Theorem: C03S02.sumOfSquares_mul
Proof state before:
α : Type u_1
inst✝ : CommRing α
x y : α
sosx : SumOfSquares x
sosy : SumOfSquares y
⊢ SumOfSquares (x * y)
Tactic:
rcases sosx with ⟨a, b, xeq⟩
Proof state after:
case intro.intro
α : Type u_1
inst✝ : CommRing α
x y : α
sosy : SumOfSquares y
a b : α
xeq : x = a ^ 2 + b ^ 2
⊢ SumOfSquares (x * y)
Theorem: C03S02.sumOfSquares_mul
Proof state before:
case intro.intro
α : Type u_1
inst✝ : CommRing α
x y : α
sosy : SumOfSquares y
a b : α
xeq : x = a ^ 2 + b ^ 2
⊢ SumOfSquares (x * y)
Tactic:
rcases sosy with ⟨c, d, yeq⟩
Proof state after:
case intro.intro.intro.intro
α : Type u_1
inst✝ : CommRing α
x y a b : α
xeq : x = a ^ 2 + b ^ 2
c d : α
yeq : y = c ^ 2 + d ^ 2
⊢ SumOfSquares (x * y)
Theorem: C03S02.sumOfSquares_mul
Proof state before:
case intro.intro.intro.intro
α : Type u_1
inst✝ : CommRing α
x y a b : α
xeq : x = a ^ 2 + b ^ 2
c d : α
yeq : y = c ^ 2 + d ^ 2
⊢ SumOfSquares (x * y)
Tactic:
rw [xeq, yeq]
Proof state after:
case intro.intro.intro.intro
α : Type u_1
inst✝ : CommRing α
x y a b : α
xeq : x = a ^ 2 + b ^ 2
c d : α
yeq : y = c ^ 2 + d ^ 2
⊢ SumOfSquares ((a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2))
Theorem: C03S02.sumOfSquares_mul
Proof state before:
case intro.intro.intro.intro
α : Type u_1
inst✝ : CommRing α
x y a b : α
xeq : x = a ^ 2 + b ^ 2
c d : α
yeq : y = c ^ 2 + d ^ 2
⊢ SumOfSquares ((a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2))
Tactic:
use a * c - b * d, a * d + b * c
Proof state after:
case h
α : Type u_1
inst✝ : CommRing α
x y a b : α
xeq : x = a ^ 2 + b ^ 2
c d : α
yeq : y = c ^ 2 + d ^ 2
⊢ (a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2) = (a * c - b * d) ^ 2 + (a * d + b * c) ^ 2
Theorem: C03S02.sumOfSquares_mul
Proof state before:
case h
α : Type u_1
inst✝ : CommRing α
x y a b : α
xeq : x = a ^ 2 + b ^ 2
c d : α
yeq : y = c ^ 2 + d ^ 2
⊢ (a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2) = (a * c - b * d) ^ 2 + (a * d + b * c) ^ 2
Tactic:
ring
Proof state after:
no goals
Theorem: C03S02.sumOfSquares_mul'
Proof state before:
α : Type u_1
inst✝ : CommRing α
x y : α
sosx : SumOfSquares x
sosy : SumOfSquares y
⊢ SumOfSquares (x * y)
Tactic:
rcases sosx with ⟨a, b, rfl⟩
Proof state after:
case intro.intro
α : Type u_1
inst✝ : CommRing α
y : α
sosy : SumOfSquares y
a b : α
⊢ SumOfSquares ((a ^ 2 + b ^ 2) * y)
Theorem: C03S02.sumOfSquares_mul'
Proof state before:
case intro.intro
α : Type u_1
inst✝ : CommRing α
y : α
sosy : SumOfSquares y
a b : α
⊢ SumOfSquares ((a ^ 2 + b ^ 2) * y)
Tactic:
rcases sosy with ⟨c, d, rfl⟩
Proof state after:
case intro.intro.intro.intro
α : Type u_1
inst✝ : CommRing α
a b c d : α
⊢ SumOfSquares ((a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2))
Theorem: C03S02.sumOfSquares_mul'
Proof state before:
case intro.intro.intro.intro
α : Type u_1
inst✝ : CommRing α
a b c d : α
⊢ SumOfSquares ((a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2))
Tactic:
use a * c - b * d, a * d + b * c
Proof state after:
case h
α : Type u_1
inst✝ : CommRing α
a b c d : α
⊢ (a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2) = (a * c - b * d) ^ 2 + (a * d + b * c) ^ 2
Theorem: C03S02.sumOfSquares_mul'
Proof state before:
case h
α : Type u_1
inst✝ : CommRing α
a b c d : α
⊢ (a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2) = (a * c - b * d) ^ 2 + (a * d + b * c) ^ 2
Tactic:
ring
Proof state after:
no goals
Theorem: C03S01.my_lemma3
Proof state before:
⊢ ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε
Tactic:
intro x y ε epos ele1 xlt ylt
Proof state after:
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ |x * y| < ε
Theorem: C03S01.my_lemma3
Proof state before:
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ |x * y| < ε
Tactic:
sorry
Proof state after:
no goals
Theorem: C03S01.my_lemma4
Proof state before:
⊢ ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε
Tactic:
intro x y ε epos ele1 xlt ylt
Proof state after:
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ |x * y| < ε
Theorem: C03S01.my_lemma4
Proof state before:
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ |x * y| < ε
Tactic:
calc
  |x * y| = |x| * |y| := by apply abs_mul
  _ ≤ |x| * ε := by apply mul_le_mul; linarith; linarith; apply abs_nonneg; apply abs_nonneg;
  _ < 1 * ε := by rw [mul_lt_mul_right epos]; linarith
  _ = ε := by apply one_mul
Proof state after:
no goals
Theorem: C03S01.my_lemma4
Proof state before:
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ |x * y| = |x| * |y|
Tactic:
apply abs_mul
Proof state after:
no goals
Theorem: C03S01.my_lemma4
Proof state before:
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ |x| * |y| ≤ |x| * ε
Tactic:
apply mul_le_mul
Proof state after:
case h₁
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ |x| ≤ |x|

case h₂
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ |y| ≤ ε

case c0
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ 0 ≤ |y|

case b0
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ 0 ≤ |x|
Theorem: C03S01.my_lemma4
Proof state before:
case h₁
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ |x| ≤ |x|

case h₂
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ |y| ≤ ε

case c0
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ 0 ≤ |y|

case b0
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ 0 ≤ |x|
Tactic:
linarith
Proof state after:
case h₂
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ |y| ≤ ε

case c0
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ 0 ≤ |y|

case b0
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ 0 ≤ |x|
Theorem: C03S01.my_lemma4
Proof state before:
case h₂
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ |y| ≤ ε

case c0
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ 0 ≤ |y|

case b0
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ 0 ≤ |x|
Tactic:
linarith
Proof state after:
case c0
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ 0 ≤ |y|

case b0
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ 0 ≤ |x|
Theorem: C03S01.my_lemma4
Proof state before:
case c0
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ 0 ≤ |y|

case b0
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ 0 ≤ |x|
Tactic:
apply abs_nonneg
Proof state after:
case b0
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ 0 ≤ |x|
Theorem: C03S01.my_lemma4
Proof state before:
case b0
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ 0 ≤ |x|
Tactic:
apply abs_nonneg
Proof state after:
no goals
Theorem: C03S01.my_lemma4
Proof state before:
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ |x| * ε < 1 * ε
Tactic:
rw [mul_lt_mul_right epos]
Proof state after:
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ |x| < 1
Theorem: C03S01.my_lemma4
Proof state before:
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ |x| < 1
Tactic:
linarith
Proof state after:
no goals
Theorem: C03S01.my_lemma4
Proof state before:
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ 1 * ε = ε
Tactic:
apply one_mul
Proof state after:
no goals
Theorem: C03S01.Subset.trans
Proof state before:
α : Type u_1
r s t : Set α
⊢ r ⊆ s → s ⊆ t → r ⊆ t
Tactic:
sorry
Proof state after:
no goals
Theorem: C02S04.aux
Proof state before:
a b c d : ℝ
⊢ min a b + c ≤ min (a + c) (b + c)
Tactic:
apply le_min
Proof state after:
case h₁
a b c d : ℝ
⊢ min a b + c ≤ a + c

case h₂
a b c d : ℝ
⊢ min a b + c ≤ b + c
Theorem: C02S04.aux
Proof state before:
case h₂
a b c d : ℝ
⊢ min a b + c ≤ b + c
Tactic:
apply add_le_add_right
Proof state after:
case h₂.bc
a b c d : ℝ
⊢ min a b ≤ b
Theorem: C02S04.aux
Proof state before:
case h₂.bc
a b c d : ℝ
⊢ min a b ≤ b
Tactic:
apply min_le_right
Proof state after:
no goals
Theorem: C02S04.aux
Proof state before:
case h₁
a b c d : ℝ
⊢ min a b + c ≤ a + c
Tactic:
apply add_le_add_right
Proof state after:
case h₁.bc
a b c d : ℝ
⊢ min a b ≤ a
Theorem: C02S04.aux
Proof state before:
case h₁.bc
a b c d : ℝ
⊢ min a b ≤ a
Tactic:
apply min_le_left
Proof state after:
no goals
Theorem: Int.div'_add_mod'
Proof state before:
a b : ℤ
⊢ b * a.div' b + a.mod' b = a
Tactic:
rw [div', mod']
Proof state after:
a b : ℤ
⊢ b * ((a + b / 2) / b) + ((a + b / 2) % b - b / 2) = a
Theorem: Int.div'_add_mod'
Proof state before:
a b : ℤ
⊢ b * ((a + b / 2) / b) + ((a + b / 2) % b - b / 2) = a
Tactic:
linarith [Int.ediv_add_emod (a + b / 2) b]
Proof state after:
no goals
Theorem: Int.abs_mod'_le
Proof state before:
a b : ℤ
h : 0 < b
⊢ |a.mod' b| ≤ b / 2
Tactic:
rw [mod', abs_le]
Proof state after:
a b : ℤ
h : 0 < b
⊢ -(b / 2) ≤ (a + b / 2) % b - b / 2 ∧ (a + b / 2) % b - b / 2 ≤ b / 2
Theorem: Int.abs_mod'_le
Proof state before:
a b : ℤ
h : 0 < b
⊢ -(b / 2) ≤ (a + b / 2) % b - b / 2 ∧ (a + b / 2) % b - b / 2 ≤ b / 2
Tactic:
constructor
Proof state after:
case left
a b : ℤ
h : 0 < b
⊢ -(b / 2) ≤ (a + b / 2) % b - b / 2

case right
a b : ℤ
h : 0 < b
⊢ (a + b / 2) % b - b / 2 ≤ b / 2
Theorem: Int.abs_mod'_le
Proof state before:
case right
a b : ℤ
h : 0 < b
⊢ (a + b / 2) % b - b / 2 ≤ b / 2
Tactic:
have := Int.emod_lt_of_pos (a + b / 2) h
Proof state after:
case right
a b : ℤ
h : 0 < b
this : (a + b / 2) % b < b
⊢ (a + b / 2) % b - b / 2 ≤ b / 2
Theorem: Int.abs_mod'_le
Proof state before:
case right
a b : ℤ
h : 0 < b
this : (a + b / 2) % b < b
⊢ (a + b / 2) % b - b / 2 ≤ b / 2
Tactic:
have := Int.ediv_add_emod b 2
Proof state after:
case right
a b : ℤ
h : 0 < b
this✝ : (a + b / 2) % b < b
this : 2 * (b / 2) + b % 2 = b
⊢ (a + b / 2) % b - b / 2 ≤ b / 2
Theorem: Int.abs_mod'_le
Proof state before:
case right
a b : ℤ
h : 0 < b
this✝ : (a + b / 2) % b < b
this : 2 * (b / 2) + b % 2 = b
⊢ (a + b / 2) % b - b / 2 ≤ b / 2
Tactic:
have := Int.emod_lt_of_pos b zero_lt_two
Proof state after:
case right
a b : ℤ
h : 0 < b
this✝¹ : (a + b / 2) % b < b
this✝ : 2 * (b / 2) + b % 2 = b
this : b % 2 < 2
⊢ (a + b / 2) % b - b / 2 ≤ b / 2
Theorem: Int.abs_mod'_le
Proof state before:
case right
a b : ℤ
h : 0 < b
this✝¹ : (a + b / 2) % b < b
this✝ : 2 * (b / 2) + b % 2 = b
this : b % 2 < 2
⊢ (a + b / 2) % b - b / 2 ≤ b / 2
Tactic:
revert this
Proof state after:
case right
a b : ℤ
h : 0 < b
this✝ : (a + b / 2) % b < b
this : 2 * (b / 2) + b % 2 = b
⊢ b % 2 < 2 → (a + b / 2) % b - b / 2 ≤ b / 2
Theorem: Int.abs_mod'_le
Proof state before:
case right
a b : ℤ
h : 0 < b
this✝ : (a + b / 2) % b < b
this : 2 * (b / 2) + b % 2 = b
⊢ b % 2 < 2 → (a + b / 2) % b - b / 2 ≤ b / 2
Tactic:
intro this
Proof state after:
case right
a b : ℤ
h : 0 < b
this✝¹ : (a + b / 2) % b < b
this✝ : 2 * (b / 2) + b % 2 = b
this : b % 2 < 2
⊢ (a + b / 2) % b - b / 2 ≤ b / 2
Theorem: Int.abs_mod'_le
Proof state before:
case right
a b : ℤ
h : 0 < b
this✝¹ : (a + b / 2) % b < b
this✝ : 2 * (b / 2) + b % 2 = b
this : b % 2 < 2
⊢ (a + b / 2) % b - b / 2 ≤ b / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: Int.abs_mod'_le
Proof state before:
case left
a b : ℤ
h : 0 < b
⊢ -(b / 2) ≤ (a + b / 2) % b - b / 2
Tactic:
linarith [Int.emod_nonneg (a + b / 2) h.ne']
Proof state after:
no goals
Theorem: Int.mod'_eq
Proof state before:
a b : ℤ
⊢ a.mod' b = a - b * a.div' b
Tactic:
linarith [div'_add_mod' a b]
Proof state after:
no goals
Theorem: aux
Proof state before:
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : x ^ 2 + y ^ 2 = 0
⊢ x ^ 2 = 0
Tactic:
apply le_antisymm _ (sq_nonneg x)
Proof state after:
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : x ^ 2 + y ^ 2 = 0
⊢ x ^ 2 ≤ 0
Theorem: aux
Proof state before:
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : x ^ 2 + y ^ 2 = 0
⊢ x ^ 2 ≤ 0
Tactic:
rw [← h]
Proof state after:
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : x ^ 2 + y ^ 2 = 0
⊢ x ^ 2 ≤ x ^ 2 + y ^ 2
Theorem: aux
Proof state before:
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : x ^ 2 + y ^ 2 = 0
⊢ x ^ 2 ≤ x ^ 2 + y ^ 2
Tactic:
apply le_add_of_nonneg_right (sq_nonneg y)
Proof state after:
no goals
Theorem: sq_add_sq_eq_zero
Proof state before:
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
⊢ x ^ 2 + y ^ 2 = 0 ↔ x = 0 ∧ y = 0
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
⊢ x ^ 2 + y ^ 2 = 0 → x = 0 ∧ y = 0

case mpr
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
⊢ x = 0 ∧ y = 0 → x ^ 2 + y ^ 2 = 0
Theorem: sq_add_sq_eq_zero
Proof state before:
case mpr
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
⊢ x = 0 ∧ y = 0 → x ^ 2 + y ^ 2 = 0
Tactic:
rintro ⟨rfl, rfl⟩
Proof state after:
case mpr.intro
α : Type u_1
inst✝ : LinearOrderedRing α
⊢ 0 ^ 2 + 0 ^ 2 = 0
Theorem: sq_add_sq_eq_zero
Proof state before:
case mpr.intro
α : Type u_1
inst✝ : LinearOrderedRing α
⊢ 0 ^ 2 + 0 ^ 2 = 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: sq_add_sq_eq_zero
Proof state before:
case mp
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
⊢ x ^ 2 + y ^ 2 = 0 → x = 0 ∧ y = 0
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : x ^ 2 + y ^ 2 = 0
⊢ x = 0 ∧ y = 0
Theorem: sq_add_sq_eq_zero
Proof state before:
case mp
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : x ^ 2 + y ^ 2 = 0
⊢ x = 0 ∧ y = 0
Tactic:
constructor
Proof state after:
case mp.left
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : x ^ 2 + y ^ 2 = 0
⊢ x = 0

case mp.right
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : x ^ 2 + y ^ 2 = 0
⊢ y = 0
Theorem: sq_add_sq_eq_zero
Proof state before:
case mp.right
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : x ^ 2 + y ^ 2 = 0
⊢ y = 0
Tactic:
rw [add_comm] at h
Proof state after:
case mp.right
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : y ^ 2 + x ^ 2 = 0
⊢ y = 0
Theorem: sq_add_sq_eq_zero
Proof state before:
case mp.right
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : y ^ 2 + x ^ 2 = 0
⊢ y = 0
Tactic:
exact aux h
Proof state after:
no goals
Theorem: sq_add_sq_eq_zero
Proof state before:
case mp.left
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : x ^ 2 + y ^ 2 = 0
⊢ x = 0
Tactic:
exact aux h
Proof state after:
no goals
Theorem: GaussInt.norm_nonneg
Proof state before:
x : GaussInt
⊢ 0 ≤ x.norm
Tactic:
apply add_nonneg <;>
apply sq_nonneg
Proof state after:
no goals
Theorem: GaussInt.norm_eq_zero
Proof state before:
x : GaussInt
⊢ x.norm = 0 ↔ x = 0
Tactic:
rw [norm, sq_add_sq_eq_zero, GaussInt.ext_iff]
Proof state after:
x : GaussInt
⊢ x.re = 0 ∧ x.im = 0 ↔ x.re = re 0 ∧ x.im = im 0
Theorem: GaussInt.norm_eq_zero
Proof state before:
x : GaussInt
⊢ x.re = 0 ∧ x.im = 0 ↔ x.re = re 0 ∧ x.im = im 0
Tactic:
rfl
Proof state after:
no goals
Theorem: GaussInt.norm_pos
Proof state before:
x : GaussInt
⊢ 0 < x.norm ↔ x ≠ 0
Tactic:
rw [lt_iff_le_and_ne, ne_comm, Ne, norm_eq_zero]
Proof state after:
x : GaussInt
⊢ 0 ≤ x.norm ∧ ¬x = 0 ↔ x ≠ 0
Theorem: GaussInt.norm_pos
Proof state before:
x : GaussInt
⊢ 0 ≤ x.norm ∧ ¬x = 0 ↔ x ≠ 0
Tactic:
simp [norm_nonneg]
Proof state after:
no goals
Theorem: GaussInt.norm_mul
Proof state before:
x y : GaussInt
⊢ (x * y).norm = x.norm * y.norm
Tactic:
simp [norm]
Proof state after:
x y : GaussInt
⊢ (x.re * y.re - x.im * y.im) ^ 2 + (x.re * y.im + x.im * y.re) ^ 2 = (x.re ^ 2 + x.im ^ 2) * (y.re ^ 2 + y.im ^ 2)
Theorem: GaussInt.norm_mul
Proof state before:
x y : GaussInt
⊢ (x.re * y.re - x.im * y.im) ^ 2 + (x.re * y.im + x.im * y.re) ^ 2 = (x.re ^ 2 + x.im ^ 2) * (y.re ^ 2 + y.im ^ 2)
Tactic:
ring
Proof state after:
no goals
Theorem: GaussInt.norm_conj
Proof state before:
x : GaussInt
⊢ x.conj.norm = x.norm
Tactic:
simp [norm]
Proof state after:
no goals
Theorem: GaussInt.norm_mod_lt
Proof state before:
x y : GaussInt
hy : y ≠ 0
⊢ (x % y).norm < y.norm
Tactic:
have norm_y_pos : 0 < norm y := by rwa [norm_pos]
Proof state after:
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
⊢ (x % y).norm < y.norm
Theorem: GaussInt.norm_mod_lt
Proof state before:
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
⊢ (x % y).norm < y.norm
Tactic:
have H1 : x % y * conj y = ⟨Int.mod' (x * conj y).re (norm y), Int.mod' (x * conj y).im (norm y)⟩
Proof state after:
case H1
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
⊢ x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }

x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
⊢ (x % y).norm < y.norm
Theorem: GaussInt.norm_mod_lt
Proof state before:
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
⊢ (x % y).norm < y.norm
Tactic:
have H2 : norm (x % y) * norm y ≤ norm y / 2 * norm y
Proof state after:
case H2
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
⊢ (x % y).norm * y.norm ≤ y.norm / 2 * y.norm

x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
H2 : (x % y).norm * y.norm ≤ y.norm / 2 * y.norm
⊢ (x % y).norm < y.norm
Theorem: GaussInt.norm_mod_lt
Proof state before:
x y : GaussInt
hy : y ≠ 0
⊢ 0 < y.norm
Tactic:
rwa [norm_pos]
Proof state after:
no goals
Theorem: GaussInt.norm_mod_lt
Proof state before:
case H1
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
⊢ x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
Tactic:
ext <;> simp [Int.mod'_eq, mod_def, div_def, norm] <;> ring
Proof state after:
no goals
Theorem: GaussInt.norm_mod_lt
Proof state before:
case H2
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
⊢ (x % y).norm * y.norm ≤ y.norm / 2 * y.norm
Tactic:
calc
  norm (x % y) * norm y = norm (x % y * conj y) := by simp only [norm_mul, norm_conj]
  _ = |Int.mod' (x.re * y.re + x.im * y.im) (norm y)| ^ 2
      + |Int.mod' (-(x.re * y.im) + x.im * y.re) (norm y)| ^ 2 := by simp [H1, norm, sq_abs]
  _ ≤ (y.norm / 2) ^ 2 + (y.norm / 2) ^ 2 := by gcongr <;> apply Int.abs_mod'_le _ _ norm_y_pos
  _ = norm y / 2 * (norm y / 2 * 2) := by ring
  _ ≤ norm y / 2 * norm y := by gcongr; apply Int.ediv_mul_le; norm_num
Proof state after:
no goals
Theorem: GaussInt.norm_mod_lt
Proof state before:
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
⊢ (x % y).norm * y.norm = (x % y * y.conj).norm
Tactic:
simp only [norm_mul, norm_conj]
Proof state after:
no goals
Theorem: GaussInt.norm_mod_lt
Proof state before:
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
⊢ (x % y * y.conj).norm =
    |(x.re * y.re + x.im * y.im).mod' y.norm| ^ 2 + |(-(x.re * y.im) + x.im * y.re).mod' y.norm| ^ 2
Tactic:
simp [H1, norm, sq_abs]
Proof state after:
no goals
Theorem: GaussInt.norm_mod_lt
Proof state before:
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
⊢ |(x.re * y.re + x.im * y.im).mod' y.norm| ^ 2 + |(-(x.re * y.im) + x.im * y.re).mod' y.norm| ^ 2 ≤
    (y.norm / 2) ^ 2 + (y.norm / 2) ^ 2
Tactic:
gcongr <;> apply Int.abs_mod'_le _ _ norm_y_pos
Proof state after:
no goals
Theorem: GaussInt.norm_mod_lt
Proof state before:
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
⊢ (y.norm / 2) ^ 2 + (y.norm / 2) ^ 2 = y.norm / 2 * (y.norm / 2 * 2)
Tactic:
ring
Proof state after:
no goals
Theorem: GaussInt.norm_mod_lt
Proof state before:
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
⊢ y.norm / 2 * (y.norm / 2 * 2) ≤ y.norm / 2 * y.norm
Tactic:
gcongr
Proof state after:
case h
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
⊢ y.norm / 2 * 2 ≤ y.norm
Theorem: GaussInt.norm_mod_lt
Proof state before:
case h
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
⊢ y.norm / 2 * 2 ≤ y.norm
Tactic:
apply Int.ediv_mul_le
Proof state after:
case h.H
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
⊢ 2 ≠ 0
Theorem: GaussInt.norm_mod_lt
Proof state before:
case h.H
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
⊢ 2 ≠ 0
Tactic:
norm_num
Proof state after:
no goals