awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
hi : xi = 0
hj : xj = 0
mpr : Eq (α := Π₀ (i : ι), β i) (single (β := β) i 0) (single (β := β) j xj)
⊢ Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
have mpr₁ : Eq (α := Π₀ (i : ι), β i) (single (β := β) i 0) (single (β := β) j 0)
Tactic: rw [hi, hj, DFinsupp.single_zero, DFinsupp.single_zero]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
hi : xi = 0
hj : xj = 0
mpr : Eq (α := Π₀ (i : ι), β i) (single (β := β) i 0) (single (β := β) j xj)
mpr₁ : Eq (α := Π₀ (i : ι), β i) (single (β := β) i 0) (single (β := β) j 0)
⊢ Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
have mpr₂ : Eq (α := Π₀ (i : ι), β i) 0 (single (β := β) j 0)
Tactic: rw [hi, hj, DFinsupp.single_zero, DFinsupp.single_zero]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
hi : xi = 0
hj : xj = 0
mpr : Eq (α := Π₀ (i : ι), β i) (single (β := β) i 0) (single (β := β) j xj)
mpr₁ : Eq (α := Π₀ (i : ι), β i) (single (β := β) i 0) (single (β := β) j 0)
mpr₂ : Eq (α := Π₀ (i : ι), β i) 0 (single (β := β) j 0)
⊢ Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
have mpr₃ : Eq (α := Π₀ (i : ι), β i) 0 0
Tactic: rw [hi, hj, DFinsupp.single_zero, DFinsupp.single_zero]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i : ι
xi : β i
⊢ Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) 0 ↔ xi = 0
have rw : i = i ∧ HEq xi (β := β i) 0 ∨ xi = 0 ∧ Eq.{v + 1} (α := β i) 0 0 ↔ xi = 0
Tactic: rw [← single_zero i, single_eq_single_iff]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
p : ι → Prop
inst_2 : DecidablePred p
i : ι
x : β i
⊢ Eq (α := Π₀ (i : ι), β i) (filter (β := β) p (single (β := β) i x)) (if p i then single (β := β) i x else 0)
have h : ∀ (j : ι),
  (filter (β := β) p (single (β := β) i x) : (a : ι) → β a) j =
    (if p i then single (β := β) i x else 0 : (a : ι) → β a) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (hypothesis)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
p : ι → Prop
inst_2 : DecidablePred p
i : ι
x : β i
j : ι
⊢ (filter (β := β) p (single (β := β) i x) : (a : ι) → β a) j =
    (if p i then single (β := β) i x else 0 : (a : ι) → β a) j
have this : (if p i then single (β := β) i x else 0 : (a : ι) → β a) j =
  if p i then (single (β := β) i x : (a : ι) → β a) j else (0 : (a : ι) → β a) j
