Theorem: OddPrimeOrFour.factors (FltRegular/FltThree/Edwards.lean)

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

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

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

State before:
case inl
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hx : x.natAbs = 4
⊢ |x| = { re := 1, im := 1 }.norm
Tactic:
simp only [Zsqrtd.norm_def, mul_one, sub_neg_eq_add, Int.abs_eq_natAbs, hx]
State after:
case inl
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hx : x.natAbs = 4
⊢ ↑4 = 1 + 3

State before:
case inl
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hx : x.natAbs = 4
⊢ ↑4 = 1 + 3
Tactic:
norm_num
State after:
no goals

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

State before:
case inr.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hprime : x.natAbs.Prime
hodd : Odd x
⊢ ∃ c, |x| = c.norm ∧ 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 ∣ a.norm
hprime : x.natAbs.Prime
hodd : Odd x
c : ℤ√(-3)
hc : |x| = c.norm
⊢ ∃ c, |x| = c.norm ∧ 0 ≤ c.re ∧ c.im ≠ 0

State before:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hprime : x.natAbs.Prime
hodd : Odd x
c : ℤ√(-3)
hc : |x| = c.norm
⊢ ∃ c, |x| = c.norm ∧ 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 ∣ a.norm
hprime : x.natAbs.Prime
hodd : Odd x
c : ℤ√(-3)
hc : |x| = c.norm
⊢ ∃ c_1, c.norm = c_1.norm ∧ 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 ∣ a.norm
hprime : x.natAbs.Prime
hodd : Odd x
c : ℤ√(-3)
hc : |x| = c.norm
⊢ ∃ c_1, c.norm = c_1.norm ∧ 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 ∣ a.norm
hprime : x.natAbs.Prime
hodd : Odd x
c : ℤ√(-3)
hc : |x| = c.norm
⊢ c.im ≠ 0

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

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

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

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