ι : Type ?u.790472
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
h : ¬i ∈ s
f : α → β
b : β
⊢ ∀ (x : α), x ∈ s → Function.update f i b x = f x
ι : Type ?u.790472
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
h : ¬i ∈ s
f : α → β
b : β
⊢ ∏ x in s, Function.update f i b x = ∏ x in s, f x
apply prod_congr rfl
ι : Type ?u.790472
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
h : ¬i ∈ s
f : α → β
b : β
j : α
hj : j ∈ s
⊢ Function.update f i b j = f j
ι : Type ?u.790472
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
h : ¬i ∈ s
f : α → β
b : β
⊢ ∀ (x : α), x ∈ s → Function.update f i b x = f x
intros j hj
ι : Type ?u.790472
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
h : ¬i ∈ s
f : α → β
b : β
j : α
hj : j ∈ s
this : j ≠ i
⊢ Function.update f i b j = f j
ι : Type ?u.790472
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
h : ¬i ∈ s
f : α → β
b : β
j : α
hj : j ∈ s
⊢ Function.update f i b j = f j
have : j ≠ i := by
  rintro rfl
  exact h hj
no goals
ι : Type ?u.790472
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
h : ¬i ∈ s
f : α → β
b : β
j : α
hj : j ∈ s
this : j ≠ i
⊢ Function.update f i b j = f j
simp [this]
ι : Type ?u.790472
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
f : α → β
b : β
j : α
hj : j ∈ s
h : ¬j ∈ s
⊢ False
ι : Type ?u.790472
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
h : ¬i ∈ s
f : α → β
b : β
j : α
hj : j ∈ s
⊢ j ≠ i
rintro rfl
no goals
ι : Type ?u.790472
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
f : α → β
b : β
j : α
hj : j ∈ s
h : ¬j ∈ s
⊢ False
exact h hj