awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support
suffices suffices₁ suffices₂ : Multiset.Pairwise (Disjoint on Finsupp.support) s.val
suffices₃ :
  ∀ (l : List (ι →₀ M)) (hl : l.toFinset = s) (hn : l.Nodup), Multiset.Pairwise (Disjoint on Finsupp.support) s.val
suffices₄ :
  ∀ (l : List (ι →₀ M)) (hn : l.Nodup) (hs : (↑l.toFinset : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support),
    Multiset.Pairwise (Disjoint on Finsupp.support) l.toFinset.val
hr :
  ∀ (l : List (ι →₀ M)) (hn : l.Nodup) (hs : (↑l.toFinset : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support),
    Symmetric (α := ι →₀ M) (Disjoint on Finsupp.support)
⊢ (s.sum id).support = s.sup Finsupp.support
have hr₁ : ∀ (l : List (ι →₀ M)) (hn : l.Nodup) (hs : (↑l.toFinset : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support) ⦃x y : ι →₀ M⦄
  (hxy : (Disjoint on Finsupp.support) x y), (Disjoint on Finsupp.support) y x
Tactic: classical
  suffices s.1.Pairwise (_root_.Disjoint on Finsupp.support) by
    convert! Multiset.support_sum_eq s.1 this
    exact (Finset.sum_val _).symm
  obtain ⟨l, hl, hn⟩ : ∃ l : List (ι →₀ M), l.toFinset = s ∧ l.Nodup := by
    refine ⟨s.toList, ?_, Finset.nodup_toList _⟩
    simp
  subst hl
  rwa [List.toFinset_val, List.dedup_eq_self.mpr hn, Multiset.pairwise_coe_iff_pairwise, ←
    List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint hn]
  intro x y hxy
  exact symmetric_disjoint hxy
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), a ∈ s ↔ f a ≠ 0
t : Finset α
hg : ∀ (a : α), a ∈ t ↔ f a ≠ 0
⊢ { support := s, toFun := f, mem_support_toFun := hf : α →₀ M } = { support := t, toFun := f, mem_support_toFun := hg }
have e_support : s = t
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), a ∈ s ↔ f a ≠ 0
t : Finset α
hg : ∀ (a : α), a ∈ t ↔ f a ≠ 0
⊢ s = t
have e_support : ∀ (a : α), a ∈ s ↔ a ∈ t
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : IsEmpty α
f g : α →₀ M
⊢ f = g
have h : ∀ (x : α), Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Subsingleton M
f g : α →₀ M
⊢ f = g
have h : ∀ (x : α), Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
h : Nontrivial (α →₀ M)
⊢ Nontrivial M
have contrapose! : ∀ (h : Subsingleton M), Subsingleton (α →₀ M)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f : α →₀ M
⊢ Eq (α := (a : α) → M) (⇑f : (a : α) → M) 0 ↔ f = 0
have rw : Eq (α := (a : α) → M) (⇑f : (a : α) → M) (⇑0 : (a : α) → M) ↔ f = 0
Tactic: rw [← coe_zero, DFunLike.coe_fn_eq]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f : α →₀ M
rw : Eq (α := (a : α) → M) (⇑f : (a : α) → M) (⇑0 : (a : α) → M) ↔ f = 0
⊢ Eq (α := (a : α) → M) (⇑f : (a : α) → M) 0 ↔ f = 0
have rw₁ : f = 0 ↔ f = 0
Tactic: rw [← coe_zero, DFunLike.coe_fn_eq]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (hypothesis)
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f g : α →₀ M
h_1 : f.support = g.support ∧ ∀ x ∈ f.support, Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
a : α
h : a ∉ f.support
⊢ Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) ((g : (a : α) → M) a : M)
have hf : Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
Tactic: have hf : f a = 0 := notMem_support_iff.1 h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f g : α →₀ M
h_1 : f.support = g.support ∧ ∀ x ∈ f.support, Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
a : α
h : a ∉ f.support
hf : Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
⊢ Eq.{u_4 + 1} (α := M) ((g : (a : α) → M) a : M) (0 : M)
have rwa : ∀ (h : a ∉ g.support) (hf : Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)),
  Eq.{u_4 + 1} (α := M) ((g : (a : α) → M) a : M) (0 : M)
