awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Countable.Small
Goal:
α : Type v
h : ¬Small.{w, v} α
rw : ¬Countable α
⊢ Uncountable α

Tactic:
rw [uncountable_iff_not_countable]

Premises used: uncountable_iff_not_countable
-- Module: Mathlib.Data.Countable.Small
Goal:
α : Type v
h : ¬Small.{w, v} α
⊢ ¬Countable α

Tactic:
mt (@Countable.toSmall α) h

Premises used: mt, Countable.toSmall
-- Module: Mathlib.Data.Countable.Small
Goal:
α : Type v
h : ¬Small.{w, v} α
⊢ ¬Countable α

Tactic:
exact mt (@Countable.toSmall α) h

Premises used: mt, Countable.toSmall
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
β : ι → Type v
α : Type u_1
inst : (i : ι) → AddCommMonoid (β i)
s : Finset α
g : α → Π₀ (i : ι), β i
⊢ (⇑(∑ a ∈ s, g a) : (a : ι) → β a) = ∑ a ∈ s, (⇑(g a) : (a : ι) → β a)

Tactic:
map_sum coeFnAddMonoidHom g s

Premises used: map_sum, DFinsupp.coeFnAddMonoidHom
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
β : ι → Type v
α : Type u_1
inst : (i : ι) → AddCommMonoid (β i)
s : Finset α
g : α → Π₀ (i : ι), β i
i : ι
⊢ (∑ a ∈ s, g a : (a : ι) → β a) i = ∑ a ∈ s, (g a : (a : ι) → β a) i

Tactic:
map_sum (evalAddMonoidHom i) g s

Premises used: DFinsupp.evalAddMonoidHom, map_sum
-- 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 γ
f : Π₀ (i : ι), β i
g : (i : ι) → β i → γ
s : Finset ι
hs : f.support (β := β) ⊆ s
map_zero : ∀ i ∈ s, g i 0 = 1
apply : ∀ x ∈ s, x ∉ f.support (β := β) → g x ((f : (a : ι) → β a) x) = 1
⊢ Eq.{w + 1} (α := γ) (∏ i ∈ f.support (β := β), g i ((f : (a : ι) → β a) i)) (∏ i ∈ s, g i ((f : (a : ι) → β a) i))

Tactic:
apply Finset.prod_subset hs

Premises used: Finset.prod_subset
-- 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 γ
f : Π₀ (i : ι), β i
g : (i : ι) → β i → γ
s : Finset ι
hs : f.support (β := β) ⊆ s
map_zero : ∀ i ∈ s, g i 0 = 1
i : ι
hi : i ∈ s
hi' : i ∉ f.support (β := β)
⊢ (f : (a : ι) → β a) i = 0

Tactic:
simp only [DFinsupp.mem_support_toFun, ne_eq, not_not] at hi'

Premises used: DFinsupp.mem_support_toFun, Classical.not_not, ne_eq
-- 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 γ
f : Π₀ (i : ι), β i
g : (i : ι) → β i → γ
s : Finset ι
hs : f.support (β := β) ⊆ s
map_zero : ∀ i ∈ s, g i 0 = 1
i : ι
hi : i ∈ s
hi' : (f : (a : ι) → β a) i = 0
a : i ∈ s
⊢ g i ((f : (a : ι) → β a) i) = 1

