case h₁
ι : Type ?u.807675
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
S : Finset α
g1 g2 : α → β
h✝ : ∀ (a : α), a ∈ S → g1 a ∣ g2 a
h : ∀ (a : α), a ∈ ∅ → g1 a ∣ g2 a
⊢ Finset.prod ∅ g1 ∣ Finset.prod ∅ g2

case h₂
ι : Type ?u.807675
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f g : α → β
inst✝ : CommMonoid β
S : Finset α
g1 g2 : α → β
h✝ : ∀ (a : α), a ∈ S → g1 a ∣ g2 a
a : α
T : Finset α
_haS : a ∈ S
_hTS : T ⊆ S
haT : ¬a ∈ T
IH : (∀ (a : α), a ∈ T → g1 a ∣ g2 a) → Finset.prod T g1 ∣ Finset.prod T g2
h : ∀ (a_1 : α), a_1 ∈ insert a T → g1 a_1 ∣ g2 a_1
⊢ Finset.prod (insert a T) g1 ∣ Finset.prod (insert a T) g2
ι : Type ?u.807675
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
S : Finset α
g1 g2 : α → β
h : ∀ (a : α), a ∈ S → g1 a ∣ g2 a
⊢ Finset.prod S g1 ∣ Finset.prod S g2
induction' S using Finset.induction_on' with a T _haS _hTS haT IH
case h₂
ι : Type ?u.807675
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f g : α → β
inst✝ : CommMonoid β
S : Finset α
g1 g2 : α → β
h✝ : ∀ (a : α), a ∈ S → g1 a ∣ g2 a
a : α
T : Finset α
_haS : a ∈ S
_hTS : T ⊆ S
haT : ¬a ∈ T
IH : (∀ (a : α), a ∈ T → g1 a ∣ g2 a) → Finset.prod T g1 ∣ Finset.prod T g2
h : ∀ (a_1 : α), a_1 ∈ insert a T → g1 a_1 ∣ g2 a_1
⊢ g1 a * ∏ x in T, g1 x ∣ g2 a * ∏ x in T, g2 x
case h₂
ι : Type ?u.807675
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f g : α → β
inst✝ : CommMonoid β
S : Finset α
g1 g2 : α → β
h✝ : ∀ (a : α), a ∈ S → g1 a ∣ g2 a
a : α
T : Finset α
_haS : a ∈ S
_hTS : T ⊆ S
haT : ¬a ∈ T
IH : (∀ (a : α), a ∈ T → g1 a ∣ g2 a) → Finset.prod T g1 ∣ Finset.prod T g2
h : ∀ (a_1 : α), a_1 ∈ insert a T → g1 a_1 ∣ g2 a_1
⊢ Finset.prod (insert a T) g1 ∣ Finset.prod (insert a T) g2
rw [Finset.prod_insert haT, Finset.prod_insert haT]
no goals
case h₂
ι : Type ?u.807675
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f g : α → β
inst✝ : CommMonoid β
S : Finset α
g1 g2 : α → β
h✝ : ∀ (a : α), a ∈ S → g1 a ∣ g2 a
a : α
T : Finset α
_haS : a ∈ S
_hTS : T ⊆ S
haT : ¬a ∈ T
IH : (∀ (a : α), a ∈ T → g1 a ∣ g2 a) → Finset.prod T g1 ∣ Finset.prod T g2
h : ∀ (a_1 : α), a_1 ∈ insert a T → g1 a_1 ∣ g2 a_1
⊢ g1 a * ∏ x in T, g1 x ∣ g2 a * ∏ x in T, g2 x
exact mul_dvd_mul (h a $ T.mem_insert_self a) (IH fun b hb ↦ h b $ Finset.mem_insert_of_mem hb)
no goals
case h₁
ι : Type ?u.807675
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
S : Finset α
g1 g2 : α → β
h✝ : ∀ (a : α), a ∈ S → g1 a ∣ g2 a
h : ∀ (a : α), a ∈ ∅ → g1 a ∣ g2 a
⊢ Finset.prod ∅ g1 ∣ Finset.prod ∅ g2
simp