awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a : α
h : f.support ⊆ {a}
x : α
hx : ¬x = a
⊢ Eq.{u_5 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)

Tactic:
exact notMem_support_iff.1 (mt (fun hx => (mem_singleton.1 (h hx))) hx)

Premises used: Finset.mem_singleton, Finsupp.notMem_support_iff, mt, Iff.mp
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a₁ a₂ : α
b₁ b₂ : M
mp : Eq (α := α →₀ M) (single a₁ b₁) (single a₂ b₂) → a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
mpr : a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0 → Eq (α := α →₀ M) (single a₁ b₁) (single a₂ b₂)
⊢ Eq (α := α →₀ M) (single a₁ b₁) (single a₂ b₂) ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Tactic:
constructor
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : Eq (α := α →₀ M) (single a₁ b₁) (single a₂ b₂)
pos : ∀ (h : a₁ = a₂), a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
neg : ∀ (h : ¬a₁ = a₂), a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Tactic:
by_cases h : a₁ = a₂
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : Eq (α := α →₀ M) (single a₁ b₁) (single a₂ b₂)
h : a₁ = a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Tactic:
Or.inl ⟨h, ?_⟩

Premises used: And.intro, Or.inl
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : Eq (α := α →₀ M) (single a₁ b₁) (single a₂ b₂)
h : a₁ = a₂
pos : b₁ = b₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Tactic:
refine Or.inl ⟨h, ?_⟩

Premises used: Or.inl
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : Eq (α := α →₀ M) (single a₁ b₁) (single a₂ b₂)
h : a₁ = a₂
pos : ∀ (eq : Eq (α := α →₀ M) (single a₂ b₁) (single a₂ b₂)) (h : a₁ = a₂), b₁ = b₂
pos₁ pos₂ pos₃ pos₄ : ∀ (eq : b₁ = b₂) (h : a₁ = a₂), b₁ = b₂
⊢ b₁ = b₂

Tactic:
rwa [h, (single_injective a₂).eq_iff] at eq

Premises used: Finsupp.single_injective, Function.Injective.eq_iff
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : Eq (α := α →₀ M) (single a₁ b₁) (single a₂ b₂)
h : ¬a₁ = a₂
⊢ ∀ (x : α), Eq.{u_5 + 1} (α := M) ((single a₁ b₁ : (a : α) → M) x : M) ((single a₂ b₂ : (a : α) → M) x : M)

Tactic:
rw [DFunLike.ext_iff] at eq

Premises used: DFunLike.ext_iff
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : Eq (α := α →₀ M) (single a₁ b₁) (single a₂ b₂)
h : ¬a₁ = a₂
eq₁ : ∀ (x : α), Eq.{u_5 + 1} (α := M) ((single a₁ b₁ : (a : α) → M) x : M) ((single a₂ b₂ : (a : α) → M) x : M)
⊢ ¬a₁ = a₂

Tactic:
rw [DFunLike.ext_iff] at eq

Premises used: DFunLike.ext_iff
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : ∀ (x : α), Eq.{u_5 + 1} (α := M) ((single a₁ b₁ : (a : α) → M) x : M) ((single a₂ b₂ : (a : α) → M) x : M)
h : ¬a₁ = a₂
⊢ Eq.{u_5 + 1} (α := M) ((single a₁ b₁ : (a : α) → M) a₁ : M) ((single a₂ b₂ : (a : α) → M) a₁ : M)

Tactic:
have h₁ := eq a₁
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : ∀ (x : α), Eq.{u_5 + 1} (α := M) ((single a₁ b₁ : (a : α) → M) x : M) ((single a₂ b₂ : (a : α) → M) x : M)
h : ¬a₁ = a₂
h₁ : Eq.{u_5 + 1} (α := M) ((single a₁ b₁ : (a : α) → M) a₁ : M) ((single a₂ b₂ : (a : α) → M) a₁ : M)
⊢ Eq.{u_5 + 1} (α := M) ((single a₁ b₁ : (a : α) → M) a₂ : M) ((single a₂ b₂ : (a : α) → M) a₂ : M)

