awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finsupp.Sigma (goal)
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)
have 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)
Tactic: subst hk
Cleared hypotheses: k, f, g, hk
-- Lean 4 proof step from Mathlib.Data.Finsupp.Sigma (goal)
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 (ι := ι).split (αs := ι) k = f
have h : ∀ (i : ι k),
  Eq.{u_3 + 1} (α := M) ((f.embSigma (ι := ι).split (αs := ι) k : (a : ι k) → M) i : M) ((f : (a : ι k) → M) i : M)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Finsupp.Sigma (goal)
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
⊢ f.embSigma (ι := ι).split (αs := ι) k' = 0
have h : ∀ (i : ι k'),
  Eq.{u_3 + 1} (α := M) ((f.embSigma (ι := ι).split (αs := ι) k' : (a : ι k') → M) i : M) ((0 : (a : ι k') → M) i : M)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a a' : α
b : M
inst_1 : Decidable (a = a')
⊢ (single a b : (a : α) → M) a' = if a = a' then b else 0
have simp_rw : (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]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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
⊢ (single a b : (a : α) → M) a' = if a = a' then b else 0
have simp_rw₁ : ({ support := if b = 0 then ∅ else {a}, toFun := Pi.single (M := fun (a : α) ↦ M) a b, mem_support_toFun := sorry } :
      (a : α) → M)
    a' =
  if a' = a then b else 0
Tactic: simp_rw [@eq_comm _ a a', single, coe_mk, Pi.single_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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
⊢ (single a b : (a : α) → M) a' = if a = a' then b else 0
have simp_rw₂ : Pi.single (M := fun (a : α) ↦ M) a b a' = if a' = a then b else 0
Tactic: simp_rw [@eq_comm _ a a', single, coe_mk, Pi.single_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a a' : α
b : M
inst_1 : Decidable (a = a')
⊢ (single a b : (a : α) → M) a' = if a = a' then b else 0
have simp_rw : (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]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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
⊢ (single a b : (a : α) → M) a' = if a = a' then b else 0
have simp_rw₁ : ({ support := if b = 0 then ∅ else {a}, toFun := Pi.single (M := fun (a : α) ↦ M) a b, mem_support_toFun := sorry } :
      (a : α) → M)
    a' =
  if a' = a then b else 0
Tactic: classical
  simp_rw [@eq_comm _ a a', single, coe_mk, Pi.single_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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
⊢ (single a b : (a : α) → M) a' = if a = a' then b else 0
have simp_rw₂ : Pi.single (M := fun (a : α) ↦ M) a b a' = if a' = a then b else 0
Tactic: classical
  simp_rw [@eq_comm _ a a', single, coe_mk, Pi.single_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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) (Pi.single (M := fun (j : α) ↦ M) a b)
have h : ∀ (x : α), Eq.{u_5 + 1} (α := M) ((single a b : (a : α) → M) x : M) (Pi.single (M := fun (j : α) ↦ M) a b x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
f : α → M
⊢ Set.indicator {a} f = (⇑(single a (f a)) : (a : α) → M)
have rw : Eq (α := (x : α) → M) (Pi.single (M := fun (j : α) ↦ M) a (f a)) (⇑(single a (f a)) : (a : α) → M)
Tactic: rw [Set.indicator_singleton, single_eq_pi_single]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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)
⊢ Set.indicator {a} f = (⇑(single a (f a)) : (a : α) → M)
have rw₁ : Eq (α := (x : α) → M) (Pi.single (M := fun (j : α) ↦ M) a (f a)) (Pi.single (M := fun (j : α) ↦ M) a (f a))
Tactic: rw [Set.indicator_singleton, single_eq_pi_single]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
f : α → M
⊢ Set.indicator {a} f = (⇑(single a (f a)) : (a : α) → M)
have classical : Eq (α := (x : α) → M) (Pi.single (M := fun (j : α) ↦ M) a (f a)) (⇑(single a (f a)) : (a : α) → M)
Tactic: classical rw [Set.indicator_singleton, single_eq_pi_single]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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)
⊢ Set.indicator {a} f = (⇑(single a (f a)) : (a : α) → M)
have classical₁ : Eq (α := (x : α) → M) (Pi.single (M := fun (j : α) ↦ M) a (f a)) (Pi.single (M := fun (j : α) ↦ M) a (f a))
Tactic: classical rw [Set.indicator_singleton, single_eq_pi_single]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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)
have rw : Eq.{u_5 + 1} (α := M) ((single a b₂ : (a : α) → M) a : M) ((single a b₂ : (a : α) → M) a : M)
Tactic: rw [eq]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (hypothesis)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
b₁ b₂ : M
eq : Eq (α := α →₀ M) (single a b₁) (single a b₂)
⊢ b₁ = b₂
have this : 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]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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)
⊢ b₁ = b₂
have rwa : ∀ (this : b₁ = (single a b₂ : (a : α) → M) a), b₁ = b₂
Tactic: rwa [single_eq_same, single_eq_same] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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₂
⊢ b₁ = b₂
have rwa₁ : ∀ (this : b₁ = b₂), b₁ = b₂
Tactic: rwa [single_eq_same, single_eq_same] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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
have refine : f.support ⊆ {a} ∧ (f : (a : α) → M) a = b → f = single a b
Tactic: refine ⟨fun h => h.symm ▸ ⟨support_single_subset, single_eq_same⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a : α
h : f.support ⊆ {a}
⊢ f = single a ((f : (a : α) → M) a)
have h₁ : ∀ (x : α),
  Eq.{u_5 + 1} (α := M) ((f : (a : α) → M) x : M) (((single a ((f : (a : α) → M) a) : α →₀ M) : (a : α) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a : α
h : f.support ⊆ {a}
x : α
⊢ Eq.{u_5 + 1} (α := M) ((f : (a : α) → M) x : M) (((single a ((f : (a : α) → M) a) : α →₀ M) : (a : α) → M) x : M)
have 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)
Tactic: by_cases hx : x = a
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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)
⊢ Eq.{u_5 + 1} (α := M) ((f : (a : α) → M) x : M) (((single a ((f : (a : α) → M) a) : α →₀ M) : (a : α) → M) x : M)
have 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)
Tactic: by_cases hx : x = a
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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)
have neg : Eq.{u_5 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
Tactic: simp only [hx, single_eq_same, single_eq_of_ne, Ne, not_false_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a₁ a₂ : α
b₁ b₂ : M
⊢ Eq (α := α →₀ M) (single a₁ b₁) (single a₂ b₂) ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
have mp : Eq (α := α →₀ M) (single a₁ b₁) (single a₂ b₂) → a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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
⊢ Eq (α := α →₀ M) (single a₁ b₁) (single a₂ b₂) ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
have mpr : a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0 → Eq (α := α →₀ M) (single a₁ b₁) (single a₂ b₂)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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₂)
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
have pos : ∀ (h : a₁ = a₂), a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
Tactic: by_cases h : a₁ = a₂
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
have neg : ∀ (h : ¬a₁ = a₂), a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
Tactic: by_cases h : a₁ = a₂
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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
have pos : b₁ = b₂
Tactic: refine Or.inl ⟨h, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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₂
⊢ b₁ = b₂
have pos : ∀ (eq : Eq (α := α →₀ M) (single a₂ b₁) (single a₂ b₂)) (h : a₁ = a₂), b₁ = b₂
Tactic: rwa [h, (single_injective a₂).eq_iff] at eq
Cleared hypotheses: eq, h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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₂
⊢ b₁ = b₂
have pos₁ : ∀ (eq : b₁ = b₂) (h : a₁ = a₂), b₁ = b₂
Tactic: rwa [h, (single_injective a₂).eq_iff] at eq
Cleared hypotheses: eq, h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (hypothesis)
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
have eq₁ : ∀ (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
Cleared hypotheses: eq, h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (hypothesis)
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₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
have h₁ : Eq.{u_5 + 1} (α := M) ((single a₁ b₁ : (a : α) → M) a₁ : M) ((single a₂ b₂ : (a : α) → M) a₁ : M)
Tactic: have h₁ := eq a₁
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (hypothesis)
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)
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
have h₂ : Eq.{u_5 + 1} (α := M) ((single a₁ b₁ : (a : α) → M) a₂ : M) ((single a₂ b₂ : (a : α) → M) a₂ : M)
Tactic: have h₂ := eq a₂
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a₁ a₂ : α
b₁ b₂ : M
⊢ Eq (α := α →₀ M) (single a₁ b₁) (single a₂ b₂) ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
have mp : 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
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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
⊢ Eq (α := α →₀ M) (single a₁ b₁) (single a₂ b₂) ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
have mpr : a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0 → Eq (α := α →₀ M) (single a₁ b₁) (single a₂ b₂)
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
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
b b' : M
hb : b ≠ 0
hb' : b' ≠ 0
i j : α
⊢ Disjoint (support (single i b)) (support (single j b')) ↔ i ≠ j
have rw : Disjoint {i} (support (single j b')) ↔ i ≠ j
Tactic: rw [support_single _ hb, support_single _ hb', disjoint_singleton]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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
⊢ Disjoint (support (single i b)) (support (single j b')) ↔ i ≠ j
have rw₁ : Disjoint (α := Finset α) {i} {j} ↔ i ≠ j
Tactic: rw [support_single _ hb, support_single _ hb', disjoint_singleton]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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
⊢ Disjoint (support (single i b)) (support (single j b')) ↔ i ≠ j
have rw₂ : i ≠ j ↔ i ≠ j
Tactic: rw [support_single _ hb, support_single _ hb', disjoint_singleton]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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
⊢ Nontrivial (α →₀ M)
have inhabit : ∀ (inhabited_h : Inhabited α), Nontrivial (α →₀ M)
Tactic: inhabit α
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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 α
⊢ Nontrivial (α →₀ M)
have rcases : ∀ (x : M) (hx : x ≠ 0), Nontrivial (α →₀ M)
Tactic: rcases exists_ne (0 : M) with ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f g : α →₀ M
hfg : f ≠ g
⊢ Nonempty α ∧ Nontrivial M
have obtain : ∀ (a : α) (ha : Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) ((g : (a : α) → M) a : M)), Nonempty α ∧ Nontrivial M
Tactic: obtain ⟨a, ha⟩ := ne_iff.mp hfg
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a a' : α
b : M
inst_1 : Unique α
b' : M
⊢ Eq (α := α →₀ M) (single a b) (single a' b') ↔ b = b'
have rw : Eq.{u_5 + 1} (α := M) ((single a b : (a : α) → M) default : M) ((single a' b' : (a : α) → M) default : M) ↔ b = b'
Tactic: rw [Finsupp.unique_ext_iff, Unique.eq_default a, Unique.eq_default a', single_eq_same,
    single_eq_same]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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'
⊢ Eq (α := α →₀ M) (single a b) (single a' b') ↔ b = b'
have rw₁ : Eq.{u_5 + 1} (α := M) ((single default b : (a : α) → M) default : M) ((single a' b' : (a : α) → M) default : M) ↔ b = b'
Tactic: rw [Finsupp.unique_ext_iff, Unique.eq_default a, Unique.eq_default a', single_eq_same,
    single_eq_same]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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'
⊢ Eq (α := α →₀ M) (single a b) (single a' b') ↔ b = b'
have rw₂ : Eq.{u_5 + 1} (α := M) ((single default b : (a : α) → M) default : M) ((single default b' : (a : α) → M) default : M) ↔
  b = b'
Tactic: rw [Finsupp.unique_ext_iff, Unique.eq_default a, Unique.eq_default a', single_eq_same,
    single_eq_same]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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'
⊢ Eq (α := α →₀ M) (single a b) (single a' b') ↔ b = b'
have rw₃ : b = (single default b' : (a : α) → M) default ↔ b = b'
Tactic: rw [Finsupp.unique_ext_iff, Unique.eq_default a, Unique.eq_default a', single_eq_same,
    single_eq_same]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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'
⊢ Eq (α := α →₀ M) (single a b) (single a' b') ↔ b = b'
have rw₄ : b = b' ↔ b = b'
Tactic: rw [Finsupp.unique_ext_iff, Unique.eq_default a, Unique.eq_default a', single_eq_same,
    single_eq_same]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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
⊢ f.support ⊆ {a}
have rw : support (single a b) ⊆ {a}
Tactic: rw [hb, support_subset_singleton, single_eq_same]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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}
⊢ f.support ⊆ {a}
have rw₁ : Eq (α := α →₀ M) (single a b) (single a ((single a b : (a : α) → M) a))
Tactic: rw [hb, support_subset_singleton, single_eq_same]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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))
⊢ f.support ⊆ {a}
have rw₂ : Eq (α := α →₀ M) (single a b) (single a b)
Tactic: rw [hb, support_subset_singleton, single_eq_same]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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
⊢ single a ((fun (f : α →₀ M) ↦ ((f : (a : α) → M) a : M)) f) = f
have 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)
Tactic: ext b
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
inst_2 : Finite α
x : α
m : M
⊢ Eq (α := α →₀ M)
    ((Equiv.symm equivFunOnFinite : (a : α → M) → α →₀ M) (Pi.single (M := fun (a : α) ↦ M) x m) : α →₀ M)
    (single x m : α →₀ M)
have rw : Eq (α := α →₀ M)
  ((Equiv.symm equivFunOnFinite : (a : α → M) → α →₀ M) ((equivFunOnFinite : (a : α →₀ M) → α → M) (single x m)) :
    α →₀ M)
  (single x m : α →₀ M)
Tactic: rw [← equivFunOnFinite_single, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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)
⊢ Eq (α := α →₀ M)
    ((Equiv.symm equivFunOnFinite : (a : α → M) → α →₀ M) (Pi.single (M := fun (a : α) ↦ M) x m) : α →₀ M)
    (single x m : α →₀ M)
have rw₁ : Eq (α := α →₀ M) (single x m) (single x m)
Tactic: rw [← equivFunOnFinite_single, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
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
⊢ Finset α
have haveI : (this : DecidableEq α) → Finset α
Tactic: haveI := Classical.decEq α