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

State before:
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
hf' : ∀ (x : ℤ), x ∈ f → 0 ≤ x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
⊢ f = factorsOddPrimeOrFour a
Tactic:
rw [← Multiset.rel_eq]
State after:
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
hf' : ∀ (x : ℤ), x ∈ f → 0 ≤ x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
⊢ Multiset.Rel (fun x x_1 => x = x_1) f (factorsOddPrimeOrFour a)

State before:
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
hf' : ∀ (x : ℤ), x ∈ f → 0 ≤ x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
⊢ Multiset.Rel (fun x x_1 => x = x_1) f (factorsOddPrimeOrFour a)
Tactic:
apply Multiset.Rel.mono (factorsOddPrimeOrFour.associated' hf ha heven hassoc)
State after:
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
hf' : ∀ (x : ℤ), x ∈ f → 0 ≤ x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
⊢ ∀ (a_1 : ℤ), a_1 ∈ f → ∀ (b : ℤ), b ∈ factorsOddPrimeOrFour a → Associated a_1 b → a_1 = b

State before:
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
hf' : ∀ (x : ℤ), x ∈ f → 0 ≤ x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
⊢ ∀ (a_1 : ℤ), a_1 ∈ f → ∀ (b : ℤ), b ∈ factorsOddPrimeOrFour a → Associated a_1 b → a_1 = b
Tactic:
intro x hx y hy hxy
State after:
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
hf' : ∀ (x : ℤ), x ∈ f → 0 ≤ x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
x : ℤ
hx : x ∈ f
y : ℤ
hy : y ∈ factorsOddPrimeOrFour a
hxy : Associated x y
⊢ x = y

State before:
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
hf' : ∀ (x : ℤ), x ∈ f → 0 ≤ x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
x : ℤ
hx : x ∈ f
y : ℤ
hy : y ∈ factorsOddPrimeOrFour a
hxy : Associated x y
⊢ x = y
Tactic:
exact Int.eq_of_associated_of_nonneg hxy (hf' x hx) (factorsOddPrimeOrFour.nonneg hy)
State after:
no goals