case intro.intro
ι : Type ?u.819790
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : NonUnitalNonAssocSemiring β
s : Finset α
f : α → β
b : β
h : ∀ (i : α), i ∈ s → Commute b (f i)
i : α
hi : i ∈ s.val
hb : f i ∈ Multiset.map (fun i => f i) s.val
⊢ Commute b (f i)
ι : Type ?u.819790
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : NonUnitalNonAssocSemiring β
s : Finset α
f : α → β
b✝ : β
h : ∀ (i : α), i ∈ s → Commute b✝ (f i)
b : β
hb : b ∈ Multiset.map (fun i => f i) s.val
⊢ Commute b✝ b
obtain ⟨i, hi, rfl⟩ := Multiset.mem_map.mp hb
no goals
case intro.intro
ι : Type ?u.819790
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : NonUnitalNonAssocSemiring β
s : Finset α
f : α → β
b : β
h : ∀ (i : α), i ∈ s → Commute b (f i)
i : α
hi : i ∈ s.val
hb : f i ∈ Multiset.map (fun i => f i) s.val
⊢ Commute b (f i)
exact h _ hi