Tactic:
rw [hi', map_zero]
-- 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 γ
f : Π₀ (i : ι), β i
g : (i : ι) → β i → γ
s : Finset ι
hs : f.support (β := β) ⊆ s
map_zero : ∀ i ∈ s, g i 0 = 1
i : ι
hi : i ∈ s
hi' : (f : (a : ι) → β a) i = 0
⊢ i ∈ s

Tactic:
hi
-- 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 γ
f : Π₀ (i : ι), β i
g : (i : ι) → β i → γ
s : Finset ι
hs : f.support (β := β) ⊆ s
map_zero : ∀ i ∈ s, g i 0 = 1
i : ι
hi : i ∈ s
hi' : (f : (a : ι) → β a) i = 0
⊢ i ∈ s

Tactic:
exact hi
-- 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 γ
f1 f2 : Π₀ (i : ι), β i
g1 g2 : (i : ι) → β i → γ
h : ∀ x ∈ f1.support (β := β) ∪ f2.support (β := β), g1 x ((f1 : (a : ι) → β a) x) = g2 x ((f2 : (a : ι) → β a) x)
h1 : ∀ x ∈ f1.support (β := β) ∪ f2.support (β := β), g1 x 0 = 1
h2 : ∀ x ∈ f1.support (β := β) ∪ f2.support (β := β), g2 x 0 = 1
rw :
  Eq.{w + 1} (α := γ) (∏ i ∈ f1.support (β := β) ∪ f2.support (β := β), g1 i ((f1 : (a : ι) → β a) i))
    (∏ i ∈ f1.support (β := β) ∪ f2.support (β := β), g2 i ((f2 : (a : ι) → β a) i))
⊢ f1.prod (β := β) g1 = f2.prod (β := β) g2

Tactic:
rw [prod_of_support_subset Finset.subset_union_left h1,
    prod_of_support_subset Finset.subset_union_right h2]

Premises used: DFinsupp.prod_of_support_subset, Finset.subset_union_left, Finset.subset_union_right
-- 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 γ
f1 f2 : Π₀ (i : ι), β i
g1 g2 : (i : ι) → β i → γ
h : ∀ x ∈ f1.support (β := β) ∪ f2.support (β := β), g1 x ((f1 : (a : ι) → β a) x) = g2 x ((f2 : (a : ι) → β a) x)
h1 : ∀ x ∈ f1.support (β := β) ∪ f2.support (β := β), g1 x 0 = 1
h2 : ∀ x ∈ f1.support (β := β) ∪ f2.support (β := β), g2 x 0 = 1
⊢ Eq.{w + 1} (α := γ) (∏ i ∈ f1.support (β := β) ∪ f2.support (β := β), g1 i ((f1 : (a : ι) → β a) i))
    (∏ i ∈ f1.support (β := β) ∪ f2.support (β := β), g2 i ((f2 : (a : ι) → β a) i))

Tactic:
Finset.prod_congr rfl h

Premises used: Finset.prod_congr, rfl
-- 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 γ
f1 f2 : Π₀ (i : ι), β i
g1 g2 : (i : ι) → β i → γ
h : ∀ x ∈ f1.support (β := β) ∪ f2.support (β := β), g1 x ((f1 : (a : ι) → β a) x) = g2 x ((f2 : (a : ι) → β a) x)
h1 : ∀ x ∈ f1.support (β := β) ∪ f2.support (β := β), g1 x 0 = 1
h2 : ∀ x ∈ f1.support (β := β) ∪ f2.support (β := β), g2 x 0 = 1
⊢ Eq.{w + 1} (α := γ) (∏ i ∈ f1.support (β := β) ∪ f2.support (β := β), g1 i ((f1 : (a : ι) → β a) i))
    (∏ i ∈ f1.support (β := β) ∪ f2.support (β := β), g2 i ((f2 : (a : ι) → β a) i))

Tactic:
exact Finset.prod_congr rfl h

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
R : Type u_1
S : Type u_2
H : Type u_3
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : CommMonoid R
inst_4 : CommMonoid S
inst_5 : FunLike H R S
inst_6 : MonoidHomClass H R S
h : H
f : Π₀ (i : ι), β i
g : (i : ι) → β i → R
⊢ Eq.{u_2 + 1} (α := S) ((h : (a : R) → S) (f.prod (β := β) g) : S)
    (f.prod (β := β) fun (a : ι) (b : β a) ↦ (h : (a : R) → S) (g a b) : S)

Tactic:
map_prod _ _ _

Premises used: map_prod, DFinsupp.prod
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst_4 : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst_5 : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
rw :
  prod (β := β₂)
      (mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
        f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)))
      h =
    g.prod (β := β₁) fun (i : ι) (b : β₁ i) ↦ h i (f i b)
⊢ (mapRange (β₁ := β₁) (β₂ := β₂) f hf g).prod (β := β₂) h = g.prod (β := β₁) fun (i : ι) (b : β₁ i) ↦ h i (f i b)

Tactic:
rw [mapRange_def]

Premises used: DFinsupp.mapRange_def
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst_4 : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst_5 : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
⊢ prod (β := β₂)
      (mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
        f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)))
      h =
    g.prod (β := β₁) fun (i : ι) (b : β₁ i) ↦ h i (f i b)

Tactic:
(Finset.prod_subset support_mk_subset ?_).trans ?_

