awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddCommMonoid (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : CommMonoid γ
f 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₂
f_eq : ∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((f : (a : ι) → β a) i) = f.prod (β := β) h
⊢ ∀ x ∈ f.support (β := β) ∪ g.support (β := β), x ∉ g.support (β := β) → h x ((g : (a : ι) → β a) x) = 1

Tactic:
simp +contextual [h_zero]
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddCommMonoid (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : CommMonoid γ
f 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₂
f_eq : ∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((f : (a : ι) → β a) i) = f.prod (β := β) h
g_eq : ∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((g : (a : ι) → β a) i) = g.prod (β := β) h
⊢ ∀ x ∈ f.support (β := β) ∪ g.support (β := β), x ∉ (f + g).support (β := β) → h x ((f + g : (a : ι) → β a) x) = 1

Tactic:
simp +contextual [h_zero]
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddCommMonoid (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : CommMonoid γ
f 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₂
f_eq : ∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((f : (a : ι) → β a) i) = f.prod (β := β) h
g_eq : ∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((g : (a : ι) → β a) i) = g.prod (β := β) h
⊢ ∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((f + g : (a : ι) → β a) i) =
    HMul.hMul (α := γ) (∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((f : (a : ι) → β a) i))
      (∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((g : (a : ι) → β a) i))

Tactic:
simp [h_add, Finset.prod_mul_distrib]

Premises used: Finset.prod_mul_distrib
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddCommMonoid (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : CommMonoid γ
f 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₂
f_eq : ∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((f : (a : ι) → β a) i) = f.prod (β := β) h
g_eq : ∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((g : (a : ι) → β a) i) = g.prod (β := β) h
⊢ ∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((f + g : (a : ι) → β a) i) =
    HMul.hMul (α := γ) (∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((f : (a : ι) → β a) i))
      (∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((g : (a : ι) → β a) i))

Tactic:
{ simp [h_add, Finset.prod_mul_distrib] }

Premises used: Finset.prod_mul_distrib
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddCommMonoid (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : CommMonoid γ
f 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₂
f_eq : ∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((f : (a : ι) → β a) i) = f.prod (β := β) h
g_eq : ∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((g : (a : ι) → β a) i) = g.prod (β := β) h
rw :
  f.prod (β := β) h * ∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((g : (a : ι) → β a) i) =
    f.prod (β := β) h * g.prod (β := β) h
rw₁ rw₂ : f.prod (β := β) h * g.prod (β := β) h = f.prod (β := β) h * g.prod (β := β) h
⊢ HMul.hMul (α := γ) (∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((f : (a : ι) → β a) i))
      (∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((g : (a : ι) → β a) i)) =
    f.prod (β := β) h * g.prod (β := β) h

Tactic:
rw [f_eq, g_eq]
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : (i : ι) → Zero (β i)
inst_3 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_4 : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
this :
  Eq.{w + 1} (α := γ) (∏ i ∈ v.support (β := β), f i ((v : (a : ι) → β a) i)) (∏ i : ι, f i ((v : (a : ι) → β a) i))
⊢ v.prod (β := β) f = ∏ i : ι, f i ((equivFunOnFintype (β := β) : (a : Π₀ (i : ι), β i) → (i : ι) → β i) v i)

Tactic:
simp [DFinsupp.prod, this]

Premises used: DFinsupp.prod
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : (i : ι) → Zero (β i)
inst_3 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_4 : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
suffices :
  Eq.{w + 1} (α := γ) (∏ i ∈ v.support (β := β), f i ((v : (a : ι) → β a) i)) (∏ i : ι, f i ((v : (a : ι) → β a) i))
⊢ v.prod (β := β) f = ∏ i : ι, f i ((equivFunOnFintype (β := β) : (a : Π₀ (i : ι), β i) → (i : ι) → β i) v i)

Tactic:
suffices (∏ i ∈ v.support, f i (v i)) = ∏ i, f i (v i) by simp [DFinsupp.prod, this]
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : (i : ι) → Zero (β i)
inst_3 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_4 : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
apply :
  ∀ (x : ι), Membership.mem (γ := Finset ι) Finset.univ x → x ∉ v.support (β := β) → f x ((v : (a : ι) → β a) x) = 1
⊢ Eq.{w + 1} (α := γ) (∏ i ∈ v.support (β := β), f i ((v : (a : ι) → β a) i)) (∏ i : ι, f i ((v : (a : ι) → β a) i))

Tactic:
apply Finset.prod_subset v.support.subset_univ

Premises used: DFinsupp.support, Finset.prod_subset, Finset.subset_univ
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : (i : ι) → Zero (β i)
inst_3 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_4 : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
i : ι
_ : Membership.mem (γ := Finset ι) Finset.univ i → i ∉ v.support (β := β) → f i ((v : (a : ι) → β a) i) = 1
⊢ Membership.mem (γ := Finset ι) Finset.univ i → i ∉ v.support (β := β) → f i ((v : (a : ι) → β a) i) = 1

Tactic:
_
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : (i : ι) → Zero (β i)
inst_3 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_4 : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
hi : i ∉ v.support (β := β)
⊢ (v : (a : ι) → β a) i = 0

Tactic:
rw [mem_support_iff, not_not] at hi

Premises used: Classical.not_not, DFinsupp.mem_support_iff
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : (i : ι) → Zero (β i)
inst_3 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_4 : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
hi : (v : (a : ι) → β a) i = 0
rw : f i 0 = 1
rw₁ rw₂ : Eq.{w + 1} (α := γ) 1 1
⊢ f i ((v : (a : ι) → β a) i) = 1

Tactic:
rw [hi, hf]
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : CommMonoidWithZero γ
inst_3 : Nontrivial γ
inst_4 : NoZeroDivisors γ
inst_5 : (i : ι) → DecidableEq (β i)
f : Π₀ (i : ι), β i
g : (i : ι) → β i → γ
⊢ f.prod (β := β) g = 0 ↔ ∃ i ∈ f.support (β := β), g i ((f : (a : ι) → β a) i) = 0

Tactic:
Finset.prod_eq_zero_iff

Premises used: DFinsupp.prod, Finset.prod_eq_zero_iff
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : CommMonoidWithZero γ
inst_3 : Nontrivial γ
inst_4 : NoZeroDivisors γ
inst_5 : (i : ι) → DecidableEq (β i)
f : Π₀ (i : ι), β i
g : (i : ι) → β i → γ
⊢ f.prod (β := β) g ≠ 0 ↔ ∀ i ∈ f.support (β := β), g i ((f : (a : ι) → β a) i) ≠ 0

Tactic:
Finset.prod_ne_zero_iff

Premises used: Finset.prod_ne_zero_iff, DFinsupp.prod
-- 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) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
dsimp :
  Eq.{w + 1} (α := γ) (∑ i ∈ sx.toFinset, (φ i : (a : β i) → γ) ((f : (a : ι) → β a) i))
    (∑ i ∈ sy.toFinset, (φ i : (a : β i) → γ) ((f : (a : ι) → β a) i))
⊢ Eq.{w + 1} (α := γ)
    ((fun (s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0 }) ↦
        (∑ i ∈ (↑s : Multiset ι).toFinset, (φ i : (a : β i) → γ) ((f : (a : ι) → β a) i) : γ))
      (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0) sx hx))
    ((fun (s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0 }) ↦
        (∑ i ∈ (↑s : Multiset ι).toFinset, (φ i : (a : β i) → γ) ((f : (a : ι) → β a) i) : γ))
      (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0) sy hy))

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

