Theorem: factors_2_even (Flt/OddPrimeOrFour.lean)

State before:
z : ℤ
hz : z ≠ 0
⊢ evenFactorExp (4 * z) = 2 + evenFactorExp z
Tactic:
have h₀ : (4 : ℤ) ≠ 0 := four_ne_zero
State after:
z : ℤ
hz : z ≠ 0
h₀ : 4 ≠ 0
⊢ evenFactorExp (4 * z) = 2 + evenFactorExp z

State before:
z : ℤ
hz : z ≠ 0
h₀ : 4 ≠ 0
⊢ evenFactorExp (4 * z) = 2 + evenFactorExp z
Tactic:
have h₁ : (2 : Int) ^ 2 = 4 := by norm_num
State after:
z : ℤ
hz : z ≠ 0
h₀ : 4 ≠ 0
h₁ : 2 ^ 2 = 4
⊢ evenFactorExp (4 * z) = 2 + evenFactorExp z

State before:
z : ℤ
hz : z ≠ 0
h₀ : 4 ≠ 0
h₁ : 2 ^ 2 = 4
⊢ evenFactorExp (4 * z) = 2 + evenFactorExp z
Tactic:
simp [evenFactorExp]
State after:
z : ℤ
hz : z ≠ 0
h₀ : 4 ≠ 0
h₁ : 2 ^ 2 = 4
⊢ Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors (4 * z)) =
    2 + Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors z)

State before:
z : ℤ
hz : z ≠ 0
h₀ : 4 ≠ 0
h₁ : 2 ^ 2 = 4
⊢ Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors (4 * z)) =
    2 + Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors z)
Tactic:
rw [UniqueFactorizationMonoid.normalizedFactors_mul h₀ hz, Multiset.count_add, ← h₁,
  UniqueFactorizationMonoid.normalizedFactors_pow, Multiset.count_nsmul,
  UniqueFactorizationMonoid.normalizedFactors_irreducible Int.prime_two.irreducible,
  Int.normalize_of_nonneg zero_le_two, Multiset.count_singleton_self, mul_one]
State after:
no goals

State before:
z : ℤ
hz : z ≠ 0
h₀ : 4 ≠ 0
⊢ 2 ^ 2 = 4
Tactic:
norm_num
State after:
no goals