Theorem: factors_2_even' (Flt/Edwards.lean)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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