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 : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → ZeroHom.{v, w} (β i) γ
simp :
  Eq.{w + 1} (α := γ)
    (Trunc.lift.{u + 1, w + 1} (α := { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ Eq.{v + 1} (α := β i) 0 0 })
      (fun (s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ Eq.{v + 1} (α := β i) 0 0 }) ↦ (0 : γ)) ⋯
      (support' (β := fun (i : ι) ↦ β i) 0 :
        Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ Eq.{v + 1} (α := β i) (toFun (β := fun (i : ι) ↦ β i) 0 i) 0 }))
    0
⊢ Eq.{w + 1} (α := γ)
    ((fun
          (c :
            ∀
              (a b :
                { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ Eq.{v + 1} (α := β i) (toFun (β := fun (i : ι) ↦ β i) 0 i) 0 }),
              Eq.{w + 1} (α := γ)
                ((fun
                      (s :
                        { s : Multiset ι //
                          ∀ (i : ι), i ∈ s ∨ Eq.{v + 1} (α := β i) (toFun (β := fun (i : ι) ↦ β i) 0 i) 0 }) ↦
                    (∑ i ∈ (↑s : Multiset ι).toFinset, (φ i : (a : β i) → γ) ((0 : (a : ι) → β a) i) : γ))
                  a)
                ((fun
                      (s :
                        { s : Multiset ι //
                          ∀ (i : ι), i ∈ s ∨ Eq.{v + 1} (α := β i) (toFun (β := fun (i : ι) ↦ β i) 0 i) 0 }) ↦
                    (∑ i ∈ (↑s : Multiset ι).toFinset, (φ i : (a : β i) → γ) ((0 : (a : ι) → β a) i) : γ))
                  b)) ↦
        Trunc.lift
          (fun
              (s :
                { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ Eq.{v + 1} (α := β i) (toFun (β := fun (i : ι) ↦ β i) 0 i) 0 }) ↦
            ∑ i ∈ (↑s : Multiset ι).toFinset, (φ i : (a : β i) → γ) ((0 : (a : ι) → β a) i))
          c (support' (β := fun (i : ι) ↦ β i) 0))
      ⋯)
    0

Tactic:
simp only [toFun_eq_coe, coe_zero, Pi.zero_apply, map_zero, Finset.sum_const_zero]

Premises used: Pi.zero_apply, map_zero, Finset.sum_const_zero, DFinsupp.toFun_eq_coe, DFinsupp.coe_zero
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → ZeroHom.{v, w} (β i) γ
⊢ Eq.{w + 1} (α := γ)
    (Trunc.lift.{u + 1, w + 1} (α := { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ Eq.{v + 1} (α := β i) 0 0 })
      (fun (s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ Eq.{v + 1} (α := β i) 0 0 }) ↦ (0 : γ)) ⋯
      (support' (β := fun (i : ι) ↦ β i) 0 :
        Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ Eq.{v + 1} (α := β i) (toFun (β := fun (i : ι) ↦ β i) 0 i) 0 }))
    0

Tactic:
rfl
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → ZeroHom.{v, w} (β i) γ
i : ι
x : β i
dsimp :
  Eq.{w + 1} (α := γ) (∑ i_1 ∈ Multiset.toFinset {i}, (φ i_1 : (a : β i_1) → γ) (Pi.single (M := β) i x i_1) : γ)
    ((φ i : (a : β i) → γ) x : γ)
⊢ Eq.{w + 1} (α := γ) ((sumZeroHom (β := β) φ : (a : Π₀ (i : ι), β i) → γ) (single (β := β) i x) : γ)
    ((φ i : (a : β i) → γ) x : γ)

Tactic:
dsimp [sumZeroHom, single, Trunc.lift_mk]

Premises used: DFinsupp.sumZeroHom, DFinsupp.single, Trunc.lift_mk
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → ZeroHom.{v, w} (β i) γ
i : ι
x : β i
rw :
  Eq.{w + 1} (α := γ) (∑ i_1 ∈ {i}, (φ i_1 : (a : β i_1) → γ) (Pi.single (M := β) i x i_1) : γ)
    ((φ i : (a : β i) → γ) x : γ)
