awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : sg.toFinset ⊆ (sf + sg).toFinset
⊢ Eq.{w + 1} (α := γ) (∑ x ∈ (sf + sg).toFinset, (φ x : (a : β x) → γ) (g x))
    (∑ x ∈ sg.toFinset, (φ x : (a : β x) → γ) (g x))
have mk₁ : ∀ x ∈ (sf + sg).toFinset, x ∉ sg.toFinset → Eq.{w + 1} (α := γ) ((φ x : (a : β x) → γ) (g 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 ∈ sg.toFinset → i ∈ (sf + sg).toFinset
have mk : i ∈ sg → 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 ∉ sg.toFinset
⊢ Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) (g i) : γ) (0 : γ)
have H2₁ : i ∉ sg
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 ∉ sg
⊢ Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) (g i) : γ) (0 : γ)
have mk : Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) 0 : γ) (0 : γ)
Tactic: rw [(hg 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 ∉ sg
mk : Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) 0 : γ) (0 : γ)
⊢ Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) (g i) : γ) (0 : γ)
have mk₁ : Eq.{w + 1} (α := γ) 0 0
Tactic: rw [(hg i).resolve_left H2, 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 : AddCommMonoid γ
i : ι
φ : AddMonoidHom.{v, w} (β i) γ
⊢ (↑(sumAddHom (β := β) (Pi.single (M := fun (i : ι) ↦ AddMonoidHom.{v, w} (β i) γ) i φ)) :
      ZeroHom (Π₀ (i : ι), β i) γ) =
    (↑(φ.comp (evalAddMonoidHom (β := β) i)) : ZeroHom (Π₀ (i : ι), β i) γ)
have 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) γ)))
Tactic: convert! sumZeroHom_piSingle i φ.toZeroHom using 1
-- 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 : AddCommMonoid γ
i : ι
φ : AddMonoidHom.{v, w} (β i) γ
| sumZeroHom (β := β) fun (i_1 : ι) ↦
    (↑(Pi.single (M := fun (i : ι) ↦ AddMonoidHom.{v, w} (β i) γ) i φ i_1) : ZeroHom (β i_1) γ)
have h : ∀ (i_1 : ι), (↑(Pi.single (M := fun (i : ι) ↦ AddMonoidHom.{v, w} (β i) γ) i φ i_1) : ZeroHom (β i_1) γ)
Tactic: enter [1, i]
-- 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 : AddCommMonoid γ
i_1 : ι
φ : AddMonoidHom.{v, w} (β i_1) γ
i : ι
| (↑(Pi.single (M := fun (i : ι) ↦ AddMonoidHom.{v, w} (β i) γ) i_1 φ i) : ZeroHom (β i) γ)
have h : (Pi.single (M := fun (i : ι) ↦ ZeroHom.{v, w} (β i) γ) i_1 (↑φ : ZeroHom (β i_1) γ) i : ZeroHom.{v, w} (β i) γ)
Tactic: rw [Pi.apply_single (fun i (x : β i →+ γ) => x.toZeroHom) (fun _ => rfl)]
-- 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 : AddCommMonoid γ
i : ι
φ : AddMonoidHom.{v, w} (β i) γ
| sumZeroHom (β := β) fun (i_1 : ι) ↦
    (↑(Pi.single (M := fun (i : ι) ↦ AddMonoidHom.{v, w} (β i) γ) i φ i_1) : ZeroHom (β i_1) γ)
have h : ∀ (i_1 : ι),
  (Pi.single (M := fun (i : ι) ↦ ZeroHom.{v, w} (β i) γ) i (↑φ : ZeroHom (β i) γ) i_1 : ZeroHom.{v, w} (β i_1) γ)
Tactic: enter [1, i]
      rw [Pi.apply_single (fun i (x : β i →+ γ) => x.toZeroHom) (fun _ => rfl)]
-- 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 : AddCommMonoid γ
i : ι
φ : AddMonoidHom.{v, w} (β 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) γ)))
have 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) γ)))
Tactic: conv_lhs =>
      enter [1, i]
      rw [Pi.apply_single (fun i (x : β i →+ γ) => x.toZeroHom) (fun _ => rfl)]
