awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Surjective f
x : β →₀ M
⊢ mapDomain f (mapDomain (surjInv hf) x) = x
have h : mapDomain (f ∘ surjInv hf) x = x
Tactic: rw [← mapDomain_comp, (rightInverse_surjInv hf).id, mapDomain_id]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Surjective f
x : β →₀ M
h : mapDomain (f ∘ surjInv hf) x = x
⊢ mapDomain f (mapDomain (surjInv hf) x) = x
have h₁ : mapDomain id x = x
Tactic: rw [← mapDomain_comp, (rightInverse_surjInv hf).id, mapDomain_id]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Surjective f
x : β →₀ M
h : mapDomain (f ∘ surjInv hf) x = x
h₁ : mapDomain id x = x
⊢ mapDomain f (mapDomain (surjInv hf) x) = x
have h₂ : x = x
Tactic: rw [← mapDomain_comp, (rightInverse_surjInv hf).id, mapDomain_id]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_6
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
f : α → β
g : M →+ N
⊢ AddMonoidHom.comp (addMonoidHom f) (mapRange.addMonoidHom g) =
    AddMonoidHom.comp (mapRange.addMonoidHom g) (addMonoidHom f)
have H : ∀ (x : α) (x_1 : M) (a : β),
  Eq.{u_6 + 1} (α := N)
    (((((AddMonoidHom.comp (addMonoidHom f) (mapRange.addMonoidHom g)).comp (singleAddHom x) : (a : M) → β →₀ N) x_1 :
            β →₀ N) :
          (a : β) → N)
        a :
      N)
    (((((AddMonoidHom.comp (mapRange.addMonoidHom g) (addMonoidHom f)).comp (singleAddHom x) : (a : M) → β →₀ N) x_1 :
            β →₀ N) :
          (a : β) → N)
        a :
      N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : AddZeroClass α
inst_1 : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
⊢ (f.update i a).sum g + g i ((f : (a : ι) → α) i) = f.sum g + g i a
have rw : (erase i f).sum g + sum (single i a) g + g i ((f : (a : ι) → α) i) = f.sum g + g i a
Tactic: rw [update_eq_erase_add_single, sum_add_index' hg hgg]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : AddZeroClass α
inst_1 : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
| f.sum g + g i a
have rw : (f.update i ((f : (a : ι) → α) i)).sum g + g i a
Tactic: rw [← Finsupp.update_self f i]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : AddZeroClass α
inst_1 : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
⊢ (erase i f).sum g + sum (single i a) g + g i ((f : (a : ι) → α) i) = f.sum g + g i a
have conv_rhs : (erase i f).sum g + sum (single i a) g + g i ((f : (a : ι) → α) i) = (f.update i ((f : (a : ι) → α) i)).sum g + g i a
Tactic: conv_rhs => rw [← Finsupp.update_self f i]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : AddZeroClass α
inst_1 : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
⊢ (erase i f).sum g + sum (single i a) g + g i ((f : (a : ι) → α) i) = (f.update i ((f : (a : ι) → α) i)).sum g + g i a
have rw : (erase i f).sum g + (sum (single i a) g + g i ((f : (a : ι) → α) i)) =
  (erase i f).sum g + (sum (single i ((f : (a : ι) → α) i)) g + g i a)
Tactic: rw [update_eq_erase_add_single, sum_add_index' hg hgg, add_assoc, add_assoc]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : AddZeroClass α
inst_1 : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
⊢ (erase i f).sum g + (sum (single i a) g + g i ((f : (a : ι) → α) i)) =
    (erase i f).sum g + (sum (single i ((f : (a : ι) → α) i)) g + g i a)
have e_a : sum (single i a) g + g i ((f : (a : ι) → α) i) = sum (single i ((f : (a : ι) → α) i)) g + g i a
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : AddZeroClass α
inst_1 : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
⊢ sum (single i a) g + g i ((f : (a : ι) → α) i) = sum (single i ((f : (a : ι) → α) i)) g + g i a
have e_a : g i ((f : (a : ι) → α) i) + sum (single i a) g = sum (single i ((f : (a : ι) → α) i)) g + g i a
Tactic: rw [add_comm, sum_single_index (hg _), sum_single_index (hg _)]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : AddZeroClass α
inst_1 : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
e_a : g i ((f : (a : ι) → α) i) + sum (single i a) g = sum (single i ((f : (a : ι) → α) i)) g + g i a
⊢ sum (single i a) g + g i ((f : (a : ι) → α) i) = sum (single i ((f : (a : ι) → α) i)) g + g i a
have e_a₁ : g i ((f : (a : ι) → α) i) + g i a = sum (single i ((f : (a : ι) → α) i)) g + g i a
Tactic: rw [add_comm, sum_single_index (hg _), sum_single_index (hg _)]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : AddZeroClass α
inst_1 : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
e_a : g i ((f : (a : ι) → α) i) + sum (single i a) g = sum (single i ((f : (a : ι) → α) i)) g + g i a
e_a₁ : g i ((f : (a : ι) → α) i) + g i a = sum (single i ((f : (a : ι) → α) i)) g + g i a
⊢ sum (single i a) g + g i ((f : (a : ι) → α) i) = sum (single i ((f : (a : ι) → α) i)) g + g i a
have e_a₂ : g i ((f : (a : ι) → α) i) + g i a = g i ((f : (a : ι) → α) i) + g i a
Tactic: rw [add_comm, sum_single_index (hg _), sum_single_index (hg _)]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₁
v₂ : α →₀ M
hv₂ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₂
eq : mapDomain f v₁ = mapDomain f v₂
⊢ v₁ = v₂
have h : ∀ (a : α), Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₁
v₂ : α →₀ M
hv₂ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₂
eq : mapDomain f v₁ = mapDomain f v₂
a : α
⊢ Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)
have pos : ∀ (h : a ∈ v₁.support ∪ v₂.support), Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)
Tactic: by_cases h : a ∈ v₁.support ∪ v₂.support
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₁
v₂ : α →₀ M
hv₂ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₂
eq : mapDomain f v₁ = mapDomain f v₂
a : α
pos : ∀ (h : a ∈ v₁.support ∪ v₂.support), Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)
⊢ Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)
have neg : ∀ (h : a ∉ v₁.support ∪ v₂.support), Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)
Tactic: by_cases h : a ∈ v₁.support ∪ v₂.support
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₁
v₂ : α →₀ M
hv₂ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₂
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)
have rw : a ∈ S
Tactic: rw [← mapDomain_apply' S _ hv₁ hf _, ← mapDomain_apply' S _ hv₂ hf _, eq]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₁
v₂ : α →₀ M
hv₂ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₂
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ S
have a₁ : a ∈ (↑v₁.support : Set α) ∪ (↑v₂.support : Set α)
Tactic: apply Set.union_subset hv₁ hv₂
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₁
v₂ : α →₀ M
hv₂ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₂
eq : mapDomain f v₁ = mapDomain f v₂
a : α
⊢ Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)
have pos : ∀ (h : a ∈ v₁.support ∪ v₂.support), Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)
Tactic: classical
    by_cases h : a ∈ v₁.support ∪ v₂.support
    · rw [← mapDomain_apply' S _ hv₁ hf _, ← mapDomain_apply' S _ hv₂ hf _, eq] <;>
        · apply Set.union_subset hv₁ hv₂
          exact mod_cast h
    · simp_all
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₁
v₂ : α →₀ M
hv₂ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₂
eq : mapDomain f v₁ = mapDomain f v₂
a : α
pos : ∀ (h : a ∈ v₁.support ∪ v₂.support), Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)
⊢ Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)
have neg : ∀ (h : a ∉ v₁.support ∪ v₂.support), Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)
Tactic: classical
    by_cases h : a ∈ v₁.support ∪ v₂.support
    · rw [← mapDomain_apply' S _ hv₁ hf _, ← mapDomain_apply' S _ hv₂ hf _, eq] <;>
        · apply Set.union_subset hv₁ hv₂
          exact mod_cast h
    · simp_all
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_12
inst : AddCommMonoid M
f : α ≃ β
l : α →₀ M
⊢ equivMapDomain f l = mapDomain (⇑f : (a : α) → β) l
have h : ∀ (x : β),
  Eq.{u_12 + 1} (α := M) ((equivMapDomain f l : (a : β) → M) x : M)
    ((mapDomain (⇑f : (a : α) → β) l : (a : β) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero M
f : α → β
l : β →₀ M
hf : Set.InjOn f (f ⁻¹' (↑l.support : Set β))
a : α
⊢ a ∈ l.support.preimage f hf ↔ Ne.{u_5 + 1} (α := M) ((l : (a : β) → M) (f a) : M) (0 : M)
have rw : f a ∈ l.support ↔ Ne.{u_5 + 1} (α := M) ((l : (a : β) → M) (f a) : M) (0 : M)
Tactic: rw [Finset.mem_preimage]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' (↑l.support : Set β)) (↑l.support : Set β)
⊢ comapDomain f l ⋯ = 0 → l = 0
have rw : { support := l.support.preimage f sorry, toFun := fun (a : α) ↦ (l : (a : β) → M) (f a), mem_support_toFun := sorry :
        α →₀ M }.support =
    ∅ →
  l.support = ∅
Tactic: rw [← support_eq_empty, ← support_eq_empty, comapDomain]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' (↑l.support : Set β)) (↑l.support : Set β)
⊢ { support := l.support.preimage f ⋯, toFun := fun (a : α) ↦ (l : (a : β) → M) (f a), mem_support_toFun := ⋯ :
          α →₀ M }.support =
      ∅ →
    l.support = ∅
have simp_rw : (∀ (a : α), f a ∉ l.support) → ∀ (a : β), a ∉ l.support
Tactic: simp_rw [Finset.ext_iff, Finset.notMem_empty, iff_false, mem_preimage]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' (↑l.support : Set β)) (↑l.support : Set β)
h : ∀ (a : α), f a ∉ l.support
a : β
ha : a ∈ l.support
⊢ False
have obtain : ∀ (b : α) (hb : b ∈ f ⁻¹' (↑l.support : Set β) ∧ f b = a), False
Tactic: obtain ⟨b, hb⟩ := hf.2.2 ha
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
b : β
hb : b ∉ Set.range f
m : M
hf : Set.InjOn f (f ⁻¹' (↑(support (single b m)) : Set β))
⊢ comapDomain f (single b m) hf = 0
have h : ∀ (a : α), Eq.{u_5 + 1} (α := M) ((comapDomain f (single b m) hf : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
b : β
hb : b ∉ Set.range f
m : M
hf : Set.InjOn f (f ⁻¹' (↑(support (single b m)) : Set β))
a : α
⊢ Eq.{u_5 + 1} (α := M) ((comapDomain f (single b m) hf : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)
have h : b = f a → m = 0
Tactic: simp only [comapDomain, single_apply, coe_mk, coe_zero, Pi.zero_apply, ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
b : β
hb : b ∉ Set.range f
m : M
hf : Set.InjOn f (f ⁻¹' (↑(support (single b m)) : Set β))
⊢ comapDomain f (single b m) hf = 0
have h : ∀ (a : α), Eq.{u_5 + 1} (α := M) ((comapDomain f (single b m) hf : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)
Tactic: classical
  ext a
  simp only [comapDomain, single_apply, coe_mk, coe_zero, Pi.zero_apply, ite_eq_right_iff]
  rintro rfl
  simp at hb
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
b : β
hb : b ∉ Set.range f
m : M
hf : Set.InjOn f (f ⁻¹' (↑(support (single b m)) : Set β))
h : ∀ (a : α), Eq.{u_5 + 1} (α := M) ((comapDomain f (single b m) hf : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)
⊢ comapDomain f (single b m) hf = 0
have h₁ : ∀ (a : α), b = f a → m = 0
Tactic: classical
  ext a
  simp only [comapDomain, single_apply, coe_mk, coe_zero, Pi.zero_apply, ite_eq_right_iff]
  rintro rfl
  simp at hb
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
b : β
hb : b ∉ Set.range f
m : M
hf : Set.InjOn f (f ⁻¹' (↑(support (single b m)) : Set β))
h : ∀ (a : α), Eq.{u_5 + 1} (α := M) ((comapDomain f (single b m) hf : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)
h₁ : ∀ (a : α), b = f a → m = 0
⊢ comapDomain f (single b m) hf = 0
have h₂ : ∀ (a : α) (hb : f a ∉ Set.range f) (hf : Set.InjOn f (f ⁻¹' (↑(support (single (f a) m)) : Set β))), m = 0
Tactic: classical
  ext a
  simp only [comapDomain, single_apply, coe_mk, coe_zero, Pi.zero_apply, ite_eq_right_iff]
  rintro rfl
  simp at hb
Cleared hypotheses: b, hb, hf
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ↪ β
g : β →₀ M
hg : (↑g.support : Set β) ⊆ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
⊢ embDomain f (comapDomain (⇑f : (a : α) → β) g ⋯) = g
have h : ∀ (b : β),
  Eq.{u_5 + 1} (α := M) ((embDomain f (comapDomain (⇑f : (a : α) → β) g sorry) : (a : β) → M) b : M)
    ((g : (a : β) → M) b : M)
Tactic: ext b
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ↪ β
g : β →₀ M
hg : (↑g.support : Set β) ⊆ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
b : β
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f (comapDomain (⇑f : (a : α) → β) g ⋯) : (a : β) → M) b : M)
    ((g : (a : β) → M) b : M)
have pos : ∀ (hb : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b),
  Eq.{u_5 + 1} (α := M) ((embDomain f (comapDomain (⇑f : (a : α) → β) g sorry) : (a : β) → M) b : M)
    ((g : (a : β) → M) b : M)
Tactic: by_cases hb : b ∈ Set.range f
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ↪ β
g : β →₀ M
hg : (↑g.support : Set β) ⊆ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
b : β
pos :
  ∀ (hb : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b),
    Eq.{u_5 + 1} (α := M) ((embDomain f (comapDomain (⇑f : (a : α) → β) g ⋯) : (a : β) → M) b : M)
      ((g : (a : β) → M) b : M)
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f (comapDomain (⇑f : (a : α) → β) g ⋯) : (a : β) → M) b : M)
    ((g : (a : β) → M) b : M)
have neg : ∀ (hb : b ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)),
  Eq.{u_5 + 1} (α := M) ((embDomain f (comapDomain (⇑f : (a : α) → β) g sorry) : (a : β) → M) b : M)
    ((g : (a : β) → M) b : M)
Tactic: by_cases hb : b ∈ Set.range f
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ↪ β
g : β →₀ M
hg : (↑g.support : Set β) ⊆ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
b : β
hb : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f (comapDomain (⇑f : (a : α) → β) g ⋯) : (a : β) → M) b : M)
    ((g : (a : β) → M) b : M)
have pos : ∀ (a : α),
  Eq.{u_5 + 1} (α := M) ((embDomain f (comapDomain (⇑f : (a : α) → β) g sorry) : (a : β) → M) ((f : (a : α) → β) a : β) : M)
    ((g : (a : β) → M) ((f : (a : α) → β) a : β) : M)
Tactic: obtain ⟨a, rfl⟩ := hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ↪ β
g : β →₀ M
hg : (↑g.support : Set β) ⊆ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
a : α
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f (comapDomain (⇑f : (a : α) → β) g ⋯) : (a : β) → M) ((f : (a : α) → β) a : β) : M)
    ((g : (a : β) → M) ((f : (a : α) → β) a : β) : M)
have pos : Eq.{u_5 + 1} (α := M) ((comapDomain (⇑f : (a : α) → β) g sorry : (a : α) → M) a : M)
  ((g : (a : β) → M) ((f : (a : α) → β) a : β) : M)
Tactic: rw [embDomain_apply_self, comapDomain_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ↪ β
g : β →₀ M
hg : (↑g.support : Set β) ⊆ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
a : α
pos :
  Eq.{u_5 + 1} (α := M) ((comapDomain (⇑f : (a : α) → β) g ⋯ : (a : α) → M) a : M)
    ((g : (a : β) → M) ((f : (a : α) → β) a : β) : M)
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f (comapDomain (⇑f : (a : α) → β) g ⋯) : (a : β) → M) ((f : (a : α) → β) a : β) : M)
    ((g : (a : β) → M) ((f : (a : α) → β) a : β) : M)
have pos₁ : Eq.{u_5 + 1} (α := M) ((g : (a : β) → M) ((f : (a : α) → β) a : β) : M)
  ((g : (a : β) → M) ((f : (a : α) → β) a : β) : M)
Tactic: rw [embDomain_apply_self, comapDomain_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ↪ β
g : β →₀ M
hg : (↑g.support : Set β) ⊆ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
b : β
hb : b ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f (comapDomain (⇑f : (a : α) → β) g ⋯) : (a : β) → M) b : M)
    ((g : (a : β) → M) b : M)
have hg₁ : Eq.{u_5 + 1} (α := M) ((g : (a : β) → M) b : M) (0 : M)
Tactic: replace hg : g b = 0 := notMem_support_iff.mp <| mt (hg ·) hb
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ↪ β
g : β →₀ M
b : β
hb : b ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
hg : Eq.{u_5 + 1} (α := M) ((g : (a : β) → M) b : M) (0 : M)
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f (comapDomain (⇑f : (a : α) → β) g ⋯) : (a : β) → M) b : M)
    ((g : (a : β) → M) b : M)
have neg : Eq.{u_5 + 1} (α := M) (0 : M) ((g : (a : β) → M) b : M)
Tactic: rw [embDomain_notin_range _ _ _ hb, hg]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ↪ β
g : β →₀ M
b : β
hb : b ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
hg : Eq.{u_5 + 1} (α := M) ((g : (a : β) → M) b : M) (0 : M)
neg : Eq.{u_5 + 1} (α := M) (0 : M) ((g : (a : β) → M) b : M)
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f (comapDomain (⇑f : (a : α) → β) g ⋯) : (a : β) → M) b : M)
    ((g : (a : β) → M) b : M)
have neg₁ : Eq.{u_5 + 1} (α := M) 0 0
Tactic: rw [embDomain_notin_range _ _ _ hb, hg]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ↪ β
l : α →₀ M
⊢ comapDomain (⇑f : (a : α) → β) (embDomain f l) ⋯ = l
have h : ∀ (a : α),
  Eq.{u_5 + 1} (α := M) ((comapDomain (⇑f : (a : α) → β) (embDomain f l) sorry : (a : α) → M) a : M)
    ((l : (a : α) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
hif : Set.InjOn f (f ⁻¹' (↑(support.{u_2, u_5} (M := M) 0) : Set β))
⊢ comapDomain f 0 hif = 0
have h : ∀ (a : α), Eq.{u_5 + 1} (α := M) ((comapDomain f 0 hif : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' (↑(support (single (f a) m)) : Set β))
⊢ comapDomain f (single (f a) m) hif = single a m
have inl : ∀ (hif : Set.InjOn f (f ⁻¹' (↑(support.{u_2, u_5} (M := M) (single (f a) 0)) : Set β))),
  comapDomain f (single (f a) 0) hif = single a 0
Tactic: rcases eq_or_ne m 0 with (rfl | hm)
Cleared hypotheses: m, hif
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' (↑(support (single (f a) m)) : Set β))
inl :
  ∀ (hif : Set.InjOn f (f ⁻¹' (↑(support.{u_2, u_5} (M := M) (single (f a) 0)) : Set β))),
    comapDomain f (single (f a) 0) hif = single a 0
⊢ comapDomain f (single (f a) m) hif = single a m
have inr : ∀ (hm : m ≠ 0), comapDomain f (single (f a) m) hif = single a m
Tactic: rcases eq_or_ne m 0 with (rfl | hm)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
a : α
hif : Set.InjOn f (f ⁻¹' (↑(support.{u_2, u_5} (M := M) (single (f a) 0)) : Set β))
⊢ comapDomain f (single (f a) 0) hif = single a 0
have inl : Eq (α := α →₀ M) (comapDomain f 0 sorry) 0
Tactic: simp_rw [single_zero, comapDomain_zero]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' (↑(support (single (f a) m)) : Set β))
hm : m ≠ 0
⊢ comapDomain f (single (f a) m) hif = single a m
have inr : f ⁻¹' {f a} ⊆ {a} ∧ m = m
Tactic: rw [eq_single_iff, comapDomain_apply, comapDomain_support, ← Finset.coe_subset, coe_preimage,
      support_single _ hm, coe_singleton, coe_singleton, single_eq_same]