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

State before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ Even (evenFactorExp a.norm.natAbs)
Tactic:
induction' hn : a.norm.natAbs using Nat.strong_induction_on with n ih generalizing a
State after:
case h
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
⊢ Even (evenFactorExp n)

State before:
case h
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
⊢ Even (evenFactorExp n)
Tactic:
by_cases hparity : Even a.norm.natAbs
State after:
case pos
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
⊢ Even (evenFactorExp n)

case neg
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : ¬Even a.norm.natAbs
⊢ Even (evenFactorExp n)

State before:
case pos
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
⊢ Even (evenFactorExp n)
Tactic:
obtain ⟨u, huvcoprime, huvprod⟩ := step1' hcoprime (Int.natAbs_even.mp hparity)
State after:
case pos.intro.intro
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
⊢ Even (evenFactorExp n)

State before:
case pos.intro.intro
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
⊢ Even (evenFactorExp n)
Tactic:
have huv := Spts.ne_zero_of_coprime' _ huvcoprime
State after:
case pos.intro.intro
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
⊢ Even (evenFactorExp n)

State before:
case pos.intro.intro
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
⊢ Even (evenFactorExp n)
Tactic:
have h₄ : Int.natAbs 4 = 4 := by norm_num
State after:
case pos.intro.intro
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
h₄ : Int.natAbs 4 = 4
⊢ Even (evenFactorExp n)

State before:
case pos.intro.intro
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
h₄ : Int.natAbs 4 = 4
⊢ Even (evenFactorExp n)
Tactic:
rw [← hn, huvprod, Int.natAbs_mul, h₄, factors_2_even (by simpa using huv), Nat.even_add]
State after:
case pos.intro.intro
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
h₄ : Int.natAbs 4 = 4
⊢ Even 2 ↔ Even (evenFactorExp u.norm.natAbs)

State before:
case pos.intro.intro
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
h₄ : Int.natAbs 4 = 4
⊢ Even 2 ↔ Even (evenFactorExp u.norm.natAbs)
Tactic:
apply iff_of_true even_two
State after:
case pos.intro.intro
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
h₄ : Int.natAbs 4 = 4
⊢ Even (evenFactorExp u.norm.natAbs)

State before:
case pos.intro.intro
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
h₄ : Int.natAbs 4 = 4
⊢ Even (evenFactorExp u.norm.natAbs)
Tactic:
apply ih _ _ huvcoprime rfl
State after:
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
h₄ : Int.natAbs 4 = 4
⊢ u.norm.natAbs < n

State before:
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
h₄ : Int.natAbs 4 = 4
⊢ u.norm.natAbs < n
Tactic:
rw [← hn, huvprod, Int.natAbs_mul, lt_mul_iff_one_lt_left (Int.natAbs_pos.mpr huv)]
State after:
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
h₄ : Int.natAbs 4 = 4
⊢ 1 < Int.natAbs 4

State before:
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
h₄ : Int.natAbs 4 = 4
⊢ 1 < Int.natAbs 4
Tactic:
norm_num
State after:
no goals

State before:
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
⊢ Int.natAbs 4 = 4
Tactic:
norm_num
State after:
no goals

State before:
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
h₄ : Int.natAbs 4 = 4
⊢ u.norm.natAbs ≠ 0
Tactic:
simpa using huv
State after:
no goals

State before:
case neg
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : ¬Even a.norm.natAbs
⊢ Even (evenFactorExp n)
Tactic:
convert even_zero (α := ℕ)
State after:
case h.e'_3
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : ¬Even a.norm.natAbs
⊢ evenFactorExp n = 0

State before:
case h.e'_3
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : ¬Even a.norm.natAbs
⊢ evenFactorExp n = 0
Tactic:
simp only [evenFactorExp, Multiset.count_eq_zero, hn]
State after:
case h.e'_3
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : ¬Even a.norm.natAbs
⊢ 2 ∉ UniqueFactorizationMonoid.normalizedFactors n

State before:
case h.e'_3
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : ¬Even a.norm.natAbs
⊢ 2 ∉ UniqueFactorizationMonoid.normalizedFactors n
Tactic:
contrapose! hparity with hfactor
State after:
case h.e'_3
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hfactor : 2 ∈ UniqueFactorizationMonoid.normalizedFactors n
⊢ Even a.norm.natAbs

State before:
case h.e'_3
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hfactor : 2 ∈ UniqueFactorizationMonoid.normalizedFactors n
⊢ Even a.norm.natAbs
Tactic:
rw [hn, even_iff_two_dvd]
State after:
case h.e'_3
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hfactor : 2 ∈ UniqueFactorizationMonoid.normalizedFactors n
⊢ 2 ∣ n

State before:
case h.e'_3
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hfactor : 2 ∈ UniqueFactorizationMonoid.normalizedFactors n
⊢ 2 ∣ n
Tactic:
exact UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors hfactor
State after:
no goals