Premises used: Subtype.coe_mk, DFinsupp.toFun_eq_coe
-- 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) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
⊢ sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset

Tactic:
have H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset := Finset.inter_subset_left
-- 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) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
⊢ sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset

Tactic:
have H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset := Finset.inter_subset_right
-- 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) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
⊢ Eq.{w + 1} (α := γ) (∑ i ∈ sx.toFinset, (φ i : (a : β i) → γ) ((f : (a : ι) → β a) i))
    (∑ i ∈ sy.toFinset, (φ i : (a : β i) → γ) ((f : (a : ι) → β a) i))

Tactic:
(Finset.sum_subset H1 ?_).symm.trans
          ((Finset.sum_congr rfl ?_).trans (Finset.sum_subset H2 ?_))

Premises used: Finset.sum_subset, Eq.symm, Finset.sum_congr, rfl, Eq.trans
-- 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) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
refine_1 :
  ∀ x ∈ sx.toFinset,
    x ∉ sx.toFinset ∩ sy.toFinset → Eq.{w + 1} (α := γ) ((φ x : (a : β x) → γ) ((f : (a : ι) → β a) x) : γ) (0 : γ)
refine_2 :
  ∀ x ∈ sx.toFinset ∩ sy.toFinset,
    Eq.{w + 1} (α := γ) ((φ x : (a : β x) → γ) ((f : (a : ι) → β a) x) : γ)
      ((φ x : (a : β x) → γ) ((f : (a : ι) → β a) x) : γ)
refine_3 :
  ∀ x ∈ sy.toFinset,
    x ∉ sx.toFinset ∩ sy.toFinset → Eq.{w + 1} (α := γ) ((φ x : (a : β x) → γ) ((f : (a : ι) → β a) x) : γ) (0 : γ)
⊢ Eq.{w + 1} (α := γ) (∑ i ∈ sx.toFinset, (φ i : (a : β i) → γ) ((f : (a : ι) → β a) i))
    (∑ i ∈ sy.toFinset, (φ i : (a : β i) → γ) ((f : (a : ι) → β a) i))

Tactic:
refine
        (Finset.sum_subset H1 ?_).symm.trans
          ((Finset.sum_congr rfl ?_).trans (Finset.sum_subset H2 ?_))

Premises used: Finset.sum_subset, Eq.symm, Finset.sum_congr, rfl, Eq.trans
-- 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) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1_1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2_1 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sx.toFinset
H2 : i ∉ sx.toFinset ∩ sy.toFinset
⊢ ¬(i ∈ sx.toFinset ∧ i ∈ sy.toFinset)

