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

State before:
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
⊢ Multiset.Rel Associated f (factorsOddPrimeOrFour a)
Tactic:
apply factors_unique_prod' hf
State after:
case a
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
⊢ ∀ (x : ℤ), x ∈ factorsOddPrimeOrFour a → OddPrimeOrFour x

case a
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
⊢ Associated (Multiset.prod f) (Multiset.prod (factorsOddPrimeOrFour a))

State before:
case a
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
⊢ ∀ (x : ℤ), x ∈ factorsOddPrimeOrFour a → OddPrimeOrFour x
Tactic:
intro x hx
State after:
case a
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
x : ℤ
hx : x ∈ factorsOddPrimeOrFour a
⊢ OddPrimeOrFour x

State before:
case a
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
x : ℤ
hx : x ∈ factorsOddPrimeOrFour a
⊢ OddPrimeOrFour x
Tactic:
simp only [factorsOddPrimeOrFour, Multiset.mem_add] at hx
State after:
case a
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
x : ℤ
hx : x ∈ Multiset.replicate (evenFactorExp a / 2) 4 ∨ x ∈ oddFactors a
⊢ OddPrimeOrFour x

State before:
case a
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
x : ℤ
hx : x ∈ Multiset.replicate (evenFactorExp a / 2) 4 ∨ x ∈ oddFactors a
⊢ OddPrimeOrFour x
Tactic:
apply Or.imp _ _ hx
State after:
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
x : ℤ
hx : x ∈ Multiset.replicate (evenFactorExp a / 2) 4 ∨ x ∈ oddFactors a
⊢ x ∈ Multiset.replicate (evenFactorExp a / 2) 4 → x = 4

a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
x : ℤ
hx : x ∈ Multiset.replicate (evenFactorExp a / 2) 4 ∨ x ∈ oddFactors a
⊢ x ∈ oddFactors a → Prime x ∧ Odd x

State before:
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
x : ℤ
hx : x ∈ Multiset.replicate (evenFactorExp a / 2) 4 ∨ x ∈ oddFactors a
⊢ x ∈ Multiset.replicate (evenFactorExp a / 2) 4 → x = 4
Tactic:
exact Multiset.eq_of_mem_replicate
State after:
no goals

State before:
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
x : ℤ
hx : x ∈ Multiset.replicate (evenFactorExp a / 2) 4 ∨ x ∈ oddFactors a
⊢ x ∈ oddFactors a → Prime x ∧ Odd x
Tactic:
simp only [oddFactors, Multiset.mem_filter]
State after:
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
x : ℤ
hx : x ∈ Multiset.replicate (evenFactorExp a / 2) 4 ∨ x ∈ oddFactors a
⊢ x ∈ UniqueFactorizationMonoid.normalizedFactors a ∧ Odd x → Prime x ∧ Odd x

State before:
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
x : ℤ
hx : x ∈ Multiset.replicate (evenFactorExp a / 2) 4 ∨ x ∈ oddFactors a
⊢ x ∈ UniqueFactorizationMonoid.normalizedFactors a ∧ Odd x → Prime x ∧ Odd x
Tactic:
exact And.imp_left (UniqueFactorizationMonoid.prime_of_normalized_factor _)
State after:
no goals

State before:
case a
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
⊢ Associated (Multiset.prod f) (Multiset.prod (factorsOddPrimeOrFour a))
Tactic:
rwa [factorsOddPrimeOrFour.prod' ha heven]
State after:
no goals