ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : (i : ι) → AddGroup (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommGroup γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂
this :
  ↑(↑liftAddHom fun a => AddMonoidHom.ofMapSub (h a) (_ : ∀ (b₁ b₂ : β a), h a (b₁ - b₂) = h a b₁ - h a b₂)) (f - g) =
    ↑(↑liftAddHom fun a => AddMonoidHom.ofMapSub (h a) (_ : ∀ (b₁ b₂ : β a), h a (b₁ - b₂) = h a b₁ - h a b₂)) f -
      ↑(↑liftAddHom fun a => AddMonoidHom.ofMapSub (h a) (_ : ∀ (b₁ b₂ : β a), h a (b₁ - b₂) = h a b₁ - h a b₂)) g
⊢ sum (f - g) h = sum f h - sum g h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : (i : ι) → AddGroup (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommGroup γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂
⊢ sum (f - g) h = sum f h - sum g h
have := (liftAddHom (β := β) fun a => AddMonoidHom.ofMapSub (h a) (h_sub a)).map_sub f g
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : (i : ι) → AddGroup (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommGroup γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂
this✝² :
  ↑(sumAddHom fun a => AddMonoidHom.ofMapSub (h a) (_ : ∀ (b₁ b₂ : β a), h a (b₁ - b₂) = h a b₁ - h a b₂)) (f - g) =
    ↑(sumAddHom fun a => AddMonoidHom.ofMapSub (h a) (_ : ∀ (b₁ b₂ : β a), h a (b₁ - b₂) = h a b₁ - h a b₂)) f -
      ↑(sumAddHom fun a => AddMonoidHom.ofMapSub (h a) (_ : ∀ (b₁ b₂ : β a), h a (b₁ - b₂) = h a b₁ - h a b₂)) g
this✝¹ :
  (sum (f - g) fun x => ↑(AddMonoidHom.ofMapSub (h x) (_ : ∀ (b₁ b₂ : β x), h x (b₁ - b₂) = h x b₁ - h x b₂))) =
    ↑(sumAddHom fun a => AddMonoidHom.ofMapSub (h a) (_ : ∀ (b₁ b₂ : β a), h a (b₁ - b₂) = h a b₁ - h a b₂)) f -
      ↑(sumAddHom fun a => AddMonoidHom.ofMapSub (h a) (_ : ∀ (b₁ b₂ : β a), h a (b₁ - b₂) = h a b₁ - h a b₂)) g
this✝ :
  (sum (f - g) fun x => ↑(AddMonoidHom.ofMapSub (h x) (_ : ∀ (b₁ b₂ : β x), h x (b₁ - b₂) = h x b₁ - h x b₂))) =
    (sum f fun x => ↑(AddMonoidHom.ofMapSub (h x) (_ : ∀ (b₁ b₂ : β x), h x (b₁ - b₂) = h x b₁ - h x b₂))) -
      ↑(sumAddHom fun a => AddMonoidHom.ofMapSub (h a) (_ : ∀ (b₁ b₂ : β a), h a (b₁ - b₂) = h a b₁ - h a b₂)) g
this :
  (sum (f - g) fun x => ↑(AddMonoidHom.ofMapSub (h x) (_ : ∀ (b₁ b₂ : β x), h x (b₁ - b₂) = h x b₁ - h x b₂))) =
    (sum f fun x => ↑(AddMonoidHom.ofMapSub (h x) (_ : ∀ (b₁ b₂ : β x), h x (b₁ - b₂) = h x b₁ - h x b₂))) -
      sum g fun x => ↑(AddMonoidHom.ofMapSub (h x) (_ : ∀ (b₁ b₂ : β x), h x (b₁ - b₂) = h x b₁ - h x b₂))
⊢ sum (f - g) h = sum f h - sum g h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : (i : ι) → AddGroup (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommGroup γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂
this :
  ↑(↑liftAddHom fun a => AddMonoidHom.ofMapSub (h a) (_ : ∀ (b₁ b₂ : β a), h a (b₁ - b₂) = h a b₁ - h a b₂)) (f - g) =
    ↑(↑liftAddHom fun a => AddMonoidHom.ofMapSub (h a) (_ : ∀ (b₁ b₂ : β a), h a (b₁ - b₂) = h a b₁ - h a b₂)) f -
      ↑(↑liftAddHom fun a => AddMonoidHom.ofMapSub (h a) (_ : ∀ (b₁ b₂ : β a), h a (b₁ - b₂) = h a b₁ - h a b₂)) g
⊢ sum (f - g) h = sum f h - sum g h
rw [liftAddHom_apply, sumAddHom_apply, sumAddHom_apply, sumAddHom_apply] at this
no goals
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : (i : ι) → AddGroup (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommGroup γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂
this✝² :
  ↑(sumAddHom fun a => AddMonoidHom.ofMapSub (h a) (_ : ∀ (b₁ b₂ : β a), h a (b₁ - b₂) = h a b₁ - h a b₂)) (f - g) =
    ↑(sumAddHom fun a => AddMonoidHom.ofMapSub (h a) (_ : ∀ (b₁ b₂ : β a), h a (b₁ - b₂) = h a b₁ - h a b₂)) f -
      ↑(sumAddHom fun a => AddMonoidHom.ofMapSub (h a) (_ : ∀ (b₁ b₂ : β a), h a (b₁ - b₂) = h a b₁ - h a b₂)) g
this✝¹ :
  (sum (f - g) fun x => ↑(AddMonoidHom.ofMapSub (h x) (_ : ∀ (b₁ b₂ : β x), h x (b₁ - b₂) = h x b₁ - h x b₂))) =
    ↑(sumAddHom fun a => AddMonoidHom.ofMapSub (h a) (_ : ∀ (b₁ b₂ : β a), h a (b₁ - b₂) = h a b₁ - h a b₂)) f -
      ↑(sumAddHom fun a => AddMonoidHom.ofMapSub (h a) (_ : ∀ (b₁ b₂ : β a), h a (b₁ - b₂) = h a b₁ - h a b₂)) g
this✝ :
  (sum (f - g) fun x => ↑(AddMonoidHom.ofMapSub (h x) (_ : ∀ (b₁ b₂ : β x), h x (b₁ - b₂) = h x b₁ - h x b₂))) =
    (sum f fun x => ↑(AddMonoidHom.ofMapSub (h x) (_ : ∀ (b₁ b₂ : β x), h x (b₁ - b₂) = h x b₁ - h x b₂))) -
      ↑(sumAddHom fun a => AddMonoidHom.ofMapSub (h a) (_ : ∀ (b₁ b₂ : β a), h a (b₁ - b₂) = h a b₁ - h a b₂)) g
this :
  (sum (f - g) fun x => ↑(AddMonoidHom.ofMapSub (h x) (_ : ∀ (b₁ b₂ : β x), h x (b₁ - b₂) = h x b₁ - h x b₂))) =
    (sum f fun x => ↑(AddMonoidHom.ofMapSub (h x) (_ : ∀ (b₁ b₂ : β x), h x (b₁ - b₂) = h x b₁ - h x b₂))) -
      sum g fun x => ↑(AddMonoidHom.ofMapSub (h x) (_ : ∀ (b₁ b₂ : β x), h x (b₁ - b₂) = h x b₁ - h x b₂))
⊢ sum (f - g) h = sum f h - sum g h
exact this