Tactic: have := apply_ite (fun x : Π₀ i, β i => x j) (p i) (single i x) 0
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
p : ι → Prop
inst_2 : DecidablePred p
i : ι
x : β i
h : p i
⊢ Eq (α := Π₀ (i : ι), β i) (filter (β := β) p (single (β := β) i x)) (single (β := β) i x)
have rw : Eq (α := Π₀ (i : ι), β i) (if p i then single (β := β) i x else 0) (single (β := β) i x)
Tactic: rw [filter_single, if_pos h]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
p : ι → Prop
inst_2 : DecidablePred p
i : ι
x : β i
h : p i
rw : Eq (α := Π₀ (i : ι), β i) (if p i then single (β := β) i x else 0) (single (β := β) i x)
⊢ Eq (α := Π₀ (i : ι), β i) (filter (β := β) p (single (β := β) i x)) (single (β := β) i x)
have rw₁ : Eq (α := Π₀ (i : ι), β i) (single (β := β) i x) (single (β := β) i x)
Tactic: rw [filter_single, if_pos h]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
p : ι → Prop
inst_2 : DecidablePred p
i : ι
x : β i
h : ¬p i
⊢ Eq (α := Π₀ (i : ι), β i) (filter (β := β) p (single (β := β) i x)) 0
have rw : Eq (α := Π₀ (i : ι), β i) (if p i then single (β := β) i x else 0) 0
Tactic: rw [filter_single, if_neg h]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
p : ι → Prop
inst_2 : DecidablePred p
i : ι
x : β i
h : ¬p i
rw : Eq (α := Π₀ (i : ι), β i) (if p i then single (β := β) i x else 0) 0
⊢ Eq (α := Π₀ (i : ι), β i) (filter (β := β) p (single (β := β) i x)) 0
have rw₁ : Eq (α := Π₀ (i : ι), β i) 0 0
Tactic: rw [filter_single, if_neg h]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : Sigma.mk (β := β) i xi = Sigma.mk (β := β) j xj
⊢ Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
have refl : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) i xi)
Tactic: cases h
Cleared hypotheses: j, xj, h
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
⊢ filter (β := β) (fun (x : ι) ↦ i = x) f = single (β := β) i ((f : (a : ι) → β a) i)
have h : ∀ (i_1 : ι),
  (filter (β := β) (fun (x : ι) ↦ i = x) f : (a : ι) → β a) i_1 =
    (single (β := β) i ((f : (a : ι) → β a) i) : (a : ι) → β a) i_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i i_1 : ι
⊢ (filter (β := β) (fun (x : ι) ↦ i = x) f : (a : ι) → β a) i_1 =
    (single (β := β) i ((f : (a : ι) → β a) i) : (a : ι) → β a) i_1
have h : (if i = i_1 then (f : (a : ι) → β a) i_1 else 0) =
  if h : i = i_1 then Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ β x) h ((f : (a : ι) → β a) i) else 0
Tactic: rw [filter_apply, single_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i i_1 : ι
⊢ (if i = i_1 then (f : (a : ι) → β a) i_1 else 0) =
    if h : i = i_1 then Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ β x) h ((f : (a : ι) → β a) i) else 0
have h : ∀ (h : i = i_1),
  (f : (a : ι) → β a) i_1 = Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ β x) h ((f : (a : ι) → β a) i)
Tactic: split
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i i_1 : ι
h :
  ∀ (h : i = i_1),
    (f : (a : ι) → β a) i_1 = Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ β x) h ((f : (a : ι) → β a) i)
⊢ (if i = i_1 then (f : (a : ι) → β a) i_1 else 0) =
    if h : i = i_1 then Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ β x) h ((f : (a : ι) → β a) i) else 0
have h₁ : ¬i = i_1 → Eq.{v + 1} (α := β i_1) 0 0
Tactic: split
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i i_1 : ι
h : i = i_1
⊢ (f : (a : ι) → β a) i_1 = Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ β x) h ((f : (a : ι) → β a) i)
have h : (f : (a : ι) → β a) i_1 = Eq.recOn (motive := fun (x : ι) (x_1 : i_1 = x) ↦ β x) sorry ((f : (a : ι) → β a) i_1)
Tactic: subst i
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
x : Π₀ (i : ι), β i
i : ι
⊢ piecewise (β := β) (single (β := β) i ((x : (a : ι) → β a) i)) (erase (β := β) i x) {i} = x
have h : ∀ (j : ι),
  (piecewise (β := β) (single (β := β) i ((x : (a : ι) → β a) i)) (erase (β := β) i x) {i} : (a : ι) → β a) j =
    (x : (a : ι) → β a) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
x : Π₀ (i : ι), β i
i j : ι
⊢ (piecewise (β := β) (single (β := β) i ((x : (a : ι) → β a) i)) (erase (β := β) i x) {i} : (a : ι) → β a) j =
    (x : (a : ι) → β a) j
have h : (if Membership.mem (γ := Set ι) {i} j then (single (β := β) i ((x : (a : ι) → β a) i) : (a : ι) → β a) j
  else (erase (β := β) i x : (a : ι) → β a) j) =
  (x : (a : ι) → β a) j
