no goals
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝ : AddCommMonoid γ
κ : Type u_1
h : ι ≃ κ
f : ⨁ (i : ι), β i
k : κ
⊢ ↑(↑(equivCongrLeft h) f) k = ↑f (↑h.symm k)
exact Dfinsupp.comapDomain'_apply _ h.right_inv _ _