Theorem: factorsOddPrimeOrFour.prod' (FltRegular/FltThree/OddPrimeOrFour.lean)

State before:
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ (factorsOddPrimeOrFour a).prod = a
Tactic:
have h₁ : (2 : ℕ) ^ 2 = 4 := by norm_num
State after:
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
h₁ : 2 ^ 2 = 4
⊢ (factorsOddPrimeOrFour a).prod = a

State before:
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
h₁ : 2 ^ 2 = 4
⊢ (factorsOddPrimeOrFour a).prod = a
Tactic:
have := UniqueFactorizationMonoid.normalizedFactors_prod ha.ne'
State after:
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
h₁ : 2 ^ 2 = 4
this : Associated (UniqueFactorizationMonoid.normalizedFactors a).prod a
⊢ (factorsOddPrimeOrFour a).prod = a

State before:
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
h₁ : 2 ^ 2 = 4
this : Associated (UniqueFactorizationMonoid.normalizedFactors a).prod a
⊢ (factorsOddPrimeOrFour a).prod = a
Tactic:
rw [associated_eq_eq] at this
State after:
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
h₁ : 2 ^ 2 = 4
this : (UniqueFactorizationMonoid.normalizedFactors a).prod = a
⊢ (factorsOddPrimeOrFour a).prod = a

State before:
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
h₁ : 2 ^ 2 = 4
this : (UniqueFactorizationMonoid.normalizedFactors a).prod = a
⊢ (factorsOddPrimeOrFour a).prod = a
Tactic:
conv_rhs => rw [←this]
State after:
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
h₁ : 2 ^ 2 = 4
this : (UniqueFactorizationMonoid.normalizedFactors a).prod = a
⊢ (factorsOddPrimeOrFour a).prod = (UniqueFactorizationMonoid.normalizedFactors a).prod

State before:
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
h₁ : 2 ^ 2 = 4
this : (UniqueFactorizationMonoid.normalizedFactors a).prod = a
⊢ (factorsOddPrimeOrFour a).prod = (UniqueFactorizationMonoid.normalizedFactors a).prod
Tactic:
obtain ⟨m, hm⟩ := even_iff_two_dvd.mp heven
State after:
case intro
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
h₁ : 2 ^ 2 = 4
this : (UniqueFactorizationMonoid.normalizedFactors a).prod = a
m : ℕ
hm : evenFactorExp a = 2 * m
⊢ (factorsOddPrimeOrFour a).prod = (UniqueFactorizationMonoid.normalizedFactors a).prod

State before:
case intro
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
h₁ : 2 ^ 2 = 4
this : (UniqueFactorizationMonoid.normalizedFactors a).prod = a
m : ℕ
hm : evenFactorExp a = 2 * m
⊢ (factorsOddPrimeOrFour a).prod = (UniqueFactorizationMonoid.normalizedFactors a).prod
Tactic:
rw [even_and_odd_factors' _, Multiset.prod_add, factorsOddPrimeOrFour, Multiset.prod_add, hm,
  Nat.mul_div_right _ zero_lt_two, Multiset.prod_replicate, Multiset.prod_replicate, pow_mul, h₁]
State after:
no goals

State before:
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ 2 ^ 2 = 4
Tactic:
norm_num
State after:
no goals