rw₁ : Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) (Pi.single (M := β) i x i) : γ) ((φ i : (a : β i) → γ) x : γ)
rw₂ rw₃ : Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) x : γ) ((φ i : (a : β i) → γ) x : γ)
⊢ Eq.{w + 1} (α := γ) (∑ i_1 ∈ Multiset.toFinset {i}, (φ i_1 : (a : β i_1) → γ) (Pi.single (M := β) i x i_1) : γ)
    ((φ i : (a : β i) → γ) x : γ)

Tactic:
rw [Multiset.toFinset_singleton, Finset.sum_singleton, Pi.single_eq_same]

Premises used: Finset.sum_singleton, Pi.single_eq_same, Multiset.toFinset_singleton
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
i : ι
φ : ZeroHom.{v, w} (β i) γ
h :
  ∀ (f : (i : ι) → β i) (support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }) (sf : Multiset ι)
    (hf : ∀ (i : ι), i ∈ sf ∨ f i = 0),
    Eq.{w + 1} (α := γ)
      ((sumZeroHom (β := β) (Pi.single (M := fun (i : ι) ↦ ZeroHom.{v, w} (β i) γ) i φ) : (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) sf hf))) :
        γ)
      ((φ.comp { toFun := fun (x : Π₀ (i : ι), β i) ↦ (x : (a : ι) → β a) i, map_zero' := ⋯ } :
            (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) sf hf))) :
        γ)
