awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
g h : (i : ι) → AddMonoidHom.{v, w} (β i) γ
⊢ (sumAddHom (β := β) fun (i : ι) ↦ g i + h i) = sumAddHom (β := β) g + sumAddHom (β := β) h

Tactic:
map_add liftAddHom _ _

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

Tactic:
liftAddHom_singleAddHom

Premises used: DFinsupp.liftAddHom_singleAddHom, DFinsupp.sumAddHom
-- 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) γ
⊢ g.comp (sumAddHom (β := β) f) = sumAddHom (β := β) fun (a : ι) ↦ g.comp (f a)

Tactic:
comp_liftAddHom _ _

Premises used: DFinsupp.comp_liftAddHom, DFinsupp.sumAddHom
-- Module: Mathlib.Data.DFinsupp.BigOperators
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₂
⊢ ((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 :
        γ)

Tactic:
have := (liftAddHom fun a => AddMonoidHom.ofMapSub (h a) (h_sub a)).map_sub f g
-- Module: Mathlib.Data.DFinsupp.BigOperators
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 (β := β) fun (x : ι) ↦ (⇑(AddMonoidHom.ofMapSub (h x) ⋯) : (a : β x) → γ)) =
    HSub.hSub (α := γ) (f.sum (β := β) fun (x : ι) ↦ (⇑(AddMonoidHom.ofMapSub (h x) ⋯) : (a : β x) → γ))
      (g.sum (β := β) fun (x : ι) ↦ (⇑(AddMonoidHom.ofMapSub (h x) ⋯) : (a : β x) → γ))

Tactic:
rw [liftAddHom_apply, sumAddHom_apply, sumAddHom_apply, sumAddHom_apply] at this

Premises used: DFinsupp.liftAddHom_apply, DFinsupp.sumAddHom_apply
-- Module: Mathlib.Data.DFinsupp.BigOperators
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 :
  ((f - g).sum (β := β) fun (x : ι) ↦ (⇑(AddMonoidHom.ofMapSub (h x) ⋯) : (a : β x) → γ)) =
    HSub.hSub (α := γ) (f.sum (β := β) fun (x : ι) ↦ (⇑(AddMonoidHom.ofMapSub (h x) ⋯) : (a : β x) → γ))
      (g.sum (β := β) fun (x : ι) ↦ (⇑(AddMonoidHom.ofMapSub (h x) ⋯) : (a : β x) → γ))
⊢ (f - g).sum (β := β) h = f.sum (β := β) h - g.sum (β := β) h

Tactic:
this
-- Module: Mathlib.Data.DFinsupp.BigOperators
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 :
  ((f - g).sum (β := β) fun (x : ι) ↦ (⇑(AddMonoidHom.ofMapSub (h x) ⋯) : (a : β x) → γ)) =
    HSub.hSub (α := γ) (f.sum (β := β) fun (x : ι) ↦ (⇑(AddMonoidHom.ofMapSub (h x) ⋯) : (a : β x) → γ))
      (g.sum (β := β) fun (x : ι) ↦ (⇑(AddMonoidHom.ofMapSub (h x) ⋯) : (a : β x) → γ))
⊢ (f - g).sum (β := β) h = f.sum (β := β) h - g.sum (β := β) h

