awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
k : κ
f : Finsupp.{u_2, u_3} (ι k) M
i : ι k
rw :
  Eq.{u_3 + 1} (α := M)
    ((embDomain (Embedding.sigmaMk (β := ι) k) f : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) : M)
    ((f : (a : ι k) → M) i : M)
⊢ Eq.{u_3 + 1} (α := M) ((f.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) : M)
    ((f : (a : ι k) → M) i : M)

Tactic:
rw [embSigma]

Premises used: Finsupp.embSigma
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
k : κ
f : Finsupp.{u_2, u_3} (ι k) M
i : ι k
⊢ Eq.{u_3 + 1} (α := M)
    ((embDomain (Embedding.sigmaMk (β := ι) k) f : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) : M)
    ((f : (a : ι k) → M) i : M)

Tactic:
embDomain_apply_self (Embedding.sigmaMk k) f i

Premises used: Set.Mem, setOf, Finsupp.embDomain_apply_self, Function.Embedding.sigmaMk
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
k : κ
f : Finsupp.{u_2, u_3} (ι k) M
i : ι k
⊢ Eq.{u_3 + 1} (α := M)
    ((embDomain (Embedding.sigmaMk (β := ι) k) f : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) : M)
    ((f : (a : ι k) → M) i : M)

Tactic:
exact embDomain_apply_self (Embedding.sigmaMk k) f i

Premises used: Finsupp.embDomain_apply_self, Function.Embedding.sigmaMk
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
k k' : κ
f : Finsupp.{u_2, u_3} (ι k) M
hk : k' ≠ k
i : ι k'
h :
  Sigma.mk (β := fun (k : κ) ↦ ι k) k' i ∉
    Set.range (ι := ι k) (⇑(Embedding.sigmaMk (β := ι) k) : (a : ι k) → (k : κ) × ι k)
⊢ Eq.{u_3 + 1} (α := M) ((f.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) : M)
    (0 : M)

Tactic:
apply embDomain_notin_range

Premises used: Finsupp.embDomain_notin_range
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
k k' : κ
f : Finsupp.{u_2, u_3} (ι k) M
hk : k' ≠ k
i : ι k'
⊢ Sigma.mk (β := fun (k : κ) ↦ ι k) k' i ∉
    Set.range (ι := ι k) (⇑(Embedding.sigmaMk (β := ι) k) : (a : ι k) → (k : κ) × ι k)

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
k : κ
f : Finsupp.{u_2, u_3} (ι k) M
⊢ f.embSigma (ι := ι).support = Finset.map (Embedding.sigmaMk (β := ι) k) f.support

Tactic:
simp [embSigma]

Premises used: Finsupp.embSigma
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
k : κ
⊢ Eq (α := (k : κ) × ι k →₀ M) (embSigma (ι := ι) (k := k) 0) 0

Tactic:
simp [embSigma]

Premises used: Finsupp.embSigma
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
k : κ
f : Finsupp.{u_2, u_3} (ι k) M
⊢ f.embSigma (ι := ι) = 0 ↔ f = 0

Tactic:
simp [embSigma]

Premises used: Finsupp.embSigma
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
k : κ
f g : Finsupp.{u_2, u_3} (ι k) M
h : f.embSigma (ι := ι) = g.embSigma (ι := ι)
h₁ : ∀ (i : ι k), Eq.{u_3 + 1} (α := M) ((f : (a : ι k) → M) i : M) ((g : (a : ι k) → M) i : M)
⊢ f = g

Tactic:
ext i
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
k : κ
f g : Finsupp.{u_2, u_3} (ι k) M
h : f.embSigma (ι := ι) = g.embSigma (ι := ι)
i : ι k
⊢ Eq.{u_3 + 1} (α := M) ((f.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) : M)
    ((g.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) : M)

