case h₁
ι : Type ?u.85910
α : Type u_2
β : Type u_1
γ : Type ?u.85919
inst✝ : CommMonoid β
S : Multiset α
g1 g2 : α → β
h : ∀ (a : α), a ∈ S → g1 a ∣ g2 a
⊢ prod (map g1 0) ∣ prod (map g2 0)

case h₂
ι : Type ?u.85910
α : Type u_2
β : Type u_1
γ : Type ?u.85919
inst✝ : CommMonoid β
S : Multiset α
g1 g2 : α → β
h : ∀ (a : α), a ∈ S → g1 a ∣ g2 a
⊢ ∀ {a : α} {s : Multiset α},
    a ∈ S → s ⊆ S → prod (map g1 s) ∣ prod (map g2 s) → prod (map g1 (insert a s)) ∣ prod (map g2 (insert a s))
ι : Type ?u.85910
α : Type u_2
β : Type u_1
γ : Type ?u.85919
inst✝ : CommMonoid β
S : Multiset α
g1 g2 : α → β
h : ∀ (a : α), a ∈ S → g1 a ∣ g2 a
⊢ prod (map g1 S) ∣ prod (map g2 S)
apply Multiset.induction_on' S
case h₂
ι : Type ?u.85910
α : Type u_2
β : Type u_1
γ : Type ?u.85919
inst✝ : CommMonoid β
S : Multiset α
g1 g2 : α → β
h : ∀ (a : α), a ∈ S → g1 a ∣ g2 a
a : α
T : Multiset α
haS : a ∈ S
a✝ : T ⊆ S
IH : prod (map g1 T) ∣ prod (map g2 T)
⊢ prod (map g1 (insert a T)) ∣ prod (map g2 (insert a T))
case h₂
ι : Type ?u.85910
α : Type u_2
β : Type u_1
γ : Type ?u.85919
inst✝ : CommMonoid β
S : Multiset α
g1 g2 : α → β
h : ∀ (a : α), a ∈ S → g1 a ∣ g2 a
⊢ ∀ {a : α} {s : Multiset α},
    a ∈ S → s ⊆ S → prod (map g1 s) ∣ prod (map g2 s) → prod (map g1 (insert a s)) ∣ prod (map g2 (insert a s))
intro a T haS _ IH
no goals
case h₂
ι : Type ?u.85910
α : Type u_2
β : Type u_1
γ : Type ?u.85919
inst✝ : CommMonoid β
S : Multiset α
g1 g2 : α → β
h : ∀ (a : α), a ∈ S → g1 a ∣ g2 a
a : α
T : Multiset α
haS : a ∈ S
a✝ : T ⊆ S
IH : prod (map g1 T) ∣ prod (map g2 T)
⊢ prod (map g1 (insert a T)) ∣ prod (map g2 (insert a T))
simp [mul_dvd_mul (h a haS) IH]
no goals
case h₁
ι : Type ?u.85910
α : Type u_2
β : Type u_1
γ : Type ?u.85919
inst✝ : CommMonoid β
S : Multiset α
g1 g2 : α → β
h : ∀ (a : α), a ∈ S → g1 a ∣ g2 a
⊢ prod (map g1 0) ∣ prod (map g2 0)
simp