awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
f g : Π₀ (i : ι), β i
⊢ f ≠ g ↔ ∃ (i : ι), (f : (a : ι) → β a) i ≠ (g : (a : ι) → β a) i

Tactic:
DFunLike.ne_iff

Premises used: DFunLike.ne_iff
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
f : (i : ι) → β i
s : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }
⊢ (⇑(mk' (β := fun (i : ι) ↦ β i) f s) : (a : ι) → β a) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
⊢ (⇑0 : (a : ι) → β a) = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
i : ι
⊢ (0 : (a : ι) → β a) i = 0

Tactic:
rfl

Premises used: rfl
-- 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)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
x : Π₀ (i : ι), β₁ i
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x.toFun (β := fun (i : ι) ↦ β₁ i) i = 0 }
i : ι
h : (x : (a : ι) → β₁ a) i = 0
rw : (fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i)) i = f i 0
rw₁ rw₂ : (fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i)) i = f i ((x : (a : ι) → β₁ a) i)
⊢ Eq.{v₂ + 1} (α := β₂ i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i)) i) 0

Tactic:
rw [← hf i, ← h]
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β₁ i)
inst_1 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
i : ι
⊢ (mapRange (β₁ := β₁) (β₂ := β₂) f hf g : (a : ι) → β₂ a) i = f i ((g : (a : ι) → β₁ a) i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β₁ : ι → Type v₁
inst : (i : ι) → Zero (β₁ i)
h : ∀ (i : ι), Eq.{v₁ + 1} (α := β₁ i) (id 0) 0
g : Π₀ (i : ι), β₁ i
h₁ : ∀ (i : ι), (mapRange (β₁ := β₁) (β₂ := β₁) (fun (i : ι) ↦ id) h g : (a : ι) → β₁ a) i = (g : (a : ι) → β₁ a) i
⊢ mapRange (β₁ := β₁) (β₂ := β₁) (fun (i : ι) ↦ id) h g = g

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β₁ : ι → Type v₁
inst : (i : ι) → Zero (β₁ i)
h : ∀ (i : ι), Eq.{v₁ + 1} (α := β₁ i) (id 0) 0
g : Π₀ (i : ι), β₁ i
i : ι
⊢ (mapRange (β₁ := β₁) (β₂ := β₁) (fun (i : ι) ↦ id) h g : (a : ι) → β₁ a) i = (g : (a : ι) → β₁ a) i

Tactic:
rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
f₂ : (i : ι) → β i → β₁ i
hf : ∀ (i : ι), f i 0 = 0
hf₂ : ∀ (i : ι), f₂ i 0 = 0
h : ∀ (i : ι), (f i ∘ f₂ i) 0 = 0
g : Π₀ (i : ι), β i
h₁ :
  ∀ (i : ι),
    (mapRange (β₁ := β) (β₂ := β₂) (fun (i : ι) ↦ f i ∘ f₂ i) h g : (a : ι) → β₂ a) i =
      (mapRange (β₁ := β₁) (β₂ := β₂) f hf (mapRange (β₁ := β) (β₂ := β₁) f₂ hf₂ g) : (a : ι) → β₂ a) i
⊢ mapRange (β₁ := β) (β₂ := β₂) (fun (i : ι) ↦ f i ∘ f₂ i) h g =
    mapRange (β₁ := β₁) (β₂ := β₂) f hf (mapRange (β₁ := β) (β₂ := β₁) f₂ hf₂ g)

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
f₂ : (i : ι) → β i → β₁ i
hf : ∀ (i : ι), f i 0 = 0
hf₂ : ∀ (i : ι), f₂ i 0 = 0
h : ∀ (i : ι), (f i ∘ f₂ i) 0 = 0
g : Π₀ (i : ι), β i
i : ι
h₁ : (f i ∘ f₂ i) ((g : (a : ι) → β a) i) = f i (f₂ i ((g : (a : ι) → β a) i))
⊢ (mapRange (β₁ := β) (β₂ := β₂) (fun (i : ι) ↦ f i ∘ f₂ i) h g : (a : ι) → β₂ a) i =
    (mapRange (β₁ := β₁) (β₂ := β₂) f hf (mapRange (β₁ := β) (β₂ := β₁) f₂ hf₂ g) : (a : ι) → β₂ a) i

Tactic:
simp only [mapRange_apply]

Premises used: DFinsupp.mapRange_apply
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
f₂ : (i : ι) → β i → β₁ i
hf : ∀ (i : ι), f i 0 = 0
hf₂ : ∀ (i : ι), f₂ i 0 = 0
h : ∀ (i : ι), (f i ∘ f₂ i) 0 = 0
g : Π₀ (i : ι), β i
i : ι
⊢ (f i ∘ f₂ i) ((g : (a : ι) → β a) i) = f i (f₂ i ((g : (a : ι) → β a) i))

Tactic:
rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β₁ i)
inst_1 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
h : ∀ (i : ι), (mapRange (β₁ := β₁) (β₂ := β₂) f hf 0 : (a : ι) → β₂ a) i = (0 : (a : ι) → β₂ a) i
⊢ mapRange (β₁ := β₁) (β₂ := β₂) f hf 0 = 0

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β₁ i)
inst_1 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
i : ι
⊢ (mapRange (β₁ := β₁) (β₂ := β₂) f hf 0 : (a : ι) → β₂ a) i = (0 : (a : ι) → β₂ a) i

Tactic:
simp only [mapRange_apply, coe_zero, Pi.zero_apply, hf]

Premises used: Pi.zero_apply, DFinsupp.mapRange_apply, DFinsupp.coe_zero
-- 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)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
refine :
  (xs : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x.toFun (β := fun (i : ι) ↦ β₁ i) i = 0 }) →
    Trunc
      { s : Multiset ι //
        ∀ (i : ι),
          i ∈ s ∨ Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0 }
⊢ Trunc
    { s : Multiset ι //
      ∀ (i : ι),
        i ∈ s ∨ Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0 }

Tactic:
refine x.support'.bind fun xs => ?_

Premises used: Trunc.bind, DFinsupp.support'
-- 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)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
xs : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x.toFun (β := fun (i : ι) ↦ β₁ i) i = 0 }
refine :
  (ys : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ y.toFun (β := fun (i : ι) ↦ β₂ i) i = 0 }) →
    { s : Multiset ι //
      ∀ (i : ι),
        i ∈ s ∨ Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0 }
⊢ Trunc
    { s : Multiset ι //
      ∀ (i : ι),
        i ∈ s ∨ Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0 }

Tactic:
refine y.support'.map fun ys => ?_

Premises used: Trunc.map, DFinsupp.support'
-- 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)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
xs : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x.toFun (β := fun (i : ι) ↦ β₁ i) i = 0 }
ys : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ y.toFun (β := fun (i : ι) ↦ β₂ i) i = 0 }
refine :
  ∀ (i : ι),
    i ∈ (↑xs : Multiset ι) + (↑ys : Multiset ι) ∨
      Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0
⊢ { s : Multiset ι //
    ∀ (i : ι),
      i ∈ s ∨ Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0 }

Tactic:
refine ⟨xs + ys, fun i => ?_⟩
-- 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)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
xs : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x.toFun (β := fun (i : ι) ↦ β₁ i) i = 0 }
ys : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ y.toFun (β := fun (i : ι) ↦ β₂ i) i = 0 }
i : ι
inl :
  ∀ (h1 : i ∈ (↑xs : Multiset ι)),
    i ∈ (↑xs : Multiset ι) + (↑ys : Multiset ι) ∨
      Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0
inr :
  ∀ (h1 : (x : (a : ι) → β₁ a) i = 0),
    i ∈ (↑xs : Multiset ι) + (↑ys : Multiset ι) ∨
      Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0
⊢ i ∈ (↑xs : Multiset ι) + (↑ys : Multiset ι) ∨
    Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0

Tactic:
obtain h1 | (h1 : x i = 0) := xs.prop i

Premises used: Subtype.prop, DFunLike.coe
-- 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)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
xs : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x.toFun (β := fun (i : ι) ↦ β₁ i) i = 0 }
ys : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ y.toFun (β := fun (i : ι) ↦ β₂ i) i = 0 }
i : ι
h1 : i ∈ (↑xs : Multiset ι)
⊢ i ∈ (↑xs : Multiset ι) + (↑ys : Multiset ι) ∨
    Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0

Tactic:
grind
-- 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)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
xs : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x.toFun (β := fun (i : ι) ↦ β₁ i) i = 0 }
ys : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ y.toFun (β := fun (i : ι) ↦ β₂ i) i = 0 }
i : ι
h1 : (x : (a : ι) → β₁ a) i = 0
inr :
  ∀ (h2 : i ∈ (↑ys : Multiset ι)),
    i ∈ (↑xs : Multiset ι) + (↑ys : Multiset ι) ∨
      Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0
inr₁ :
  ∀ (h2 : (y : (a : ι) → β₂ a) i = 0),
    i ∈ (↑xs : Multiset ι) + (↑ys : Multiset ι) ∨
      Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0
⊢ i ∈ (↑xs : Multiset ι) + (↑ys : Multiset ι) ∨
    Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0

Tactic:
obtain h2 | (h2 : y i = 0) := ys.prop i

Premises used: Subtype.prop, DFunLike.coe
-- 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)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
xs : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x.toFun (β := fun (i : ι) ↦ β₁ i) i = 0 }
ys : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ y.toFun (β := fun (i : ι) ↦ β₂ i) i = 0 }
i : ι
h1 : (x : (a : ι) → β₁ a) i = 0
h2 : i ∈ (↑ys : Multiset ι)
⊢ i ∈ (↑xs : Multiset ι) + (↑ys : Multiset ι) ∨
    Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0

Tactic:
grind
-- 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)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
xs : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x.toFun (β := fun (i : ι) ↦ β₁ i) i = 0 }
ys : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ y.toFun (β := fun (i : ι) ↦ β₂ i) i = 0 }
i : ι
h1 : (x : (a : ι) → β₁ a) i = 0
h2 : (y : (a : ι) → β₂ a) i = 0
⊢ i ∈ (↑xs : Multiset ι) + (↑ys : Multiset ι) ∨
    Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0

Tactic:
grind
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
g₁ : Π₀ (i : ι), β₁ i
g₂ : Π₀ (i : ι), β₂ i
i : ι
⊢ (zipWith (β := β) (β₁ := β₁) (β₂ := β₂) f hf g₁ g₂ : (a : ι) → β a) i =
    f i ((g₁ : (a : ι) → β₁ a) i) ((g₂ : (a : ι) → β₂ a) i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
x y : Π₀ (i : ι), β i
s : Set ι
inst_1 : (i : ι) → Decidable (i ∈ s)
i : ι
⊢ (x.piecewise (β := β) y s : (a : ι) → β a) i = if i ∈ s then (x : (a : ι) → β a) i else (y : (a : ι) → β a) i

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
x y : Π₀ (i : ι), β i
s : Set ι
inst_1 : (i : ι) → Decidable (i ∈ s)
⊢ (⇑(x.piecewise (β := β) y s) : (a : ι) → β a) = s.piecewise (β := β) (⇑x : (a : ι) → β a) (⇑y : (a : ι) → β a)

Tactic:
rfl

Premises used: Set.piecewise, rfl, ite
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → AddZeroClass (β i)
g₁ g₂ : Π₀ (i : ι), β i
i : ι
⊢ (g₁ + g₂ : (a : ι) → β a) i = (g₁ : (a : ι) → β a) i + (g₂ : (a : ι) → β a) i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → AddZeroClass (β i)
g₁ g₂ : Π₀ (i : ι), β i
⊢ (⇑(g₁ + g₂) : (a : ι) → β a) = (⇑g₁ : (a : ι) → β a) + (⇑g₂ : (a : ι) → β a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → AddMonoid (β i)
b : ℕ
v : Π₀ (i : ι), β i
i : ι
⊢ (b • v : (a : ι) → β a) i = b • (v : (a : ι) → β a) i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → AddMonoid (β i)
b : ℕ
v : Π₀ (i : ι), β i
⊢ (⇑(b • v) : (a : ι) → β a) = b • (⇑v : (a : ι) → β a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → AddZeroClass (β i)
v : Π₀ (i : ι), β i
⊢ (coeFnAddMonoidHom (β := β) : (a : Π₀ (i : ι), β i) → (i : ι) → β i) v = (⇑v : (a : ι) → β a)

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → AddGroup (β i)
g₁ g₂ : Π₀ (i : ι), β i
⊢ (⇑(g₁ - g₂) : (a : ι) → β a) = (⇑g₁ : (a : ι) → β a) - (⇑g₂ : (a : ι) → β a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → AddGroup (β i)
b : ℤ
v : Π₀ (i : ι), β i
i : ι
⊢ (b • v : (a : ι) → β a) i = b • (v : (a : ι) → β a) i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → AddGroup (β i)
b : ℤ
v : Π₀ (i : ι), β i
⊢ (⇑(b • v) : (a : ι) → β a) = b • (⇑v : (a : ι) → β a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
p : ι → Prop
inst_1 : DecidablePred p
x : Π₀ (i : ι), β i
xs : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x.toFun (β := fun (i : ι) ↦ β i) i = 0 }
i : ι
H : (x : (a : ι) → β a) i = 0
⊢ Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ if p i then (x : (a : ι) → β a) i else 0) i) 0

Tactic:
simp only [H, ite_self]

Premises used: ite_self
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
p : ι → Prop
inst_1 : DecidablePred p
i : ι
f : Π₀ (i : ι), β i
⊢ (filter (β := β) p f : (a : ι) → β a) i = if p i then (f : (a : ι) → β a) i else 0

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
p : ι → Prop
inst_1 : DecidablePred p
f : Π₀ (i : ι), β i
i : ι
h : p i
⊢ (filter (β := β) p f : (a : ι) → β a) i = (f : (a : ι) → β a) i

Tactic:
grind
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
p : ι → Prop
inst_1 : DecidablePred p
f : Π₀ (i : ι), β i
i : ι
h : ¬p i
⊢ (filter (β := β) p f : (a : ι) → β a) i = 0

Tactic:
grind
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
p : ι → Prop
inst_1 : DecidablePred p
i : ι
simp : ((if p i then (f : (a : ι) → β a) i else 0) + if ¬p i then (f : (a : ι) → β a) i else 0) = (f : (a : ι) → β a) i
⊢ (filter (β := β) p f + filter (β := β) (fun (i : ι) ↦ ¬p i) f : (a : ι) → β a) i = (f : (a : ι) → β a) i

Tactic:
simp only [add_apply, filter_apply]

Premises used: DFinsupp.filter_apply, DFinsupp.add_apply
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
p : ι → Prop
inst_1 : DecidablePred p
i : ι
pos : p i → (f : (a : ι) → β a) i + 0 = (f : (a : ι) → β a) i
neg : ¬p i → 0 + (f : (a : ι) → β a) i = (f : (a : ι) → β a) i
⊢ ((if p i then (f : (a : ι) → β a) i else 0) + if ¬p i then (f : (a : ι) → β a) i else 0) = (f : (a : ι) → β a) i

Tactic:
split_ifs
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
p : ι → Prop
inst_1 : DecidablePred p
i : ι
h : p i
⊢ (f : (a : ι) → β a) i + 0 = (f : (a : ι) → β a) i

Tactic:
simp only [add_zero, zero_add]

Premises used: zero_add, add_zero
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
p : ι → Prop
inst_1 : DecidablePred p
i : ι
h : ¬p i
⊢ 0 + (f : (a : ι) → β a) i = (f : (a : ι) → β a) i

Tactic:
simp only [add_zero, zero_add]

Premises used: zero_add, add_zero
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ (i : ι), (filter (β := β) p 0 : (a : ι) → β a) i = (0 : (a : ι) → β a) i
⊢ Eq (α := Π₀ (i : ι), β i) (filter (β := β) p 0) 0

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
p : ι → Prop
inst_1 : DecidablePred p
i : ι
⊢ (filter (β := β) p 0 : (a : ι) → β a) i = (0 : (a : ι) → β a) i

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → AddZeroClass (β i)
p : ι → Prop
inst_1 : DecidablePred p
f g : Π₀ (i : ι), β i
h :
  ∀ (i : ι),
    (filter (β := β) p (f + g) : (a : ι) → β a) i = (filter (β := β) p f + filter (β := β) p g : (a : ι) → β a) i
⊢ filter (β := β) p (f + g) = filter (β := β) p f + filter (β := β) p g

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → AddZeroClass (β i)
p : ι → Prop
inst_1 : DecidablePred p
f g : Π₀ (i : ι), β i
i : ι
⊢ (filter (β := β) p (f + g) : (a : ι) → β a) i = (filter (β := β) p f + filter (β := β) p g : (a : ι) → β a) i

Tactic:
simp [ite_add_zero]

Premises used: ite_add_zero
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → AddGroup (β i)
p : ι → Prop
inst_1 : DecidablePred p
f : Π₀ (i : ι), β i
⊢ filter (β := β) p (-f) = -filter (β := β) p f

Tactic:
(filterAddMonoidHom β p).map_neg f

Premises used: AddMonoidHom.map_neg, DFinsupp.filter, DFinsupp.filterAddMonoidHom
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → AddGroup (β i)
p : ι → Prop
inst_1 : DecidablePred p
f g : Π₀ (i : ι), β i
⊢ filter (β := β) p (f - g) = filter (β := β) p f - filter (β := β) p g

Tactic:
(filterAddMonoidHom β p).map_sub f g

Premises used: DFinsupp.filter, AddMonoidHom.map_sub, DFinsupp.filterAddMonoidHom
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
p : ι → Prop
inst_1 : DecidablePred p
⊢ Eq (α := Π₀ (i : Subtype p), β (↑i : ι)) (subtypeDomain (β := β) p 0) 0

Tactic:
rfl

Premises used: Multiset.map, List.map, Trunc.map, Trunc.bind, Multiset.zero, Trunc.mk, DFinsupp.subtypeDomain, Multiset.ofList, Trunc.liftOn, rfl, Multiset.filter
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
p : ι → Prop
inst_1 : DecidablePred p
i : Subtype p
v : Π₀ (i : ι), β i
⊢ (subtypeDomain (β := β) p v : (a : Subtype p) → β (↑a : ι)) i = (v : (a : ι) → β a) (↑i : ι)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → AddZeroClass (β i)
p : ι → Prop
inst_1 : DecidablePred p
v v' : Π₀ (i : ι), β i
⊢ subtypeDomain (β := β) p (v + v') = subtypeDomain (β := β) p v + subtypeDomain (β := β) p v'

Tactic:
DFunLike.coe_injective rfl

Premises used: DFunLike.coe_injective, rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → AddGroup (β i)
p : ι → Prop
inst_1 : DecidablePred p
v : Π₀ (i : ι), β i
⊢ subtypeDomain (β := β) p (-v) = -subtypeDomain (β := β) p v

Tactic:
DFunLike.coe_injective rfl

Premises used: DFunLike.coe_injective, rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → AddGroup (β i)
p : ι → Prop
inst_1 : DecidablePred p
v v' : Π₀ (i : ι), β i
⊢ subtypeDomain (β := β) p (v - v') = subtypeDomain (β := β) p v - subtypeDomain (β := β) p v'

Tactic:
DFunLike.coe_injective rfl

Premises used: DFunLike.coe_injective, rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
f : Π₀ (i : ι), β i
⊢ Set.Finite.{u} (α := ι) {i : ι | (f : (a : ι) → β a) i ≠ 0}

Tactic:
Trunc.induction_on f.support' fun xs ↦
    xs.1.finite_toSet.subset fun i H ↦ ((xs.prop i).resolve_right H)

Premises used: Trunc.induction_on, DFinsupp.support'
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
s : Finset ι
x : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
⊢ (mk (β := β) s x : (a : ι) → β a) i =
    if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0

Tactic:
rfl

Premises used: dite, rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
s : Finset ι
x : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
hi : i ∈ s
⊢ (mk (β := β) s x : (a : ι) → β a) i = x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi)

Tactic:
dif_pos hi

Premises used: dif_pos, dite
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
s : Finset ι
x : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
hi : i ∉ s
⊢ (mk (β := β) s x : (a : ι) → β a) i = 0

Tactic:
dif_neg hi

Premises used: dif_neg, dite
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
H : Eq (α := Π₀ (i : ι), β i) (mk (β := β) s x) (mk (β := β) s y)
h : ∀ (i : (↑(↑s : Set ι) : Type u)), x i = y i
⊢ x = y

Tactic:
ext i
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
H : Eq (α := Π₀ (i : ι), β i) (mk (β := β) s x) (mk (β := β) s y)
i : (↑(↑s : Set ι) : Type u)
⊢ Eq (α := β (↑i : ι)) ((mk (β := β) s x : (a : ι) → β a) (↑i : ι)) ((mk (β := β) s y : (a : ι) → β a) (↑i : ι))

Tactic:
grind