Theorem: step4_3 (Flt/Edwards.lean)

State before:
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
⊢ abs p.re = abs p'.re ∧ abs p.im = abs p'.im
Tactic:
have hdvd : p'.norm ∣ p.norm := by rw [heq]
State after:
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
⊢ abs p.re = abs p'.re ∧ abs p.im = abs p'.im

State before:
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
⊢ abs p.re = abs p'.re ∧ abs p.im = abs p'.im
Tactic:
have him : p'.im ≠ 0 := by
  apply OddPrimeOrFour.im_ne_zero _ hcoprime'
  rwa [← heq]
State after:
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
⊢ abs p.re = abs p'.re ∧ abs p.im = abs p'.im

State before:
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
⊢ Zsqrtd.norm p' ∣ Zsqrtd.norm p
Tactic:
rw [heq]
State after:
no goals

State before:
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
⊢ p'.im ≠ 0
Tactic:
apply OddPrimeOrFour.im_ne_zero _ hcoprime'
State after:
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
⊢ OddPrimeOrFour (Zsqrtd.norm p')

State before:
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
⊢ OddPrimeOrFour (Zsqrtd.norm p')
Tactic:
rwa [← heq]
State after:
no goals

State before:
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
⊢ OddPrimeOrFour (Zsqrtd.norm p')
Tactic:
rwa [← heq]
State after:
no goals

State before:
case intro.intro.intro.inr
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
u : ℤ√(-3)
h1 : Zsqrtd.norm p = Zsqrtd.norm p' * Zsqrtd.norm u
H : p = star p' * u
⊢ abs p.re = abs p'.re ∧ abs p.im = abs p'.im
Tactic:
rw [heq] at h1
State after:
case intro.intro.intro.inr
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
u : ℤ√(-3)
h1 : Zsqrtd.norm p' = Zsqrtd.norm p' * Zsqrtd.norm u
H : p = star p' * u
⊢ abs p.re = abs p'.re ∧ abs p.im = abs p'.im

State before:
case intro.intro.intro.inr
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
u : ℤ√(-3)
h1 : Zsqrtd.norm p' = Zsqrtd.norm p' * Zsqrtd.norm u
H : p = star p' * u
⊢ abs p.re = abs p'.re ∧ abs p.im = abs p'.im
Tactic:
have := Int.eq_one_of_mul_eq_self_right (Spts.ne_zero_of_coprime' _ hcoprime') h1.symm
State after:
case intro.intro.intro.inr
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
u : ℤ√(-3)
h1 : Zsqrtd.norm p' = Zsqrtd.norm p' * Zsqrtd.norm u
H : p = star p' * u
this : Zsqrtd.norm u = 1
⊢ abs p.re = abs p'.re ∧ abs p.im = abs p'.im

State before:
case intro.intro.intro.inr
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
u : ℤ√(-3)
h1 : Zsqrtd.norm p' = Zsqrtd.norm p' * Zsqrtd.norm u
H : p = star p' * u
this : Zsqrtd.norm u = 1
⊢ abs p.re = abs p'.re ∧ abs p.im = abs p'.im
Tactic:
obtain ⟨ha, hb⟩ := Spts.eq_one this
State after:
case intro.intro.intro.inr.intro
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
u : ℤ√(-3)
h1 : Zsqrtd.norm p' = Zsqrtd.norm p' * Zsqrtd.norm u
H : p = star p' * u
this : Zsqrtd.norm u = 1
ha : abs u.re = 1
hb : u.im = 0
⊢ abs p.re = abs p'.re ∧ abs p.im = abs p'.im

State before:
case intro.intro.intro.inr.intro
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
u : ℤ√(-3)
h1 : Zsqrtd.norm p' = Zsqrtd.norm p' * Zsqrtd.norm u
H : p = star p' * u
this : Zsqrtd.norm u = 1
ha : abs u.re = 1
hb : u.im = 0
⊢ abs p.re = abs p'.re ∧ abs p.im = abs p'.im
Tactic:
simp only [hb, Zsqrtd.ext, Zsqrtd.mul_re, Zsqrtd.mul_im, add_zero, zero_add,
  MulZeroClass.mul_zero] at H
State after:
case intro.intro.intro.inr.intro
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
u : ℤ√(-3)
h1 : Zsqrtd.norm p' = Zsqrtd.norm p' * Zsqrtd.norm u
this : Zsqrtd.norm u = 1
ha : abs u.re = 1
hb : u.im = 0
H : p.re = (star p').re * u.re ∧ p.im = (star p').im * u.re
⊢ abs p.re = abs p'.re ∧ abs p.im = abs p'.im

State before:
case intro.intro.intro.inr.intro
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
u : ℤ√(-3)
h1 : Zsqrtd.norm p' = Zsqrtd.norm p' * Zsqrtd.norm u
this : Zsqrtd.norm u = 1
ha : abs u.re = 1
hb : u.im = 0
H : p.re = (star p').re * u.re ∧ p.im = (star p').im * u.re
⊢ abs p.re = abs p'.re ∧ abs p.im = abs p'.im
Tactic:
rw [H.1, H.2, abs_mul, abs_mul, ha, mul_one, mul_one]
State after:
case intro.intro.intro.inr.intro
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
u : ℤ√(-3)
h1 : Zsqrtd.norm p' = Zsqrtd.norm p' * Zsqrtd.norm u
this : Zsqrtd.norm u = 1
ha : abs u.re = 1
hb : u.im = 0
H : p.re = (star p').re * u.re ∧ p.im = (star p').im * u.re
⊢ abs (star p').re = abs p'.re ∧ abs (star p').im = abs p'.im

State before:
case intro.intro.intro.inr.intro
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
u : ℤ√(-3)
h1 : Zsqrtd.norm p' = Zsqrtd.norm p' * Zsqrtd.norm u
this : Zsqrtd.norm u = 1
ha : abs u.re = 1
hb : u.im = 0
H : p.re = (star p').re * u.re ∧ p.im = (star p').im * u.re
⊢ abs (star p').re = abs p'.re ∧ abs (star p').im = abs p'.im
Tactic:
simp
State after:
no goals