Tactic:
have := congr_fun (congrArg (⇑) h) ⟨k, i⟩
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
k : κ
f g : Finsupp.{u_2, u_3} (ι k) M
h : f.embSigma (ι := ι) = g.embSigma (ι := ι)
i : ι k
this :
  Eq.{u_3 + 1} (α := M) ((f.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) : M)
    ((g.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) : M)
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : ι k) → M) i : M) ((g : (a : ι k) → M) i : M)

Tactic:
simpa using this
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
k : κ
f g : Finsupp.{u_2, u_3} (ι k) M
⊢ f.embSigma (ι := ι) = g.embSigma (ι := ι) ↔ f = g

Tactic:
embSigma_injective.eq_iff

Premises used: Function.Injective.eq_iff, Finsupp.embSigma_injective
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : AddMonoid M
k : κ
f g : Finsupp.{u_2, u_3} (ι k) M
h :
  ∀ (k' : κ) (i : ι k'),
    Eq.{u_3 + 1} (α := M)
      (((f + g).embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) : M)
      ((f.embSigma (ι := ι) + g.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) :
        M)
⊢ (f + g).embSigma (ι := ι) = f.embSigma (ι := ι) + g.embSigma (ι := ι)

Tactic:
ext ⟨k', i⟩
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : AddMonoid M
k : κ
f g : Finsupp.{u_2, u_3} (ι k) M
k' : κ
i : ι k'
pos :
  ∀ (hk : k' = k),
    Eq.{u_3 + 1} (α := M)
      (((f + g).embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) : M)
      ((f.embSigma (ι := ι) + g.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) :
        M)
neg :
  ∀ (hk : ¬k' = k),
    Eq.{u_3 + 1} (α := M)
      (((f + g).embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) : M)
      ((f.embSigma (ι := ι) + g.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) :
        M)
⊢ Eq.{u_3 + 1} (α := M)
    (((f + g).embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) : M)
    ((f.embSigma (ι := ι) + g.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) : M)

Tactic:
by_cases hk : k' = k
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : AddMonoid M
k : κ
f g : Finsupp.{u_2, u_3} (ι k) M
k' : κ
i : ι k'
hk : k' = k
pos :
  ∀ (f g : Finsupp.{u_2, u_3} (ι k') M),
    Eq.{u_3 + 1} (α := M)
      (((f + g).embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) : M)
      ((f.embSigma (ι := ι) + g.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) :
        M)
⊢ Eq.{u_3 + 1} (α := M)
    (((f + g).embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) : M)
    ((f.embSigma (ι := ι) + g.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) : M)

Tactic:
subst hk
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : AddMonoid M
k' : κ
i : ι k'
f g : Finsupp.{u_2, u_3} (ι k') M
⊢ Eq.{u_3 + 1} (α := M)
    (((f + g).embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) : M)
    ((f.embSigma (ι := ι) + g.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) : M)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : AddMonoid M
k : κ
f g : Finsupp.{u_2, u_3} (ι k) M
k' : κ
i : ι k'
hk : ¬k' = k
⊢ Eq.{u_3 + 1} (α := M)
    (((f + g).embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) : M)
    ((f.embSigma (ι := ι) + g.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) : M)

Tactic:
simp [embSigma_apply_of_ne _ hk]

Premises used: Finsupp.embSigma_apply_of_ne
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
k : κ
i : ι k
m : M
⊢ Eq (α := (k : κ) × ι k →₀ M) (embSigma (ι := ι) (single i m)) (single (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) m)

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
k : κ
i : ι k
m : M
⊢ Eq (α := (k : κ) × ι k →₀ M) (embSigma (ι := ι) (single i m)) (single (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) m)

Tactic:
classical
  grind
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
k : κ
f : Finsupp.{u_2, u_3} (ι k) M
h :
  ∀ (i : ι k),
    Eq.{u_3 + 1} (α := M) ((f.embSigma (ι := ι).split (αs := ι) k : (a : ι k) → M) i : M) ((f : (a : ι k) → M) i : M)
⊢ f.embSigma (ι := ι).split (αs := ι) k = f

Tactic:
ext i
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
k : κ
f : Finsupp.{u_2, u_3} (ι k) M
i : ι k
⊢ Eq.{u_3 + 1} (α := M) ((f.embSigma (ι := ι).split (αs := ι) k : (a : ι k) → M) i : M) ((f : (a : ι k) → M) i : M)

Tactic:
simp [split_apply]

Premises used: Finsupp.split_apply
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
k k' : κ
f : Finsupp.{u_2, u_3} (ι k) M
hk : k' ≠ k
h :
  ∀ (i : ι k'),
    Eq.{u_3 + 1} (α := M) ((f.embSigma (ι := ι).split (αs := ι) k' : (a : ι k') → M) i : M) ((0 : (a : ι k') → M) i : M)
⊢ f.embSigma (ι := ι).split (αs := ι) k' = 0

Tactic:
ext i
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
k k' : κ
f : Finsupp.{u_2, u_3} (ι k) M
hk : k' ≠ k
i : ι k'
⊢ Eq.{u_3 + 1} (α := M) ((f.embSigma (ι := ι).split (αs := ι) k' : (a : ι k') → M) i : M) ((0 : (a : ι k') → M) i : M)

Tactic:
simp [split_apply, embSigma_apply_of_ne _ hk]

Premises used: Finsupp.embSigma_apply_of_ne, Finsupp.split_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_1 a'_1 : α
b_1 : M
a : α
b : M
a' : α
⊢ Membership.mem (γ := Finset α) (if b = 0 then ∅ else {a}) a' ↔
    Ne.{u_5 + 1} (α := M) (Pi.single (M := fun (a : α) ↦ M) a b a' : M) (0 : M)

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a a' : α
b : M
inst_1 : Decidable (a = a')
simp_rw : (single a b : (a : α) → M) a' = if a' = a then b else 0
simp_rw₁ :
  ({ support := if b = 0 then ∅ else {a}, toFun := Pi.single (M := fun (a : α) ↦ M) a b, mem_support_toFun := ⋯ } :
        (a : α) → M)
      a' =
    if a' = a then b else 0
simp_rw₂ : Pi.single (M := fun (a : α) ↦ M) a b a' = if a' = a then b else 0
⊢ (single a b : (a : α) → M) a' = if a = a' then b else 0

Tactic:
simp_rw [@eq_comm _ a a', single, coe_mk, Pi.single_apply]

Premises used: Pi.single_apply, eq_comm, Finsupp.coe_mk, Finsupp.single
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a a' : α
b : M
inst_1 : Decidable (a = a')
simp_rw : (single a b : (a : α) → M) a' = if a' = a then b else 0
simp_rw₁ :
  ({ support := if b = 0 then ∅ else {a}, toFun := Pi.single (M := fun (a : α) ↦ M) a b, mem_support_toFun := ⋯ } :
        (a : α) → M)
      a' =
    if a' = a then b else 0
simp_rw₂ : Pi.single (M := fun (a : α) ↦ M) a b a' = if a' = a then b else 0
⊢ (single a b : (a : α) → M) a' = if a = a' then b else 0

Tactic:
classical
  simp_rw [@eq_comm _ a a', single, coe_mk, Pi.single_apply]

Premises used: Pi.single_apply, eq_comm, Finsupp.coe_mk, Finsupp.single
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
hf : Injective f
x z : α
y : M
⊢ Eq.{u_5 + 1} (α := M) ((single (f x) y : (a : β) → M) (f z) : M) ((single x y : (a : α) → M) z : M)

Tactic:
simp only [single_apply, hf.eq_iff]

Premises used: Function.Injective.eq_iff, Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
hf : Injective f
x z : α
y : M
⊢ Eq.{u_5 + 1} (α := M) ((single (f x) y : (a : β) → M) (f z) : M) ((single x y : (a : α) → M) z : M)

Tactic:
classical simp only [single_apply, hf.eq_iff]

Premises used: Function.Injective.eq_iff, Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
a : α
b : M
h : ∀ (x : α), Eq.{u_5 + 1} (α := M) ((single a b : (a : α) → M) x : M) (Pi.single (M := fun (j : α) ↦ M) a b x : M)
⊢ Eq (α := (a : α) → M) (⇑(single a b) : (a : α) → M) (Pi.single (M := fun (j : α) ↦ M) a b)

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
a : α
b : M
x : α
⊢ Eq.{u_5 + 1} (α := M) ((single a b : (a : α) → M) x : M) (Pi.single (M := fun (j : α) ↦ M) a b x : M)

Tactic:
simp [single_apply, Pi.single_apply, eq_comm]

Premises used: Pi.single_apply, eq_comm, Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
f : α → M
rw : Eq (α := (x : α) → M) (Pi.single (M := fun (j : α) ↦ M) a (f a)) (⇑(single a (f a)) : (a : α) → M)
rw₁ rw₂ : Eq (α := (x : α) → M) (Pi.single (M := fun (j : α) ↦ M) a (f a)) (Pi.single (M := fun (j : α) ↦ M) a (f a))
⊢ Set.indicator {a} f = (⇑(single a (f a)) : (a : α) → M)

Tactic:
rw [Set.indicator_singleton, single_eq_pi_single]

Premises used: Finsupp.single_eq_pi_single, Set.indicator_singleton
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
f : α → M
classical : Eq (α := (x : α) → M) (Pi.single (M := fun (j : α) ↦ M) a (f a)) (⇑(single a (f a)) : (a : α) → M)
classical₁ classical₂ :
  Eq (α := (x : α) → M) (Pi.single (M := fun (j : α) ↦ M) a (f a)) (Pi.single (M := fun (j : α) ↦ M) a (f a))
⊢ Set.indicator {a} f = (⇑(single a (f a)) : (a : α) → M)

Tactic:
classical rw [Set.indicator_singleton, single_eq_pi_single]

Premises used: Finsupp.single_eq_pi_single, Set.indicator_singleton
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
b : M
⊢ Eq (α := (a : α) → M) (⇑(single a b) : (a : α) → M) (Set.indicator {a} fun (x : α) ↦ b)

Tactic:
(set_indicator_singleton a (fun _ => b)).symm

Premises used: Finsupp.set_indicator_singleton, Eq.symm
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
b : M
⊢ (single a b : (a : α) → M) a = b

Tactic:
Pi.single_eq_same (M := fun _ ↦ M) a b

Premises used: Function.update, Pi.single, dite, Pi.single_eq_same
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
b : M
⊢ (single a b : (a : α) → M) a = b

Tactic:
exact Pi.single_eq_same (M := fun _ ↦ M) a b

Premises used: Pi.single_eq_same
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
b : M
⊢ (single a b : (a : α) → M) a = b

Tactic:
classical exact Pi.single_eq_same (M := fun _ ↦ M) a b
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a a' : α
b : M
h : a' ≠ a
⊢ Eq.{u_5 + 1} (α := M) ((single a b : (a : α) → M) a' : M) (0 : M)

Tactic:
Pi.single_eq_of_ne h _

Premises used: Function.update, Pi.single_eq_of_ne, Pi.single, dite
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a a' : α
b : M
h : a' ≠ a
⊢ Eq.{u_5 + 1} (α := M) ((single a b : (a : α) → M) a' : M) (0 : M)

Tactic:
exact Pi.single_eq_of_ne h _

Premises used: Pi.single_eq_of_ne
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a a' : α
b : M
h : a' ≠ a
⊢ Eq.{u_5 + 1} (α := M) ((single a b : (a : α) → M) a' : M) (0 : M)

Tactic:
classical exact Pi.single_eq_of_ne h _
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a a' : α
b : M
h : a ≠ a'
⊢ Eq.{u_5 + 1} (α := M) ((single a b : (a : α) → M) a' : M) (0 : M)

Tactic:
Pi.single_eq_of_ne' h _

Premises used: Function.update, Pi.single, dite, Pi.single_eq_of_ne'
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a a' : α
b : M
h : a ≠ a'
⊢ Eq.{u_5 + 1} (α := M) ((single a b : (a : α) → M) a' : M) (0 : M)

Tactic:
exact Pi.single_eq_of_ne' h _

Premises used: Pi.single_eq_of_ne'
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a a' : α
b : M
h : a ≠ a'
⊢ Eq.{u_5 + 1} (α := M) ((single a b : (a : α) → M) a' : M) (0 : M)

Tactic:
classical exact Pi.single_eq_of_ne' h _
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
a : α
b : M
⊢ Eq (α := (a : α) → M) (⇑(single a b) : (a : α) → M) (update (β := fun (a : α) ↦ M) 0 a b)

Tactic:
single_eq_pi_single a b

Premises used: Pi.single, Finsupp.single_eq_pi_single
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
⊢ Eq (α := (a : α) → M) ((fun (f : α →₀ M) ↦ ((⇑f : (a : α) → M) : (a : α) → M)) (single a 0))
    ((fun (f : α →₀ M) ↦ ((⇑f : (a : α) → M) : (a : α) → M)) 0)

Tactic:
simpa only [single_eq_update, coe_zero] using Function.update_eq_self a (0 : α → M)

Premises used: Function.update_eq_self, Finsupp.single_eq_update, OfNat.ofNat, Finsupp.coe_zero
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
⊢ Eq (α := (a : α) → M) ((fun (f : α →₀ M) ↦ ((⇑f : (a : α) → M) : (a : α) → M)) (single a 0))
    ((fun (f : α →₀ M) ↦ ((⇑f : (a : α) → M) : (a : α) → M)) 0)

Tactic:
classical simpa only [single_eq_update, coe_zero] using Function.update_eq_self a (0 : α → M)

Premises used: Finsupp.single_eq_update, Finsupp.coe_zero
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a a' : α
b : M
⊢ Eq (α := α →₀ M) (single a ((single a' b : (a : α) → M) a) : α →₀ M)
    ((single a' (single a' b) : (a : α) → α →₀ M) a : α →₀ M)

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

Tactic:
classical
  grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
b : M
a : α
hb : b ≠ 0
⊢ support (single a b) = {a}

Tactic:
if_neg hb

Premises used: if_neg, ite
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
b : M
⊢ support (single a b) ⊆ {a}

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
b : M
⊢ support (single a b) ⊆ {a}

Tactic:
classical
  grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
b : M
x : α
⊢ Membership.mem (α := M) (γ := Set M) {0, b} ((single a b : (a : α) → M) x : M)

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
b : M
x : α
⊢ Membership.mem (α := M) (γ := Set M) {0, b} ((single a b : (a : α) → M) x : M)

Tactic:
classical
  grind
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
b : M
⊢ Subset (α := Set M) (Set.range.{u_5, u_1 + 1} (ι := α) (⇑(single a b) : (a : α) → M)) {0, b}

Tactic:
Set.range_subset_iff.2 single_apply_mem

Premises used: Iff.mpr, Finsupp.single_apply_mem, Set.range_subset_iff
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
b₁ b₂ : M
eq : Eq (α := α →₀ M) (single a b₁) (single a b₂)
rw rw₁ : 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:
rw [eq]
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
b₁ b₂ : M
eq : Eq (α := α →₀ M) (single a b₁) (single a b₂)
⊢ Eq.{u_5 + 1} (α := M) ((single a b₁ : (a : α) → M) a : M) ((single a b₂ : (a : α) → M) a : M)

Tactic:
have : (single a b₁ : α →₀ M) a = (single a b₂ : α →₀ M) a := by rw [eq]
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
b₁ b₂ : M
eq : Eq (α := α →₀ M) (single a b₁) (single a b₂)
this : Eq.{u_5 + 1} (α := M) ((single a b₁ : (a : α) → M) a : M) ((single a b₂ : (a : α) → M) a : M)
rwa : ∀ (this : b₁ = (single a b₂ : (a : α) → M) a), b₁ = b₂
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : b₁ = b₂), b₁ = b₂
⊢ b₁ = b₂

Tactic:
rwa [single_eq_same, single_eq_same] at this

Premises used: Finsupp.single_eq_same
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a x : α
b : M
⊢ Eq.{u_5 + 1} (α := M) ((single a b : (a : α) → M) x : M) (0 : M) ↔ x = a → b = 0

Tactic:
simp [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 x : α
b : M
⊢ Eq.{u_5 + 1} (α := M) ((single a b : (a : α) → M) x : M) (0 : M) ↔ x = a → b = 0

Tactic:
classical simp [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 x : α
b : M
⊢ Ne.{u_5 + 1} (α := M) ((single a b : (a : α) → M) x : M) (0 : M) ↔ x = a ∧ b ≠ 0

Tactic:
simp [single_apply_eq_zero]

Premises used: Finsupp.single_apply_eq_zero
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a a' : α
b : M
⊢ a ∈ support (single a' b) ↔ a = a' ∧ b ≠ 0

Tactic:
simp [single_apply_eq_zero]

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

Tactic:
⟨fun h => h.symm ▸ ⟨support_single_subset, single_eq_same⟩, ?_⟩

Premises used: Finsupp.single_eq_same, Eq.rec, And.intro, Iff.intro, Finsupp.support_single_subset, Eq.symm
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a : α
b : M
refine : f.support ⊆ {a} ∧ (f : (a : α) → M) a = b → f = single a b
⊢ f = single a b ↔ f.support ⊆ {a} ∧ (f : (a : α) → M) a = b

Tactic:
refine ⟨fun h => h.symm ▸ ⟨support_single_subset, single_eq_same⟩, ?_⟩
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a : α
h : f.support ⊆ {a}
h₁ :
  ∀ (x : α),
    Eq.{u_5 + 1} (α := M) ((f : (a : α) → M) x : M) (((single a ((f : (a : α) → M) a) : α →₀ M) : (a : α) → M) x : M)
⊢ f = single a ((f : (a : α) → M) a)

Tactic:
ext x
-- Module: Mathlib.Data.Finsupp.Single
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a : α
h : f.support ⊆ {a}
x : α
pos :
  ∀ (hx : x = a),
    Eq.{u_5 + 1} (α := M) ((f : (a : α) → M) x : M) (((single a ((f : (a : α) → M) a) : α →₀ M) : (a : α) → M) x : M)
neg :
  ∀ (hx : ¬x = a),
    Eq.{u_5 + 1} (α := M) ((f : (a : α) → M) x : M) (((single a ((f : (a : α) → M) a) : α →₀ M) : (a : α) → M) x : M)
⊢ Eq.{u_5 + 1} (α := M) ((f : (a : α) → M) x : M) (((single a ((f : (a : α) → M) a) : α →₀ M) : (a : α) → M) x : M)

Tactic:
by_cases hx : x = a
-- 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) (((single a ((f : (a : α) → M) a) : α →₀ M) : (a : α) → M) x : M)

Tactic:
simp only [hx, single_eq_same, single_eq_of_ne, Ne, not_false_iff]

Premises used: Finsupp.single_eq_same, Finsupp.single_eq_of_ne, Ne, not_false_iff
-- 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
neg : Eq.{u_5 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
⊢ Eq.{u_5 + 1} (α := M) ((f : (a : α) → M) x : M) (((single a ((f : (a : α) → M) a) : α →₀ M) : (a : α) → M) x : M)

Tactic:
simp only [hx, single_eq_same, single_eq_of_ne, Ne, not_false_iff]

Premises used: Finsupp.single_eq_same, Finsupp.single_eq_of_ne, Ne, not_false_iff
-- 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:
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