Tactic: rw [piecewise_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
x : Π₀ (i : ι), β i
i j : ι
⊢ (if Membership.mem (γ := Set ι) {i} j then (single (β := β) i ((x : (a : ι) → β a) i) : (a : ι) → β a) j
    else (erase (β := β) i x : (a : ι) → β a) j) =
    (x : (a : ι) → β a) j
have pos : ∀ (h : Membership.mem (γ := Set ι) {i} j),
  (single (β := β) i ((x : (a : ι) → β a) i) : (a : ι) → β a) j = (x : (a : ι) → β a) j
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
x : Π₀ (i : ι), β i
i j : ι
pos :
  ∀ (h : Membership.mem (γ := Set ι) {i} j),
    (single (β := β) i ((x : (a : ι) → β a) i) : (a : ι) → β a) j = (x : (a : ι) → β a) j
⊢ (if Membership.mem (γ := Set ι) {i} j then (single (β := β) i ((x : (a : ι) → β a) i) : (a : ι) → β a) j
    else (erase (β := β) i x : (a : ι) → β a) j) =
    (x : (a : ι) → β a) j
have neg : ∀ (h : j ∉ {i}), (erase (β := β) i x : (a : ι) → β a) j = (x : (a : ι) → β a) j
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
x : Π₀ (i : ι), β i
i j : ι
h : Membership.mem (γ := Set ι) {i} j
⊢ (single (β := β) i ((x : (a : ι) → β a) i) : (a : ι) → β a) j = (x : (a : ι) → β a) j
have pos : (single (β := β) i ((x : (a : ι) → β a) i) : (a : ι) → β a) i = (x : (a : ι) → β a) i
Tactic: rw [(id h : j = i), single_eq_same]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
x : Π₀ (i : ι), β i
i j : ι
h : Membership.mem (γ := Set ι) {i} j
pos : (single (β := β) i ((x : (a : ι) → β a) i) : (a : ι) → β a) i = (x : (a : ι) → β a) i
⊢ (single (β := β) i ((x : (a : ι) → β a) i) : (a : ι) → β a) j = (x : (a : ι) → β a) j
have pos₁ : (x : (a : ι) → β a) i = (x : (a : ι) → β a) i
Tactic: rw [(id h : j = i), single_eq_same]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
inst : DecidableEq ι
β : ι → Type u_1
inst_1 : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i : ι
⊢ erase (β := β) i f = f - single (β := β) i ((f : (a : ι) → β a) i)
have h : ∀ (j : ι), (erase (β := β) i f : (a : ι) → β a) j = (f - single (β := β) i ((f : (a : ι) → β a) i) : (a : ι) → β a) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
inst : DecidableEq ι
β : ι → Type u_1
inst_1 : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i j : ι
⊢ (erase (β := β) i f : (a : ι) → β a) j = (f - single (β := β) i ((f : (a : ι) → β a) i) : (a : ι) → β a) j
have h : (erase (β := β) j f : (a : ι) → β a) j = (f - single (β := β) j ((f : (a : ι) → β a) j) : (a : ι) → β a) j
Tactic: rcases eq_or_ne j i with (rfl | h)
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
inst : DecidableEq ι
β : ι → Type u_1
inst_1 : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i j : ι
h : (erase (β := β) j f : (a : ι) → β a) j = (f - single (β := β) j ((f : (a : ι) → β a) j) : (a : ι) → β a) j
⊢ (erase (β := β) i f : (a : ι) → β a) j = (f - single (β := β) i ((f : (a : ι) → β a) i) : (a : ι) → β a) j
have h₁ : ∀ (h : j ≠ i),
  (erase (β := β) i f : (a : ι) → β a) j = (f - single (β := β) i ((f : (a : ι) → β a) i) : (a : ι) → β a) j
Tactic: rcases eq_or_ne j i with (rfl | h)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
j i : ι
x : β i
⊢ Eq (α := Π₀ (i : ι), β i) (erase (β := β) j (single (β := β) i x)) (if i = j then 0 else single (β := β) i x)
have rw : Eq (α := Π₀ (i : ι), β i) (filter (β := β) (fun (x : ι) ↦ x ≠ j) (single (β := β) i x))
  (if i = j then 0 else single (β := β) i x)
Tactic: rw [← filter_ne_eq_erase, filter_single, ite_not]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
j i : ι
x : β i
rw :
  Eq (α := Π₀ (i : ι), β i) (filter (β := β) (fun (x : ι) ↦ x ≠ j) (single (β := β) i x))
    (if i = j then 0 else single (β := β) i x)
⊢ Eq (α := Π₀ (i : ι), β i) (erase (β := β) j (single (β := β) i x)) (if i = j then 0 else single (β := β) i x)
have rw₁ : Eq (α := Π₀ (i : ι), β i) (if i ≠ j then single (β := β) i x else 0) (if i = j then 0 else single (β := β) i x)
Tactic: rw [← filter_ne_eq_erase, filter_single, ite_not]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
j i : ι
x : β i
rw :
  Eq (α := Π₀ (i : ι), β i) (filter (β := β) (fun (x : ι) ↦ x ≠ j) (single (β := β) i x))
    (if i = j then 0 else single (β := β) i x)
rw₁ : Eq (α := Π₀ (i : ι), β i) (if i ≠ j then single (β := β) i x else 0) (if i = j then 0 else single (β := β) i x)
⊢ Eq (α := Π₀ (i : ι), β i) (erase (β := β) j (single (β := β) i x)) (if i = j then 0 else single (β := β) i x)
have rw₂ : Eq (α := Π₀ (i : ι), β i) (if i = j then 0 else single (β := β) i x) (if i = j then 0 else single (β := β) i x)
Tactic: rw [← filter_ne_eq_erase, filter_single, ite_not]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i : ι
x : β i
⊢ Eq (α := Π₀ (i : ι), β i) (erase (β := β) i (single (β := β) i x)) 0
have rw : Eq (α := Π₀ (i : ι), β i) (if i = i then 0 else single (β := β) i x) 0
Tactic: rw [erase_single, if_pos rfl]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i : ι
x : β i
rw : Eq (α := Π₀ (i : ι), β i) (if i = i then 0 else single (β := β) i x) 0
⊢ Eq (α := Π₀ (i : ι), β i) (erase (β := β) i (single (β := β) i x)) 0
have rw₁ : Eq (α := Π₀ (i : ι), β i) 0 0
Tactic: rw [erase_single, if_pos rfl]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
x : β i
h : i ≠ j
⊢ Eq (α := Π₀ (i : ι), β i) (erase (β := β) j (single (β := β) i x)) (single (β := β) i x)
have rw : Eq (α := Π₀ (i : ι), β i) (if i = j then 0 else single (β := β) i x) (single (β := β) i x)
Tactic: rw [erase_single, if_neg h]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
x : β i
h : i ≠ j
rw : Eq (α := Π₀ (i : ι), β i) (if i = j then 0 else single (β := β) i x) (single (β := β) i x)
⊢ Eq (α := Π₀ (i : ι), β i) (erase (β := β) j (single (β := β) i x)) (single (β := β) i x)
have rw₁ : Eq (α := Π₀ (i : ι), β i) (single (β := β) i x) (single (β := β) i x)
Tactic: rw [erase_single, if_neg h]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
b : β i
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0 }
j : ι
⊢ j ∈ i ::ₘ (↑s : Multiset ι) ∨ Function.update (β := β) (⇑f : (a : ι) → β a) i b j = 0
have inl : i ∈ i ::ₘ (↑s : Multiset ι) ∨ Function.update (β := β) (⇑f : (a : ι) → β a) i b i = 0
Tactic: rcases eq_or_ne i j with (rfl | hi)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
b : β i
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0 }
j : ι
inl : i ∈ i ::ₘ (↑s : Multiset ι) ∨ Function.update (β := β) (⇑f : (a : ι) → β a) i b i = 0
⊢ j ∈ i ::ₘ (↑s : Multiset ι) ∨ Function.update (β := β) (⇑f : (a : ι) → β a) i b j = 0
have inr : ∀ (hi : i ≠ j), j ∈ i ::ₘ (↑s : Multiset ι) ∨ Function.update (β := β) (⇑f : (a : ι) → β a) i b j = 0
Tactic: rcases eq_or_ne i j with (rfl | hi)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
b : β i
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0 }
j : ι
hi : i ≠ j
⊢ j ∈ i ::ₘ (↑s : Multiset ι) ∨ Function.update (β := β) (⇑f : (a : ι) → β a) i b j = 0
have inr : ∀ (hj : j ∈ (↑s : Multiset ι)), j ∈ i ::ₘ (↑s : Multiset ι) ∨ Function.update (β := β) (⇑f : (a : ι) → β a) i b j = 0
Tactic: obtain hj | (hj : f j = 0) := s.prop j
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
b : β i
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0 }
j : ι
hi : i ≠ j
inr :
  ∀ (hj : j ∈ (↑s : Multiset ι)), j ∈ i ::ₘ (↑s : Multiset ι) ∨ Function.update (β := β) (⇑f : (a : ι) → β a) i b j = 0
