awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → AddMonoidHom.{v, w} (β i) γ
f : (i : ι) → β i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'_1 : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
i : ι
h : i ∈ (sf + sg).toFinset
H2 : i ∉ sf
mk : Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) 0 : γ) (0 : γ)
mk₁ mk₂ : Eq.{w + 1} (α := γ) 0 0
⊢ Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) (f i) : γ) (0 : γ)

Tactic:
rw [(hf i).resolve_left H2, map_zero]

Premises used: map_zero, Or.resolve_left
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → AddMonoidHom.{v, w} (β i) γ
f : (i : ι) → β i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'_1 : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
⊢ Eq.{w + 1} (α := γ) (∑ x ∈ (sf + sg).toFinset, (φ x : (a : β x) → γ) (g x))
    (∑ x ∈ sg.toFinset, (φ x : (a : β x) → γ) (g x))

Tactic:
(Finset.sum_subset ?_ ?_).symm

Premises used: Finset.sum_subset, Eq.symm
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → AddMonoidHom.{v, w} (β i) γ
f : (i : ι) → β i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'_1 : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
mk : sg.toFinset ⊆ (sf + sg).toFinset
mk₁ : ∀ x ∈ (sf + sg).toFinset, x ∉ sg.toFinset → Eq.{w + 1} (α := γ) ((φ x : (a : β x) → γ) (g x) : γ) (0 : γ)
⊢ Eq.{w + 1} (α := γ) (∑ x ∈ (sf + sg).toFinset, (φ x : (a : β x) → γ) (g x))
    (∑ x ∈ sg.toFinset, (φ x : (a : β x) → γ) (g x))

Tactic:
refine (Finset.sum_subset ?_ ?_).symm

Premises used: Finset.sum_subset, Eq.symm
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → AddMonoidHom.{v, w} (β i) γ
f : (i : ι) → β i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'_1 : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
i : ι
mk : i ∈ sg → i ∈ sf ∨ i ∈ sg
⊢ i ∈ sg.toFinset → i ∈ (sf + sg).toFinset

Tactic:
simp only [Multiset.mem_toFinset, Multiset.mem_add]

Premises used: Multiset.mem_add, Multiset.mem_toFinset
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → AddMonoidHom.{v, w} (β i) γ
f : (i : ι) → β i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'_1 : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
i : ι
⊢ i ∈ sg → i ∈ sf ∨ i ∈ sg

Tactic:
Or.inr

Premises used: Or.inr
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → AddMonoidHom.{v, w} (β i) γ
f : (i : ι) → β i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'_1 : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
i : ι
⊢ i ∈ sg → i ∈ sf ∨ i ∈ sg

Tactic:
exact Or.inr

Premises used: Or.inr
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → AddMonoidHom.{v, w} (β i) γ
f : (i : ι) → β i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'_1 : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
i : ι
mk : i ∈ (sf + sg).toFinset → i ∉ sg.toFinset → Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) (g i) : γ) (0 : γ)
⊢ i ∈ (sf + sg).toFinset → i ∉ sg.toFinset → Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) (g i) : γ) (0 : γ)

Tactic:
_
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → AddMonoidHom.{v, w} (β i) γ
f : (i : ι) → β i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'_1 : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
i : ι
h : i ∈ (sf + sg).toFinset
H2 : i ∉ sg.toFinset
⊢ i ∉ sg

Tactic:
simp only [Multiset.mem_toFinset] at H2

Premises used: Multiset.mem_toFinset
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → AddMonoidHom.{v, w} (β i) γ
f : (i : ι) → β i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'_1 : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
i : ι
h : i ∈ (sf + sg).toFinset
H2 : i ∉ sg
mk : Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) 0 : γ) (0 : γ)
mk₁ mk₂ : Eq.{w + 1} (α := γ) 0 0
⊢ Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) (g i) : γ) (0 : γ)

Tactic:
rw [(hg i).resolve_left H2, map_zero]