Tactic:
exact this
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
γ : Type w
α : Type x
inst_1 : (i : ι) → AddCommMonoid (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : CommMonoid γ
s : Finset α
g : α → Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
⊢ ∏ i ∈ ∅, (g i).prod (β := β) h = prod (β := β) (∑ i ∈ ∅, g i) h

Tactic:
simp [prod_zero_index]

Premises used: DFinsupp.prod_zero_index
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
γ : Type w
α : Type x
inst_1 : (i : ι) → AddCommMonoid (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : CommMonoid γ
s : Finset α
g : α → Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
⊢ ∀ (a : α) (s : Finset α),
    a ∉ s →
      ∏ i ∈ s, (g i).prod (β := β) h = prod (β := β) (∑ i ∈ s, g i) h →
        ∏ i ∈ insert a s, (g i).prod (β := β) h = prod (β := β) (∑ i ∈ insert a s, g i) h

Tactic:
simp +contextual [prod_add_index, h_zero, h_add]

Premises used: DFinsupp.prod_add_index
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
γ : Type w
α : Type x
inst_1 : (i : ι) → AddCommMonoid (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : CommMonoid γ
s : Finset α
g : α → Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
⊢ ∏ i ∈ s, (g i).prod (β := β) h = prod (β := β) (∑ i ∈ s, g i) h

Tactic:
exact Finset.induction_on s (by simp [prod_zero_index])
        (by simp +contextual [prod_add_index, h_zero, h_add])
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
γ : Type w
α : Type x
inst_1 : (i : ι) → AddCommMonoid (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : CommMonoid γ
s : Finset α
g : α → Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
⊢ ∏ i ∈ s, (g i).prod (β := β) h = prod (β := β) (∑ i ∈ s, g i) h

Tactic:
classical
  exact Finset.induction_on s (by simp [prod_zero_index])
        (by simp +contextual [prod_add_index, h_zero, h_add])
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
ι₁ : Type u₁
inst_1 : DecidableEq ι₁
β₁ : ι₁ → Type v₁
inst_2 : (i₁ : ι₁) → Zero (β₁ i₁)
inst_3 : (i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)
inst_4 : (i : ι) → AddCommMonoid (β i)
inst_5 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_6 : CommMonoid γ
f : Π₀ (i₁ : ι₁), β₁ i₁
g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
⊢ (f.sum (β := β₁) g).prod (β := β) h = f.prod (β := β₁) fun (i : ι₁) (b : β₁ i) ↦ (g i b).prod (β := β) h

Tactic:
(prod_finsetSum_index h_zero h_add).symm

Premises used: DFinsupp.sum, DFinsupp.prod, DFinsupp.prod_finsetSum_index, Eq.symm
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddCommMonoid (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
⊢ 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
-- Module: Mathlib.Data.DFinsupp.BigOperators
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)
⊢ 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

Premises used: DFinsupp.liftAddHom_apply, DFinsupp.sumAddHom_apply
-- Module: Mathlib.Data.DFinsupp.BigOperators
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)
    (f.sum (β := β) fun (x : ι) ↦ (⇑(singleAddHom β x) : (a : β x) → Π₀ (i : ι), β i) : Π₀ (i : ι), β i)
    ((AddMonoidHom.id (Π₀ (i : ι), β i) : (a : Π₀ (i : ι), β i) → Π₀ (i : ι), β i) f : Π₀ (i : ι), β i)
⊢ f.sum (β := β) (single (β := β)) = f

Tactic:
this

Premises used: DFinsupp.single
-- Module: Mathlib.Data.DFinsupp.BigOperators
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)
    (f.sum (β := β) fun (x : ι) ↦ (⇑(singleAddHom β x) : (a : β x) → Π₀ (i : ι), β i) : Π₀ (i : ι), β i)
    ((AddMonoidHom.id (Π₀ (i : ι), β i) : (a : Π₀ (i : ι), β i) → Π₀ (i : ι), β i) f : Π₀ (i : ι), β i)
⊢ f.sum (β := β) (single (β := β)) = f

Tactic:
exact this
-- Module: Mathlib.Data.DFinsupp.BigOperators
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

Tactic:
Finset.prod_bij (fun p _ ↦ p) ?_ ?_ ?_ ?_

Premises used: DFinsupp.prod, Subtype.val, Finset.prod_bij
-- Module: Mathlib.Data.DFinsupp.BigOperators
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₂
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
refine_4 :
  ∀ (a : Subtype p) (ha : a ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))),
    (fun (i : Subtype p) (b : β (↑i : ι)) ↦ h (↑i : ι) b) a
        ((subtypeDomain (β := β) p v : (a : Subtype p) → β (↑a : ι)) a) =
      h
        ((fun (p_1 : Subtype p)
              (x : p_1 ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))) ↦
            (↑p_1 : ι))
          a ha)
        ((v : (a : ι) → β a)
          ((fun (p_1 : Subtype p)
                (x : p_1 ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))) ↦
              (↑p_1 : ι))
            a ha))
⊢ ((subtypeDomain (β := β) p v).prod (β := fun (i : Subtype p) ↦ β (↑i : ι)) fun (i : Subtype p) (b : β (↑i : ι)) ↦
      h (↑i : ι) b) =
    v.prod (β := β) h

Tactic:
refine Finset.prod_bij (fun p _ ↦ p) ?_ ?_ ?_ ?_

Premises used: Finset.prod_bij
-- Module: Mathlib.Data.DFinsupp.BigOperators
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
⊢ ∀ (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:
aesop
-- Module: Mathlib.Data.DFinsupp.BigOperators
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
⊢ ∀ (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:
aesop
-- Module: Mathlib.Data.DFinsupp.BigOperators
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
⊢ ∀ 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:
aesop
-- Module: Mathlib.Data.DFinsupp.BigOperators
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
⊢ ∀ (a : Subtype p) (ha : a ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))),
    (fun (i : Subtype p) (b : β (↑i : ι)) ↦ h (↑i : ι) b) a
        ((subtypeDomain (β := β) p v : (a : Subtype p) → β (↑a : ι)) a) =
      h
        ((fun (p_1 : Subtype p)
              (x : p_1 ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))) ↦
            (↑p_1 : ι))
          a ha)
        ((v : (a : ι) → β a)
          ((fun (p_1 : Subtype p)
                (x : p_1 ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))) ↦
              (↑p_1 : ι))
            a ha))

