awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this : DecidableEq α
⊢ Finset α
have haveI : (this : DecidableEq M) → Finset α
Tactic: haveI := Classical.decEq M
-- 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
i : α
inst_1 : DecidableEq α
⊢ (f.update a b : (a : α) → M) i = if i = a then b else (f : (a : α) → M) i
have 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 sorry else (f : (a : α) → M) a_1,
        mem_support_toFun := sorry } :
      (a : α) → M)
    i =
  if i = a then b else (f : (a : α) → M) i
Tactic: delta update Function.update
-- 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 a' : α
f : α →₀ M
⊢ Eq.{u_5 + 1} (α := M) ((erase a f : (a : α) → M) a' : M) (if a' = a then 0 else (f : (a : α) → M) a' : M)
have rw : Eq.{u_5 + 1} (α := M) (if a' = a then 0 else (f : (a : α) → M) a' : M) (if a' = a then 0 else (f : (a : α) → M) a' : M)
Tactic: rw [erase, coe_mk]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
⊢ map f l.support = {a}
have rw : (embDomain f l).support = {a}
Tactic: rw [← support_embDomain, h, support_single _ hb]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
rw : (embDomain f l).support = {a}
⊢ map f l.support = {a}
have rw₁ : support (single a b) = {a}
Tactic: rw [← support_embDomain, h, support_single _ hb]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
rw : (embDomain f l).support = {a}
rw₁ : support (single a b) = {a}
⊢ map f l.support = {a}
have rw₂ : Eq (α := Finset β) {a} {a}
Tactic: rw [← support_embDomain, h, support_single _ hb]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (hypothesis)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
⊢ ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
have h_map_support : map f l.support = {a}
Tactic: have h_map_support : Finset.map f l.support = {a} := by
      rw [← support_embDomain, h, support_single _ hb]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (hypothesis)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
⊢ ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
have ha : a ∈ map f l.support
Tactic: have ha : a ∈ Finset.map f l.support := by simp only [h_map_support, Finset.mem_singleton]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
⊢ ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
have rcases : ∀ (c : α) (_hc₁ : c ∈ l.support) (hc₂ : (f : (a : α) → β) c = a), ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
Tactic: rcases Finset.mem_map.1 ha with ⟨c, _hc₁, hc₂⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : (f : (a : α) → β) c = a
⊢ ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
have h₁ : l = single c b ∧ (f : (a : α) → β) c = a
Tactic: use c
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : (f : (a : α) → β) c = a
⊢ l = single c b ∧ (f : (a : α) → β) c = a
have h₁ : l = single c b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : (f : (a : α) → β) c = a
⊢ l = single c b
have h₁ : ∀ (d : α), Eq.{u_5 + 1} (α := M) ((l : (a : α) → M) d : M) ((single c b : (a : α) → M) d : M)
Tactic: ext d
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : (f : (a : α) → β) c = a
d : α
⊢ Eq.{u_5 + 1} (α := M) ((l : (a : α) → M) d : M) ((single c b : (a : α) → M) d : M)
have h₁ : Eq.{u_5 + 1} (α := M) ((single a b : (a : β) → M) ((f : (a : α) → β) d : β) : M) ((single c b : (a : α) → M) d : M)
Tactic: rw [← embDomain_apply_self f l, h]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
⊢ ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
have have : map f l.support = {a}
Tactic: classical
    have h_map_support : Finset.map f l.support = {a} := by
      rw [← support_embDomain, h, support_single _ hb]
    have ha : a ∈ Finset.map f l.support := by simp only [h_map_support, Finset.mem_singleton]
    rcases Finset.mem_map.1 ha with ⟨c, _hc₁, hc₂⟩
    use c
    constructor
    · ext d
      rw [← embDomain_apply_self f l, h]
      grind
    · exact hc₂
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
have : map f l.support = {a}
⊢ ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
have have₁ : ∀ (h_map_support : map f l.support = {a}), ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
Tactic: classical
    have h_map_support : Finset.map f l.support = {a} := by
      rw [← support_embDomain, h, support_single _ hb]
    have ha : a ∈ Finset.map f l.support := by simp only [h_map_support, Finset.mem_singleton]
    rcases Finset.mem_map.1 ha with ⟨c, _hc₁, hc₂⟩
    use c
    constructor
    · ext d
      rw [← embDomain_apply_self f l, h]
      grind
    · exact hc₂
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
have : map f l.support = {a}
have₁ : ∀ (h_map_support : map f l.support = {a}), ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
have₂ : map f l.support = {a}
have₃ have₄ : ∀ (h_map_support : map f l.support = {a}), ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
⊢ ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
have have₅ : ∀ (h_map_support : map f l.support = {a}) (ha : a ∈ map f l.support),
  ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
Tactic: classical
    have h_map_support : Finset.map f l.support = {a} := by
      rw [← support_embDomain, h, support_single _ hb]
    have ha : a ∈ Finset.map f l.support := by simp only [h_map_support, Finset.mem_singleton]
    rcases Finset.mem_map.1 ha with ⟨c, _hc₁, hc₂⟩
    use c
    constructor
    · ext d
      rw [← embDomain_apply_self f l, h]
      grind
    · exact hc₂
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
have : map f l.support = {a}
have₁ : ∀ (h_map_support : map f l.support = {a}), ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
have₂ : map f l.support = {a}
have₃ have₄ : ∀ (h_map_support : map f l.support = {a}), ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
have₅ :
  ∀ (h_map_support : map f l.support = {a}) (ha : a ∈ map f l.support),
    ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
⊢ ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
have have₆ : ∀ (h_map_support : map f l.support = {a}) (ha : a ∈ map f l.support) (c : α) (_hc₁ : c ∈ l.support)
  (hc₂ : (f : (a : α) → β) c = a), ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
Tactic: classical
    have h_map_support : Finset.map f l.support = {a} := by
      rw [← support_embDomain, h, support_single _ hb]
    have ha : a ∈ Finset.map f l.support := by simp only [h_map_support, Finset.mem_singleton]
    rcases Finset.mem_map.1 ha with ⟨c, _hc₁, hc₂⟩
    use c
    constructor
    · ext d
      rw [← embDomain_apply_self f l, h]
      grind
    · exact hc₂
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
have : map f l.support = {a}
have₁ : ∀ (h_map_support : map f l.support = {a}), ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
have₂ : map f l.support = {a}
have₃ have₄ : ∀ (h_map_support : map f l.support = {a}), ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
have₅ :
  ∀ (h_map_support : map f l.support = {a}) (ha : a ∈ map f l.support),
    ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
have₆ :
  ∀ (h_map_support : map f l.support = {a}) (ha : a ∈ map f l.support) (c : α) (_hc₁ : c ∈ l.support)
    (hc₂ : (f : (a : α) → β) c = a), ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
⊢ ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
have h₁ : ∀ (h_map_support : map f l.support = {a}) (ha : a ∈ map f l.support) (c : α) (_hc₁ : c ∈ l.support)
  (hc₂ : (f : (a : α) → β) c = a), l = single c b ∧ (f : (a : α) → β) c = a
Tactic: classical
    have h_map_support : Finset.map f l.support = {a} := by
      rw [← support_embDomain, h, support_single _ hb]
    have ha : a ∈ Finset.map f l.support := by simp only [h_map_support, Finset.mem_singleton]
    rcases Finset.mem_map.1 ha with ⟨c, _hc₁, hc₂⟩
    use c
    constructor
    · ext d
      rw [← embDomain_apply_self f l, h]
      grind
    · exact hc₂
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
have : map f l.support = {a}
have₁ : ∀ (h_map_support : map f l.support = {a}), ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
have₂ : map f l.support = {a}
have₃ have₄ : ∀ (h_map_support : map f l.support = {a}), ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
have₅ :
  ∀ (h_map_support : map f l.support = {a}) (ha : a ∈ map f l.support),
    ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
have₆ :
  ∀ (h_map_support : map f l.support = {a}) (ha : a ∈ map f l.support) (c : α) (_hc₁ : c ∈ l.support)
    (hc₂ : (f : (a : α) → β) c = a), ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
h₁ :
  ∀ (h_map_support : map f l.support = {a}) (ha : a ∈ map f l.support) (c : α) (_hc₁ : c ∈ l.support)
    (hc₂ : (f : (a : α) → β) c = a), l = single c b ∧ (f : (a : α) → β) c = a
⊢ ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
have h₂ : ∀ (h_map_support : map f l.support = {a}) (ha : a ∈ map f l.support) (c : α) (_hc₁ : c ∈ l.support)
  (hc₂ : (f : (a : α) → β) c = a), l = single c b
Tactic: classical
    have h_map_support : Finset.map f l.support = {a} := by
      rw [← support_embDomain, h, support_single _ hb]
    have ha : a ∈ Finset.map f l.support := by simp only [h_map_support, Finset.mem_singleton]
    rcases Finset.mem_map.1 ha with ⟨c, _hc₁, hc₂⟩
    use c
    constructor
    · ext d
      rw [← embDomain_apply_self f l, h]
      grind
    · exact hc₂
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
have : map f l.support = {a}
have₁ : ∀ (h_map_support : map f l.support = {a}), ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
have₂ : map f l.support = {a}
have₃ have₄ : ∀ (h_map_support : map f l.support = {a}), ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
have₅ :
  ∀ (h_map_support : map f l.support = {a}) (ha : a ∈ map f l.support),
    ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
have₆ :
  ∀ (h_map_support : map f l.support = {a}) (ha : a ∈ map f l.support) (c : α) (_hc₁ : c ∈ l.support)
    (hc₂ : (f : (a : α) → β) c = a), ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
h₁ :
  ∀ (h_map_support : map f l.support = {a}) (ha : a ∈ map f l.support) (c : α) (_hc₁ : c ∈ l.support)
    (hc₂ : (f : (a : α) → β) c = a), l = single c b ∧ (f : (a : α) → β) c = a
h₂ :
  ∀ (h_map_support : map f l.support = {a}) (ha : a ∈ map f l.support) (c : α) (_hc₁ : c ∈ l.support)
    (hc₂ : (f : (a : α) → β) c = a), l = single c b
⊢ ∃ (x : α), l = single x b ∧ (f : (a : α) → β) x = a
have h₃ : ∀ (h_map_support : map f l.support = {a}) (ha : a ∈ map f l.support) (c : α) (_hc₁ : c ∈ l.support)
  (hc₂ : (f : (a : α) → β) c = a), (f : (a : α) → β) c = a
Tactic: classical
    have h_map_support : Finset.map f l.support = {a} := by
      rw [← support_embDomain, h, support_single _ hb]
    have ha : a ∈ Finset.map f l.support := by simp only [h_map_support, Finset.mem_singleton]
    rcases Finset.mem_map.1 ha with ⟨c, _hc₁, hc₂⟩
    use c
    constructor
    · ext d
      rw [← embDomain_apply_self f l, h]
      grind
    · exact hc₂
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ↪ β
a : α
m : M
⊢ Eq (α := β →₀ M) (embDomain f (single a m)) (single ((f : (a : α) → β) a) m)
have h : ∀ (b : β),
  Eq.{u_5 + 1} (α := M) ((embDomain f (single a m) : (a : β) → M) b : M)
    (((single ((f : (a : α) → β) a) m : β →₀ M) : (a : β) → M) b : M)
Tactic: ext b
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ↪ β
a : α
m : M
b : β
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f (single a m) : (a : β) → M) b : M)
    (((single ((f : (a : α) → β) a) m : β →₀ M) : (a : β) → M) b : M)
