ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
this : ↑(↑liftAddHom (singleAddHom β)) f = ↑(AddMonoidHom.id (Π₀ (i : ι), β i)) f
⊢ sum f single = f
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
⊢ sum f single = f
have := FunLike.congr_fun (liftAddHom_singleAddHom (β := β)) f
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
this✝ : ↑(sumAddHom (singleAddHom β)) f = ↑(AddMonoidHom.id (Π₀ (i : ι), β i)) f
this : (sum f fun x => ↑(singleAddHom β x)) = ↑(AddMonoidHom.id (Π₀ (i : ι), β i)) f
⊢ sum f single = f
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
this : ↑(↑liftAddHom (singleAddHom β)) f = ↑(AddMonoidHom.id (Π₀ (i : ι), β i)) f
⊢ sum f single = f
rw [liftAddHom_apply, sumAddHom_apply] at this
no goals
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
this✝ : ↑(sumAddHom (singleAddHom β)) f = ↑(AddMonoidHom.id (Π₀ (i : ι), β i)) f
this : (sum f fun x => ↑(singleAddHom β x)) = ↑(AddMonoidHom.id (Π₀ (i : ι), β i)) f
⊢ sum f single = f
exact this