Tactic:
aesop
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
γ : Type w
ι : Type u_1
β : ι → Type v
inst : (i : ι) → AddCommMonoid (β i)
s : Finset γ
h : γ → Π₀ (i : ι), β i
p : ι → Prop
inst_1 : DecidablePred p
⊢ Eq (α := Π₀ (i : Subtype p), β (↑i : ι)) (subtypeDomain (β := β) p (∑ c ∈ s, h c) : Π₀ (i : Subtype p), β (↑i : ι))
    (∑ c ∈ s, subtypeDomain (β := β) p (h c) : Π₀ (i : Subtype p), β (↑i : ι))

Tactic:
map_sum (subtypeDomainAddMonoidHom β p) _ s

Premises used: map_sum, DFinsupp.subtypeDomain, DFinsupp.subtypeDomainAddMonoidHom
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
γ : Type w
ι : Type u_1
β : ι → Type v
δ : γ → Type x
inst : DecidableEq γ
inst_1 : (c : γ) → Zero (δ c)
inst_2 : (c : γ) → (x : δ c) → Decidable (x ≠ 0)
inst_3 : (i : ι) → AddCommMonoid (β i)
p : ι → Prop
inst_4 : DecidablePred p
s : Π₀ (c : γ), δ c
h : (c : γ) → δ c → Π₀ (i : ι), β i
⊢ subtypeDomain (β := β) p (s.sum (β := δ) h) = s.sum (β := δ) fun (c : γ) (d : δ c) ↦ subtypeDomain (β := β) p (h c d)

Tactic:
subtypeDomain_sum

Premises used: DFinsupp.sum, DFinsupp.subtypeDomain_sum
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
R : Type u_1
S : Type u_2
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : MulOneClass R
inst_4 : CommMonoid S
f : Π₀ (i : ι), β i
g : (i : ι) → β i → R →* S
⊢ Eq (α := (a : R) → S) (⇑(f.prod (β := β) g) : (a : R) → S)
    (f.prod (β := β) fun (a : ι) (b : β a) ↦ (⇑(g a b) : (a : R) → S))

Tactic:
coe_finsetProd _ _

Premises used: MonoidHom.coe_finsetProd, DFinsupp.prod
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
R : Type u_1
S : Type u_2
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : MulOneClass R
inst_4 : CommMonoid S
f : Π₀ (i : ι), β i
g : (i : ι) → β i → R →* S
r : R
⊢ Eq.{u_2 + 1} (α := S) ((f.prod (β := β) g : (a : R) → S) r : S)
    (f.prod (β := β) fun (a : ι) (b : β a) ↦ (g a b : (a : R) → S) r : S)

Tactic:
finsetProd_apply _ _ _

Premises used: MonoidHom.finsetProd_apply, DFinsupp.prod
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
R : Type u_1
S : Type u_2
inst_1 : AddCommMonoid R
inst_2 : AddCommMonoid S
inst_3 : (i : ι) → AddZeroClass (β i)
h : R →+ S
f : Π₀ (i : ι), β i
g : (i : ι) → AddMonoidHom.{v, u_1} (β i) R
⊢ Eq.{u_2 + 1} (α := S) ((h : (a : R) → S) ((sumAddHom (β := β) g : (a : Π₀ (i : ι), β i) → R) f : R) : S)
    ((sumAddHom (β := β) fun (i : ι) ↦ h.comp (g i) : (a : Π₀ (i : ι), β i) → S) f : S)

Tactic:
DFunLike.congr_fun (comp_liftAddHom h g) f

Premises used: DFunLike.congr_fun, DFinsupp.comp_liftAddHom
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
R : Type u_1
S : Type u_2
inst_1 : AddZeroClass R
inst_2 : AddCommMonoid S
inst_3 : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
g : (i : ι) → β i →+ R →+ S
r : R
⊢ Eq.{u_2 + 1} (α := S) ((((sumAddHom (β := β) g : (a : Π₀ (i : ι), β i) → R →+ S) f : R →+ S) : (a : R) → S) r : S)
    ((sumAddHom (β := β) fun (i : ι) ↦ comp ((eval : (a : R) → (R →+ S) →+ S) r) (g i) : (a : Π₀ (i : ι), β i) → S) f :
      S)

