Theorem: step1'' (FltRegular/FltThree/Edwards.lean)

State before:
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = 4 * u.norm
Tactic:
obtain ⟨u, h2⟩ := step1 hcoprime heven
State after:
case intro
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
h2 : a = { re := 1, im := 1 } * u ∨ a = { re := 1, im := -1 } * u
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = 4 * u.norm

State before:
case intro
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
h2 : a = { re := 1, im := 1 } * u ∨ a = { re := 1, im := -1 } * u
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = 4 * u.norm
Tactic:
set q : ℤ√(-3) := ⟨1, 1⟩
State after:
case intro
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = { re := 1, im := -1 } * u
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = 4 * u.norm

State before:
case intro
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = { re := 1, im := -1 } * u
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = 4 * u.norm
Tactic:
replace h2 : a = q * u ∨ a = star q * u := h2
State after:
case intro
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = 4 * u.norm

State before:
case intro
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = 4 * u.norm
Tactic:
obtain ⟨hp', hq'⟩ := Spts.four hp hq
State after:
case intro.intro
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hp' : |p.re| = 1
hq' : |p.im| = 1
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = 4 * u.norm

State before:
case intro.intro
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hp' : |p.re| = 1
hq' : |p.im| = 1
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = 4 * u.norm
Tactic:
refine' ⟨p.re * u, _, _, _⟩
State after:
case intro.intro.refine'_1
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hp' : |p.re| = 1
hq' : |p.im| = 1
⊢ IsCoprime (↑p.re * u).re (↑p.re * u).im

case intro.intro.refine'_2
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hp' : |p.re| = 1
hq' : |p.im| = 1
⊢ a = p * (↑p.re * u) ∨ a = star p * (↑p.re * u)

case intro.intro.refine'_3
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hp' : |p.re| = 1
hq' : |p.im| = 1
⊢ a.norm = 4 * (↑p.re * u).norm

State before:
case intro.intro.refine'_1
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hp' : |p.re| = 1
hq' : |p.im| = 1
⊢ IsCoprime (↑p.re * u).re (↑p.re * u).im
Tactic:
rw [← Int.isUnit_iff_abs_eq] at hp'
State after:
case intro.intro.refine'_1
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hp' : IsUnit p.re
hq' : |p.im| = 1
⊢ IsCoprime (↑p.re * u).re (↑p.re * u).im

