awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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
⊢ Eq.{w + 1} (α := γ) ((sumZeroHom (β := β) φ : (a : Π₀ (i : ι), β i) → γ) (single (β := β) i x) : γ)
    ((φ i : (a : β i) → γ) x : γ)
have 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 : γ)
Tactic: dsimp [sumZeroHom, single, Trunc.lift_mk]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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
⊢ Eq.{w + 1} (α := γ) (∑ i_1 ∈ Multiset.toFinset {i}, (φ i_1 : (a : β i_1) → γ) (Pi.single (M := β) i x i_1) : γ)
    ((φ i : (a : β i) → γ) x : γ)
have rw : Eq.{w + 1} (α := γ) (∑ i_1 ∈ {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]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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 : γ)
⊢ Eq.{w + 1} (α := γ) (∑ i_1 ∈ Multiset.toFinset {i}, (φ i_1 : (a : β i_1) → γ) (Pi.single (M := β) i x i_1) : γ)
    ((φ i : (a : β i) → γ) x : γ)
have rw₁ : Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) (Pi.single (M := β) i x i) : γ) ((φ i : (a : β i) → γ) x : γ)
Tactic: rw [Multiset.toFinset_singleton, Finset.sum_singleton, Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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 : γ)
⊢ Eq.{w + 1} (α := γ) (∑ i_1 ∈ Multiset.toFinset {i}, (φ i_1 : (a : β i_1) → γ) (Pi.single (M := β) i x i_1) : γ)
    ((φ i : (a : β i) → γ) x : γ)
have rw₂ : Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) x : γ) ((φ i : (a : β i) → γ) x : γ)
Tactic: rw [Multiset.toFinset_singleton, Finset.sum_singleton, Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
i : ι
φ : ZeroHom.{v, w} (β i) γ
⊢ 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' := ⋯ })
have 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' := sorry } : (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: ext ⟨f, sf, hf⟩
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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
⊢ 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))) :
      γ)
have 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) : γ)
Tactic: simp only [sumZeroHom, Trunc.lift, toFun_eq_coe, ZeroHom.coe_mk, coe_mk', ZeroHom.coe_comp,
    Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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
⊢ 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) : γ)
have 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 : γ)
Tactic: rw [Finset.sum_eq_single i (fun j _ hji => ?_) (fun hi => ?_), Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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 : γ)
⊢ 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) : γ)
have 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 : γ)
Tactic: rw [Finset.sum_eq_single i (fun j _ hji => ?_) (fun hi => ?_), Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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
⊢ Eq.{w + 1} (α := γ) ((sumZeroHom (β := β) φ : (a : Π₀ (i : ι), β i) → γ) f : γ)
    (f.sum (β := β) fun (x : ι) ↦ (⇑(φ x) : (a : β x) → γ) : γ)
have 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) → γ) :
      γ)
Tactic: rcases f with ⟨f, s, hf⟩
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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
⊢ 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) → γ) :
      γ)
have 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))
Tactic: change (∑ i ∈ _, _) = ∑ i ∈ _ with _, _
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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
⊢ 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 :
      γ)
have mk : Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) (f i) : γ) (if f i ≠ 0 then (φ i : (a : β i) → γ) (f i) else 0 : γ)
Tactic: dsimp only [coe_mk', Subtype.coe_mk] at *
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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
⊢ Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) (f i) : γ) (if f i ≠ 0 then (φ i : (a : β i) → γ) (f i) else 0 : γ)
have pos : ∀ (h : f i ≠ 0), Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) (f i) : γ) ((φ i : (a : β i) → γ) (f i) : γ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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) : γ)
⊢ Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) (f i) : γ) (if f i ≠ 0 then (φ i : (a : β i) → γ) (f i) else 0 : γ)
have neg : ∀ (h : ¬f i ≠ 0), Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) (f i) : γ) (0 : γ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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) : γ) (0 : γ)
have neg : Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) 0 : γ) (0 : γ)
Tactic: rw [not_not.mp h, map_zero]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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 : γ)
⊢ Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) (f i) : γ) (0 : γ)
have neg₁ : Eq.{w + 1} (α := γ) 0 0
Tactic: rw [not_not.mp h, map_zero]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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
⊢ 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))
have mk : Eq.{w + 1} (α := γ) (∑ x ∈ (sf + sg).toFinset, (φ x : (a : β x) → γ) (f x))
  (∑ x ∈ sf.toFinset, (φ x : (a : β x) → γ) (f x))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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))
⊢ 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))
have mk₁ : Eq.{w + 1} (α := γ) (∑ x ∈ (sf + sg).toFinset, (φ x : (a : β x) → γ) (g x))
  (∑ x ∈ sg.toFinset, (φ x : (a : β x) → γ) (g x))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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))
have mk : sf.toFinset ⊆ (sf + sg).toFinset
Tactic: refine (Finset.sum_subset ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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
⊢ Eq.{w + 1} (α := γ) (∑ x ∈ (sf + sg).toFinset, (φ x : (a : β x) → γ) (f x))
    (∑ x ∈ sf.toFinset, (φ x : (a : β x) → γ) (f x))
have mk₁ : ∀ x ∈ (sf + sg).toFinset, x ∉ sf.toFinset → Eq.{w + 1} (α := γ) ((φ x : (a : β x) → γ) (f x) : γ) (0 : γ)
Tactic: refine (Finset.sum_subset ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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.toFinset → i ∈ (sf + sg).toFinset
have mk : i ∈ sf → i ∈ sf ∨ i ∈ sg
Tactic: simp only [Multiset.mem_toFinset, Multiset.mem_add]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (hypothesis)
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
⊢ Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) (f i) : γ) (0 : γ)
have H2₁ : i ∉ sf
Tactic: simp only [Multiset.mem_toFinset] at H2
Cleared hypotheses: H2
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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
⊢ Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) (f i) : γ) (0 : γ)
have mk : Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) 0 : γ) (0 : γ)
Tactic: rw [(hf i).resolve_left H2, map_zero]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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 : γ)
⊢ Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) (f i) : γ) (0 : γ)
have mk₁ : Eq.{w + 1} (α := γ) 0 0
Tactic: rw [(hf i).resolve_left H2, map_zero]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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))
have mk : sg.toFinset ⊆ (sf + sg).toFinset
Tactic: refine (Finset.sum_subset ?_ ?_).symm