case mk'.mk.mk.mk'.mk.mk
ι : Type u
γ✝ : Type w
β : ι → Type v
β₁✝ : ι → Type v₁
β₂✝ : ι → Type v₂
dec : DecidableEq ι
ι₁ : Type u_1
ι₂ : Type u_2
β₁ : ι₁ → Type u_3
β₂ : ι₂ → Type u_4
γ : Type u_5
inst✝⁴ : DecidableEq ι₁
inst✝³ : DecidableEq ι₂
inst✝² : (i : ι₁) → AddZeroClass (β₁ i)
inst✝¹ : (i : ι₂) → AddZeroClass (β₂ i)
inst✝ : AddCommMonoid γ
h : (i : ι₁) → (j : ι₂) → β₁ i →+ β₂ j →+ γ
f₁ : (i : ι₁) → β₁ i
support'✝¹ : Trunc { s // ∀ (i : ι₁), i ∈ s ∨ f₁ i = 0 }
s₁ : Multiset ι₁
h₁ : ∀ (i : ι₁), i ∈ s₁ ∨ f₁ i = 0
f₂ : (i : ι₂) → β₂ i
support'✝ : Trunc { s // ∀ (i : ι₂), i ∈ s ∨ f₂ i = 0 }
s₂ : Multiset ι₂
h₂ : ∀ (i : ι₂), i ∈ s₂ ∨ f₂ i = 0
⊢ ↑(sumAddHom fun i₂ =>
          ↑(sumAddHom fun i₁ => h i₁ i₂) { toFun := f₁, support' := Quot.mk Setoid.r { val := s₁, property := h₁ } })
      { toFun := f₂, support' := Quot.mk Setoid.r { val := s₂, property := h₂ } } =
    ↑(sumAddHom fun i₁ =>
          ↑(sumAddHom fun i₂ => AddMonoidHom.flip (h i₁ i₂))
            { toFun := f₂, support' := Quot.mk Setoid.r { val := s₂, property := h₂ } })
      { toFun := f₁, support' := Quot.mk Setoid.r { val := s₁, property := h₁ } }
ι : Type u
γ✝ : Type w
β : ι → Type v
β₁✝ : ι → Type v₁
β₂✝ : ι → Type v₂
dec : DecidableEq ι
ι₁ : Type u_1
ι₂ : Type u_2
β₁ : ι₁ → Type u_3
β₂ : ι₂ → Type u_4
γ : Type u_5
inst✝⁴ : DecidableEq ι₁
inst✝³ : DecidableEq ι₂
inst✝² : (i : ι₁) → AddZeroClass (β₁ i)
inst✝¹ : (i : ι₂) → AddZeroClass (β₂ i)
inst✝ : AddCommMonoid γ
f₁ : Π₀ (i : ι₁), β₁ i
f₂ : Π₀ (i : ι₂), β₂ i
h : (i : ι₁) → (j : ι₂) → β₁ i →+ β₂ j →+ γ
⊢ ↑(sumAddHom fun i₂ => ↑(sumAddHom fun i₁ => h i₁ i₂) f₁) f₂ =
    ↑(sumAddHom fun i₁ => ↑(sumAddHom fun i₂ => AddMonoidHom.flip (h i₁ i₂)) f₂) f₁
obtain ⟨⟨f₁, s₁, h₁⟩, ⟨f₂, s₂, h₂⟩⟩ := f₁, f₂
case mk'.mk.mk.mk'.mk.mk
ι : Type u
γ✝ : Type w
β : ι → Type v
β₁✝ : ι → Type v₁
β₂✝ : ι → Type v₂
dec : DecidableEq ι
ι₁ : Type u_1
ι₂ : Type u_2
β₁ : ι₁ → Type u_3
β₂ : ι₂ → Type u_4
γ : Type u_5
inst✝⁴ : DecidableEq ι₁
inst✝³ : DecidableEq ι₂
inst✝² : (i : ι₁) → AddZeroClass (β₁ i)
inst✝¹ : (i : ι₂) → AddZeroClass (β₂ i)
inst✝ : AddCommMonoid γ
h : (i : ι₁) → (j : ι₂) → β₁ i →+ β₂ j →+ γ
f₁ : (i : ι₁) → β₁ i
support'✝¹ : Trunc { s // ∀ (i : ι₁), i ∈ s ∨ f₁ i = 0 }
s₁ : Multiset ι₁
h₁ : ∀ (i : ι₁), i ∈ s₁ ∨ f₁ i = 0
f₂ : (i : ι₂) → β₂ i
support'✝ : Trunc { s // ∀ (i : ι₂), i ∈ s ∨ f₂ i = 0 }
s₂ : Multiset ι₂
h₂ : ∀ (i : ι₂), i ∈ s₂ ∨ f₂ i = 0
⊢ ∑ x in Multiset.toFinset s₂, ∑ x_1 in Multiset.toFinset s₁, ↑(↑(h x_1 x) (f₁ x_1)) (f₂ x) =
    ∑ x in Multiset.toFinset s₁, ∑ x_1 in Multiset.toFinset s₂, ↑(↑(h x x_1) (f₁ x)) (f₂ x_1)
case mk'.mk.mk.mk'.mk.mk
ι : Type u
γ✝ : Type w
β : ι → Type v
β₁✝ : ι → Type v₁
β₂✝ : ι → Type v₂
dec : DecidableEq ι
ι₁ : Type u_1
ι₂ : Type u_2
β₁ : ι₁ → Type u_3
β₂ : ι₂ → Type u_4
γ : Type u_5
inst✝⁴ : DecidableEq ι₁
inst✝³ : DecidableEq ι₂
inst✝² : (i : ι₁) → AddZeroClass (β₁ i)
inst✝¹ : (i : ι₂) → AddZeroClass (β₂ i)
inst✝ : AddCommMonoid γ
h : (i : ι₁) → (j : ι₂) → β₁ i →+ β₂ j →+ γ
f₁ : (i : ι₁) → β₁ i
support'✝¹ : Trunc { s // ∀ (i : ι₁), i ∈ s ∨ f₁ i = 0 }
s₁ : Multiset ι₁
h₁ : ∀ (i : ι₁), i ∈ s₁ ∨ f₁ i = 0
f₂ : (i : ι₂) → β₂ i
support'✝ : Trunc { s // ∀ (i : ι₂), i ∈ s ∨ f₂ i = 0 }
s₂ : Multiset ι₂
h₂ : ∀ (i : ι₂), i ∈ s₂ ∨ f₂ i = 0
⊢ ↑(sumAddHom fun i₂ =>
          ↑(sumAddHom fun i₁ => h i₁ i₂) { toFun := f₁, support' := Quot.mk Setoid.r { val := s₁, property := h₁ } })
      { toFun := f₂, support' := Quot.mk Setoid.r { val := s₂, property := h₂ } } =
    ↑(sumAddHom fun i₁ =>
          ↑(sumAddHom fun i₂ => AddMonoidHom.flip (h i₁ i₂))
            { toFun := f₂, support' := Quot.mk Setoid.r { val := s₂, property := h₂ } })
      { toFun := f₁, support' := Quot.mk Setoid.r { val := s₁, property := h₁ } }
simp only [sumAddHom, AddMonoidHom.finset_sum_apply, Quotient.liftOn_mk, AddMonoidHom.coe_mk,
  AddMonoidHom.flip_apply, Trunc.lift, toFun_eq_coe, ZeroHom.coe_mk, coe_mk']
no goals
case mk'.mk.mk.mk'.mk.mk
ι : Type u
γ✝ : Type w
β : ι → Type v
β₁✝ : ι → Type v₁
β₂✝ : ι → Type v₂
dec : DecidableEq ι
ι₁ : Type u_1
ι₂ : Type u_2
β₁ : ι₁ → Type u_3
β₂ : ι₂ → Type u_4
γ : Type u_5
inst✝⁴ : DecidableEq ι₁
inst✝³ : DecidableEq ι₂
inst✝² : (i : ι₁) → AddZeroClass (β₁ i)
inst✝¹ : (i : ι₂) → AddZeroClass (β₂ i)
inst✝ : AddCommMonoid γ
h : (i : ι₁) → (j : ι₂) → β₁ i →+ β₂ j →+ γ
f₁ : (i : ι₁) → β₁ i
support'✝¹ : Trunc { s // ∀ (i : ι₁), i ∈ s ∨ f₁ i = 0 }
s₁ : Multiset ι₁
h₁ : ∀ (i : ι₁), i ∈ s₁ ∨ f₁ i = 0
f₂ : (i : ι₂) → β₂ i
support'✝ : Trunc { s // ∀ (i : ι₂), i ∈ s ∨ f₂ i = 0 }
s₂ : Multiset ι₂
h₂ : ∀ (i : ι₂), i ∈ s₂ ∨ f₂ i = 0
⊢ ∑ x in Multiset.toFinset s₂, ∑ x_1 in Multiset.toFinset s₁, ↑(↑(h x_1 x) (f₁ x_1)) (f₂ x) =
    ∑ x in Multiset.toFinset s₁, ∑ x_1 in Multiset.toFinset s₂, ↑(↑(h x x_1) (f₁ x)) (f₂ x_1)
exact Finset.sum_comm