Tactic:
rw [Finset.mem_inter] at H2

Premises used: Finset.mem_inter
-- 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) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1_1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2_1 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sx.toFinset
H2 : ¬(i ∈ sx.toFinset ∧ i ∈ sy.toFinset)
⊢ i ∈ sx

Tactic:
simp only [Multiset.mem_toFinset] at H1 H2

Premises used: Multiset.mem_toFinset
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → ZeroHom.{v, w} (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1_1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2_1 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sx.toFinset
H2 : ¬(i ∈ sx.toFinset ∧ i ∈ sy.toFinset)
H1₁ : i ∈ sx
⊢ ¬(i ∈ sx ∧ i ∈ sy)

Tactic:
simp only [Multiset.mem_toFinset] at H1 H2

Premises used: Multiset.mem_toFinset
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → ZeroHom.{v, w} (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1_1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2_1 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sx
H2 : ¬(i ∈ sx ∧ i ∈ sy)
⊢ Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) 0 : γ) (0 : γ)

Tactic:
map_zero (φ i)

Premises used: map_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) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1_1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2_1 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sx
H2 : ¬(i ∈ sx ∧ i ∈ sy)
h : (f : (a : ι) → β a) i = 0
⊢ Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) ((f : (a : ι) → β a) i) : γ) (0 : γ)

Tactic:
convert! map_zero (φ i)

Premises used: map_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) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1_1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2_1 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sx
H2 : ¬(i ∈ sx ∧ i ∈ sy)
⊢ (f : (a : ι) → β a) i = 0

Tactic:
(hy i).resolve_left (mt (And.intro H1) H2)

Premises used: mt, Or.resolve_left, And.intro
-- 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) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1_1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2_1 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sx
H2 : ¬(i ∈ sx ∧ i ∈ sy)
⊢ (f : (a : ι) → β a) i = 0

Tactic:
exact (hy i).resolve_left (mt (And.intro H1) H2)

Premises used: mt, Or.resolve_left, And.intro
-- 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) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
refine_2 :
  i ∈ sx.toFinset ∩ sy.toFinset →
    Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) ((f : (a : ι) → β a) i) : γ)
      ((φ i : (a : β i) → γ) ((f : (a : ι) → β a) i) : γ)
⊢ i ∈ sx.toFinset ∩ sy.toFinset →
    Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) ((f : (a : ι) → β a) i) : γ)
      ((φ i : (a : β i) → γ) ((f : (a : ι) → β a) i) : γ)

Tactic:
_
-- 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) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
h : i ∈ sx.toFinset ∩ sy.toFinset
⊢ Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) ((f : (a : ι) → β a) i) : γ)
    ((φ i : (a : β i) → γ) ((f : (a : ι) → β a) i) : γ)

Tactic:
rfl
-- 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) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1_1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2_1 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sy.toFinset
H2 : i ∉ sx.toFinset ∩ sy.toFinset
⊢ ¬(i ∈ sx.toFinset ∧ i ∈ sy.toFinset)

Tactic:
rw [Finset.mem_inter] at H2

Premises used: Finset.mem_inter
-- 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) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1_1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2_1 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sy.toFinset
H2 : ¬(i ∈ sx.toFinset ∧ i ∈ sy.toFinset)
⊢ i ∈ sy

Tactic:
simp only [Multiset.mem_toFinset] at H1 H2

Premises used: Multiset.mem_toFinset
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → ZeroHom.{v, w} (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1_1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2_1 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sy.toFinset
H2 : ¬(i ∈ sx.toFinset ∧ i ∈ sy.toFinset)
H1₁ : i ∈ sy
⊢ ¬(i ∈ sx ∧ i ∈ sy)

Tactic:
simp only [Multiset.mem_toFinset] at H1 H2

Premises used: Multiset.mem_toFinset
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → ZeroHom.{v, w} (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1_1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2_1 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sy
H2 : ¬(i ∈ sx ∧ i ∈ sy)
⊢ Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) 0 : γ) (0 : γ)

Tactic:
map_zero (φ i)

Premises used: map_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) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1_1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2_1 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sy
H2 : ¬(i ∈ sx ∧ i ∈ sy)
h : (f : (a : ι) → β a) i = 0
⊢ Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) ((f : (a : ι) → β a) i) : γ) (0 : γ)

Tactic:
convert! map_zero (φ i)

Premises used: map_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) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1_1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2_1 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sy
H2 : ¬(i ∈ sx ∧ i ∈ sy)
⊢ (f : (a : ι) → β a) i = 0

Tactic:
(hx i).resolve_left (mt (fun H3 => And.intro H3 H1) H2)

Premises used: mt, Or.resolve_left, And.intro
-- 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) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1_1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2_1 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sy
H2 : ¬(i ∈ sx ∧ i ∈ sy)
⊢ (f : (a : ι) → β a) i = 0

Tactic:
exact (hx i).resolve_left (mt (fun H3 => And.intro H3 H1) H2)

Premises used: mt, Or.resolve_left, And.intro