Theorem: exists_associated_mem_of_dvd_prod'' (Flt/OddPrimeOrFour.lean)

State before:
p : ℤ
hp : OddPrimeOrFour p
s : Multiset ℤ
hs : ∀ (r : ℤ), r ∈ s → OddPrimeOrFour r
hdvd : p ∣ Multiset.prod s
⊢ ∃ q, q ∈ s ∧ Associated p q
Tactic:
induction' s using Multiset.induction_on with a s ih hs
State after:
case h₁
p : ℤ
hp : OddPrimeOrFour p
s : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s
hs : ∀ (r : ℤ), r ∈ 0 → OddPrimeOrFour r
hdvd : p ∣ Multiset.prod 0
⊢ ∃ q, q ∈ 0 ∧ Associated p q

case h₂
p : ℤ
hp : OddPrimeOrFour p
s✝ : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s✝ → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s✝
a : ℤ
s : Multiset ℤ
ih : (∀ (r : ℤ), r ∈ s → OddPrimeOrFour r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ Associated p q
hs : ∀ (r : ℤ), r ∈ a ::ₘ s → OddPrimeOrFour r
hdvd : p ∣ Multiset.prod (a ::ₘ s)
⊢ ∃ q, q ∈ a ::ₘ s ∧ Associated p q

State before:
case h₁
p : ℤ
hp : OddPrimeOrFour p
s : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s
hs : ∀ (r : ℤ), r ∈ 0 → OddPrimeOrFour r
hdvd : p ∣ Multiset.prod 0
⊢ ∃ q, q ∈ 0 ∧ Associated p q
Tactic:
simp [hp.not_unit, ← isUnit_iff_dvd_one] at hdvd
State after:
no goals

State before:
case h₂
p : ℤ
hp : OddPrimeOrFour p
s✝ : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s✝ → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s✝
a : ℤ
s : Multiset ℤ
ih : (∀ (r : ℤ), r ∈ s → OddPrimeOrFour r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ Associated p q
hs : ∀ (r : ℤ), r ∈ a ::ₘ s → OddPrimeOrFour r
hdvd : p ∣ Multiset.prod (a ::ₘ s)
⊢ ∃ q, q ∈ a ::ₘ s ∧ Associated p q
Tactic:
rw [Multiset.prod_cons] at hdvd
State after:
case h₂
p : ℤ
hp : OddPrimeOrFour p
s✝ : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s✝ → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s✝
a : ℤ
s : Multiset ℤ
ih : (∀ (r : ℤ), r ∈ s → OddPrimeOrFour r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ Associated p q
hs : ∀ (r : ℤ), r ∈ a ::ₘ s → OddPrimeOrFour r
hdvd : p ∣ a * Multiset.prod s
⊢ ∃ q, q ∈ a ::ₘ s ∧ Associated p q

State before:
case h₂
p : ℤ
hp : OddPrimeOrFour p
s✝ : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s✝ → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s✝
a : ℤ
s : Multiset ℤ
ih : (∀ (r : ℤ), r ∈ s → OddPrimeOrFour r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ Associated p q
hs : ∀ (r : ℤ), r ∈ a ::ₘ s → OddPrimeOrFour r
hdvd : p ∣ a * Multiset.prod s
⊢ ∃ q, q ∈ a ::ₘ s ∧ Associated p q
Tactic:
have := hs a (Multiset.mem_cons_self _ _)
State after:
case h₂
p : ℤ
hp : OddPrimeOrFour p
s✝ : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s✝ → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s✝
a : ℤ
s : Multiset ℤ
ih : (∀ (r : ℤ), r ∈ s → OddPrimeOrFour r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ Associated p q
hs : ∀ (r : ℤ), r ∈ a ::ₘ s → OddPrimeOrFour r
hdvd : p ∣ a * Multiset.prod s
this : OddPrimeOrFour a
⊢ ∃ q, q ∈ a ::ₘ s ∧ Associated p q

State before:
case h₂
p : ℤ
hp : OddPrimeOrFour p
s✝ : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s✝ → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s✝
a : ℤ
s : Multiset ℤ
ih : (∀ (r : ℤ), r ∈ s → OddPrimeOrFour r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ Associated p q
hs : ∀ (r : ℤ), r ∈ a ::ₘ s → OddPrimeOrFour r
hdvd : p ∣ a * Multiset.prod s
this : OddPrimeOrFour a
⊢ ∃ q, q ∈ a ::ₘ s ∧ Associated p q
Tactic:
obtain h | h := dvd_or_dvd this hp hdvd
State after:
case h₂.inl
p : ℤ
hp : OddPrimeOrFour p
s✝ : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s✝ → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s✝
a : ℤ
s : Multiset ℤ
ih : (∀ (r : ℤ), r ∈ s → OddPrimeOrFour r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ Associated p q
hs : ∀ (r : ℤ), r ∈ a ::ₘ s → OddPrimeOrFour r
hdvd : p ∣ a * Multiset.prod s
this : OddPrimeOrFour a
h : p ∣ a
⊢ ∃ q, q ∈ a ::ₘ s ∧ Associated p q

case h₂.inr
p : ℤ
hp : OddPrimeOrFour p
s✝ : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s✝ → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s✝
a : ℤ
s : Multiset ℤ
ih : (∀ (r : ℤ), r ∈ s → OddPrimeOrFour r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ Associated p q
hs : ∀ (r : ℤ), r ∈ a ::ₘ s → OddPrimeOrFour r
hdvd : p ∣ a * Multiset.prod s
this : OddPrimeOrFour a
h : p ∣ Multiset.prod s
⊢ ∃ q, q ∈ a ::ₘ s ∧ Associated p q

State before:
case h₂.inl
p : ℤ
hp : OddPrimeOrFour p
s✝ : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s✝ → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s✝
a : ℤ
s : Multiset ℤ
ih : (∀ (r : ℤ), r ∈ s → OddPrimeOrFour r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ Associated p q
hs : ∀ (r : ℤ), r ∈ a ::ₘ s → OddPrimeOrFour r
hdvd : p ∣ a * Multiset.prod s
this : OddPrimeOrFour a
h : p ∣ a
⊢ ∃ q, q ∈ a ::ₘ s ∧ Associated p q
Tactic:
exact ⟨a, Multiset.mem_cons_self _ _, associated_of_dvd this hp h⟩
State after:
no goals

State before:
case h₂.inr
p : ℤ
hp : OddPrimeOrFour p
s✝ : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s✝ → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s✝
a : ℤ
s : Multiset ℤ
ih : (∀ (r : ℤ), r ∈ s → OddPrimeOrFour r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ Associated p q
hs : ∀ (r : ℤ), r ∈ a ::ₘ s → OddPrimeOrFour r
hdvd : p ∣ a * Multiset.prod s
this : OddPrimeOrFour a
h : p ∣ Multiset.prod s
⊢ ∃ q, q ∈ a ::ₘ s ∧ Associated p q
Tactic:
obtain ⟨q, hq₁, hq₂⟩ := ih (fun r hr => hs _ (Multiset.mem_cons_of_mem hr)) h
State after:
case h₂.inr.intro.intro
p : ℤ
hp : OddPrimeOrFour p
s✝ : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s✝ → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s✝
a : ℤ
s : Multiset ℤ
ih : (∀ (r : ℤ), r ∈ s → OddPrimeOrFour r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ Associated p q
hs : ∀ (r : ℤ), r ∈ a ::ₘ s → OddPrimeOrFour r
hdvd : p ∣ a * Multiset.prod s
this : OddPrimeOrFour a
h : p ∣ Multiset.prod s
q : ℤ
hq₁ : q ∈ s
hq₂ : Associated p q
⊢ ∃ q, q ∈ a ::ₘ s ∧ Associated p q

State before:
case h₂.inr.intro.intro
p : ℤ
hp : OddPrimeOrFour p
s✝ : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s✝ → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s✝
a : ℤ
s : Multiset ℤ
ih : (∀ (r : ℤ), r ∈ s → OddPrimeOrFour r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ Associated p q
hs : ∀ (r : ℤ), r ∈ a ::ₘ s → OddPrimeOrFour r
hdvd : p ∣ a * Multiset.prod s
this : OddPrimeOrFour a
h : p ∣ Multiset.prod s
q : ℤ
hq₁ : q ∈ s
hq₂ : Associated p q
⊢ ∃ q, q ∈ a ::ₘ s ∧ Associated p q
Tactic:
exact ⟨q, Multiset.mem_cons_of_mem hq₁, hq₂⟩
State after:
no goals