Premises used: DFinsupp.support_mk_subset, Finset.prod_subset, DFinsupp.prod, Eq.trans
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst_4 : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst_5 : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
refine_1 :
  ∀ x ∈ g.support (β := β₁),
    x ∉
        support (β := β₂)
          (mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
            f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι))) →
      h x
          ((mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
                f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)) :
              (a : ι) → β₂ a)
            x) =
        1
refine_2 :
  Eq.{w + 1} (α := γ)
    (∏ x ∈ g.support (β := β₁),
      h x
        ((mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
              f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)) :
            (a : ι) → β₂ a)
          x))
    (g.prod (β := β₁) fun (i : ι) (b : β₁ i) ↦ h i (f i b))
⊢ prod (β := β₂)
      (mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
        f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)))
      h =
    g.prod (β := β₁) fun (i : ι) (b : β₁ i) ↦ h i (f i b)

Tactic:
refine (Finset.prod_subset support_mk_subset ?_).trans ?_

Premises used: DFinsupp.support_mk_subset, Finset.prod_subset, Eq.trans
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst_4 : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst_5 : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
i : ι
h1 : i ∈ g.support (β := β₁)
h2 :
  i ∉
    support (β := β₂)
      (mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
        f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)))
⊢ ¬(g : (a : ι) → β₁ a) i = 0

Tactic:
simp only [mem_support_toFun, ne_eq] at h1

Premises used: DFinsupp.mem_support_toFun, ne_eq
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst_4 : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst_5 : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
i : ι
h2 :
  i ∉
    support (β := β₂)
      (mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
        f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)))
h1 : ¬(g : (a : ι) → β₁ a) i = 0
⊢ f i ((g : (a : ι) → β₁ a) i) = 0

Tactic:
simp only [Finset.coe_sort_coe, mem_support_toFun, mk_apply, ne_eq, h1, not_false_iff,
      dite_eq_ite, ite_true, not_not] at h2

Premises used: Finset.coe_sort_coe, DFinsupp.mem_support_toFun, Classical.not_not, ite_true, ne_eq, DFinsupp.mk_apply, dite_eq_ite, not_false_iff
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst_4 : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst_5 : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
i : ι
h1 : ¬(g : (a : ι) → β₁ a) i = 0
h2 : f i ((g : (a : ι) → β₁ a) i) = 0
⊢ h i
      ((mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
            f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)) :
          (a : ι) → β₂ a)
        i) =
    1

Tactic:
simp [h2, h0]
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst_4 : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst_5 : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
⊢ Eq.{w + 1} (α := γ)
    (∏ x ∈ g.support (β := β₁),
      h x
        ((mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
              f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)) :
            (a : ι) → β₂ a)
          x))
    (g.prod (β := β₁) fun (i : ι) (b : β₁ i) ↦ h i (f i b))

Tactic:
Finset.prod_congr rfl ?_

Premises used: Finset.prod_congr, DFinsupp.prod, rfl
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst_4 : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst_5 : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
refine_2 :
  ∀ x ∈ g.support (β := β₁),
    h x
        ((mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
              f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)) :
            (a : ι) → β₂ a)
          x) =
      (fun (i : ι) (b : β₁ i) ↦ h i (f i b)) x ((g : (a : ι) → β₁ a) x)
⊢ Eq.{w + 1} (α := γ)
    (∏ x ∈ g.support (β := β₁),
      h x
        ((mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
              f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)) :
            (a : ι) → β₂ a)
          x))
    (g.prod (β := β₁) fun (i : ι) (b : β₁ i) ↦ h i (f i b))

Tactic:
refine Finset.prod_congr rfl ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst_4 : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst_5 : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
i : ι
h1 : i ∈ g.support (β := β₁)
⊢ ¬(g : (a : ι) → β₁ a) i = 0

Tactic:
simp only [mem_support_toFun, ne_eq] at h1

Premises used: DFinsupp.mem_support_toFun, ne_eq
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst_4 : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst_5 : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
i : ι
h1 : ¬(g : (a : ι) → β₁ a) i = 0
⊢ h i
      ((mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
            f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)) :
          (a : ι) → β₂ a)
        i) =
    (fun (i : ι) (b : β₁ i) ↦ h i (f i b)) i ((g : (a : ι) → β₁ a) i)