⊢ j ∈ i ::ₘ (↑s : Multiset ι) ∨ Function.update (β := β) (⇑f : (a : ι) → β a) i b j = 0
have inr₁ : ∀ (hj : (f : (a : ι) → β a) j = 0),
  j ∈ i ::ₘ (↑s : Multiset ι) ∨ Function.update (β := β) (⇑f : (a : ι) → β a) i b j = 0
Tactic: obtain hj | (hj : f j = 0) := s.prop j
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
⊢ f.update (β := β) i ((f : (a : ι) → β a) i) = f
have h : ∀ (i_1 : ι), (f.update (β := β) i ((f : (a : ι) → β a) i) : (a : ι) → β a) i_1 = (f : (a : ι) → β a) i_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
⊢ f.update (β := β) i 0 = erase (β := β) i f
have h : ∀ (j : ι), (f.update (β := β) i 0 : (a : ι) → β a) j = (erase (β := β) i f : (a : ι) → β a) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i j : ι
⊢ (f.update (β := β) i 0 : (a : ι) → β a) j = (erase (β := β) i f : (a : ι) → β a) j
have h : (f.update (β := β) i 0 : (a : ι) → β a) i = (erase (β := β) i f : (a : ι) → β a) i
Tactic: rcases eq_or_ne i j with (rfl | hi)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i j : ι
h : (f.update (β := β) i 0 : (a : ι) → β a) i = (erase (β := β) i f : (a : ι) → β a) i
⊢ (f.update (β := β) i 0 : (a : ι) → β a) j = (erase (β := β) i f : (a : ι) → β a) j
have h₁ : ∀ (hi : i ≠ j), (f.update (β := β) i 0 : (a : ι) → β a) j = (erase (β := β) i f : (a : ι) → β a) j
Tactic: rcases eq_or_ne i j with (rfl | hi)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
inst : DecidableEq ι
β : ι → Type u_1
inst_1 : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
⊢ f.update (β := β) i b = single (β := β) i b + erase (β := β) i f
have h : ∀ (j : ι), (f.update (β := β) i b : (a : ι) → β a) j = (single (β := β) i b + erase (β := β) i f : (a : ι) → β a) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
inst : DecidableEq ι
β : ι → Type u_1
inst_1 : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
j : ι
⊢ (f.update (β := β) i b : (a : ι) → β a) j = (single (β := β) i b + erase (β := β) i f : (a : ι) → β a) j
have h : (f.update (β := β) i b : (a : ι) → β a) i = (single (β := β) i b + erase (β := β) i f : (a : ι) → β a) i
Tactic: rcases eq_or_ne i j with (rfl | h)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
inst : DecidableEq ι
β : ι → Type u_1
inst_1 : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
j : ι
h : (f.update (β := β) i b : (a : ι) → β a) i = (single (β := β) i b + erase (β := β) i f : (a : ι) → β a) i
⊢ (f.update (β := β) i b : (a : ι) → β a) j = (single (β := β) i b + erase (β := β) i f : (a : ι) → β a) j
have h₁ : ∀ (h : i ≠ j), (f.update (β := β) i b : (a : ι) → β a) j = (single (β := β) i b + erase (β := β) i f : (a : ι) → β a) j
Tactic: rcases eq_or_ne i j with (rfl | h)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
inst : DecidableEq ι
β : ι → Type u_1
inst_1 : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
⊢ f.update (β := β) i b = erase (β := β) i f + single (β := β) i b
have h : ∀ (j : ι), (f.update (β := β) i b : (a : ι) → β a) j = (erase (β := β) i f + single (β := β) i b : (a : ι) → β a) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
inst : DecidableEq ι
β : ι → Type u_1
inst_1 : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
j : ι
⊢ (f.update (β := β) i b : (a : ι) → β a) j = (erase (β := β) i f + single (β := β) i b : (a : ι) → β a) j
have h : (f.update (β := β) i b : (a : ι) → β a) i = (erase (β := β) i f + single (β := β) i b : (a : ι) → β a) i
Tactic: rcases eq_or_ne i j with (rfl | h)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
inst : DecidableEq ι
β : ι → Type u_1
inst_1 : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
j : ι
h : (f.update (β := β) i b : (a : ι) → β a) i = (erase (β := β) i f + single (β := β) i b : (a : ι) → β a) i
⊢ (f.update (β := β) i b : (a : ι) → β a) j = (erase (β := β) i f + single (β := β) i b : (a : ι) → β a) j
have h₁ : ∀ (h : i ≠ j), (f.update (β := β) i b : (a : ι) → β a) j = (erase (β := β) i f + single (β := β) i b : (a : ι) → β a) j
Tactic: rcases eq_or_ne i j with (rfl | h)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
inst : DecidableEq ι
β : ι → Type u_1
inst_1 : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
⊢ f.update (β := β) i b = f - single (β := β) i ((f : (a : ι) → β a) i) + single (β := β) i b
have rw : erase (β := β) i f + single (β := β) i b = f - single (β := β) i ((f : (a : ι) → β a) i) + single (β := β) i b
Tactic: rw [update_eq_erase_add_single f i b, erase_eq_sub_single f i]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
inst : DecidableEq ι
β : ι → Type u_1
inst_1 : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
rw : erase (β := β) i f + single (β := β) i b = f - single (β := β) i ((f : (a : ι) → β a) i) + single (β := β) i b
⊢ f.update (β := β) i b = f - single (β := β) i ((f : (a : ι) → β a) i) + single (β := β) i b
have rw₁ : f - single (β := β) i ((f : (a : ι) → β a) i) + single (β := β) i b =
  f - single (β := β) i ((f : (a : ι) → β a) i) + single (β := β) i b
Tactic: rw [update_eq_erase_add_single f i b, erase_eq_sub_single f i]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
i : ι
f : Π₀ (i : ι), β i
i' : ι
h : i = i'
⊢ (single (β := β) i ((f : (a : ι) → β a) i) + erase (β := β) i f : (a : ι) → β a) i' = (f : (a : ι) → β a) i'
have subst : (single (β := β) i ((f : (a : ι) → β a) i) + erase (β := β) i f : (a : ι) → β a) i = (f : (a : ι) → β a) i
Tactic: subst h
Cleared hypotheses: i', h
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
i : ι
f : Π₀ (i : ι), β i
i' : ι
h : i = i'
⊢ (erase (β := β) i f + single (β := β) i ((f : (a : ι) → β a) i) : (a : ι) → β a) i' = (f : (a : ι) → β a) i'
have subst : (erase (β := β) i f + single (β := β) i ((f : (a : ι) → β a) i) : (a : ι) → β a) i = (f : (a : ι) → β a) i
Tactic: subst h
Cleared hypotheses: i', h