Tactic:
have h₂ := eq a₂
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : ∀ (x : α), Eq.{u_5 + 1} (α := M) ((single a₁ b₁ : (a : α) → M) x : M) ((single a₂ b₂ : (a : α) → M) x : M)
h : ¬a₁ = a₂
h₁ : Eq.{u_5 + 1} (α := M) ((single a₁ b₁ : (a : α) → M) a₁ : M) ((single a₂ b₂ : (a : α) → M) a₁ : M)
h₂ : Eq.{u_5 + 1} (α := M) ((single a₁ b₁ : (a : α) → M) a₂ : M) ((single a₂ b₂ : (a : α) → M) a₂ : M)
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a₁ a₂ : α
b₁ b₂ : M
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0 → Eq (α := α →₀ M) (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₁ b₂ : M
mp : Eq (α := α →₀ M) (single a₁ b₁) (single a₂ b₂) → a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
mpr mpr₁ : a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0 → Eq (α := α →₀ M) (single a₁ b₁) (single a₂ b₂)
⊢ Eq (α := α →₀ M) (single a₁ b₁) (single a₂ b₂) ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Tactic:
classical
  constructor
  · intro eq
    by_cases h : a₁ = a₂
    · refine Or.inl ⟨h, ?_⟩
      rwa [h, (single_injective a₂).eq_iff] at eq
    · rw [DFunLike.ext_iff] at eq
      have h₁ := eq a₁
      have h₂ := eq a₂
      grind
  · grind

Premises used: Finsupp.single_injective, Function.Injective.eq_iff, DFunLike.ext_iff, Or.inl
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
b : M
h : b ≠ 0
⊢ Injective (β := α →₀ M) fun (a : α) ↦ single a b

Tactic:
fun _a _a' H => (((single_eq_single_iff _ _ _ _).mp H).resolve_right fun hb => h hb.1).left

Premises used: Finsupp.single_eq_single_iff, And.left, Iff.mp, Function.Injective, Or.resolve_right
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a a' : α
b : M
h : b ≠ 0
⊢ Eq (α := α →₀ M) (single a b) (single a' b) ↔ a = a'

Tactic:
(single_left_injective h).eq_iff

Premises used: Function.Injective.eq_iff, Finsupp.single_left_injective
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
⊢ Surjective (β := M) fun (f : α →₀ M) ↦ (f : (a : α) → M) a

Tactic:
RightInverse.surjective fun _ ↦ single_eq_same

Premises used: Finsupp.single_eq_same, Function.RightInverse.surjective
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
b : M
i : α
h : b ≠ 0
⊢ support (single i b) ≠ ⊥

Tactic:
simpa only [support_single _ h] using singleton_ne_empty _

Premises used: Finsupp.support_single, Finset.singleton_ne_empty
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
b b' : M
hb : b ≠ 0
hb' : b' ≠ 0
i j : α
rw : Disjoint {i} (support (single j b')) ↔ i ≠ j
rw₁ : Disjoint (α := Finset α) {i} {j} ↔ i ≠ j
rw₂ rw₃ : i ≠ j ↔ i ≠ j
⊢ Disjoint (support (single i b)) (support (single j b')) ↔ i ≠ j

Tactic:
rw [support_single _ hb, support_single _ hb', disjoint_singleton]

Premises used: Finsupp.support_single, Finset.disjoint_singleton
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
b : M
⊢ Eq (α := α →₀ M) (single a b) 0 ↔ b = 0

Tactic:
simp [DFunLike.ext_iff, single_apply]

Premises used: DFunLike.ext_iff, Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
b : M
⊢ Eq (α := α →₀ M) (single a b) 0 ↔ b = 0

Tactic:
classical simp [DFunLike.ext_iff, single_apply]

Premises used: DFunLike.ext_iff, Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
b : M
⊢ Ne (α := α →₀ M) (single a b) 0 ↔ b ≠ 0

Tactic:
single_eq_zero.not

Premises used: Finsupp.single_eq_zero, Iff.not
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a₁ a₂ : α
b : M
⊢ Eq.{u_5 + 1} (α := M) ((single a₁ b : (a : α) → M) a₂ : M) ((single a₂ b : (a : α) → M) a₁ : M)

Tactic:
simp only [single_apply, eq_comm]

Premises used: eq_comm, Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a₁ a₂ : α
b : M
⊢ Eq.{u_5 + 1} (α := M) ((single a₁ b : (a : α) → M) a₂ : M) ((single a₂ b : (a : α) → M) a₁ : M)

Tactic:
classical simp only [single_apply, eq_comm]

Premises used: eq_comm, Finsupp.single_apply
-- 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 a' : α
b : M
inst_1 : Nonempty α
inst_2 : Nontrivial M
inhabit : ∀ (inhabited_h : Inhabited α), Nontrivial (α →₀ M)
⊢ Nontrivial (α →₀ M)

Tactic:
inhabit α
-- 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 a' : α
b : M
inst_1 : Nonempty α
inst_2 : Nontrivial M
inhabited_h : Inhabited α
rcases : ∀ (x : M) (hx : x ≠ 0), Nontrivial (α →₀ M)
⊢ Nontrivial (α →₀ M)

Tactic:
rcases exists_ne (0 : M) with ⟨x, hx⟩

Premises used: exists_ne, OfNat.ofNat
-- 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 a' : α
b : M
inst_1 : Nonempty α
inst_2 : Nontrivial M
inhabited_h : Inhabited α
x : M
hx : x ≠ 0
⊢ Nontrivial (α →₀ M)

Tactic:
nontrivial_of_ne (single default x) 0 (mt single_eq_zero.1 hx)

Premises used: Inhabited.default, Finsupp.single_eq_zero, mt, nontrivial_of_ne, Iff.mp, OfNat.ofNat, Finsupp.single
-- 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 a' : α
b : M
inst_1 : Nonempty α
inst_2 : Nontrivial M
inhabited_h : Inhabited α
x : M
hx : x ≠ 0
⊢ Nontrivial (α →₀ M)

Tactic:
exact nontrivial_of_ne (single default x) 0 (mt single_eq_zero.1 hx)

Premises used: Inhabited.default, Finsupp.single_eq_zero, mt, nontrivial_of_ne, Iff.mp, OfNat.ofNat, Finsupp.single
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f g : α →₀ M
hfg : f ≠ g
obtain :
  ∀ (a : α) (ha : Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) ((g : (a : α) → M) a : M)), Nonempty α ∧ Nontrivial M
⊢ Nonempty α ∧ Nontrivial M

Tactic:
obtain ⟨a, ha⟩ := ne_iff.mp hfg

Premises used: Iff.mp, Finsupp.ne_iff
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f g : α →₀ M
hfg : f ≠ g
a : α
ha : Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) ((g : (a : α) → M) a : M)
⊢ Nonempty α ∧ Nontrivial M

Tactic:
⟨⟨a⟩, _, _, ha⟩

Premises used: Nontrivial.mk, Nonempty.intro, And.intro, Exists.intro
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f g : α →₀ M
hfg : f ≠ g
a : α
ha : Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) ((g : (a : α) → M) a : M)
⊢ Nonempty α ∧ Nontrivial M

Tactic:
exact ⟨⟨a⟩, _, _, ha⟩
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : Unique α
x : α →₀ M
⊢ x = single default ((x : (a : α) → M) default)

Tactic:
ext <| Unique.forall_iff.2 single_eq_same.symm

Premises used: Iff.mpr, Finsupp.single_eq_same, Finsupp.ext, Unique.forall_iff, Eq.symm
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a a' : α
b : M
inst_1 : Unique α
b' : M
rw : Eq.{u_5 + 1} (α := M) ((single a b : (a : α) → M) default : M) ((single a' b' : (a : α) → M) default : M) ↔ b = b'
rw₁ :
  Eq.{u_5 + 1} (α := M) ((single default b : (a : α) → M) default : M) ((single a' b' : (a : α) → M) default : M) ↔
    b = b'
rw₂ :
  Eq.{u_5 + 1} (α := M) ((single default b : (a : α) → M) default : M) ((single default b' : (a : α) → M) default : M) ↔
    b = b'
rw₃ : b = (single default b' : (a : α) → M) default ↔ b = b'
rw₄ rw₅ : b = b' ↔ b = b'
⊢ Eq (α := α →₀ M) (single a b) (single a' b') ↔ b = b'

Tactic:
rw [Finsupp.unique_ext_iff, Unique.eq_default a, Unique.eq_default a', single_eq_same,
    single_eq_same]

Premises used: Finsupp.single_eq_same, Unique.eq_default, Finsupp.unique_ext_iff
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
N : Type u_7
P : Type u_8
inst : Zero N
inst_1 : Zero P
e : N → P
he : e 0 = 0
a : α
n : N
b : α
⊢ e ((single a n : (a : α) → N) b) = (single a (e n) : (a : α) → P) b

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
N : Type u_7
P : Type u_8
inst : Zero N
inst_1 : Zero P
e : N → P
he : e 0 = 0
a : α
n : N
b : α
⊢ e ((single a n : (a : α) → N) b) = (single a (e n) : (a : α) → P) b

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

Tactic:
⟨fun h =>
    ⟨mem_support_iff.1 <| h.symm ▸ Finset.mem_singleton_self a,
      eq_single_iff.2 ⟨subset_of_eq h, rfl⟩⟩,
    fun h => h.2.symm ▸ support_single _ h.1⟩

Premises used: Iff.mpr, Finsupp.mem_support_iff, Finsupp.support_single, Finset.mem_singleton_self, Finsupp.eq_single_iff, Eq.rec, subset_of_eq, And.right, And.left, And.intro, Iff.intro, Iff.mp, Eq.symm, rfl
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a : α
⊢ f.support = {a} ↔ ∃ (b : M), b ≠ 0 ∧ f = single a b

Tactic:
⟨fun h =>
    let h := support_eq_singleton.1 h
    ⟨_, h.1, h.2⟩,
    fun ⟨_b, hb, hf⟩ => hf.symm ▸ support_single _ hb⟩

Premises used: Finsupp.support_single, Finsupp.support, Eq.rec, Finsupp.support_eq_singleton, And.right, And.left, And.intro, Iff.intro, Exists.intro, Iff.mp, Singleton.singleton, Eq.symm, Eq, DFunLike.coe, _private.0.Finsupp.support_eq_singleton'.match_1
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
⊢ #f.support = 1 ↔
    ∃ (a : α), Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) ∧ f = single a ((f : (a : α) → M) a)

Tactic:
simp only [card_eq_one, support_eq_singleton]

Premises used: Finset.card_eq_one, Finsupp.support_eq_singleton
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
⊢ #f.support = 1 ↔ ∃ (a : α) (b : M), b ≠ 0 ∧ f = single a b

Tactic:
simp only [card_eq_one, support_eq_singleton']

Premises used: Finset.card_eq_one, Finsupp.support_eq_singleton'
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a : α
⊢ f.support ⊆ {a} ↔ f = single a ((f : (a : α) → M) a)

Tactic:
⟨fun h => eq_single_iff.mpr ⟨h, rfl⟩, fun h => (eq_single_iff.mp h).left⟩

Premises used: Iff.mpr, Finsupp.eq_single_iff, And.left, And.intro, Iff.intro, Iff.mp, rfl
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a : α
h : ∃ (b : M), f = single a b
b : M
hb : f = single a b
rw : support (single a b) ⊆ {a}
rw₁ : Eq (α := α →₀ M) (single a b) (single a ((single a b : (a : α) → M) a))
rw₂ rw₃ : Eq (α := α →₀ M) (single a b) (single a b)
⊢ f.support ⊆ {a}

Tactic:
rw [hb, support_subset_singleton, single_eq_same]

Premises used: Finsupp.single_eq_same, Finsupp.support_subset_singleton
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : Nonempty α
f : α →₀ M
⊢ #f.support ≤ 1 ↔ ∃ (a : α), f = single a ((f : (a : α) → M) a)

Tactic:
simp only [card_le_one_iff_subset_singleton, support_subset_singleton]

Premises used: Finset.card_le_one_iff_subset_singleton, Finsupp.support_subset_singleton
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : Nonempty α
f : α →₀ M
⊢ #f.support ≤ 1 ↔ ∃ (a : α) (b : M), f = single a b

Tactic:
simp only [card_le_one_iff_subset_singleton, support_subset_singleton']

Premises used: Finset.card_le_one_iff_subset_singleton, Finsupp.support_subset_singleton'
-- 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_1 a' : α
b : M
a : α
inst_1 : Subsingleton α
f : α →₀ M
h :
  ∀ (b : α),
    Eq.{u_5 + 1} (α := M) ((single a ((fun (f : α →₀ M) ↦ ((f : (a : α) → M) a : M)) f) : (a : α) → M) b : M)
      ((f : (a : α) → M) b : M)
⊢ single a ((fun (f : α →₀ M) ↦ ((f : (a : α) → M) a : M)) f) = f

Tactic:
ext b
-- 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_1 a' : α
b_1 : M
a : α
inst_1 : Subsingleton α
f : α →₀ M
b : α
⊢ Eq.{u_5 + 1} (α := M) ((single a ((fun (f : α →₀ M) ↦ ((f : (a : α) → M) a : M)) f) : (a : α) → M) b : M)
    ((f : (a : α) → M) b : M)

Tactic:
simp [Subsingleton.elim b a]

Premises used: Subsingleton.elim
-- 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_1 a' : α
b : M
a : α
inst_1 : Subsingleton α
x : M
⊢ (fun (f : α →₀ M) ↦ ((f : (a : α) → M) a : M)) (single a x) = x

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
inst_1 : Subsingleton α
m : M
b : α
⊢ (((Equiv.symm (uniqueEquiv a) : (a : M) → α →₀ M) m : α →₀ M) : (a : α) → M) b = m

Tactic:
simp [Subsingleton.elim b a]

Premises used: Subsingleton.elim
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
inst_2 : Finite α
x : α
m : M
⊢ Eq (α := α → M) ((equivFunOnFinite : (a : α →₀ M) → α → M) (single x m) : α → M)
    (Pi.single (M := fun (j : α) ↦ M) x m : (j : α) → M)

Tactic:
simp [Finsupp.single_eq_pi_single, equivFunOnFinite]

Premises used: Finsupp.equivFunOnFinite, Finsupp.single_eq_pi_single
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
inst_2 : Finite α
x : α
m : M
rw :
  Eq (α := α →₀ M)
    ((Equiv.symm equivFunOnFinite : (a : α → M) → α →₀ M) ((equivFunOnFinite : (a : α →₀ M) → α → M) (single x m)) :
      α →₀ M)
    (single x m : α →₀ M)
rw₁ rw₂ : Eq (α := α →₀ M) (single x m) (single x m)
⊢ Eq (α := α →₀ M)
    ((Equiv.symm equivFunOnFinite : (a : α → M) → α →₀ M) (Pi.single (M := fun (a : α) ↦ M) x m) : α →₀ M)
    (single x m : α →₀ M)

Tactic:
rw [← equivFunOnFinite_single, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, Finsupp.equivFunOnFinite_single
-- 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
f_1 : α →₀ M
a_1 : α
b_1 : M
i : α
f : α →₀ M
a : α
b : M
haveI : (this : DecidableEq α) → Finset α
⊢ Finset α

Tactic:
haveI := Classical.decEq α
-- 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
f_1 : α →₀ M
a_1 : α
b_1 : M
i : α
f : α →₀ M
a : α
b : M
this : DecidableEq α
haveI : (this : DecidableEq M) → Finset α
⊢ Finset α

Tactic:
haveI := Classical.decEq M
-- 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
f_1 : α →₀ M
a_1 : α
b_1 : M
i : α
f : α →₀ M
a : α
b : M
this_1 : DecidableEq α
this : DecidableEq M
⊢ Finset α

Tactic:
exact if b = 0 then f.support.erase a else insert a f.support

Premises used: Finsupp.support, Insert.insert, Finset.erase
-- 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
f_1 : α →₀ M
a_1 : α
b_1 : M
i_1 : α
f : α →₀ M
a : α
b : M
i : α
⊢ (i ∈ if b = 0 then f.support.erase a else insert a f.support) ↔
    Ne.{u_5 + 1} (α := M) (Function.update (β := fun (a : α) ↦ M) (⇑f : (a : α) → M) a b i : 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
f_1 : α →₀ M
a_1 : α
b_1 : M
i_1 : α
f : α →₀ M
a : α
b : M
i : α
⊢ (i ∈ if b = 0 then f.support.erase a else insert a f.support) ↔
    Ne.{u_5 + 1} (α := M) (Function.update (β := fun (a : α) ↦ M) (⇑f : (a : α) → M) a b i : M) (0 : M)

Tactic:
classical
    grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a : α
b : M
i : α
inst_1 : DecidableEq α
delta :
  ({ support := if b = 0 then f.support.erase a else insert a f.support,
          toFun := fun (a_1 : α) ↦
            if h : a_1 = a then Eq.ndrec (motive := fun (a : α) ↦ M) b ⋯ else (f : (a : α) → M) a_1,
          mem_support_toFun := ⋯ } :
        (a : α) → M)
      i =
    if i = a then b else (f : (a : α) → M) i
⊢ (f.update a b : (a : α) → M) i = if i = a then b else (f : (a : α) → M) i

Tactic:
delta update Function.update

Premises used: Function.update, Finsupp.update
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a : α
b : M
i : α
inst_1 : DecidableEq α
⊢ ({ support := if b = 0 then f.support.erase a else insert a f.support,
          toFun := fun (a_1 : α) ↦
            if h : a_1 = a then Eq.ndrec (motive := fun (a : α) ↦ M) b ⋯ else (f : (a : α) → M) a_1,
          mem_support_toFun := ⋯ } :
        (a : α) → M)
      i =
    if i = a then b else (f : (a : α) → M) i

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a : α
b : M
inst_1 : DecidableEq α
⊢ Eq (α := (a : α) → M) (⇑(f.update a b) : (a : α) → M) (Function.update (β := fun (a : α) ↦ M) (⇑f : (a : α) → M) a b)

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

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

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

Tactic:
rfl

Premises used: Multiset.cons, Multiset.zero, Finset.empty, Pi.single, Multiset.ofList, List.erase, Multiset.erase, Finset.erase, Multiset.ndinsert, rfl, Finsupp.single, ite
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a : α
b : M
inst_1 : DecidableEq α
inst_2 : DecidableEq M
⊢ (f.update a b).support = if b = 0 then f.support.erase a else insert a f.support

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

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

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

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a₁ a₂ : α
h : a₁ ≠ a₂
m₁ m₂ : M
⊢ (f.update a₁ m₁).update a₂ m₂ = (f.update a₂ m₂).update a₁ m₁

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a₁ a₂ : α
h : a₁ ≠ a₂
m₁ m₂ : M
⊢ (f.update a₁ m₁).update a₂ m₂ = (f.update a₂ m₂).update a₁ m₁

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

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

Tactic:
classical
  grind