Tactic:
simp [h1]
-- 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 γ
h : (i : ι) → β i → γ
⊢ prod (β := β) 0 h = 1

Tactic:
rfl

Premises used: Multiset.foldr, Multiset.prod, Finset.prod, DFinsupp.prod, List.foldr, rfl
-- 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 γ
i : ι
b : β i
h : (i : ι) → β i → γ
h_zero : h i 0 = 1
pos : ∀ (h_1 : b ≠ 0), prod (β := β) (single (β := β) i b) h = h i b
neg : ∀ (h_1 : ¬b ≠ 0), prod (β := β) (single (β := β) i b) h = h i b
⊢ prod (β := β) (single (β := β) i b) h = h i b

Tactic:
by_cases h : b ≠ 0
-- 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 γ
i : ι
b : β i
h_1 : (i : ι) → β i → γ
h_zero : h_1 i 0 = 1
h : b ≠ 0
⊢ prod (β := β) (single (β := β) i b) h_1 = h_1 i b

Tactic:
simp [DFinsupp.prod, support_single h]

Premises used: DFinsupp.support_single, DFinsupp.prod
-- 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 γ
i : ι
b : β i
h_1 : (i : ι) → β i → γ
h_zero : h_1 i 0 = 1
h : ¬b ≠ 0
⊢ b = 0

Tactic:
rw [not_not] at h

Premises used: Classical.not_not
-- 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 γ
i : ι
b : β i
h_1 : (i : ι) → β i → γ
h_zero : h_1 i 0 = 1
h : b = 0
neg : prod (β := β) 0 h_1 = 1
⊢ prod (β := β) (single (β := β) i b) h_1 = h_1 i b

Tactic:
simp [h, h_zero]
-- 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 γ
i : ι
b : β i
h_1 : (i : ι) → β i → γ
h_zero : h_1 i 0 = 1
h : b = 0
⊢ prod (β := β) 0 h_1 = 1

Tactic:
rfl
-- 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 : CommMonoid γ
g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h0 : ∀ (i : ι), h i 0 = 1
⊢ (-g).prod (β := β) h = g.prod (β := β) fun (i : ι) (b : β i) ↦ h i (-b)

Tactic:
prod_mapRange_index h0

Premises used: DFinsupp.prod_mapRange_index
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
γ : Type w
ι₁ : Type u_3
ι₂ : Type u_4
β₁ : ι₁ → Type u_1
β₂ : ι₂ → Type u_2
inst : DecidableEq ι₁
inst_1 : DecidableEq ι₂
inst_2 : (i : ι₁) → Zero (β₁ i)
inst_3 : (i : ι₂) → Zero (β₂ i)
inst_4 : (i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)
inst_5 : (i : ι₂) → (x : β₂ i) → Decidable (x ≠ 0)
inst_6 : CommMonoid γ
f₁ : Π₀ (i : ι₁), β₁ i
f₂ : Π₀ (i : ι₂), β₂ i
h : (i : ι₁) → β₁ i → (i : ι₂) → β₂ i → γ
⊢ Eq.{w + 1} (α := γ)
    (f₁.prod (β := β₁) fun (i₁ : ι₁) (x₁ : β₁ i₁) ↦ f₂.prod (β := β₂) fun (i₂ : ι₂) (x₂ : β₂ i₂) ↦ h i₁ x₁ i₂ x₂)
    (f₂.prod (β := β₂) fun (i₂ : ι₂) (x₂ : β₂ i₂) ↦ f₁.prod (β := β₁) fun (i₁ : ι₁) (x₁ : β₁ i₁) ↦ h i₁ x₁ i₂ x₂)

Tactic:
Finset.prod_comm

Premises used: DFinsupp.prod, Finset.prod_comm
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u_1
β : ι → Type v
ι₁ : Type u₁
inst : DecidableEq ι₁
β₁ : ι₁ → Type v₁
inst_1 : (i₁ : ι₁) → Zero (β₁ i₁)
inst_2 : (i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)
inst_3 : (i : ι) → AddCommMonoid (β i)
f : Π₀ (i₁ : ι₁), β₁ i₁
g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i
i₂ : ι
⊢ (f.sum (β := β₁) g : (a : ι) → β a) i₂ = f.sum (β := β₁) fun (i₁ : ι₁) (b : β₁ i₁) ↦ (g i₁ b : (a : ι) → β a) i₂