State before:
case intro.intro.refine'_1
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hp' : IsUnit p.re
hq' : |p.im| = 1
⊢ IsCoprime (↑p.re * u).re (↑p.re * u).im
Tactic:
rw [Zsqrtd.smul_re, Zsqrtd.smul_im, isCoprime_mul_unit_left hp']
State after:
case intro.intro.refine'_1
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hp' : IsUnit p.re
hq' : |p.im| = 1
⊢ IsCoprime u.re u.im

State before:
case intro.intro.refine'_1
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hp' : IsUnit p.re
hq' : |p.im| = 1
⊢ IsCoprime u.re u.im
Tactic:
apply Zsqrtd.coprime_of_dvd_coprime hcoprime
State after:
case intro.intro.refine'_1
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hp' : IsUnit p.re
hq' : |p.im| = 1
⊢ u ∣ a

State before:
case intro.intro.refine'_1
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hp' : IsUnit p.re
hq' : |p.im| = 1
⊢ u ∣ a
Tactic:
obtain rfl | rfl := h2 <;> apply dvd_mul_left
State after:
no goals

State before:
case intro.intro.refine'_2
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hp' : |p.re| = 1
hq' : |p.im| = 1
⊢ a = p * (↑p.re * u) ∨ a = star p * (↑p.re * u)
Tactic:
rw [abs_eq <| zero_le_one' ℤ] at hp' hq'
State after:
case intro.intro.refine'_2
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hp' : p.re = 1 ∨ p.re = -1
hq' : p.im = 1 ∨ p.im = -1
⊢ a = p * (↑p.re * u) ∨ a = star p * (↑p.re * u)

State before:
case intro.intro.refine'_2.inl
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hq' : p.im = 1 ∨ p.im = -1
hp' : p.re = 1
h4 : p = q ∨ p = star q
⊢ a = p * (↑p.re * u) ∨ a = star p * (↑p.re * u)
Tactic:
simp only [hp', one_mul, Int.cast_one]
State after:
case intro.intro.refine'_2.inl
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hq' : p.im = 1 ∨ p.im = -1
hp' : p.re = 1
h4 : p = q ∨ p = star q
⊢ a = p * u ∨ a = star p * u

State before:
case intro.intro.refine'_2.inl
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hq' : p.im = 1 ∨ p.im = -1
hp' : p.re = 1
h4 : p = q ∨ p = star q
⊢ a = p * u ∨ a = star p * u
Tactic:
cases h4 <;> cases h2 <;> simp [*, or_comm]
State after:
no goals

State before:
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hq' : p.im = 1 ∨ p.im = -1
hp' : p.re = 1
⊢ p.im = -1 → p = star q
Tactic:
intro h5
State after:
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hq' : p.im = 1 ∨ p.im = -1
hp' : p.re = 1
h5 : p.im = -1
⊢ p = star q

State before:
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hq' : p.im = 1 ∨ p.im = -1
hp' : p.re = 1
h5 : p.im = -1
⊢ p = star q
Tactic:
simp [Zsqrtd.ext_iff, hp', h5]
State after:
no goals

State before:
case intro.intro.refine'_2.inr
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hq' : p.im = 1 ∨ p.im = -1
hp' : p.re = -1
h4 : p = -q ∨ p = -star q
⊢ a = p * (↑p.re * u) ∨ a = star p * (↑p.re * u)
Tactic:
simp only [hp', one_mul, Zsqrtd.norm_neg, Int.cast_one, Int.cast_neg, neg_one_mul]
State after:
case intro.intro.refine'_2.inr
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hq' : p.im = 1 ∨ p.im = -1
hp' : p.re = -1
h4 : p = -q ∨ p = -star q
⊢ a = p * -u ∨ a = star p * -u

State before:
case intro.intro.refine'_2.inr
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hq' : p.im = 1 ∨ p.im = -1
hp' : p.re = -1
h4 : p = -q ∨ p = -star q
⊢ a = p * -u ∨ a = star p * -u
Tactic:
cases h4 <;> cases h2 <;> simp [*]
State after:
no goals

State before:
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hq' : p.im = 1 ∨ p.im = -1
hp' : p.re = -1
⊢ p = -q ∨ p = -star q
Tactic:
apply Or.imp _ _ hq'.symm
State after:
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hq' : p.im = 1 ∨ p.im = -1
hp' : p.re = -1
⊢ p.im = -1 → p = -q

a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hq' : p.im = 1 ∨ p.im = -1
hp' : p.re = -1
⊢ p.im = 1 → p = -star q

State before:
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hq' : p.im = 1 ∨ p.im = -1
hp' : p.re = -1
⊢ p.im = -1 → p = -q
Tactic:
intro h5
State after:
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hq' : p.im = 1 ∨ p.im = -1
hp' : p.re = -1
h5 : p.im = -1
⊢ p = -q

State before:
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hq' : p.im = 1 ∨ p.im = -1
hp' : p.re = -1
h5 : p.im = -1
⊢ p = -q
Tactic:
simp [Zsqrtd.ext_iff, hp', h5]
State after:
no goals

State before:
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hq' : p.im = 1 ∨ p.im = -1
hp' : p.re = -1
⊢ p.im = 1 → p = -star q
Tactic:
intro h5
State after:
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hq' : p.im = 1 ∨ p.im = -1
hp' : p.re = -1
h5 : p.im = 1
⊢ p = -star q

State before:
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hq' : p.im = 1 ∨ p.im = -1
hp' : p.re = -1
h5 : p.im = 1
⊢ p = -star q
Tactic:
simp [Zsqrtd.ext_iff, hp', h5]
State after:
no goals

State before:
case intro.intro.refine'_3
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hp' : |p.re| = 1
hq' : |p.im| = 1
⊢ a.norm = 4 * (↑p.re * u).norm
Tactic:
rw [Zsqrtd.norm_mul, Zsqrtd.norm_intCast, ← sq, ← sq_abs, hp', one_pow, one_mul]
State after:
case intro.intro.refine'_3
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hp' : |p.re| = 1
hq' : |p.im| = 1
⊢ a.norm = 4 * u.norm

State before:
case intro.intro.refine'_3.inr
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
hp' : |p.re| = 1
hq' : |p.im| = 1
h2 : a = star q * u
⊢ a.norm = 4 * u.norm
Tactic:
rw [h2, Zsqrtd.norm_mul]
State after:
case intro.intro.refine'_3.inr
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
hp' : |p.re| = 1
hq' : |p.im| = 1
h2 : a = star q * u
⊢ (star q).norm * u.norm = 4 * u.norm

State before:
case intro.intro.refine'_3.inr
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
hp' : |p.re| = 1
hq' : |p.im| = 1
h2 : a = star q * u
⊢ (star q).norm * u.norm = 4 * u.norm
Tactic:
congr
State after:
no goals