Theorem: factorsOddPrimeOrFour.prod' (Flt/OddPrimeOrFour.lean)

State before:
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ Multiset.prod (factorsOddPrimeOrFour a) = a
Tactic:
apply Int.eq_of_associated_of_nonneg
State after:
case h
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ Associated (Multiset.prod (factorsOddPrimeOrFour a)) a

case ha
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ 0 ≤ Multiset.prod (factorsOddPrimeOrFour a)

case hb
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ 0 ≤ a

State before:
case h
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ Associated (Multiset.prod (factorsOddPrimeOrFour a)) a
Tactic:
have := UniqueFactorizationMonoid.normalizedFactors_prod ha.ne'
State after:
case h
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
this : Associated (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a)) a
⊢ Associated (Multiset.prod (factorsOddPrimeOrFour a)) a

State before:
case h
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
this : Associated (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a)) a
⊢ Associated (Multiset.prod (factorsOddPrimeOrFour a)) a
Tactic:
apply Associated.trans _ this
State after:
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
this : Associated (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a)) a
⊢ Associated (Multiset.prod (factorsOddPrimeOrFour a)) (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a))

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

State before:
case intro
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
this : Associated (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a)) a
m : ℕ
hm : evenFactorExp a = 2 * m
⊢ Associated (Multiset.prod (factorsOddPrimeOrFour a)) (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a))
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]
State after:
case intro
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
this : Associated (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a)) a
m : ℕ
hm : evenFactorExp a = 2 * m
⊢ Associated (4 ^ m * Multiset.prod (oddFactors a)) ((2 ^ 2) ^ m * Multiset.prod (oddFactors a))

State before:
case intro
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
this : Associated (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a)) a
m : ℕ
hm : evenFactorExp a = 2 * m
⊢ Associated (4 ^ m * Multiset.prod (oddFactors a)) ((2 ^ 2) ^ m * Multiset.prod (oddFactors a))
Tactic:
exact Associated.refl _
State after:
no goals

State before:
case ha
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ 0 ≤ Multiset.prod (factorsOddPrimeOrFour a)
Tactic:
apply Multiset.prod_nonneg
State after:
case ha.h
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ ∀ (a_1 : ℤ), a_1 ∈ factorsOddPrimeOrFour a → 0 ≤ a_1

State before:
case ha.h
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ ∀ (a_1 : ℤ), a_1 ∈ factorsOddPrimeOrFour a → 0 ≤ a_1
Tactic:
apply factorsOddPrimeOrFour.nonneg
State after:
no goals

State before:
case hb
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ 0 ≤ a
Tactic:
exact ha.le
State after:
no goals