no goals
ι : Type ?u.810222
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommSemiring β
s : Finset α
i : α
f g h : α → β
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ (j : α), j ∈ s → j ≠ i → g j = f j
h3 : ∀ (j : α), j ∈ s → j ≠ i → h j = f j
⊢ ∏ i in s, g i + ∏ i in s, h i = ∏ i in s, f i
classical
  simp_rw [prod_eq_mul_prod_diff_singleton hi, ← h1, right_distrib]
  congr 2 <;> apply prod_congr rfl <;> simpa
ι : Type ?u.810222
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommSemiring β
s : Finset α
i : α
f g h : α → β
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ (j : α), j ∈ s → j ≠ i → g j = f j
h3 : ∀ (j : α), j ∈ s → j ≠ i → h j = f j
⊢ g i * ∏ i in s \ {i}, g i + h i * ∏ i in s \ {i}, h i = g i * ∏ i in s \ {i}, f i + h i * ∏ i in s \ {i}, f i
ι : Type ?u.810222
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommSemiring β
s : Finset α
i : α
f g h : α → β
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ (j : α), j ∈ s → j ≠ i → g j = f j
h3 : ∀ (j : α), j ∈ s → j ≠ i → h j = f j
⊢ ∏ i in s, g i + ∏ i in s, h i = ∏ i in s, f i
simp_rw [prod_eq_mul_prod_diff_singleton hi, ← h1, right_distrib]
no goals
ι : Type ?u.810222
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommSemiring β
s : Finset α
i : α
f g h : α → β
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ (j : α), j ∈ s → j ≠ i → g j = f j
h3 : ∀ (j : α), j ∈ s → j ≠ i → h j = f j
⊢ g i * ∏ i in s \ {i}, g i + h i * ∏ i in s \ {i}, h i = g i * ∏ i in s \ {i}, f i + h i * ∏ i in s \ {i}, f i
congr 2 <;> apply prod_congr rfl <;> simpa