no goals
α : Type u_1
β : Type u_2
γ : Type ?u.14166
inst✝¹ : Fintype α
inst✝ : CommMonoid β
f : { a // a ∈ univ } → β
x : { x // x ∈ univ }
⊢ f x =
    f
      { val := ↑(Equiv.subtypeUnivEquiv (_ : ∀ (x : α), x ∈ univ)) x,
        property := (_ : ↑(Equiv.subtypeUnivEquiv (_ : ∀ (x : α), x ∈ univ)) x ∈ univ) }
simp