-- Mathlib/Data/DFinsupp/BigOperators.lean
theorem sumAddHom_comm {ι₁ ι₂ : Sort _} {β₁ : ι₁ → Type*} {β₂ : ι₂ → Type*} {γ : Type*}
    [DecidableEq ι₁] [DecidableEq ι₂] [∀ i, AddZeroClass (β₁ i)] [∀ i, AddZeroClass (β₂ i)]
    [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₂ => (h i₁ i₂).flip) f₂) f₁

Proof state:
case mk'.mk.mk.mk'.mk.mk
ι₁ : Type u_4
ι₂ : Type u_5
β₁ : ι₁ → Type u_1
β₂ : ι₂ → Type u_2
γ : Type u_3
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 ∈ s₂.toFinset, ∑ x_1 ∈ s₁.toFinset, ((h x_1 x) (f₁ x_1)) (f₂ x) =
    ∑ x ∈ s₁.toFinset, ∑ x_1 ∈ s₂.toFinset, ((h x x_1) (f₁ x)) (f₂ x_1)

Tactic:
exact Finset.sum_comm

Result:
no goals

Proof state:
case mk'.mk.mk.mk'.mk.mk
ι₁ : Type u_4
ι₂ : Type u_5
β₁ : ι₁ → Type u_1
β₂ : ι₂ → Type u_2
γ : Type u_3
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 ⇑trueSetoid ⟨s₁, h₁⟩ })
      { toFun := f₂, support' := Quot.mk ⇑trueSetoid ⟨s₂, h₂⟩ } =
    (sumAddHom fun i₁ => (sumAddHom fun i₂ => (h i₁ i₂).flip) { toFun := f₂, support' := Quot.mk ⇑trueSetoid ⟨s₂, h₂⟩ })
      { toFun := f₁, support' := Quot.mk ⇑trueSetoid ⟨s₁, h₁⟩ }

Tactic:
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']

Result:
case mk'.mk.mk.mk'.mk.mk
ι₁ : Type u_4
ι₂ : Type u_5
β₁ : ι₁ → Type u_1
β₂ : ι₂ → Type u_2
γ : Type u_3
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 ∈ s₂.toFinset, ∑ x_1 ∈ s₁.toFinset, ((h x_1 x) (f₁ x_1)) (f₂ x) =
    ∑ x ∈ s₁.toFinset, ∑ x_1 ∈ s₂.toFinset, ((h x x_1) (f₁ x)) (f₂ x_1)

Proof state:
ι₁ : Type u_4
ι₂ : Type u_5
β₁ : ι₁ → Type u_1
β₂ : ι₂ → Type u_2
γ : Type u_3
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₂ => (h i₁ i₂).flip) f₂) f₁

Tactic:
obtain ⟨⟨f₁, s₁, h₁⟩, ⟨f₂, s₂, h₂⟩⟩ := f₁, f₂

Result:
case mk'.mk.mk.mk'.mk.mk
ι₁ : Type u_4
ι₂ : Type u_5
β₁ : ι₁ → Type u_1
β₂ : ι₂ → Type u_2
γ : Type u_3
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 ⇑trueSetoid ⟨s₁, h₁⟩ })
      { toFun := f₂, support' := Quot.mk ⇑trueSetoid ⟨s₂, h₂⟩ } =
    (sumAddHom fun i₁ => (sumAddHom fun i₂ => (h i₁ i₂).flip) { toFun := f₂, support' := Quot.mk ⇑trueSetoid ⟨s₂, h₂⟩ })
      { toFun := f₁, support' := Quot.mk ⇑trueSetoid ⟨s₁, h₁⟩ }