-- 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 : 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) γ)))
⊢ 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) γ)))
have 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) γ)))
Tactic: conv_lhs =>
      enter [1, i]
      rw [Pi.apply_single (fun i (x : β i →+ γ) => x.toZeroHom) (fun _ => rfl)]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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) γ
⊢ 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₁ :
      γ)
have 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₁))) :
      γ)
Tactic: obtain ⟨⟨f₁, s₁, h₁⟩, ⟨f₂, s₂, h₂⟩⟩ := f₁, f₂
Cleared hypotheses: f₁, f₂
-- 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 γ
x : (i : ι) → AddMonoidHom.{v, w} (β i) γ
⊢ (fun (F : (Π₀ (i : ι), β i) →+ γ) (i : ι) ↦ F.comp (singleAddHom β i)) (sumAddHom (β := β) x) = x
have 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 : γ)
Tactic: ext
-- 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 : ι), β i) →+ γ
⊢ sumAddHom (β := β) ((fun (F : (Π₀ (i : ι), β i) →+ γ) (i : ι) ↦ F.comp (singleAddHom β i)) ψ) = ψ
have 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 : γ)
Tactic: ext
-- 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 γ
F G : (i : ι) → AddMonoidHom.{v, w} (β i) γ
⊢ sumAddHom (β := β) (F + G) = sumAddHom (β := β) F + sumAddHom (β := β) G
have 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 : γ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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 : ι
⊢ (AddEquiv.symm (liftAddHom (β := β)) : (a : (Π₀ (i : ι), β i) →+ δ) → (i : ι) → β i →+ δ)
      (g.comp ((liftAddHom (β := β) : (a : (i : ι) → β i →+ γ) → (Π₀ (i : ι), β i) →+ γ) f)) a =
    g.comp (f a)
have rw : AddMonoidHom.comp (g.comp ((liftAddHom (β := β) : (a : (i : ι) → β i →+ γ) → (Π₀ (i : ι), β i) →+ γ) f))
    (singleAddHom β a) =
  g.comp (f a)
Tactic: rw [liftAddHom_symm_apply, AddMonoidHom.comp_assoc, liftAddHom_comp_single]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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)
⊢ (AddEquiv.symm (liftAddHom (β := β)) : (a : (Π₀ (i : ι), β i) →+ δ) → (i : ι) → β i →+ δ)
      (g.comp ((liftAddHom (β := β) : (a : (i : ι) → β i →+ γ) → (Π₀ (i : ι), β i) →+ γ) f)) a =
    g.comp (f a)
have rw₁ : g.comp
    (AddMonoidHom.comp ((liftAddHom (β := β) : (a : (i : ι) → β i →+ γ) → (Π₀ (i : ι), β i) →+ γ) f)
      (singleAddHom β a)) =
  g.comp (f a)
Tactic: rw [liftAddHom_symm_apply, AddMonoidHom.comp_assoc, liftAddHom_comp_single]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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)
⊢ (AddEquiv.symm (liftAddHom (β := β)) : (a : (Π₀ (i : ι), β i) →+ δ) → (i : ι) → β i →+ δ)
      (g.comp ((liftAddHom (β := β) : (a : (i : ι) → β i →+ γ) → (Π₀ (i : ι), β i) →+ γ) f)) a =
    g.comp (f a)
