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

State before:
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
ha : 0 < f.prod
heven : Even (evenFactorExp f.prod)
⊢ factorsOddPrimeOrFour f.prod = f
Tactic:
refine factors_unique_prod' ?_ hf (factorsOddPrimeOrFour.prod' ha heven)
State after:
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
ha : 0 < f.prod
heven : Even (evenFactorExp f.prod)
⊢ ∀ x ∈ factorsOddPrimeOrFour f.prod, OddPrimeOrFour x

State before:
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
ha : 0 < f.prod
heven : Even (evenFactorExp f.prod)
⊢ ∀ x ∈ factorsOddPrimeOrFour f.prod, OddPrimeOrFour x
Tactic:
intro x hx
State after:
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
ha : 0 < f.prod
heven : Even (evenFactorExp f.prod)
x : ℕ
hx : x ∈ factorsOddPrimeOrFour f.prod
⊢ OddPrimeOrFour x

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

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

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

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

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

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