⊢ Eq (α := ZeroHom (Π₀ (i : ι), β i) γ)
    (sumZeroHom (β := β) (Pi.single (M := fun (i : ι) ↦ ZeroHom.{v, w} (β i) γ) i φ))
    (φ.comp { toFun := fun (x : Π₀ (i : ι), β i) ↦ (x : (a : ι) → β a) i, map_zero' := ⋯ })

Tactic:
ext ⟨f, sf, hf⟩
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
i : ι
φ : ZeroHom.{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
h :
  Eq.{w + 1} (α := γ)
    (∑ x ∈ sf.toFinset,
        ((Pi.single (M := fun (i : ι) ↦ ZeroHom.{v, w} (β i) γ) i φ x : ZeroHom.{v, w} (β x) γ) : (a : β x) → γ) (f x) :
      γ)
    ((φ : (a : β i) → γ) (f i) : γ)
⊢ Eq.{w + 1} (α := γ)
    ((sumZeroHom (β := β) (Pi.single (M := fun (i : ι) ↦ ZeroHom.{v, w} (β i) γ) i φ) : (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) sf hf))) :
      γ)
    ((φ.comp { toFun := fun (x : Π₀ (i : ι), β i) ↦ (x : (a : ι) → β a) i, map_zero' := ⋯ } : (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) sf hf))) :
      γ)

Tactic:
simp only [sumZeroHom, Trunc.lift, toFun_eq_coe, ZeroHom.coe_mk, coe_mk', ZeroHom.coe_comp,
    Function.comp_apply]

Premises used: ZeroHom.coe_comp, DFinsupp.sumZeroHom, DFinsupp.coe_mk', ZeroHom.coe_mk, DFinsupp.toFun_eq_coe, Function.comp_apply, Trunc.lift
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
i : ι
φ : ZeroHom.{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
rw :
  ∀ j ∈ sf.toFinset,
    ∀ (hji : j ≠ i),
      Eq.{w + 1} (α := γ)
        (((Pi.single (M := fun (i : ι) ↦ ZeroHom.{v, w} (β i) γ) i φ j : ZeroHom.{v, w} (β j) γ) : (a : β j) → γ)
            (f j) :
          γ)
        (0 : γ)
rw₁ :
  ∀ (hi : i ∉ sf.toFinset),
    Eq.{w + 1} (α := γ)
      (((Pi.single (M := fun (i : ι) ↦ ZeroHom.{v, w} (β i) γ) i φ i : ZeroHom.{v, w} (β i) γ) : (a : β i) → γ) (f i) :
        γ)
      (0 : γ)
⊢ Eq.{w + 1} (α := γ)
    (∑ x ∈ sf.toFinset,
        ((Pi.single (M := fun (i : ι) ↦ ZeroHom.{v, w} (β i) γ) i φ x : ZeroHom.{v, w} (β x) γ) : (a : β x) → γ) (f x) :
      γ)
    ((φ : (a : β i) → γ) (f i) : γ)

Tactic:
rw [Finset.sum_eq_single i (fun j _ hji => ?_) (fun hi => ?_), Pi.single_eq_same]

Premises used: Finset.sum_eq_single, Pi.single_eq_same
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
i : ι
φ : ZeroHom.{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
j : ι
h : j ∈ sf.toFinset
hji : j ≠ i
⊢ Eq.{w + 1} (α := γ)
    (((Pi.single (M := fun (i : ι) ↦ ZeroHom.{v, w} (β i) γ) i φ j : ZeroHom.{v, w} (β j) γ) : (a : β j) → γ) (f j) : γ)
    (0 : γ)

Tactic:
simp [hji]
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
i : ι
φ : ZeroHom.{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
hi : i ∉ sf.toFinset
⊢ i ∉ sf

Tactic:
simpa using hi
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
i : ι
φ : ZeroHom.{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
hi : i ∉ sf.toFinset
⊢ Eq.{w + 1} (α := γ)
    (((Pi.single (M := fun (i : ι) ↦ ZeroHom.{v, w} (β i) γ) i φ i : ZeroHom.{v, w} (β i) γ) : (a : β i) → γ) (f i) : γ)
    (0 : γ)

Tactic:
simp [(hf i).resolve_left (by simpa using hi)]

Premises used: Or.resolve_left
-- 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 : ι) → ZeroHom.{v, w} (β i) γ
f : Π₀ (i : ι), β i
mk :
  ∀ (f : (i : ι) → β i) (support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }) (s : Multiset ι)
    (hf : ∀ (i : ι), i ∈ s ∨ f i = 0),
    Eq.{w + 1} (α := γ)
      ((sumZeroHom (β := β) φ : (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 hf))) :
        γ)
      (sum (β := β)
          (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 hf)))
          fun (x : ι) ↦ (⇑(φ x) : (a : β x) → γ) :
        γ)
⊢ Eq.{w + 1} (α := γ) ((sumZeroHom (β := β) φ : (a : Π₀ (i : ι), β i) → γ) f : γ)
    (f.sum (β := β) fun (x : ι) ↦ (⇑(φ x) : (a : β x) → γ) : γ)

Tactic:
rcases f with ⟨f, s, hf⟩
-- 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 : ι) → ZeroHom.{v, w} (β i) γ
f : (i : ι) → β i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }
s : Multiset ι
hf : ∀ (i : ι), i ∈ s ∨ f i = 0
mk :
  Eq.{w + 1} (α := γ)
    (∑ i ∈ (↑(Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s hf) : Multiset ι).toFinset,
      (φ i : (a : β 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 hf)) :
            (a : ι) → β a)
          i))
    (∑ i ∈ (↑(Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s hf) : Multiset ι).toFinset with
      (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 hf)) :
            (a : ι) → β a)
          i ≠
        0,
      (fun (x : ι) ↦ ((⇑(φ x) : (a : β x) → γ) : (a : β x) → γ)) 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 hf)) :
            (a : ι) → β a)
          i))
⊢ Eq.{w + 1} (α := γ)
    ((sumZeroHom (β := β) φ : (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 hf))) :
      γ)
    (sum (β := β)
        (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 hf)))
        fun (x : ι) ↦ (⇑(φ x) : (a : β x) → γ) :
      γ)

Tactic:
change (∑ i ∈ _, _) = ∑ i ∈ _ with _, _

Premises used: Finset.sum
-- 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 : ι) → ZeroHom.{v, w} (β i) γ
f : (i : ι) → β i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }
s : Multiset ι
hf : ∀ (i : ι), i ∈ s ∨ f i = 0
i : ι
h : i ∈ (↑(Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s hf) : Multiset ι).toFinset
mk : Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) (f i) : γ) (if f i ≠ 0 then (φ i : (a : β i) → γ) (f i) else 0 : γ)
⊢ Eq.{w + 1} (α := γ)
    ((φ i : (a : β 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 hf)) :
            (a : ι) → β a)
          i) :
      γ)
    (if
          (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 hf)) :
                (a : ι) → β a)
              i ≠
            0 then
        (fun (x : ι) ↦ ((⇑(φ x) : (a : β x) → γ) : (a : β x) → γ)) 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 hf)) :
              (a : ι) → β a)
            i)
      else 0 :
      γ)