Premises used: map_zero, Or.resolve_left
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → AddMonoidHom.{v, w} (β i) γ
i : ι
x : β i
⊢ Eq.{w + 1} (α := γ) ((sumAddHom (β := β) φ : (a : Π₀ (i : ι), β i) → γ) (single (β := β) i x) : γ)
    ((φ i : (a : β i) → γ) x : γ)

Tactic:
sumZeroHom_single _ _ _

Premises used: DFinsupp.sumZeroHom_single
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
i : ι
φ : AddMonoidHom.{v, w} (β i) γ
⊢ Eq (α := ZeroHom (Π₀ (i : ι), β i) γ)
    (sumZeroHom (β := β) (Pi.single (M := fun (i : ι) ↦ ZeroHom.{v, w} (β i) γ) i (↑φ : ZeroHom (β i) γ)))
    ((↑φ : ZeroHom (β i) γ).comp { toFun := fun (x : Π₀ (i : ι), β i) ↦ (x : (a : ι) → β a) i, map_zero' := ⋯ })

Tactic:
sumZeroHom_piSingle i φ.toZeroHom

Premises used: AddMonoidHom.toZeroHom, DFinsupp.sumZeroHom_piSingle
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
i : ι
φ : AddMonoidHom.{v, w} (β i) γ
h :
  Eq (α := ZeroHom (Π₀ (i : ι), β i) γ)
    (↑(sumAddHom (β := β) (Pi.single (M := fun (i : ι) ↦ AddMonoidHom.{v, w} (β i) γ) i φ)) :
      ZeroHom (Π₀ (i : ι), β i) γ)
    (sumZeroHom (β := β) (Pi.single (M := fun (i : ι) ↦ ZeroHom.{v, w} (β i) γ) i (↑φ : ZeroHom (β i) γ)))
⊢ (↑(sumAddHom (β := β) (Pi.single (M := fun (i : ι) ↦ AddMonoidHom.{v, w} (β i) γ) i φ)) :
      ZeroHom (Π₀ (i : ι), β i) γ) =
    (↑(φ.comp (evalAddMonoidHom (β := β) i)) : ZeroHom (Π₀ (i : ι), β i) γ)

Tactic:
convert! sumZeroHom_piSingle i φ.toZeroHom using 1

Premises used: AddMonoidHom.toZeroHom, DFinsupp.sumZeroHom_piSingle
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
i : ι
φ : AddMonoidHom.{v, w} (β i) γ
h : ∀ (i_1 : ι), (↑(Pi.single (M := fun (i : ι) ↦ AddMonoidHom.{v, w} (β i) γ) i φ i_1) : ZeroHom (β i_1) γ)
| sumZeroHom (β := β) fun (i_1 : ι) ↦
    (↑(Pi.single (M := fun (i : ι) ↦ AddMonoidHom.{v, w} (β i) γ) i φ i_1) : ZeroHom (β i_1) γ)

Tactic:
enter [1, i]
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
i_1 : ι
φ : AddMonoidHom.{v, w} (β i_1) γ
i : ι
h : (Pi.single (M := fun (i : ι) ↦ ZeroHom.{v, w} (β i) γ) i_1 (↑φ : ZeroHom (β i_1) γ) i : ZeroHom.{v, w} (β i) γ)
| (↑(Pi.single (M := fun (i : ι) ↦ AddMonoidHom.{v, w} (β i) γ) i_1 φ i) : ZeroHom (β i) γ)

Tactic:
rw [Pi.apply_single (fun i (x : β i →+ γ) => x.toZeroHom) (fun _ => rfl)]

Premises used: Pi.apply_single, AddMonoidHom.toZeroHom, rfl
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
i : ι
φ : AddMonoidHom.{v, w} (β i) γ
h :
  ∀ (i_1 : ι),
    (Pi.single (M := fun (i : ι) ↦ ZeroHom.{v, w} (β i) γ) i (↑φ : ZeroHom (β i) γ) i_1 : ZeroHom.{v, w} (β i_1) γ)
| sumZeroHom (β := β) fun (i_1 : ι) ↦
    (↑(Pi.single (M := fun (i : ι) ↦ AddMonoidHom.{v, w} (β i) γ) i φ i_1) : ZeroHom (β i_1) γ)

Tactic:
enter [1, i]
      rw [Pi.apply_single (fun i (x : β i →+ γ) => x.toZeroHom) (fun _ => rfl)]

Premises used: Pi.apply_single, AddMonoidHom.toZeroHom, rfl
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
i : ι
φ : AddMonoidHom.{v, w} (β i) γ
conv_lhs :
  Eq (α := ZeroHom (Π₀ (i : ι), β i) γ)
    (sumZeroHom (β := β) fun (i_1 : ι) ↦
      (↑(Pi.single (M := fun (i : ι) ↦ AddMonoidHom.{v, w} (β i) γ) i φ i_1) : ZeroHom (β i_1) γ))
    (sumZeroHom (β := β) (Pi.single (M := fun (i : ι) ↦ ZeroHom.{v, w} (β i) γ) i (↑φ : ZeroHom (β i) γ)))
h :
  Eq (α := ZeroHom (Π₀ (i : ι), β i) γ)
    (sumZeroHom (β := β) (Pi.single (M := fun (i : ι) ↦ ZeroHom.{v, w} (β i) γ) i (↑φ : ZeroHom (β i) γ)))
    (sumZeroHom (β := β) (Pi.single (M := fun (i : ι) ↦ ZeroHom.{v, w} (β i) γ) i (↑φ : ZeroHom (β i) γ)))
⊢ Eq (α := ZeroHom (Π₀ (i : ι), β i) γ)
    (sumZeroHom (β := β) fun (i_1 : ι) ↦
      (↑(Pi.single (M := fun (i : ι) ↦ AddMonoidHom.{v, w} (β i) γ) i φ i_1) : ZeroHom (β i_1) γ))
    (sumZeroHom (β := β) (Pi.single (M := fun (i : ι) ↦ ZeroHom.{v, w} (β i) γ) i (↑φ : ZeroHom (β i) γ)))

Tactic:
conv_lhs =>
      enter [1, i]
      rw [Pi.apply_single (fun i (x : β i →+ γ) => x.toZeroHom) (fun _ => rfl)]

Premises used: Pi.apply_single, AddMonoidHom.toZeroHom, rfl
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
f : (i : ι) → AddMonoidHom.{v, w} (β i) γ
i : ι
⊢ (sumAddHom (β := β) f).comp (singleAddHom β i) = f i

Tactic:
AddMonoidHom.ext fun x => sumAddHom_single f i x

Premises used: DFinsupp.sumAddHom_single, AddMonoidHom.ext
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : AddCommMonoid γ
φ : (i : ι) → AddMonoidHom.{v, w} (β i) γ
f : Π₀ (i : ι), β i
⊢ Eq.{w + 1} (α := γ) ((sumAddHom (β := β) φ : (a : Π₀ (i : ι), β i) → γ) f : γ)
    (f.sum (β := β) fun (x : ι) ↦ (⇑(φ x) : (a : β x) → γ) : γ)

Tactic:
sumZeroHom_apply _ _

Premises used: DFinsupp.sumZeroHom_apply
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι₁ : Type u_4
ι₂ : Type u_5
β₁ : ι₁ → Type u_1
β₂ : ι₂ → Type u_2
γ : Type u_3
inst : DecidableEq ι₁
inst_1 : DecidableEq ι₂
inst_2 : (i : ι₁) → AddZeroClass (β₁ i)
inst_3 : (i : ι₂) → AddZeroClass (β₂ i)
inst_4 : AddCommMonoid γ
f₁ : Π₀ (i : ι₁), β₁ i
f₂ : Π₀ (i : ι₂), β₂ i
h : (i : ι₁) → (j : ι₂) → β₁ i →+ AddMonoidHom.{u_2, u_3} (β₂ j) γ
mk :
  ∀ (f₁ : (i : ι₁) → β₁ i) (support' : Trunc { s : Multiset ι₁ // ∀ (i : ι₁), i ∈ s ∨ f₁ i = 0 }) (s₁ : Multiset ι₁)
    (h₁ : ∀ (i : ι₁), i ∈ s₁ ∨ f₁ i = 0) (f₂ : (i : ι₂) → β₂ i)
    (support' : Trunc { s : Multiset ι₂ // ∀ (i : ι₂), i ∈ s ∨ f₂ i = 0 }) (s₂ : Multiset ι₂)
    (h₂ : ∀ (i : ι₂), i ∈ s₂ ∨ f₂ i = 0),
    Eq.{u_3 + 1} (α := γ)
      ((sumAddHom (β := β₂) fun (i₂ : ι₂) ↦
              (sumAddHom (β := β₁) fun (i₁ : ι₁) ↦ h i₁ i₂ : (a : Π₀ (i : ι₁), β₁ i) → β₂ i₂ →+ γ)
                (mk' (β := fun (i : ι₁) ↦ β₁ i) f₁
                  (Quot.mk
                    (⇑trueSetoid :
                      { s : Multiset ι₁ // ∀ (i : ι₁), i ∈ s ∨ f₁ i = 0 } →
                        { s : Multiset ι₁ // ∀ (i : ι₁), i ∈ s ∨ f₁ i = 0 } → Prop)
                    (Subtype.mk (p := fun (s : Multiset ι₁) ↦ ∀ (i : ι₁), i ∈ s ∨ f₁ i = 0) s₁ h₁))) :
            (a : Π₀ (i : ι₂), β₂ i) → γ)
          (mk' (β := fun (i : ι₂) ↦ β₂ i) f₂
            (Quot.mk
              (⇑trueSetoid :
                { s : Multiset ι₂ // ∀ (i : ι₂), i ∈ s ∨ f₂ i = 0 } →
                  { s : Multiset ι₂ // ∀ (i : ι₂), i ∈ s ∨ f₂ i = 0 } → Prop)
              (Subtype.mk (p := fun (s : Multiset ι₂) ↦ ∀ (i : ι₂), i ∈ s ∨ f₂ i = 0) s₂ h₂))) :
        γ)
      ((sumAddHom (β := β₁) fun (i₁ : ι₁) ↦
              (sumAddHom (β := β₂) fun (i₂ : ι₂) ↦ (h i₁ i₂).flip : (a : Π₀ (i : ι₂), β₂ i) → β₁ i₁ →+ γ)
                (mk' (β := fun (i : ι₂) ↦ β₂ i) f₂
                  (Quot.mk
                    (⇑trueSetoid :
                      { s : Multiset ι₂ // ∀ (i : ι₂), i ∈ s ∨ f₂ i = 0 } →
                        { s : Multiset ι₂ // ∀ (i : ι₂), i ∈ s ∨ f₂ i = 0 } → Prop)
                    (Subtype.mk (p := fun (s : Multiset ι₂) ↦ ∀ (i : ι₂), i ∈ s ∨ f₂ i = 0) s₂ h₂))) :
            (a : Π₀ (i : ι₁), β₁ i) → γ)
          (mk' (β := fun (i : ι₁) ↦ β₁ i) f₁
            (Quot.mk
              (⇑trueSetoid :
                { s : Multiset ι₁ // ∀ (i : ι₁), i ∈ s ∨ f₁ i = 0 } →
                  { s : Multiset ι₁ // ∀ (i : ι₁), i ∈ s ∨ f₁ i = 0 } → Prop)
              (Subtype.mk (p := fun (s : Multiset ι₁) ↦ ∀ (i : ι₁), i ∈ s ∨ f₁ i = 0) s₁ h₁))) :
        γ)
⊢ Eq.{u_3 + 1} (α := γ)
    ((sumAddHom (β := β₂) fun (i₂ : ι₂) ↦
            (sumAddHom (β := β₁) fun (i₁ : ι₁) ↦ h i₁ i₂ : (a : Π₀ (i : ι₁), β₁ i) → β₂ i₂ →+ γ) f₁ :
          (a : Π₀ (i : ι₂), β₂ i) → γ)
        f₂ :
      γ)
    ((sumAddHom (β := β₁) fun (i₁ : ι₁) ↦
            (sumAddHom (β := β₂) fun (i₂ : ι₂) ↦ (h i₁ i₂).flip : (a : Π₀ (i : ι₂), β₂ i) → β₁ i₁ →+ γ) f₂ :
          (a : Π₀ (i : ι₁), β₁ i) → γ)
        f₁ :
      γ)

Tactic:
obtain ⟨⟨f₁, s₁, h₁⟩, ⟨f₂, s₂, h₂⟩⟩ := f₁, f₂
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι₁ : Type u_4
ι₂ : Type u_5
β₁ : ι₁ → Type u_1
β₂ : ι₂ → Type u_2
γ : Type u_3
inst : DecidableEq ι₁
inst_1 : DecidableEq ι₂
inst_2 : (i : ι₁) → AddZeroClass (β₁ i)
inst_3 : (i : ι₂) → AddZeroClass (β₂ i)
inst_4 : AddCommMonoid γ
h : (i : ι₁) → (j : ι₂) → β₁ i →+ AddMonoidHom.{u_2, u_3} (β₂ j) γ
f₁ : (i : ι₁) → β₁ i
support' : Trunc { s : Multiset ι₁ // ∀ (i : ι₁), i ∈ s ∨ f₁ i = 0 }
s₁ : Multiset ι₁
h₁ : ∀ (i : ι₁), i ∈ s₁ ∨ f₁ i = 0
f₂ : (i : ι₂) → β₂ i
support'_1 : Trunc { s : Multiset ι₂ // ∀ (i : ι₂), i ∈ s ∨ f₂ i = 0 }
s₂ : Multiset ι₂
h₂ : ∀ (i : ι₂), i ∈ s₂ ∨ f₂ i = 0
⊢ Eq.{u_3 + 1} (α := γ)
    ((sumAddHom (β := β₂) fun (i₂ : ι₂) ↦
            (sumAddHom (β := β₁) fun (i₁ : ι₁) ↦ h i₁ i₂ : (a : Π₀ (i : ι₁), β₁ i) → β₂ i₂ →+ γ)
              (mk' (β := fun (i : ι₁) ↦ β₁ i) f₁
                (Quot.mk
                  (⇑trueSetoid :
                    { s : Multiset ι₁ // ∀ (i : ι₁), i ∈ s ∨ f₁ i = 0 } →
                      { s : Multiset ι₁ // ∀ (i : ι₁), i ∈ s ∨ f₁ i = 0 } → Prop)
                  (Subtype.mk (p := fun (s : Multiset ι₁) ↦ ∀ (i : ι₁), i ∈ s ∨ f₁ i = 0) s₁ h₁))) :
          (a : Π₀ (i : ι₂), β₂ i) → γ)
        (mk' (β := fun (i : ι₂) ↦ β₂ i) f₂
          (Quot.mk
            (⇑trueSetoid :
              { s : Multiset ι₂ // ∀ (i : ι₂), i ∈ s ∨ f₂ i = 0 } →
                { s : Multiset ι₂ // ∀ (i : ι₂), i ∈ s ∨ f₂ i = 0 } → Prop)
            (Subtype.mk (p := fun (s : Multiset ι₂) ↦ ∀ (i : ι₂), i ∈ s ∨ f₂ i = 0) s₂ h₂))) :
      γ)
    ((sumAddHom (β := β₁) fun (i₁ : ι₁) ↦
            (sumAddHom (β := β₂) fun (i₂ : ι₂) ↦ (h i₁ i₂).flip : (a : Π₀ (i : ι₂), β₂ i) → β₁ i₁ →+ γ)
              (mk' (β := fun (i : ι₂) ↦ β₂ i) f₂
                (Quot.mk
                  (⇑trueSetoid :
                    { s : Multiset ι₂ // ∀ (i : ι₂), i ∈ s ∨ f₂ i = 0 } →
                      { s : Multiset ι₂ // ∀ (i : ι₂), i ∈ s ∨ f₂ i = 0 } → Prop)
                  (Subtype.mk (p := fun (s : Multiset ι₂) ↦ ∀ (i : ι₂), i ∈ s ∨ f₂ i = 0) s₂ h₂))) :
          (a : Π₀ (i : ι₁), β₁ i) → γ)
        (mk' (β := fun (i : ι₁) ↦ β₁ i) f₁
          (Quot.mk
            (⇑trueSetoid :
              { s : Multiset ι₁ // ∀ (i : ι₁), i ∈ s ∨ f₁ i = 0 } →
                { s : Multiset ι₁ // ∀ (i : ι₁), i ∈ s ∨ f₁ i = 0 } → Prop)
            (Subtype.mk (p := fun (s : Multiset ι₁) ↦ ∀ (i : ι₁), i ∈ s ∨ f₁ i = 0) s₁ h₁))) :
      γ)

Tactic:
simpa [sumAddHom, sumZeroHom, AddMonoidHom.finsetSum_apply, AddMonoidHom.coe_mk,
      AddMonoidHom.flip_apply, Trunc.lift, toFun_eq_coe, ZeroHom.coe_mk, coe_mk']
    using Finset.sum_comm

Premises used: AddMonoidHom.coe_mk, DFinsupp.sumZeroHom, DFinsupp.coe_mk', AddMonoidHom.flip_apply, ZeroHom.coe_mk, AddMonoidHom.finsetSum_apply, DFinsupp.toFun_eq_coe, DFinsupp.sumAddHom, Finset.sum_comm, Trunc.lift
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
x : (i : ι) → AddMonoidHom.{v, w} (β i) γ
h :
  ∀ (x_1 : ι) (x_2 : β x_1),
    Eq.{w + 1} (α := γ)
      (((fun (F : (Π₀ (i : ι), β i) →+ γ) (i : ι) ↦ F.comp (singleAddHom β i)) (sumAddHom (β := β) x) x_1 :
            (a : β x_1) → γ)
          x_2 :
        γ)
      ((x x_1 : (a : β x_1) → γ) x_2 : γ)
⊢ (fun (F : (Π₀ (i : ι), β i) →+ γ) (i : ι) ↦ F.comp (singleAddHom β i)) (sumAddHom (β := β) x) = x

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
x : (i : ι) → AddMonoidHom.{v, w} (β i) γ
x_1 : ι
x_2 : β x_1
⊢ Eq.{w + 1} (α := γ)
    (((fun (F : (Π₀ (i : ι), β i) →+ γ) (i : ι) ↦ F.comp (singleAddHom β i)) (sumAddHom (β := β) x) x_1 :
          (a : β x_1) → γ)
        x_2 :
      γ)
    ((x x_1 : (a : β x_1) → γ) x_2 : γ)

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
ψ : (Π₀ (i : ι), β i) →+ γ
H :
  ∀ (x : ι) (x_1 : β x),
    Eq.{w + 1} (α := γ)
      ((AddMonoidHom.comp
              (sumAddHom (β := β) ((fun (F : (Π₀ (i : ι), β i) →+ γ) (i : ι) ↦ F.comp (singleAddHom β i)) ψ))
              (singleAddHom β x) :
            (a : β x) → γ)
          x_1 :
        γ)
      ((ψ.comp (singleAddHom β x) : (a : β x) → γ) x_1 : γ)
⊢ sumAddHom (β := β) ((fun (F : (Π₀ (i : ι), β i) →+ γ) (i : ι) ↦ F.comp (singleAddHom β i)) ψ) = ψ

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
ψ : (Π₀ (i : ι), β i) →+ γ
x : ι
x_1 : β x
⊢ Eq.{w + 1} (α := γ)
    ((AddMonoidHom.comp (sumAddHom (β := β) ((fun (F : (Π₀ (i : ι), β i) →+ γ) (i : ι) ↦ F.comp (singleAddHom β i)) ψ))
            (singleAddHom β x) :
          (a : β x) → γ)
        x_1 :
      γ)
    ((ψ.comp (singleAddHom β x) : (a : β x) → γ) x_1 : γ)

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
F G : (i : ι) → AddMonoidHom.{v, w} (β i) γ
H :
  ∀ (x : ι) (x_1 : β x),
    Eq.{w + 1} (α := γ) (((sumAddHom (β := β) (F + G)).comp (singleAddHom β x) : (a : β x) → γ) x_1 : γ)
      (((sumAddHom (β := β) F + sumAddHom (β := β) G).comp (singleAddHom β x) : (a : β x) → γ) x_1 : γ)
⊢ sumAddHom (β := β) (F + G) = sumAddHom (β := β) F + sumAddHom (β := β) G

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
F G : (i : ι) → AddMonoidHom.{v, w} (β i) γ
x : ι
x_1 : β x
⊢ Eq.{w + 1} (α := γ) (((sumAddHom (β := β) (F + G)).comp (singleAddHom β x) : (a : β x) → γ) x_1 : γ)
    (((sumAddHom (β := β) F + sumAddHom (β := β) G).comp (singleAddHom β x) : (a : β x) → γ) x_1 : γ)

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddCommMonoid (β i)
⊢ Eq (α := (Π₀ (i : ι), β i) →+ Π₀ (i : ι), β i)
    ((liftAddHom (β := β) : (a : (i : ι) → β i →+ Π₀ (i : ι), β i) → (Π₀ (i : ι), β i) →+ Π₀ (i : ι), β i)
        (singleAddHom β) :
      (Π₀ (i : ι), β i) →+ Π₀ (i : ι), β i)
    (AddMonoidHom.id (Π₀ (i : ι), β i) : (Π₀ (i : ι), β i) →+ Π₀ (i : ι), β i)

Tactic:
liftAddHom.toEquiv.apply_eq_iff_eq_symm_apply.2 rfl

Premises used: Iff.mpr, DFinsupp.liftAddHom, AddEquiv.toEquiv, rfl, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
f : (i : ι) → AddMonoidHom.{v, w} (β i) γ
i : ι
x : β i
⊢ Eq.{w + 1} (α := γ)
    ((((liftAddHom (β := β) : (a : (i : ι) → β i →+ γ) → (Π₀ (i : ι), β i) →+ γ) f : (Π₀ (i : ι), β i) →+ γ) :
          (a : Π₀ (i : ι), β i) → γ)
        (single (β := β) i x) :
      γ)
    ((f i : (a : β i) → γ) x : γ)

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
f : (i : ι) → AddMonoidHom.{v, w} (β i) γ
i : ι
⊢ AddMonoidHom.comp ((liftAddHom (β := β) : (a : (i : ι) → β i →+ γ) → (Π₀ (i : ι), β i) →+ γ) f) (singleAddHom β i) =
    f i

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
δ : Type u_1
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
inst_3 : AddCommMonoid δ
g : γ →+ δ
f : (i : ι) → AddMonoidHom.{v, w} (β i) γ
a : ι
rw :
  AddMonoidHom.comp (g.comp ((liftAddHom (β := β) : (a : (i : ι) → β i →+ γ) → (Π₀ (i : ι), β i) →+ γ) f))
      (singleAddHom β a) =
    g.comp (f a)
rw₁ :
  g.comp
      (AddMonoidHom.comp ((liftAddHom (β := β) : (a : (i : ι) → β i →+ γ) → (Π₀ (i : ι), β i) →+ γ) f)
        (singleAddHom β a)) =
    g.comp (f a)
rw₂ rw₃ : g.comp (f a) = g.comp (f a)
⊢ (AddEquiv.symm (liftAddHom (β := β)) : (a : (Π₀ (i : ι), β i) →+ δ) → (i : ι) → β i →+ δ)
      (g.comp ((liftAddHom (β := β) : (a : (i : ι) → β i →+ γ) → (Π₀ (i : ι), β i) →+ γ) f)) a =
    g.comp (f a)

Tactic:
rw [liftAddHom_symm_apply, AddMonoidHom.comp_assoc, liftAddHom_comp_single]

Premises used: AddMonoidHom.comp_assoc, DFinsupp.liftAddHom_comp_single, DFinsupp.liftAddHom_symm_apply
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
⊢ Eq (α := (Π₀ (i : ι), β i) →+ γ) (sumAddHom (β := β) fun (i : ι) ↦ 0) 0

Tactic:
map_zero liftAddHom

Premises used: map_zero, DFinsupp.liftAddHom, DFinsupp.sumAddHom