Theorem: OddPrimeOrFour.factors (Flt/Edwards.lean)

State before:
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hx : OddPrimeOrFour x
hfactor : x ∣ Zsqrtd.norm a
⊢ ∃ c, Abs.abs x = Zsqrtd.norm c ∧ 0 ≤ c.re ∧ c.im ≠ 0
Tactic:
obtain rfl | ⟨hprime, hodd⟩ := hx
State after:
case inl
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hfactor : 4 ∣ Zsqrtd.norm a
⊢ ∃ c, Abs.abs 4 = Zsqrtd.norm c ∧ 0 ≤ c.re ∧ c.im ≠ 0

case inr.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
⊢ ∃ c, Abs.abs x = Zsqrtd.norm c ∧ 0 ≤ c.re ∧ c.im ≠ 0

State before:
case inl
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hfactor : 4 ∣ Zsqrtd.norm a
⊢ ∃ c, Abs.abs 4 = Zsqrtd.norm c ∧ 0 ≤ c.re ∧ c.im ≠ 0
Tactic:
refine' ⟨⟨1, 1⟩, _, zero_le_one, one_ne_zero⟩
State after:
case inl
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hfactor : 4 ∣ Zsqrtd.norm a
⊢ Abs.abs 4 = Zsqrtd.norm { re := 1, im := 1 }

State before:
case inl
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hfactor : 4 ∣ Zsqrtd.norm a
⊢ Abs.abs 4 = Zsqrtd.norm { re := 1, im := 1 }
Tactic:
simp only [Zsqrtd.norm_def, mul_one, abs_of_pos, zero_lt_four, sub_neg_eq_add]
State after:
no goals

State before:
case inr.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
⊢ ∃ c, Abs.abs x = Zsqrtd.norm c ∧ 0 ≤ c.re ∧ c.im ≠ 0
Tactic:
obtain ⟨c, hc⟩ := _root_.factors a x hcoprime hodd hfactor
State after:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : Abs.abs x = Zsqrtd.norm c
⊢ ∃ c, Abs.abs x = Zsqrtd.norm c ∧ 0 ≤ c.re ∧ c.im ≠ 0

State before:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : Abs.abs x = Zsqrtd.norm c
⊢ ∃ c, Abs.abs x = Zsqrtd.norm c ∧ 0 ≤ c.re ∧ c.im ≠ 0
Tactic:
rw [hc]
State after:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : Abs.abs x = Zsqrtd.norm c
⊢ ∃ c_1, Zsqrtd.norm c = Zsqrtd.norm c_1 ∧ 0 ≤ c_1.re ∧ c_1.im ≠ 0

State before:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : Abs.abs x = Zsqrtd.norm c
⊢ ∃ c_1, Zsqrtd.norm c = Zsqrtd.norm c_1 ∧ 0 ≤ c_1.re ∧ c_1.im ≠ 0
Tactic:
apply Zsqrtd.exists c
State after:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : Abs.abs x = Zsqrtd.norm c
⊢ c.im ≠ 0

State before:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : Abs.abs x = Zsqrtd.norm c
⊢ c.im ≠ 0
Tactic:
intro H
State after:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : Abs.abs x = Zsqrtd.norm c
H : c.im = 0
⊢ False

State before:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : Abs.abs x = Zsqrtd.norm c
H : c.im = 0
⊢ False
Tactic:
rw [Zsqrtd.norm_def, H, MulZeroClass.mul_zero, sub_zero, ← pow_two, eq_comm] at hc
State after:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : c.re ^ 2 = Abs.abs x
H : c.im = 0
⊢ False

State before:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : c.re ^ 2 = Abs.abs x
H : c.im = 0
⊢ False
Tactic:
have := hprime.abs
State after:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : c.re ^ 2 = Abs.abs x
H : c.im = 0
this : Prime (Abs.abs x)
⊢ False

State before:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : c.re ^ 2 = Abs.abs x
H : c.im = 0
this : Prime (Abs.abs x)
⊢ False
Tactic:
rw [←hc] at this
State after:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : c.re ^ 2 = Abs.abs x
H : c.im = 0
this : Prime (c.re ^ 2)
⊢ False

State before:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : c.re ^ 2 = Abs.abs x
H : c.im = 0
this : Prime (c.re ^ 2)
⊢ False
Tactic:
exact pow_not_prime one_lt_two.ne' this
State after:
no goals