Tactic:
dsimp only [coe_mk', Subtype.coe_mk] at *

Premises used: Subtype.coe_mk, DFinsupp.coe_mk'
-- 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 : ι) → ZeroHom.{v, w} (β i) γ
f : (i : ι) → β i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }
s : Multiset ι
hf : ∀ (i : ι), i ∈ s ∨ f i = 0
i : ι
h : i ∈ s.toFinset
pos : ∀ (h : f i ≠ 0), Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) (f i) : γ) ((φ i : (a : β i) → γ) (f i) : γ)
neg : ∀ (h : ¬f i ≠ 0), Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) (f i) : γ) (0 : γ)
⊢ Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) (f i) : γ) (if f i ≠ 0 then (φ i : (a : β i) → γ) (f i) else 0 : γ)

Tactic:
split_ifs with h
-- 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 : ι) → ZeroHom.{v, w} (β i) γ
f : (i : ι) → β i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }
s : Multiset ι
hf : ∀ (i : ι), i ∈ s ∨ f i = 0
i : ι
h_1 : i ∈ s.toFinset
h : f i ≠ 0
⊢ Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) (f i) : γ) ((φ i : (a : β i) → γ) (f i) : γ)

Tactic:
rfl
-- 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 : ι) → ZeroHom.{v, w} (β i) γ
f : (i : ι) → β i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }
s : Multiset ι
hf : ∀ (i : ι), i ∈ s ∨ f i = 0
i : ι
h_1 : i ∈ s.toFinset
h : ¬f i ≠ 0
neg : Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) 0 : γ) (0 : γ)
neg₁ neg₂ : Eq.{w + 1} (α := γ) 0 0
⊢ Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) (f i) : γ) (0 : γ)

Tactic:
rw [not_not.mp h, map_zero]

Premises used: Classical.not_not, map_zero, Iff.mp
-- 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 :
  Eq.{w + 1} (α := γ) (∑ x ∈ (sf + sg).toFinset, (φ x : (a : β x) → γ) (f x))
    (∑ x ∈ sf.toFinset, (φ x : (a : β x) → γ) (f x))
mk₁ :
  Eq.{w + 1} (α := γ) (∑ x ∈ (sf + sg).toFinset, (φ x : (a : β x) → γ) (g x))
    (∑ x ∈ sg.toFinset, (φ x : (a : β x) → γ) (g x))
⊢ HAdd.hAdd (α := γ) (∑ x ∈ (sf + sg).toFinset, (φ x : (a : β x) → γ) (f x))
      (∑ x ∈ (sf + sg).toFinset, (φ x : (a : β x) → γ) (g x)) =
    HAdd.hAdd (α := γ) (∑ x ∈ sf.toFinset, (φ x : (a : β x) → γ) (f x)) (∑ x ∈ sg.toFinset, (φ x : (a : β x) → γ) (g x))

Tactic:
congr 1
-- 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) → γ) (f x))
    (∑ x ∈ sf.toFinset, (φ x : (a : β x) → γ) (f 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 : sf.toFinset ⊆ (sf + sg).toFinset
mk₁ : ∀ x ∈ (sf + sg).toFinset, x ∉ sf.toFinset → Eq.{w + 1} (α := γ) ((φ x : (a : β x) → γ) (f x) : γ) (0 : γ)
⊢ Eq.{w + 1} (α := γ) (∑ x ∈ (sf + sg).toFinset, (φ x : (a : β x) → γ) (f x))
    (∑ x ∈ sf.toFinset, (φ x : (a : β x) → γ) (f 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 ∈ sf → i ∈ sf ∨ i ∈ sg
⊢ i ∈ sf.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 ∈ sf → i ∈ sf ∨ i ∈ sg

Tactic:
Or.inl

Premises used: Or.inl
-- 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 ∈ sf → i ∈ sf ∨ i ∈ sg

Tactic:
exact Or.inl

Premises used: Or.inl
-- 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 ∉ sf.toFinset → Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) (f i) : γ) (0 : γ)
⊢ i ∈ (sf + sg).toFinset → i ∉ sf.toFinset → Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) (f 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 ∉ sf.toFinset
⊢ i ∉ sf

Tactic:
simp only [Multiset.mem_toFinset] at H2

Premises used: Multiset.mem_toFinset