ι : Type ?u.331175
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
h : s₁ ⊆ s₂
hg : ∀ (x : α), x ∈ s₂ \ s₁ → g x = 1
hfg : ∀ (x : α), x ∈ s₁ → f x = g x
⊢ ∏ i in s₁, f i = ∏ x in s₁, g x
ι : Type ?u.331175
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
h : s₁ ⊆ s₂
hg : ∀ (x : α), x ∈ s₂ \ s₁ → g x = 1
hfg : ∀ (x : α), x ∈ s₁ → f x = g x
⊢ ∏ i in s₁, f i = ∏ i in s₂, g i
rw [← prod_sdiff h, prod_eq_one hg, one_mul]
no goals
ι : Type ?u.331175
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
h : s₁ ⊆ s₂
hg : ∀ (x : α), x ∈ s₂ \ s₁ → g x = 1
hfg : ∀ (x : α), x ∈ s₁ → f x = g x
⊢ ∏ i in s₁, f i = ∏ x in s₁, g x
exact prod_congr rfl hfg