Theorem: step1a (Flt/Edwards.lean)

State before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
⊢ Odd a.re ∧ Odd a.im
Tactic:
rw [Int.odd_iff_not_even, Int.odd_iff_not_even]
State after:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
⊢ ¬Even a.re ∧ ¬Even a.im

State before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
⊢ ¬Even a.re ∧ ¬Even a.im
Tactic:
have : Even a.re ↔ Even a.im := by simpa [Zsqrtd.norm_def, parity_simps] using heven
State after:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
this : Even a.re ↔ Even a.im
⊢ ¬Even a.re ∧ ¬Even a.im

State before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
this : Even a.re ↔ Even a.im
⊢ ¬Even a.re ∧ ¬Even a.im
Tactic:
apply (iff_iff_and_or_not_and_not.mp this).resolve_left
State after:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
this : Even a.re ↔ Even a.im
⊢ ¬(Even a.re ∧ Even a.im)

State before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
this : Even a.re ↔ Even a.im
⊢ ¬(Even a.re ∧ Even a.im)
Tactic:
rw [even_iff_two_dvd, even_iff_two_dvd]
State after:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
this : Even a.re ↔ Even a.im
⊢ ¬(2 ∣ a.re ∧ 2 ∣ a.im)

State before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
this : Even a.re ↔ Even a.im
⊢ ¬(2 ∣ a.re ∧ 2 ∣ a.im)
Tactic:
rintro ⟨hre, him⟩
State after:
case intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
this : Even a.re ↔ Even a.im
hre : 2 ∣ a.re
him : 2 ∣ a.im
⊢ False

State before:
case intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
this : Even a.re ↔ Even a.im
hre : 2 ∣ a.re
him : 2 ∣ a.im
⊢ False
Tactic:
have := hcoprime.isUnit_of_dvd' hre him
State after:
case intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
this✝ : Even a.re ↔ Even a.im
hre : 2 ∣ a.re
him : 2 ∣ a.im
this : IsUnit 2
⊢ False

State before:
case intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
this✝ : Even a.re ↔ Even a.im
hre : 2 ∣ a.re
him : 2 ∣ a.im
this : IsUnit 2
⊢ False
Tactic:
rw [isUnit_iff_dvd_one] at this
State after:
case intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
this✝ : Even a.re ↔ Even a.im
hre : 2 ∣ a.re
him : 2 ∣ a.im
this : 2 ∣ 1
⊢ False

State before:
case intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
this✝ : Even a.re ↔ Even a.im
hre : 2 ∣ a.re
him : 2 ∣ a.im
this : 2 ∣ 1
⊢ False
Tactic:
norm_num at this
State after:
no goals

State before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
⊢ Even a.re ↔ Even a.im
Tactic:
simpa [Zsqrtd.norm_def, parity_simps] using heven
State after:
no goals