have rw₂ : g.comp (f a) = g.comp (f a)
Tactic: rw [liftAddHom_symm_apply, AddMonoidHom.comp_assoc, liftAddHom_comp_single]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (hypothesis)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddGroup (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : AddCommGroup γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂
⊢ (f - g).sum (β := β) h = f.sum (β := β) h - g.sum (β := β) h
have this : ((liftAddHom (β := β) : (a : (i : ι) → β i →+ γ) → (Π₀ (i : ι), β i) →+ γ) fun (a : ι) ↦ AddMonoidHom.ofMapSub (h a) sorry :
      (a : Π₀ (i : ι), β i) → γ)
    (f - g) =
  HSub.hSub (α := γ) (β := γ)
    (((liftAddHom (β := β) : (a : (i : ι) → β i →+ γ) → (Π₀ (i : ι), β i) →+ γ) fun (a : ι) ↦
            AddMonoidHom.ofMapSub (h a) sorry :
          (a : Π₀ (i : ι), β i) → γ)
        f :
      γ)
    (((liftAddHom (β := β) : (a : (i : ι) → β i →+ γ) → (Π₀ (i : ι), β i) →+ γ) fun (a : ι) ↦
            AddMonoidHom.ofMapSub (h a) sorry :
          (a : Π₀ (i : ι), β i) → γ)
        g :
      γ)
Tactic: have := (liftAddHom fun a => AddMonoidHom.ofMapSub (h a) (h_sub a)).map_sub f g
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (hypothesis)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddGroup (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : AddCommGroup γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂
this :
  ((liftAddHom (β := β) : (a : (i : ι) → β i →+ γ) → (Π₀ (i : ι), β i) →+ γ) fun (a : ι) ↦
          AddMonoidHom.ofMapSub (h a) ⋯ :
        (a : Π₀ (i : ι), β i) → γ)
      (f - g) =
    HSub.hSub (α := γ) (β := γ)
      (((liftAddHom (β := β) : (a : (i : ι) → β i →+ γ) → (Π₀ (i : ι), β i) →+ γ) fun (a : ι) ↦
              AddMonoidHom.ofMapSub (h a) ⋯ :
            (a : Π₀ (i : ι), β i) → γ)
          f :
        γ)
      (((liftAddHom (β := β) : (a : (i : ι) → β i →+ γ) → (Π₀ (i : ι), β i) →+ γ) fun (a : ι) ↦
              AddMonoidHom.ofMapSub (h a) ⋯ :
            (a : Π₀ (i : ι), β i) → γ)
          g :
        γ)
⊢ (f - g).sum (β := β) h = f.sum (β := β) h - g.sum (β := β) h
have this₁ : ((f - g).sum (β := β) fun (x : ι) ↦ (⇑(AddMonoidHom.ofMapSub (h x) sorry) : (a : β x) → γ)) =
  HSub.hSub (α := γ) (f.sum (β := β) fun (x : ι) ↦ (⇑(AddMonoidHom.ofMapSub (h x) sorry) : (a : β x) → γ))
    (g.sum (β := β) fun (x : ι) ↦ (⇑(AddMonoidHom.ofMapSub (h x) sorry) : (a : β x) → γ))
Tactic: rw [liftAddHom_apply, sumAddHom_apply, sumAddHom_apply, sumAddHom_apply] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (hypothesis)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddCommMonoid (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
⊢ f.sum (β := β) (single (β := β)) = f
have this : Eq (α := Π₀ (i : ι), β i)
  ((((liftAddHom (β := β) : (a : (i : ι) → β i →+ Π₀ (i : ι), β i) → (Π₀ (i : ι), β i) →+ Π₀ (i : ι), β i)
            (singleAddHom β) :
          (Π₀ (i : ι), β i) →+ Π₀ (i : ι), β i) :
        (a : Π₀ (i : ι), β i) → Π₀ (i : ι), β i)
      f :
    Π₀ (i : ι), β i)
  ((AddMonoidHom.id (Π₀ (i : ι), β i) : (a : Π₀ (i : ι), β i) → Π₀ (i : ι), β i) f : Π₀ (i : ι), β i)
Tactic: have := DFunLike.congr_fun (liftAddHom_singleAddHom (β := β)) f
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (hypothesis)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddCommMonoid (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
this :
  Eq (α := Π₀ (i : ι), β i)
    ((((liftAddHom (β := β) : (a : (i : ι) → β i →+ Π₀ (i : ι), β i) → (Π₀ (i : ι), β i) →+ Π₀ (i : ι), β i)
              (singleAddHom β) :
            (Π₀ (i : ι), β i) →+ Π₀ (i : ι), β i) :
          (a : Π₀ (i : ι), β i) → Π₀ (i : ι), β i)
        f :
      Π₀ (i : ι), β i)
    ((AddMonoidHom.id (Π₀ (i : ι), β i) : (a : Π₀ (i : ι), β i) → Π₀ (i : ι), β i) f : Π₀ (i : ι), β i)
⊢ f.sum (β := β) (single (β := β)) = f
have this₁ : Eq (α := Π₀ (i : ι), β i)
  (f.sum (β := β) fun (x : ι) ↦ (⇑(singleAddHom β x) : (a : β x) → Π₀ (i : ι), β i) : Π₀ (i : ι), β i)
  ((AddMonoidHom.id (Π₀ (i : ι), β i) : (a : Π₀ (i : ι), β i) → Π₀ (i : ι), β i) f : Π₀ (i : ι), β i)
Tactic: rw [liftAddHom_apply, sumAddHom_apply] at this
Cleared hypotheses: this
-- 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 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : CommMonoid γ
v : Π₀ (i : ι), β i
p : ι → Prop
inst_4 : DecidablePred p
h : (i : ι) → β i → γ
hp : ∀ x ∈ v.support (β := β), p x
⊢ ((subtypeDomain (β := β) p v).prod (β := fun (i : Subtype p) ↦ β (↑i : ι)) fun (i : Subtype p) (b : β (↑i : ι)) ↦
      h (↑i : ι) b) =
    v.prod (β := β) h
have refine_1 : ∀ (a : Subtype p) (ha : a ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))),
  (fun (p_1 : Subtype p) (x : p_1 ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))) ↦
        (↑p_1 : ι))
      a ha ∈
    v.support (β := β)