Tactic:
map_sum (evalAddMonoidHom i₂) _ f.support

Premises used: DFinsupp.evalAddMonoidHom, DFinsupp.support, DFinsupp.sum, map_sum
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
β : ι → 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)
f : Π₀ (i₁ : ι₁), β₁ i₁
g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i
⊢ ∀ (i₁ : ι),
    Ne.{v + 1} (α := β i₁) (f.sum (β := β₁) fun (i : ι₁) (b : β₁ i) ↦ (g i b : (a : ι) → β a) i₁) 0 →
      ∃ (i : ι₁), (f : (a : ι₁) → β₁ a) i ≠ 0 ∧ ¬(g i ((f : (a : ι₁) → β₁ a) i) : (a : ι) → β a) i₁ = 0

Tactic:
have :
    ∀ i₁ : ι,
      (f.sum fun (i : ι₁) (b : β₁ i) => (g i b) i₁) ≠ 0 → ∃ i : ι₁, f i ≠ 0 ∧ ¬(g i (f i)) i₁ = 0 :=
    fun i₁ h =>
    let ⟨i, hi, Ne⟩ := Finset.exists_ne_zero_of_sum_ne_zero h
    ⟨i, mem_support_iff.1 hi, Ne⟩
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
β : ι → 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)
f : Π₀ (i₁ : ι₁), β₁ i₁
g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i
this :
  ∀ (i₁ : ι),
    Ne.{v + 1} (α := β i₁) (f.sum (β := β₁) fun (i : ι₁) (b : β₁ i) ↦ (g i b : (a : ι) → β a) i₁) 0 →
      ∃ (i : ι₁), (f : (a : ι₁) → β₁ a) i ≠ 0 ∧ ¬(g i ((f : (a : ι₁) → β₁ a) i) : (a : ι) → β a) i₁ = 0
⊢ (f.sum (β := β₁) g).support (β := β) ⊆
    f.support (β := β₁).biUnion fun (i : ι₁) ↦ (g i ((f : (a : ι₁) → β₁ a) i)).support (β := β)

Tactic:
simpa [Finset.subset_iff, mem_support_iff, Finset.mem_biUnion, sum_apply] using this

Premises used: DFinsupp.sum_apply, DFinsupp.mem_support_iff, Finset.subset_iff, Finset.mem_biUnion
-- 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 : Π₀ (i : ι), β i
⊢ Eq.{w + 1} (α := γ) (f.prod (β := β) fun (x : ι) (x_1 : β x) ↦ 1) 1

Tactic:
Finset.prod_const_one

Premises used: DFinsupp.prod, Finset.prod_const_one
-- 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 : Π₀ (i : ι), β i
h₁ h₂ : (i : ι) → β i → γ
⊢ (f.prod (β := β) fun (i : ι) (b : β i) ↦ h₁ i b * h₂ i b) = f.prod (β := β) h₁ * f.prod (β := β) h₂

Tactic:
Finset.prod_mul_distrib

Premises used: Finset.prod_mul_distrib, DFinsupp.prod
-- 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 : DivisionCommMonoid γ
f : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
⊢ (f.prod (β := β) fun (i : ι) (b : β i) ↦ (h i b)⁻¹) = (f.prod (β := β) h)⁻¹

Tactic:
(map_prod (invMonoidHom : γ →* γ) _ f.support).symm

Premises used: invMonoidHom, DFinsupp.support, map_prod, DFinsupp.prod, Eq.symm
-- 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 γ
f : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
hyp : ∀ (i : ι), h i ((f : (a : ι) → β a) i) = 1
⊢ f.prod (β := β) h = 1

Tactic:
Finset.prod_eq_one fun i _ => hyp i

Premises used: Finset.prod_eq_one, DFinsupp.prod
-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
α : Type u_1
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : AddCommMonoid γ
inst_4 : DistribSMul α γ
f : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
c : α
⊢ c • f.sum (β := β) h = f.sum (β := β) fun (a : ι) (b : β a) ↦ c • h a b

Tactic:
Finset.smul_sum

Premises used: DFinsupp.sum, Finset.smul_sum
-- 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₂
⊢ ∀ x ∈ f.support (β := β) ∪ g.support (β := β), x ∉ f.support (β := β) → h x ((f : (a : ι) → β a) x) = 1

Tactic:
simp +contextual [h_zero]