have pos : ∀ (h : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b),
  Eq.{u_5 + 1} (α := M) ((embDomain f (single a m) : (a : β) → M) b : M)
    (((single ((f : (a : α) → β) a) m : β →₀ M) : (a : β) → M) b : M)
Tactic: by_cases h : b ∈ Set.range f
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ↪ β
a : α
m : M
b : β
pos :
  ∀ (h : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b),
    Eq.{u_5 + 1} (α := M) ((embDomain f (single a m) : (a : β) → M) b : M)
      (((single ((f : (a : α) → β) a) m : β →₀ M) : (a : β) → M) b : M)
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f (single a m) : (a : β) → M) b : M)
    (((single ((f : (a : α) → β) a) m : β →₀ M) : (a : β) → M) b : M)
have neg : ∀ (h : b ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)),
  Eq.{u_5 + 1} (α := M) ((embDomain f (single a m) : (a : β) → M) b : M)
    (((single ((f : (a : α) → β) a) m : β →₀ M) : (a : β) → M) b : M)
Tactic: by_cases h : b ∈ Set.range f
-- Lean 4 proof step from Mathlib.Data.Finsupp.Single (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ↪ β
a : α
m : M
⊢ Eq (α := β →₀ M) (embDomain f (single a m)) (single ((f : (a : α) → β) a) m)
have h : ∀ (b : β),
  Eq.{u_5 + 1} (α := M) ((embDomain f (single a m) : (a : β) → M) b : M)
    (((single ((f : (a : α) → β) a) m : β →₀ M) : (a : β) → M) b : M)
Tactic: classical
    ext b
    by_cases h : b ∈ Set.range f <;> grind
-- Lean 4 proof step from Mathlib.Data.Finsupp.ToDFinsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : Zero M
i : ι
m : M
⊢ Eq (α := Π₀ (x : ι), M) (toDFinsupp (single i m)) (DFinsupp.single (β := fun (i : ι) ↦ M) i m)
have h : ∀ (i_1 : ι),
  (toDFinsupp (single i m) : (a : ι) → M) i_1 = (DFinsupp.single (β := fun (i : ι) ↦ M) i m : (a : ι) → M) i_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.ToDFinsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : Zero M
inst_2 : (m : M) → Decidable (m ≠ 0)
f : ι →₀ M
⊢ f.toDFinsupp.support (β := fun (x : ι) ↦ M) = f.support
have h : ∀ (a : ι), a ∈ f.toDFinsupp.support (β := fun (x : ι) ↦ M) ↔ a ∈ f.support
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.ToDFinsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : Zero M
inst_2 : (m : M) → Decidable (m ≠ 0)
f : Π₀ (x : ι), M
⊢ f.toFinsupp.support = f.support (β := fun (x : ι) ↦ M)
have h : ∀ (a : ι), a ∈ f.toFinsupp.support ↔ a ∈ f.support (β := fun (x : ι) ↦ M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.ToDFinsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : Zero M
inst_2 : (m : M) → Decidable (m ≠ 0)
i : ι
m : M
⊢ Eq (α := ι →₀ M) (toFinsupp (single (β := fun (x : ι) ↦ M) i m)) (Finsupp.single i m)
have h : ∀ (a : ι),
  Eq.{u_3 + 1} (α := M) ((toFinsupp (single (β := fun (x : ι) ↦ M) i m) : (a : ι) → M) a : M)
    ((Finsupp.single i m : (a : ι) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.ToDFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Zero N
f : (i : ι) × η i →₀ N
i : ι
⊢ i ∈ f.splitSupport (αs := η).val ∨ f.split (αs := η) i = 0
have rw : f.split (αs := η) i ≠ 0 ∨ f.split (αs := η) i = 0
Tactic: rw [← Finset.mem_def, mem_splitSupport_iff_nonzero]
-- Lean 4 proof step from Mathlib.Data.Finsupp.ToDFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Zero N
f : Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N
⊢ (i : ι) × η i →₀ N
have haveI : (this : DecidableEq ι) → (i : ι) × η i →₀ N
Tactic: haveI := Classical.decEq ι
-- Lean 4 proof step from Mathlib.Data.Finsupp.ToDFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Zero N
f : Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N
this : DecidableEq ι
⊢ (i : ι) × η i →₀ N
have haveI : (this : (i : ι) → DecidableEq (Finsupp.{u_4, u_5} (η i) N)) → (i : ι) × η i →₀ N
Tactic: haveI := fun i => Classical.decEq (η i →₀ N)
-- Lean 4 proof step from Mathlib.Data.Finsupp.ToDFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Zero N
f : Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N
this_1 : DecidableEq ι
this : (i : ι) → DecidableEq (Finsupp.{u_4, u_5} (η i) N)
⊢ (i : ι) × η i →₀ N
have onFinset : ∀ (g : (i : ι) × η i)
  (hg :
    Ne.{u_5 + 1} (α := N)
      ((fun (ji : (i : ι) × η i) ↦
          (((f : (a : ι) → η a →₀ N) (ji.fst (β := fun (i : ι) ↦ η i)) : (a : η ji.fst) → N)
              (ji.snd (β := fun (i : ι) ↦ η i)) :
            N))
        g)
      0),
  g.fst (β := fun (i : ι) ↦ η i) ∈ f.support (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
Tactic: refine
      onFinset (Finset.sigma f.support fun j => (f j).support) (fun ji => f ji.1 ji.2) fun g hg =>
        Finset.mem_sigma.mpr ⟨?_, mem_support_iff.mpr hg⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.ToDFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Zero N
f : Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N
this_1 : DecidableEq ι
this : (i : ι) → DecidableEq (Finsupp.{u_4, u_5} (η i) N)
g : (i : ι) × η i
hg :
  Ne.{u_5 + 1} (α := N)
    ((fun (ji : (i : ι) × η i) ↦
        (((f : (a : ι) → η a →₀ N) (ji.fst (β := fun (i : ι) ↦ η i)) : (a : η ji.fst) → N)
            (ji.snd (β := fun (i : ι) ↦ η i)) :
          N))
      g)
    0
⊢ g.fst (β := fun (i : ι) ↦ η i) ∈ f.support (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
have simp : ¬Eq (α := Finsupp.{u_4, u_5} (η (g.fst (β := fun (i : ι) ↦ η i))) N)
    ((f : (a : ι) → η a →₀ N) (g.fst (β := fun (i : ι) ↦ η i))) 0
Tactic: simp only [Ne, DFinsupp.mem_support_toFun]
-- Lean 4 proof step from Mathlib.Data.Finsupp.ToDFinsupp (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Zero N
f : Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N
this_1 : DecidableEq ι
this : (i : ι) → DecidableEq (Finsupp.{u_4, u_5} (η i) N)
g : (i : ι) × η i
hg :
  ¬Eq.{u_5 + 1} (α := N)
      (((f : (a : ι) → η a →₀ N) (g.fst (β := fun (i : ι) ↦ η i)) : (a : η g.fst) → N)
          (g.snd (β := fun (i : ι) ↦ η i)) :
        N)
      (0 : N)
h :
  Eq (α := Finsupp.{u_4, u_5} (η (g.fst (β := fun (i : ι) ↦ η i))) N)
    ((f : (a : ι) → η a →₀ N) (g.fst (β := fun (i : ι) ↦ η i))) 0
⊢ False
have hg₁ : ¬Eq.{u_5 + 1} (α := N) ((0 : (a : η g.fst) → N) (g.snd (β := fun (i : ι) ↦ η i)) : N) (0 : N)
Tactic: rw [h] at hg
Cleared hypotheses: hg, h
-- Lean 4 proof step from Mathlib.Data.Finsupp.ToDFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Zero N
f : (i : ι) × η i →₀ N
⊢ (fun (f : Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) ↦
        (onFinset
            (f.support (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N).sigma (α := η) fun (j : ι) ↦
              ((f : (a : ι) → η a →₀ N) j).support)
            (fun (ji : (i : ι) × η i) ↦
              ((f : (a : ι) → η a →₀ N) (ji.fst (β := fun (i : ι) ↦ η i)) : (a : η ji.fst) → N)
                (ji.snd (β := fun (i : ι) ↦ η i)))
            ⋯ :
          (i : ι) × η i →₀ N))
      ((fun (f : (i : ι) × η i →₀ N) ↦
          (DFinsupp.mk' (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N) (f.split (αs := η))
              (Trunc.mk
                (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f.split (αs := η) i = 0)
                  f.splitSupport (αs := η).val ⋯)) :
            Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N))
        f) =
    f
have h : ∀ (a : (i : ι) × η i),
  Eq.{u_5 + 1} (α := N)
    (((fun (f : Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) ↦
              (onFinset
                  (f.support (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N).sigma (α := η) fun (j : ι) ↦
                    ((f : (a : ι) → η a →₀ N) j).support)
                  (fun (ji : (i : ι) × η i) ↦
                    ((f : (a : ι) → η a →₀ N) (ji.fst (β := fun (i : ι) ↦ η i)) : (a : η ji.fst) → N)
                      (ji.snd (β := fun (i : ι) ↦ η i)))
                  sorry :
                (i : ι) × η i →₀ N))
            ((fun (f : (i : ι) × η i →₀ N) ↦
                (DFinsupp.mk' (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N) (f.split (αs := η))
                    (Trunc.mk
                      (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f.split (αs := η) i = 0)
                        f.splitSupport (αs := η).val sorry)) :
                  Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N))
              f) :
          (a : (i : ι) × η i) → N)
        a :
      N)
    ((f : (a : (i : ι) × η i) → N) a : N)
Tactic: ext