Tactic: refine Finset.prod_bij (fun p _ ↦ p) ?_ ?_ ?_ ?_
-- 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 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : CommMonoid γ
v : Π₀ (i : ι), β i
p : ι → Prop
inst_4 : DecidablePred p
h : (i : ι) → β i → γ
hp : ∀ x ∈ v.support (β := β), p x
refine_1 :
  ∀ (a : Subtype p) (ha : a ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))),
    (fun (p_1 : Subtype p) (x : p_1 ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))) ↦
          (↑p_1 : ι))
        a ha ∈
      v.support (β := β)
⊢ ((subtypeDomain (β := β) p v).prod (β := fun (i : Subtype p) ↦ β (↑i : ι)) fun (i : Subtype p) (b : β (↑i : ι)) ↦
      h (↑i : ι) b) =
    v.prod (β := β) h
have refine_2 : ∀ (a₁ : Subtype p) (ha₁ : a₁ ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι)))
  (a₂ : Subtype p) (ha₂ : a₂ ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))),
  Eq.{u + 1} (α := ι)
      ((fun (p_1 : Subtype p) (x : p_1 ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))) ↦
          (↑p_1 : ι))
        a₁ ha₁)
      ((fun (p_1 : Subtype p) (x : p_1 ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))) ↦
          (↑p_1 : ι))
        a₂ ha₂) →
    a₁ = a₂
Tactic: refine Finset.prod_bij (fun p _ ↦ p) ?_ ?_ ?_ ?_
-- 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 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : CommMonoid γ
v : Π₀ (i : ι), β i
p : ι → Prop
inst_4 : DecidablePred p
h : (i : ι) → β i → γ
hp : ∀ x ∈ v.support (β := β), p x
refine_1 :
  ∀ (a : Subtype p) (ha : a ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))),
    (fun (p_1 : Subtype p) (x : p_1 ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))) ↦
          (↑p_1 : ι))
        a ha ∈
      v.support (β := β)
refine_2 :
  ∀ (a₁ : Subtype p) (ha₁ : a₁ ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι)))
    (a₂ : Subtype p) (ha₂ : a₂ ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))),
    Eq.{u + 1} (α := ι)
        ((fun (p_1 : Subtype p)
              (x : p_1 ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))) ↦
            (↑p_1 : ι))
          a₁ ha₁)
        ((fun (p_1 : Subtype p)
              (x : p_1 ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))) ↦
            (↑p_1 : ι))
          a₂ ha₂) →
      a₁ = a₂
⊢ ((subtypeDomain (β := β) p v).prod (β := fun (i : Subtype p) ↦ β (↑i : ι)) fun (i : Subtype p) (b : β (↑i : ι)) ↦
      h (↑i : ι) b) =
    v.prod (β := β) h
have refine_3 : ∀ b ∈ v.support (β := β),
  ∃ (a : Subtype p) (ha : a ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))),
    (fun (p_1 : Subtype p) (x : p_1 ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))) ↦
          (↑p_1 : ι))
        a ha =
      b
Tactic: refine Finset.prod_bij (fun p _ ↦ p) ?_ ?_ ?_ ?_