Tactic: rwa [h₁, notMem_support_iff] at h
Cleared hypotheses: h, hf
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f g : α →₀ M
h_1 : f.support = g.support ∧ ∀ x ∈ f.support, Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
a : α
h : a ∉ f.support
hf : Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
rwa :
  ∀ (h : a ∉ g.support) (hf : Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)),
    Eq.{u_4 + 1} (α := M) ((g : (a : α) → M) a : M) (0 : M)
⊢ Eq.{u_4 + 1} (α := M) ((g : (a : α) → M) a : M) (0 : M)
have rwa₁ : ∀ (h : Eq.{u_4 + 1} (α := M) ((g : (a : α) → M) a : M) (0 : M))
  (hf : Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)),
  Eq.{u_4 + 1} (α := M) ((g : (a : α) → M) a : M) (0 : M)
Tactic: rwa [h₁, notMem_support_iff] at h
Cleared hypotheses: h, hf
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (hypothesis)
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f g : α →₀ M
h_1 : f.support = g.support ∧ ∀ x ∈ f.support, Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
a : α
h : a ∉ f.support
hf : Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
⊢ Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) ((g : (a : α) → M) a : M)
have hg : Eq.{u_4 + 1} (α := M) ((g : (a : α) → M) a : M) (0 : M)
Tactic: have hg : g a = 0 := by rwa [h₁, notMem_support_iff] at h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f g : α →₀ M
h_1 : f.support = g.support ∧ ∀ x ∈ f.support, Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
a : α
h : a ∉ f.support
hf : Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
hg : Eq.{u_4 + 1} (α := M) ((g : (a : α) → M) a : M) (0 : M)
⊢ Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) ((g : (a : α) → M) a : M)
have rw : Eq.{u_4 + 1} (α := M) (0 : M) ((g : (a : α) → M) a : M)
Tactic: rw [hf, hg]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f g : α →₀ M
h_1 : f.support = g.support ∧ ∀ x ∈ f.support, Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
a : α
h : a ∉ f.support
hf : Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
hg : Eq.{u_4 + 1} (α := M) ((g : (a : α) → M) a : M) (0 : M)
rw : Eq.{u_4 + 1} (α := M) (0 : M) ((g : (a : α) → M) a : M)
⊢ Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) ((g : (a : α) → M) a : M)
have rw₁ : Eq.{u_4 + 1} (α := M) 0 0
Tactic: rw [hf, hg]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f : α →₀ M
⊢ f.support.Nonempty ↔ f ≠ 0
have contrapose! : f.support = ∅ ↔ f = 0
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f : α →₀ M
⊢ onFinset f.support (⇑f : (a : α) → M) ⋯ = f
have h : ∀ (a : α),
  Eq.{u_4 + 1} (α := M) ((onFinset f.support (⇑f : (a : α) → M) sorry : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
a : α
⊢ a ∈ (onFinset s f hf).support ↔ f a ≠ 0
have rw : Ne.{u_4 + 1} (α := M) ((onFinset s f hf : (a : α) → M) a : M) (0 : M) ↔ f a ≠ 0
Tactic: rw [Finsupp.mem_support_iff, Finsupp.onFinset_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
a : α
rw : Ne.{u_4 + 1} (α := M) ((onFinset s f hf : (a : α) → M) a : M) (0 : M) ↔ f a ≠ 0
⊢ a ∈ (onFinset s f hf).support ↔ f a ≠ 0
have rw₁ : f a ≠ 0 ↔ f a ≠ 0
Tactic: rw [Finsupp.mem_support_iff, Finsupp.onFinset_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f : α → M
hf : (Function.support f).Finite
⊢ (ofSupportFinite f hf).support = hf.toFinset (s := Function.support f)
have h : ∀ (a : α), a ∈ (ofSupportFinite f hf).support ↔ a ∈ hf.toFinset (s := Function.support f)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
f : M → N
hf : f 0 = 0
g : α →₀ M
a : α
⊢ (f ∘ (⇑g : (a : α) → M)) a ≠ 0 → a ∈ g.support
have rw : Eq.{u_4 + 1} (α := M) ((g : (a : α) → M) a : M) (0 : M) → (f ∘ (⇑g : (a : α) → M)) a = 0
Tactic: rw [mem_support_iff, not_imp_not]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
e : M → N
he₀ : e 0 = 0
⊢ Eq (α := Set (α →₀ N)) (Set.range (mapRange e he₀))
    {g : α →₀ N | ∀ (i : α), Membership.mem (α := N) (Set.range e) ((g : (a : α) → N) i : N)}
have h : ∀ (g : α →₀ N),
  Membership.mem (γ := Set (α →₀ N)) (Set.range (mapRange e he₀)) g ↔
    Membership.mem (γ := Set (α →₀ N))
      {g : α →₀ N | ∀ (i : α), Membership.mem (α := N) (Set.range e) ((g : (a : α) → N) i : N)} g
Tactic: ext g
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
⊢ (∃ (y : α →₀ M), mapRange e he₀ y = g) ↔ ∀ (i : α), ∃ (y : M), e y = (g : (a : α) → N) i
have h : (∃ (y : α →₀ M), mapRange e he₀ y = g) → ∀ (i : α), ∃ (y : M), e y = (g : (a : α) → N) i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
h : (∃ (y : α →₀ M), mapRange e he₀ y = g) → ∀ (i : α), ∃ (y : M), e y = (g : (a : α) → N) i
⊢ (∃ (y : α →₀ M), mapRange e he₀ y = g) ↔ ∀ (i : α), ∃ (y : M), e y = (g : (a : α) → N) i
have h₁ : (∀ (i : α), ∃ (y : M), e y = (g : (a : α) → N) i) → ∃ (y : α →₀ M), mapRange e he₀ y = g
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
h : ∀ (i : α), ∃ (y : M), e y = (g : (a : α) → N) i
⊢ ∃ (y : α →₀ M), mapRange e he₀ y = g
have h₁ : ∀ (f : (i : α) → M) (h : ∀ (i : α), e (f i) = (g : (a : α) → N) i), ∃ (y : α →₀ M), mapRange e he₀ y = g
Tactic: choose f h using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
f : (i : α) → M
h : ∀ (i : α), e (f i) = (g : (a : α) → N) i
⊢ ∃ (y : α →₀ M), mapRange e he₀ y = g
have h₁ : mapRange e he₀ (onFinset g.support (fun (x : α) ↦ if x ∈ g.support then f x else 0) sorry) = g
Tactic: use onFinset g.support (fun x ↦ if x ∈ g.support then f x else 0) (by simp_all)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
h : ∀ (i : α), ∃ (y : M), e y = (g : (a : α) → N) i
⊢ ∃ (y : α →₀ M), mapRange e he₀ y = g
have h₁ : ∀ (f : (i : α) → M) (h : ∀ (i : α), e (f i) = (g : (a : α) → N) i), ∃ (y : α →₀ M), mapRange e he₀ y = g
Tactic: classical
    choose f h using h
    use onFinset g.support (fun x ↦ if x ∈ g.support then f x else 0) (by simp_all)
    grind
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
h : ∀ (i : α), ∃ (y : M), e y = (g : (a : α) → N) i
h₁ : ∀ (f : (i : α) → M) (h : ∀ (i : α), e (f i) = (g : (a : α) → N) i), ∃ (y : α →₀ M), mapRange e he₀ y = g
⊢ ∃ (y : α →₀ M), mapRange e he₀ y = g
have h₂ : ∀ (f : (i : α) → M) (h : ∀ (i : α), e (f i) = (g : (a : α) → N) i),
  mapRange e he₀ (onFinset g.support (fun (x : α) ↦ if x ∈ g.support then f x else 0) sorry) = g
Tactic: classical
    choose f h using h
    use onFinset g.support (fun x ↦ if x ∈ g.support then f x else 0) (by simp_all)
    grind
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
e : M → N
he₀ : e 0 = 0
he : Injective e
a b : α →₀ M
h : mapRange e he₀ a = mapRange e he₀ b
⊢ a = b
have rw : ∀
  (h :
    ∀ (a_1 : α),
      Eq.{u_5 + 1} (α := N) ((mapRange e he₀ a : (a : α) → N) a_1 : N) ((mapRange e he₀ b : (a : α) → N) a_1 : N))
  (a_1 : α), Eq.{u_4 + 1} (α := M) ((a : (a : α) → M) a_1 : M) ((b : (a : α) → M) a_1 : M)
Tactic: rw [Finsupp.ext_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
e : M → N
he₀ : e 0 = 0
he : Surjective e
⊢ Surjective (α := α →₀ M) (mapRange e he₀)
have rw : Eq (α := Set (α →₀ N))
  {g : α →₀ N | ∀ (i : α), Membership.mem.{u_5, u_5} (α := N) (γ := Set N) Set.univ ((g : (a : α) → N) i : N)} Set.univ
Tactic: rw [← Set.range_eq_univ, range_mapRange, he.range_eq]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
e : M ≃ N
hf : Eq.{u_5 + 1} (α := N) ((e : (a : M) → N) 0 : N) (0 : N)
x : ι →₀ M
⊢ mapRange (⇑e.symm : (a : N) → M) ⋯ (mapRange (⇑e : (a : M) → N) hf x) = x
have h : ∀ (a : ι),
  Eq.{u_4 + 1} (α := M) ((mapRange (⇑e.symm : (a : N) → M) sorry (mapRange (⇑e : (a : M) → N) hf x) : (a : ι) → M) a : M)
    ((x : (a : ι) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
e : M ≃ N
hf : Eq.{u_5 + 1} (α := N) ((e : (a : M) → N) 0 : N) (0 : N)
x : ι →₀ N
⊢ mapRange (⇑e : (a : M) → N) hf (mapRange (⇑e.symm : (a : N) → M) ⋯ x) = x
have h : ∀ (a : ι),
  Eq.{u_5 + 1} (α := N) ((mapRange (⇑e : (a : M) → N) hf (mapRange (⇑e.symm : (a : N) → M) sorry x) : (a : ι) → N) a : N)
    ((x : (a : ι) → N) a : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
ι : Type u_3
M : Type u_4
inst : Zero M
⊢ Eq (α := (ι →₀ M) ≃ (ι →₀ M)) (equiv (Equiv.refl M) ⋯) (Equiv.refl (ι →₀ M))
have H : ∀ (x : ι →₀ M) (a : ι),
  Eq.{u_4 + 1} (α := M) ((((equiv (Equiv.refl M) sorry : (a : ι →₀ M) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) a : M)
    ((((Equiv.refl (ι →₀ M) : (a : ι →₀ M) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
e : M ≃ N
hf : Eq.{u_5 + 1} (α := N) ((e : (a : M) → N) 0 : N) (0 : N)
f₂ : N ≃ O
hf₂ : Eq.{u_6 + 1} (α := O) ((f₂ : (a : N) → O) 0 : O) (0 : O)
⊢ Eq.{u_6 + 1} (α := O) ((e.trans f₂ : (a : M) → O) 0 : O) (0 : O)
have rw : Eq.{u_6 + 1} (α := O) ((f₂ : (a : N) → O) ((e : (a : M) → N) 0 : N) : O) (0 : O)
Tactic: rw [Equiv.trans_apply, hf, hf₂]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
e : M ≃ N
hf : Eq.{u_5 + 1} (α := N) ((e : (a : M) → N) 0 : N) (0 : N)
f₂ : N ≃ O
hf₂ : Eq.{u_6 + 1} (α := O) ((f₂ : (a : N) → O) 0 : O) (0 : O)
rw : Eq.{u_6 + 1} (α := O) ((f₂ : (a : N) → O) ((e : (a : M) → N) 0 : N) : O) (0 : O)
rw₁ : Eq.{u_6 + 1} (α := O) ((f₂ : (a : N) → O) 0 : O) (0 : O)
⊢ Eq.{u_6 + 1} (α := O) ((e.trans f₂ : (a : M) → O) 0 : O) (0 : O)
have rw₂ : Eq.{u_6 + 1} (α := O) 0 0
Tactic: rw [Equiv.trans_apply, hf, hf₂]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
e : M ≃ N
hf : Eq.{u_5 + 1} (α := N) ((e : (a : M) → N) 0 : N) (0 : N)
f₂ : N ≃ O
hf₂ : Eq.{u_6 + 1} (α := O) ((f₂ : (a : N) → O) 0 : O) (0 : O)
⊢ Eq (α := (ι →₀ M) ≃ (ι →₀ O)) (equiv (e.trans f₂) ⋯) (Equiv.trans (equiv e hf) (equiv f₂ hf₂))
have H : ∀ (x : ι →₀ M) (a : ι),
  Eq.{u_6 + 1} (α := O) ((((equiv (e.trans f₂) sorry : (a : ι →₀ M) → ι →₀ O) x : ι →₀ O) : (a : ι) → O) a : O)
    ((((Equiv.trans (equiv e hf) (equiv f₂ hf₂) : (a : ι →₀ M) → ι →₀ O) x : ι →₀ O) : (a : ι) → O) a : O)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
f : α ↪ β
v : α →₀ M
a₂ : β
this : DecidableEq β
h : a₂ ∈ map f v.support
⊢ ∃! a : α, a ∈ v.support ∧ (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = a₂) a
have rcases : ∀ (a : α) (ha : a ∈ v.support) (h : Membership.mem (α := β) (map f v.support) ((f : (a : α) → β) a : β)),
  ∃! a_1 : α,
    a_1 ∈ v.support ∧ (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) a_1
Tactic: rcases Finset.mem_map.1 h with ⟨a, ha, rfl⟩
Cleared hypotheses: a₂, h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
f : α ↪ β
v : α →₀ M
a₂ : β
⊢ a₂ ∈ map f v.support ↔
    ¬Eq.{u_4 + 1} (α := M)
        (if h : a₂ ∈ map f v.support then
          (v : (a : α) → M) (choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = a₂) v.support ⋯)
        else 0)
        0
have pos : ∀ (h : a₂ ∈ map f v.support),
  a₂ ∈ map f v.support ↔
    ¬Eq.{u_4 + 1} (α := M) ((v : (a : α) → M) (choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = a₂) v.support sorry) : M)
        (0 : M)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
f : α ↪ β
v : α →₀ M
a₂ : β
pos :
  ∀ (h : a₂ ∈ map f v.support),
    a₂ ∈ map f v.support ↔
      ¬Eq.{u_4 + 1} (α := M) ((v : (a : α) → M) (choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = a₂) v.support ⋯) : M)
          (0 : M)
⊢ a₂ ∈ map f v.support ↔
    ¬Eq.{u_4 + 1} (α := M)
        (if h : a₂ ∈ map f v.support then
          (v : (a : α) → M) (choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = a₂) v.support ⋯)
        else 0)
        0
have neg : ∀ (h : a₂ ∉ map f v.support), a₂ ∈ map f v.support ↔ ¬Eq.{u_4 + 1} (α := M) 0 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
f : α ↪ β
v : α →₀ M
a₂ : β
h : a₂ ∈ map f v.support
⊢ a₂ ∈ map f v.support ↔
    ¬Eq.{u_4 + 1} (α := M) ((v : (a : α) → M) (choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = a₂) v.support ⋯) : M)
        (0 : M)
have pos : ¬Eq.{u_4 + 1} (α := M) ((v : (a : α) → M) (choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = a₂) v.support sorry) : M) (0 : M)
Tactic: simp only [h, true_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
f : α ↪ β
v : α →₀ M
a₂ : β
h : a₂ ∈ map f v.support
⊢ ¬Eq.{u_4 + 1} (α := M) ((v : (a : α) → M) (choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = a₂) v.support ⋯) : M) (0 : M)
have pos : choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = a₂) v.support sorry ∈ v.support
Tactic: rw [← notMem_support_iff, not_not]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
b : β
⊢ Eq.{u_4 + 1} (α := M) ((embDomain f v : (a : β) → M) b : M)
    (if h : ∃ (a : α), (f : (a : α) → β) a = b then
        (v : (a : α) → M) (h.choose (p := fun (a : α) ↦ (f : (a : α) → β) a = b))
      else 0 :
      M)
have simp : Eq.{u_4 + 1} (α := M)
  (if h : ∃ (a : α), Ne.{u_4 + 1} (α := M) ((v : (a : α) → M) a : M) (0 : M) ∧ (f : (a : α) → β) a = b then
    (v : (a : α) → M) (Finset.choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = b) v.support sorry)
  else 0)
  (if h : ∃ (a : α), (f : (a : α) → β) a = b then
    (v : (a : α) → M) (h.choose (p := fun (a : α) ↦ (f : (a : α) → β) a = b))
  else 0)
Tactic: simp only [embDomain, mem_map, mem_support_iff, coe_mk]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
b : β
⊢ Eq.{u_4 + 1} (α := M)
    (if h : ∃ (a : α), Ne.{u_4 + 1} (α := M) ((v : (a : α) → M) a : M) (0 : M) ∧ (f : (a : α) → β) a = b then
      (v : (a : α) → M) (Finset.choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = b) v.support ⋯)
    else 0)
    (if h : ∃ (a : α), (f : (a : α) → β) a = b then
      (v : (a : α) → M) (h.choose (p := fun (a : α) ↦ (f : (a : α) → β) a = b))
    else 0)
have pos : ∀ (h : ∃ (a : α), Ne.{u_4 + 1} (α := M) ((v : (a : α) → M) a : M) (0 : M) ∧ (f : (a : α) → β) a = b)
  (h_1 : ∃ (a : α), (f : (a : α) → β) a = b),
  Eq.{u_4 + 1} (α := M) ((v : (a : α) → M) (Finset.choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = b) v.support sorry) : M)
    ((v : (a : α) → M) (h_1.choose (p := fun (a : α) ↦ (f : (a : α) → β) a = b)) : M)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
b : β
pos :
  ∀ (h : ∃ (a : α), Ne.{u_4 + 1} (α := M) ((v : (a : α) → M) a : M) (0 : M) ∧ (f : (a : α) → β) a = b)
    (h_1 : ∃ (a : α), (f : (a : α) → β) a = b),
    Eq.{u_4 + 1} (α := M) ((v : (a : α) → M) (Finset.choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = b) v.support ⋯) : M)
      ((v : (a : α) → M) (h_1.choose (p := fun (a : α) ↦ (f : (a : α) → β) a = b)) : M)
⊢ Eq.{u_4 + 1} (α := M)
    (if h : ∃ (a : α), Ne.{u_4 + 1} (α := M) ((v : (a : α) → M) a : M) (0 : M) ∧ (f : (a : α) → β) a = b then
      (v : (a : α) → M) (Finset.choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = b) v.support ⋯)
    else 0)
    (if h : ∃ (a : α), (f : (a : α) → β) a = b then
      (v : (a : α) → M) (h.choose (p := fun (a : α) ↦ (f : (a : α) → β) a = b))
    else 0)
have neg : ∀ (h : ∃ (a : α), Ne.{u_4 + 1} (α := M) ((v : (a : α) → M) a : M) (0 : M) ∧ (f : (a : α) → β) a = b),
  (¬∃ (a : α), (f : (a : α) → β) a = b) →
    Eq.{u_4 + 1} (α := M) ((v : (a : α) → M) (Finset.choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = b) v.support sorry) : M)
      (0 : M)
Tactic: split_ifs