Theorem: mem_of_dvd_prod (FltRegular/FltThree/OddPrimeOrFour.lean)

State before:
p : ℕ
hp : OddPrimeOrFour p
s : Multiset ℕ
hs : ∀ r ∈ s, OddPrimeOrFour r
hdvd : p ∣ s.prod
⊢ p ∈ s
Tactic:
induction' s using Multiset.induction_on with a s ih hs
State after:
case empty
p : ℕ
hp : OddPrimeOrFour p
hs : ∀ r ∈ 0, OddPrimeOrFour r
hdvd : p ∣ Multiset.prod 0
⊢ p ∈ 0

case cons
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ (a ::ₘ s).prod
⊢ p ∈ a ::ₘ s

State before:
case empty
p : ℕ
hp : OddPrimeOrFour p
hs : ∀ r ∈ 0, OddPrimeOrFour r
hdvd : p ∣ Multiset.prod 0
⊢ p ∈ 0
Tactic:
simp [hp.ne_one] at hdvd
State after:
no goals

State before:
case cons
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ (a ::ₘ s).prod
⊢ p ∈ a ::ₘ s
Tactic:
rw [Multiset.prod_cons] at hdvd
State after:
case cons
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ a * s.prod
⊢ p ∈ a ::ₘ s

State before:
case cons
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ a * s.prod
⊢ p ∈ a ::ₘ s
Tactic:
have := hs a (Multiset.mem_cons_self _ _)
State after:
case cons
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ a * s.prod
this : OddPrimeOrFour a
⊢ p ∈ a ::ₘ s

State before:
case cons
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ a * s.prod
this : OddPrimeOrFour a
⊢ p ∈ a ::ₘ s
Tactic:
obtain h | h := dvd_or_dvd this hp hdvd
State after:
case cons.inl
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ a * s.prod
this : OddPrimeOrFour a
h : p ∣ a
⊢ p ∈ a ::ₘ s

case cons.inr
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ a * s.prod
this : OddPrimeOrFour a
h : p ∣ s.prod
⊢ p ∈ a ::ₘ s

State before:
case cons.inl
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ a * s.prod
this : OddPrimeOrFour a
h : p ∣ a
⊢ p ∈ a ::ₘ s
Tactic:
rw [eq_of_dvd this hp h]
State after:
case cons.inl
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ a * s.prod
this : OddPrimeOrFour a
h : p ∣ a
⊢ a ∈ a ::ₘ s

State before:
case cons.inl
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ a * s.prod
this : OddPrimeOrFour a
h : p ∣ a
⊢ a ∈ a ::ₘ s
Tactic:
exact Multiset.mem_cons_self _ _
State after:
no goals

State before:
case cons.inr
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ a * s.prod
this : OddPrimeOrFour a
h : p ∣ s.prod
⊢ p ∈ a ::ₘ s
Tactic:
have := ih (fun r hr => hs _ (Multiset.mem_cons_of_mem hr)) h
State after:
case cons.inr
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ a * s.prod
this✝ : OddPrimeOrFour a
h : p ∣ s.prod
this : p ∈ s
⊢ p ∈ a ::ₘ s

State before:
case cons.inr
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ a * s.prod
this✝ : OddPrimeOrFour a
h : p ∣ s.prod
this : p ∈ s
⊢ p ∈ a ::ₘ s
Tactic:
exact Multiset.mem_cons_of_mem this
State after:
no goals