Tactic:
map_dfinsuppSumAddHom (eval r) f g

Premises used: AddMonoidHom.map_dfinsuppSumAddHom, AddMonoidHom.eval, DFunLike.coe
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
R : Type u_1
S : Type u_2
inst_1 : AddZeroClass R
inst_2 : AddCommMonoid S
inst_3 : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
g : (i : ι) → β i →+ R →+ S
⊢ Eq (α := (a : R) → S) (⇑((sumAddHom (β := β) g : (a : Π₀ (i : ι), β i) → R →+ S) f : R →+ S) : (a : R) → S)
    ((sumAddHom (β := β) fun (i : ι) ↦ comp (coeFn R S) (g i) : (a : Π₀ (i : ι), β i) → R → S) f)

Tactic:
map_dfinsuppSumAddHom (coeFn R S) f g

Premises used: AddMonoidHom.map_dfinsuppSumAddHom, AddMonoidHom.coeFn
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
R : Type u_1
S : Type u_2
inst_1 : NonAssocSemiring R
inst_2 : NonAssocSemiring S
inst_3 : (i : ι) → AddZeroClass (β i)
h : R →+* S
f : Π₀ (i : ι), β i
g : (i : ι) → AddMonoidHom.{v, u_1} (β i) R
⊢ Eq.{u_2 + 1} (α := S) ((h : (a : R) → S) ((sumAddHom (β := β) g : (a : Π₀ (i : ι), β i) → R) f : R) : S)
    ((sumAddHom (β := β) fun (i : ι) ↦ h.toAddMonoidHom.comp (g i) : (a : Π₀ (i : ι), β i) → S) f : S)

Tactic:
DFunLike.congr_fun (comp_liftAddHom h.toAddMonoidHom g) f

Premises used: DFunLike.congr_fun, RingHom.toAddMonoidHom, DFinsupp.comp_liftAddHom
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
R : Type u_1
S : Type u_2
inst_1 : AddCommMonoid R
inst_2 : AddCommMonoid S
inst_3 : (i : ι) → AddZeroClass (β i)
h : R ≃+ S
f : Π₀ (i : ι), β i
g : (i : ι) → AddMonoidHom.{v, u_1} (β i) R
⊢ Eq.{u_2 + 1} (α := S) ((h : (a : R) → S) ((sumAddHom (β := β) g : (a : Π₀ (i : ι), β i) → R) f : R) : S)
    ((sumAddHom (β := β) fun (i : ι) ↦ AddMonoidHom.comp h.toAddMonoidHom (g i) : (a : Π₀ (i : ι), β i) → S) f : S)

Tactic:
DFunLike.congr_fun (comp_liftAddHom h.toAddMonoidHom g) f

Premises used: DFunLike.congr_fun, AddEquiv.toAddMonoidHom, DFinsupp.comp_liftAddHom
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
x x_1 : Π₀ (i : ι), β i
f₁ : (i : ι) → β i
s₁_1 : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f₁ i = 0 }
f₂ : (i : ι) → β i
s₁ : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f₂ i = 0 }
h : f₁ = f₂
subst :
  ∀ (s₁ : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f₁ i = 0 }),
    mk' (β := fun (i : ι) ↦ β i) f₁ s₁_1 = mk' (β := fun (i : ι) ↦ β i) f₁ s₁
⊢ mk' (β := fun (i : ι) ↦ β i) f₁ s₁_1 = mk' (β := fun (i : ι) ↦ β i) f₂ s₁

Tactic:
subst h
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
x x_1 : Π₀ (i : ι), β i
f₁ : (i : ι) → β i
s₁_1 s₁ : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f₁ i = 0 }
e_support' : s₁_1 = s₁
⊢ mk' (β := fun (i : ι) ↦ β i) f₁ s₁_1 = mk' (β := fun (i : ι) ↦ β i) f₁ s₁

Tactic:
congr
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
x x_1 : Π₀ (i : ι), β i
f₁ : (i : ι) → β i
s₁_1 s₁ : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f₁ i = 0 }
⊢ s₁_1 = s₁

Tactic:
subsingleton
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
f : Π₀ (i : ι), β i
⊢ f.toFun (β := fun (i : ι) ↦ β i) = (⇑f : (a : ι) → β a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
f g : Π₀ (i : ι), β i
h : ∀ (i : ι), (f : (a : ι) → β a) i = (g : (a : ι) → β a) i
⊢ f = g

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext