awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst : Zero M
a : α
f : α →₀ M
a' : α
⊢ a' ∈ f.support.erase a ↔ Ne.{u_5 + 1} (α := M) (if a' = a then 0 else (f : (a : α) → M) a' : M) (0 : M)

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst : Zero M
a : α
f : α →₀ M
a' : α
⊢ a' ∈ f.support.erase a ↔ Ne.{u_5 + 1} (α := M) (if a' = a then 0 else (f : (a : α) → M) a' : M) (0 : M)

Tactic:
classical
    grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
a a' : α
f : α →₀ M
rw :
  Eq.{u_5 + 1} (α := M) (if a' = a then 0 else (f : (a : α) → M) a' : M)
    (if a' = a then 0 else (f : (a : α) → M) a' : M)
⊢ Eq.{u_5 + 1} (α := M) ((erase a f : (a : α) → M) a' : M) (if a' = a then 0 else (f : (a : α) → M) a' : M)

Tactic:
rw [erase, coe_mk]

Premises used: Finsupp.erase, Finsupp.coe_mk
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
a a' : α
f : α →₀ M
⊢ Eq.{u_5 + 1} (α := M) (if a' = a then 0 else (f : (a : α) → M) a' : M)
    (if a' = a then 0 else (f : (a : α) → M) a' : M)

Tactic:
simp only [ite_eq_ite]

Premises used: ite_eq_ite
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
a : α
f : α →₀ M
⊢ (erase a f).support = f.support.erase a

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
a : α
f : α →₀ M
⊢ (erase a f).support = f.support.erase a

Tactic:
classical
  grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
f : α →₀ M
⊢ Eq.{u_5 + 1} (α := M) ((erase a f : (a : α) → M) a : M) (0 : M)

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
f : α →₀ M
⊢ Eq.{u_5 + 1} (α := M) ((erase a f : (a : α) → M) a : M) (0 : M)

Tactic:
classical grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a a' : α
f : α →₀ M
h : a' ≠ a
⊢ Eq.{u_5 + 1} (α := M) ((erase a f : (a : α) → M) a' : M) ((f : (a : α) → M) a' : M)

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a a' : α
f : α →₀ M
h : a' ≠ a
⊢ Eq.{u_5 + 1} (α := M) ((erase a f : (a : α) → M) a' : M) ((f : (a : α) → M) a' : M)

Tactic:
classical grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
b : M
⊢ Eq (α := α →₀ M) (erase a (single a b)) 0

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
b : M
⊢ Eq (α := α →₀ M) (erase a (single a b)) 0

Tactic:
classical grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a a' : α
b : M
h : a ≠ a'
⊢ Eq (α := α →₀ M) (erase a (single a' b)) (single a' b)

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a a' : α
b : M
h : a ≠ a'
⊢ Eq (α := α →₀ M) (erase a (single a' b)) (single a' b)

Tactic:
classical grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a : α
haf : a ∉ f.support
⊢ erase a f = f

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a : α
haf : a ∉ f.support
⊢ erase a f = f

Tactic:
classical grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
⊢ Eq (α := α →₀ M) (erase a 0) 0

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a : α
⊢ erase a f = f.update a 0

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a : α
⊢ erase a f = f.update a 0

Tactic:
classical grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a a' : α
ha : a ≠ a'
b : M
⊢ erase a (f.update a' b) = (erase a f).update a' b

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a a' : α
ha : a ≠ a'
b : M
⊢ erase a (f.update a' b) = (erase a f).update a' b

Tactic:
classical grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a : α
⊢ erase a (erase a f) = erase a f

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a : α
⊢ erase a (erase a f) = erase a f

Tactic:
classical grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a : α
b : M
⊢ (erase a f).update a b = f.update a b

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a : α
b : M
⊢ (erase a f).update a b = f.update a b

Tactic:
classical grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a : α
b : M
⊢ erase a (f.update a b) = erase a f

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a : α
b : M
⊢ erase a (f.update a b) = erase a f

Tactic:
classical grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
N : Type u_7
inst : Zero M
inst_1 : Zero N
f : M → N
hf : f 0 = 0
a : α
b : M
⊢ mapRange f hf (single a b) = single a (f b)

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
N : Type u_7
inst : Zero M
inst_1 : Zero N
f : M → N
hf : f 0 = 0
a : α
b : M
⊢ mapRange f hf (single a b) = single a (f b)

Tactic:
classical grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
rw : (embDomain f l).support = {a}
rw₁ : support (single a b) = {a}
rw₂ rw₃ : Eq (α := Finset β) {a} {a}
⊢ map f l.support = {a}

Tactic:
rw [← support_embDomain, h, support_single _ hb]

Premises used: Finsupp.support_single, Finsupp.support_embDomain
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
⊢ map f l.support = {a}

Tactic:
have h_map_support : Finset.map f l.support = {a} := by
      rw [← support_embDomain, h, support_single _ hb]
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
⊢ a ∈ map f l.support

Tactic:
simp only [h_map_support, Finset.mem_singleton]

Premises used: Finset.mem_singleton
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
⊢ a ∈ map f l.support

Tactic:
have ha : a ∈ Finset.map f l.support := by simp only [h_map_support, Finset.mem_singleton]
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
rcases :
  ∀ (c : α) (_hc₁ : c ∈ l.support) (hc₂ : (f : (a : α) → β) c = a), ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
⊢ ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a

Tactic:
rcases Finset.mem_map.1 ha with ⟨c, _hc₁, hc₂⟩

Premises used: Iff.mp, Finset.mem_map
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : (f : (a : α) → β) c = a
h₁ : l = single c b ∧ (f : (a : α) → β) c = a
⊢ ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a

Tactic:
use c
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : (f : (a : α) → β) c = a
h₁ : l = single c b
h₂ : (f : (a : α) → β) c = a
⊢ l = single c b ∧ (f : (a : α) → β) c = a

Tactic:
constructor
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : (f : (a : α) → β) c = a
h₁ : ∀ (d : α), Eq.{u_5 + 1} (α := M) ((l : (a : α) → M) d : M) ((single c b : (a : α) → M) d : M)
⊢ l = single c b

Tactic:
ext d
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : (f : (a : α) → β) c = a
d : α
h₁ : Eq.{u_5 + 1} (α := M) ((single a b : (a : β) → M) ((f : (a : α) → β) d : β) : M) ((single c b : (a : α) → M) d : M)
⊢ Eq.{u_5 + 1} (α := M) ((l : (a : α) → M) d : M) ((single c b : (a : α) → M) d : M)

Tactic:
rw [← embDomain_apply_self f l, h]

Premises used: Finsupp.embDomain_apply_self
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : (f : (a : α) → β) c = a
d : α
⊢ Eq.{u_5 + 1} (α := M) ((single a b : (a : β) → M) ((f : (a : α) → β) d : β) : M) ((single c b : (a : α) → M) d : M)

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : (f : (a : α) → β) c = a
⊢ (f : (a : α) → β) c = a

Tactic:
hc₂
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : (f : (a : α) → β) c = a
⊢ (f : (a : α) → β) c = a

Tactic:
exact hc₂
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
have : map f l.support = {a}
have₁ : ∀ (h_map_support : map f l.support = {a}), ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
have₂ : map f l.support = {a}
have₃ have₄ : ∀ (h_map_support : map f l.support = {a}), ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
have₅ :
  ∀ (h_map_support : map f l.support = {a}) (ha : a ∈ map f l.support),
    ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
have₆ :
  ∀ (h_map_support : map f l.support = {a}) (ha : a ∈ map f l.support) (c : α) (_hc₁ : c ∈ l.support)
    (hc₂ : (f : (a : α) → β) c = a), ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
h₁ :
  ∀ (h_map_support : map f l.support = {a}) (ha : a ∈ map f l.support) (c : α) (_hc₁ : c ∈ l.support)
    (hc₂ : (f : (a : α) → β) c = a), l = single c b ∧ (f : (a : α) → β) c = a
h₂ :
  ∀ (h_map_support : map f l.support = {a}) (ha : a ∈ map f l.support) (c : α) (_hc₁ : c ∈ l.support)
    (hc₂ : (f : (a : α) → β) c = a), l = single c b
h₃ h₄ :
  ∀ (h_map_support : map f l.support = {a}) (ha : a ∈ map f l.support) (c : α) (_hc₁ : c ∈ l.support)
    (hc₂ : (f : (a : α) → β) c = a), (f : (a : α) → β) c = a
⊢ ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a

Tactic:
classical
    have h_map_support : Finset.map f l.support = {a} := by
      rw [← support_embDomain, h, support_single _ hb]
    have ha : a ∈ Finset.map f l.support := by simp only [h_map_support, Finset.mem_singleton]
    rcases Finset.mem_map.1 ha with ⟨c, _hc₁, hc₂⟩
    use c
    constructor
    · ext d
      rw [← embDomain_apply_self f l, h]
      grind
    · exact hc₂

Premises used: Finsupp.embDomain_apply_self
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ↪ β
a : α
m : M
h :
  ∀ (b : β),
    Eq.{u_5 + 1} (α := M) ((embDomain f (single a m) : (a : β) → M) b : M)
      (((single ((f : (a : α) → β) a) m : β →₀ M) : (a : β) → M) b : M)
⊢ Eq (α := β →₀ M) (embDomain f (single a m)) (single ((f : (a : α) → β) a) m)

Tactic:
ext b
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ↪ β
a : α
m : M
b : β
pos :
  ∀ (h : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b),
    Eq.{u_5 + 1} (α := M) ((embDomain f (single a m) : (a : β) → M) b : M)
      (((single ((f : (a : α) → β) a) m : β →₀ M) : (a : β) → M) b : M)
neg :
  ∀ (h : b ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)),
    Eq.{u_5 + 1} (α := M) ((embDomain f (single a m) : (a : β) → M) b : M)
      (((single ((f : (a : α) → β) a) m : β →₀ M) : (a : β) → M) b : M)
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f (single a m) : (a : β) → M) b : M)
    (((single ((f : (a : α) → β) a) m : β →₀ M) : (a : β) → M) b : M)

Tactic:
by_cases h : b ∈ Set.range f

Premises used: Set.range, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ↪ β
a : α
m : M
b : β
h : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f (single a m) : (a : β) → M) b : M)
    (((single ((f : (a : α) → β) a) m : β →₀ M) : (a : β) → M) b : M)

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ↪ β
a : α
m : M
b : β
h : b ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f (single a m) : (a : β) → M) b : M)
    (((single ((f : (a : α) → β) a) m : β →₀ M) : (a : β) → M) b : M)

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ↪ β
a : α
m : M
h :
  ∀ (b : β),
    Eq.{u_5 + 1} (α := M) ((embDomain f (single a m) : (a : β) → M) b : M)
      (((single ((f : (a : α) → β) a) m : β →₀ M) : (a : β) → M) b : M)
⊢ Eq (α := β →₀ M) (embDomain f (single a m)) (single ((f : (a : α) → β) a) m)

Tactic:
classical
    ext b
    by_cases h : b ∈ Set.range f <;> grind

Premises used: Set.range, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
N : Type u_7
P : Type u_8
inst : Zero M
inst_1 : Zero N
inst_2 : Zero P
f : M → N → P
hf : f 0 0 = 0
a : α
m : M
n : N
⊢ zipWith f hf (single a m) (single a n) = single a (f m n)

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
N : Type u_7
P : Type u_8
inst : Zero M
inst_1 : Zero N
inst_2 : Zero P
f : M → N → P
hf : f 0 0 = 0
a : α
m : M
n : N
⊢ zipWith f hf (single a m) (single a n) = single a (f m n)

Tactic:
classical
  grind
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
M : Type u_3
inst : Zero M
f : ι →₀ M
⊢ (⇑f.toDFinsupp : (a : ι) → M) = (⇑f : (a : ι) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : Zero M
i : ι
m : M
h :
  ∀ (i_1 : ι),
    (toDFinsupp (single i m) : (a : ι) → M) i_1 = (DFinsupp.single (β := fun (i : ι) ↦ M) i m : (a : ι) → M) i_1
⊢ Eq (α := Π₀ (x : ι), M) (toDFinsupp (single i m)) (DFinsupp.single (β := fun (i : ι) ↦ M) i m)

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : Zero M
i : ι
m : M
i_1 : ι
⊢ (toDFinsupp (single i m) : (a : ι) → M) i_1 = (DFinsupp.single (β := fun (i : ι) ↦ M) i m : (a : ι) → M) i_1

Tactic:
simp [Finsupp.single_apply, DFinsupp.single_apply]

Premises used: Finsupp.single_apply, DFinsupp.single_apply
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : Zero M
inst_2 : (m : M) → Decidable (m ≠ 0)
f : ι →₀ M
h : ∀ (a : ι), a ∈ f.toDFinsupp.support (β := fun (x : ι) ↦ M) ↔ a ∈ f.support
⊢ f.toDFinsupp.support (β := fun (x : ι) ↦ M) = f.support

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : Zero M
inst_2 : (m : M) → Decidable (m ≠ 0)
f : ι →₀ M
a : ι
⊢ a ∈ f.toDFinsupp.support (β := fun (x : ι) ↦ M) ↔ a ∈ f.support

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : DecidableEq ι
inst_1 : Zero M
inst_2 : (m : M) → Decidable (m ≠ 0)
f : Π₀ (x : ι), M
i : ι
⊢ i ∈ f.support (β := fun (x : ι) ↦ M) ↔ (f : (a : ι) → M) i ≠ 0

Tactic:
simp only [DFinsupp.mem_support_iff]

Premises used: DFinsupp.mem_support_iff
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : Zero M
inst_2 : (m : M) → Decidable (m ≠ 0)
f : Π₀ (x : ι), M
⊢ (⇑f.toFinsupp : (a : ι) → M) = (⇑f : (a : ι) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : Zero M
inst_2 : (m : M) → Decidable (m ≠ 0)
f : Π₀ (x : ι), M
h : ∀ (a : ι), a ∈ f.toFinsupp.support ↔ a ∈ f.support (β := fun (x : ι) ↦ M)
⊢ f.toFinsupp.support = f.support (β := fun (x : ι) ↦ M)

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : Zero M
inst_2 : (m : M) → Decidable (m ≠ 0)
f : Π₀ (x : ι), M
a : ι
⊢ a ∈ f.toFinsupp.support ↔ a ∈ f.support (β := fun (x : ι) ↦ M)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : Zero M
inst_2 : (m : M) → Decidable (m ≠ 0)
i : ι
m : M
h :
  ∀ (a : ι),
    Eq.{u_3 + 1} (α := M) ((toFinsupp (single (β := fun (x : ι) ↦ M) i m) : (a : ι) → M) a : M)
      ((Finsupp.single i m : (a : ι) → M) a : M)
⊢ Eq (α := ι →₀ M) (toFinsupp (single (β := fun (x : ι) ↦ M) i m)) (Finsupp.single i m)

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : Zero M
inst_2 : (m : M) → Decidable (m ≠ 0)
i : ι
m : M
a : ι
⊢ Eq.{u_3 + 1} (α := M) ((toFinsupp (single (β := fun (x : ι) ↦ M) i m) : (a : ι) → M) a : M)
    ((Finsupp.single i m : (a : ι) → M) a : M)

Tactic:
simp [Finsupp.single_apply, DFinsupp.single_apply]

Premises used: Finsupp.single_apply, DFinsupp.single_apply
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : Zero M
inst_2 : (m : M) → Decidable (m ≠ 0)
f : ι →₀ M
⊢ f.toDFinsupp.toFinsupp = f

Tactic:
DFunLike.coe_injective rfl

Premises used: DFunLike.coe_injective, rfl
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : Zero M
inst_2 : (m : M) → Decidable (m ≠ 0)
f : Π₀ (x : ι), M
⊢ f.toFinsupp.toDFinsupp = f

Tactic:
DFunLike.coe_injective rfl

Premises used: DFunLike.coe_injective, rfl
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
M : Type u_3
inst : Zero M
⊢ Eq (α := Π₀ (x : ι), M) (toDFinsupp 0) 0

Tactic:
DFunLike.coe_injective rfl

Premises used: DFunLike.coe_injective, rfl
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
f g : ι →₀ M
⊢ (f + g).toDFinsupp = f.toDFinsupp + g.toDFinsupp

Tactic:
DFunLike.coe_injective rfl

Premises used: DFunLike.coe_injective, rfl
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddGroup M
f : ι →₀ M
⊢ (-f).toDFinsupp = -f.toDFinsupp

Tactic:
DFunLike.coe_injective rfl

Premises used: DFunLike.coe_injective, rfl
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddGroup M
f g : ι →₀ M
⊢ (f - g).toDFinsupp = f.toDFinsupp - g.toDFinsupp

Tactic:
DFunLike.coe_injective rfl

Premises used: DFunLike.coe_injective, rfl
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
r : R
f : ι →₀ M
⊢ (r • f).toDFinsupp = r • f.toDFinsupp

Tactic:
DFunLike.coe_injective rfl

Premises used: DFunLike.coe_injective, rfl
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : Zero M
inst_2 : (m : M) → Decidable (m ≠ 0)
⊢ Eq (α := ι →₀ M) (toFinsupp 0) 0

Tactic:
DFunLike.coe_injective rfl

Premises used: DFunLike.coe_injective, rfl
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddZeroClass M
inst_2 : (m : M) → Decidable (m ≠ 0)
f g : Π₀ (x : ι), M
⊢ (f + g).toFinsupp = f.toFinsupp + g.toFinsupp

Tactic:
DFunLike.coe_injective <| DFinsupp.coe_add _ _

Premises used: DFinsupp.coe_add, DFunLike.coe_injective
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddGroup M
inst_2 : (m : M) → Decidable (m ≠ 0)
f : Π₀ (x : ι), M
⊢ (-f).toFinsupp = -f.toFinsupp

Tactic:
DFunLike.coe_injective <| DFinsupp.coe_neg _

Premises used: DFinsupp.coe_neg, DFunLike.coe_injective
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddGroup M
inst_2 : (m : M) → Decidable (m ≠ 0)
f g : Π₀ (x : ι), M
⊢ (f - g).toFinsupp = f.toFinsupp - g.toFinsupp

Tactic:
DFunLike.coe_injective <| DFinsupp.coe_sub _ _

Premises used: DFunLike.coe_injective, DFinsupp.coe_sub
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : DecidableEq ι
inst_1 : Monoid R
inst_2 : AddMonoid M
inst_3 : DistribMulAction R M
inst_4 : (m : M) → Decidable (m ≠ 0)
r : R
f : Π₀ (x : ι), M
⊢ (r • f).toFinsupp = r • f.toFinsupp

Tactic:
DFunLike.coe_injective <| DFinsupp.coe_smul _ _

Premises used: DFinsupp.coe_smul, DFunLike.coe_injective
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : (m : M) → Decidable (m ≠ 0)
inst_4 : Module R M
⊢ Eq (α := (a : ι →₀ M) → Π₀ (x : ι), M) (⇑(finsuppLequivDFinsupp R) : (a : ι →₀ M) → Π₀ (x : ι), M) Finsupp.toDFinsupp

Tactic:
rfl

Premises used: Finsupp.toDFinsupp, rfl
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : (m : M) → Decidable (m ≠ 0)
inst_4 : Module R M
⊢ Eq (α := (f : Π₀ (x : ι), M) → ι →₀ M) (⇑(LinearEquiv.symm (finsuppLequivDFinsupp R)) : (a : Π₀ (x : ι), M) → ι →₀ M)
    DFinsupp.toFinsupp

Tactic:
rfl

Premises used: DFinsupp.toFinsupp, rfl
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Zero N
f : (i : ι) × η i →₀ N
i : ι
rw : f.split (αs := η) i ≠ 0 ∨ f.split (αs := η) i = 0
⊢ i ∈ f.splitSupport (αs := η).val ∨ f.split (αs := η) i = 0

Tactic:
rw [← Finset.mem_def, mem_splitSupport_iff_nonzero]

Premises used: Finsupp.mem_splitSupport_iff_nonzero, Finset.mem_def
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Zero N
f : (i : ι) × η i →₀ N
i : ι
⊢ f.split (αs := η) i ≠ 0 ∨ f.split (αs := η) i = 0

Tactic:
(em _).symm

Premises used: em, Or.symm
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Zero N
f : (i : ι) × η i →₀ N
i : ι
⊢ f.split (αs := η) i ≠ 0 ∨ f.split (αs := η) i = 0

Tactic:
exact (em _).symm

Premises used: em, Or.symm
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Zero N
f : Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N
haveI : (this : DecidableEq ι) → (i : ι) × η i →₀ N
⊢ (i : ι) × η i →₀ N

Tactic:
haveI := Classical.decEq ι