awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : DecidableEq α
f : α →₀ ℕ
a : α
⊢ Eq (α := ℕ)
    (((fun (s : Multiset α) ↦
              ({ support := s.toFinset, toFun := fun (a : α) ↦ count a s, mem_support_toFun := ⋯ } : α →₀ ℕ))
            ((fun (f : α →₀ ℕ) ↦ ((Finsupp.toMultiset : (a : α →₀ ℕ) → Multiset α) f : Multiset α)) f) :
          (a : α) → ℕ)
        a :
      ℕ)
    ((f : (a : α) → ℕ) a : ℕ)
have simp : Eq (α := ℕ) ((f : (a : α) → ℕ) a : ℕ) (0 : ℕ) → Eq (α := ℕ) (0 : ℕ) ((f : (a : α) → ℕ) a : ℕ)
Tactic: simp only [Finsupp.toMultiset_apply, Finsupp.sum, Multiset.count_sum',
        Multiset.count_singleton, mul_boole, Finsupp.coe_mk, Finsupp.mem_support_iff,
        Multiset.count_nsmul, Finset.sum_ite_eq, ite_not, ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ Eq (α := α →₀ ℕ) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) {a} : α →₀ ℕ) (Finsupp.single a 1 : α →₀ ℕ)
have h : ∀ (a_1 : α),
  Eq (α := ℕ) ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) {a} : α →₀ ℕ) : (a : α) → ℕ) a_1 : ℕ)
    ((Finsupp.single a 1 : (a : α) → ℕ) a_1 : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a a_1 : α
⊢ Eq (α := ℕ) ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) {a} : α →₀ ℕ) : (a : α) → ℕ) a_1 : ℕ)
    ((Finsupp.single a 1 : (a : α) → ℕ) a_1 : ℕ)
have h : count a_1 {a} = (Finsupp.single a 1 : (a : α) → ℕ) a_1
Tactic: rw [toFinsupp_apply, count_singleton, Finsupp.single_eq_pi_single, Pi.single_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a a_1 : α
h : count a_1 {a} = (Finsupp.single a 1 : (a : α) → ℕ) a_1
⊢ Eq (α := ℕ) ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) {a} : α →₀ ℕ) : (a : α) → ℕ) a_1 : ℕ)
    ((Finsupp.single a 1 : (a : α) → ℕ) a_1 : ℕ)
have h₁ : Eq (α := ℕ) (if a_1 = a then 1 else 0 : ℕ) ((Finsupp.single a 1 : (a : α) → ℕ) a_1 : ℕ)
Tactic: rw [toFinsupp_apply, count_singleton, Finsupp.single_eq_pi_single, Pi.single_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a a_1 : α
h : count a_1 {a} = (Finsupp.single a 1 : (a : α) → ℕ) a_1
h₁ : Eq (α := ℕ) (if a_1 = a then 1 else 0 : ℕ) ((Finsupp.single a 1 : (a : α) → ℕ) a_1 : ℕ)
⊢ Eq (α := ℕ) ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) {a} : α →₀ ℕ) : (a : α) → ℕ) a_1 : ℕ)
    ((Finsupp.single a 1 : (a : α) → ℕ) a_1 : ℕ)
have h₂ : Eq (α := ℕ) (if a_1 = a then 1 else 0 : ℕ) (Pi.single (M := fun (j : α) ↦ ℕ) a 1 a_1 : ℕ)
Tactic: rw [toFinsupp_apply, count_singleton, Finsupp.single_eq_pi_single, Pi.single_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a a_1 : α
h : count a_1 {a} = (Finsupp.single a 1 : (a : α) → ℕ) a_1
h₁ : Eq (α := ℕ) (if a_1 = a then 1 else 0 : ℕ) ((Finsupp.single a 1 : (a : α) → ℕ) a_1 : ℕ)
h₂ : Eq (α := ℕ) (if a_1 = a then 1 else 0 : ℕ) (Pi.single (M := fun (j : α) ↦ ℕ) a 1 a_1 : ℕ)
⊢ Eq (α := ℕ) ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) {a} : α →₀ ℕ) : (a : α) → ℕ) a_1 : ℕ)
    ((Finsupp.single a 1 : (a : α) → ℕ) a_1 : ℕ)
have h₃ : Eq (α := ℕ) (if a_1 = a then 1 else 0) (if a_1 = a then 1 else 0)
Tactic: rw [toFinsupp_apply, count_singleton, Finsupp.single_eq_pi_single, Pi.single_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ Eq (α := α →₀ ℕ) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) (s ∪ t) : α →₀ ℕ)
    ((toFinsupp : (a : Multiset α) → α →₀ ℕ) s ⊔ (toFinsupp : (a : Multiset α) → α →₀ ℕ) t : α →₀ ℕ)
have h : ∀ (a : α),
  Eq (α := ℕ) ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) (s ∪ t) : α →₀ ℕ) : (a : α) → ℕ) a : ℕ)
    ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) s ⊔ (toFinsupp : (a : Multiset α) → α →₀ ℕ) t : α →₀ ℕ) : (a : α) → ℕ)
        a :
      ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ Eq (α := α →₀ ℕ) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) (s ∩ t) : α →₀ ℕ)
    ((toFinsupp : (a : Multiset α) → α →₀ ℕ) s ⊓ (toFinsupp : (a : Multiset α) → α →₀ ℕ) t : α →₀ ℕ)
have h : ∀ (a : α),
  Eq (α := ℕ) ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) (s ∩ t) : α →₀ ℕ) : (a : α) → ℕ) a : ℕ)
    ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) s ⊓ (toFinsupp : (a : Multiset α) → α →₀ ℕ) t : α →₀ ℕ) : (a : α) → ℕ)
        a :
      ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
⊢ (Finsupp.sum (M := ℕ) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) s) fun (x : α) ↦ id) = s.card
have rw : card.{u_1} (α := α) ((Finsupp.toMultiset : (a : α →₀ ℕ) → Multiset α) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) s)) =
  s.card
Tactic: rw [← Finsupp.card_toMultiset, toFinsupp_toMultiset]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
rw :
  card.{u_1} (α := α) ((Finsupp.toMultiset : (a : α →₀ ℕ) → Multiset α) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) s)) =
    s.card
⊢ (Finsupp.sum (M := ℕ) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) s) fun (x : α) ↦ id) = s.card
have rw₁ : s.card = s.card
Tactic: rw [← Finsupp.card_toMultiset, toFinsupp_toMultiset]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
ι : Type u_3
m n : ι →₀ ℕ
h : m < n
⊢ LT.lt (α := ℕ) (m.sum fun (x : ι) ↦ id) (n.sum fun (x : ι) ↦ id)
have rw : Multiset.card.{u_3} (α := ι) ((toMultiset : (a : ι →₀ ℕ) → Multiset ι) m) <
  Multiset.card.{u_3} (α := ι) ((toMultiset : (a : ι →₀ ℕ) → Multiset ι) n)
Tactic: rw [← card_toMultiset, ← card_toMultiset]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
ι : Type u_3
m n : ι →₀ ℕ
h : m < n
⊢ Multiset.card.{u_3} (α := ι) ((toMultiset : (a : ι →₀ ℕ) → Multiset ι) m) <
    Multiset.card.{u_3} (α := ι) ((toMultiset : (a : ι →₀ ℕ) → Multiset ι) n)
have h₁ : LT.lt (α := Multiset ι) ((toMultiset : (a : ι →₀ ℕ) → Multiset ι) m : Multiset ι)
  ((toMultiset : (a : ι →₀ ℕ) → Multiset ι) n : Multiset ι)
Tactic: apply Multiset.card_lt_card
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
inst_1 : Fintype α
P : { P : α → ℕ // ∑ i : α, P i = n }
⊢ Eq.{u_1 + 1} (α := Multiset α)
    (↑((Equiv.symm (equivNatSumOfFintype α n) : (a : { P : α → ℕ // ∑ i : α, P i = n }) → Sym α n) P) : Multiset α)
    (∑ a : α, HSMul.hSMul (β := Multiset α) ((↑P : α → ℕ) a) {a})
have obtain : ∀ (P : α → ℕ) (hP : ∑ i : α, P i = n),
  Eq.{u_1 + 1} (α := Multiset α)
    (↑((Equiv.symm (equivNatSumOfFintype α n) : (a : { P : α → ℕ // ∑ i : α, P i = n }) → Sym α n)
          (Subtype.mk (p := fun (P : α → ℕ) ↦ ∑ i : α, P i = n) P hP)) :
      Multiset α)
    (∑ a : α,
      HSMul.hSMul (β := Multiset α) ((↑(Subtype.mk (p := fun (P : α → ℕ) ↦ ∑ i : α, P i = n) P hP) : α → ℕ) a) {a})
Tactic: obtain ⟨P, hP⟩ := P
Cleared hypotheses: P
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
inst_1 : Fintype α
P : α → ℕ
hP : ∑ i : α, P i = n
⊢ Eq.{u_1 + 1} (α := Multiset α)
    (↑((Equiv.symm (equivNatSumOfFintype α n) : (a : { P : α → ℕ // ∑ i : α, P i = n }) → Sym α n)
          (Subtype.mk (p := fun (P : α → ℕ) ↦ ∑ i : α, P i = n) P hP)) :
      Multiset α)
    (∑ a : α,
      HSMul.hSMul (β := Multiset α) ((↑(Subtype.mk (p := fun (P : α → ℕ) ↦ ∑ i : α, P i = n) P hP) : α → ℕ) a) {a})
have change : Eq (α := Multiset α)
  ((Finsupp.toMultiset : (a : α →₀ ℕ) → Multiset α) ((Equiv.symm Finsupp.equivFunOnFinite : (a : α → ℕ) → α →₀ ℕ) P) :
    Multiset α)
  (Multiset.sum
      (Multiset.map
        (fun (a : α) ↦
          HSMul.hSMul (β := Multiset α) ((↑(Subtype.mk (p := fun (P : α → ℕ) ↦ ∑ i : α, P i = n) P hP) : α → ℕ) a) {a})
        (val univ)) :
    Multiset α)
Tactic: change Finsupp.toMultiset (Finsupp.equivFunOnFinite.symm P) = Multiset.sum _
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
inst_1 : Fintype α
P : α → ℕ
hP : ∑ i : α, P i = n
⊢ Eq (α := Multiset α)
    ((Finsupp.toMultiset : (a : α →₀ ℕ) → Multiset α) ((Equiv.symm Finsupp.equivFunOnFinite : (a : α → ℕ) → α →₀ ℕ) P) :
      Multiset α)
    (Multiset.sum
        (Multiset.map
          (fun (a : α) ↦
            HSMul.hSMul (β := Multiset α) ((↑(Subtype.mk (p := fun (P : α → ℕ) ↦ ∑ i : α, P i = n) P hP) : α → ℕ) a)
              {a})
          (val univ)) :
      Multiset α)
have a : ∀ (a : α),
  Multiset.count a
      ((Finsupp.toMultiset : (a : α →₀ ℕ) → Multiset α)
        ((Equiv.symm Finsupp.equivFunOnFinite : (a : α → ℕ) → α →₀ ℕ) P)) =
    Multiset.count a
      (Multiset.sum
        (Multiset.map
          (fun (a : α) ↦
            HSMul.hSMul (β := Multiset α) ((↑(Subtype.mk (p := fun (P : α → ℕ) ↦ ∑ i : α, P i = n) P hP) : α → ℕ) a)
              {a})
          (val univ)))
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
inst_1 : Fintype α
P : α → ℕ
hP : ∑ i : α, P i = n
a : α
⊢ Multiset.count a
      ((Finsupp.toMultiset : (a : α →₀ ℕ) → Multiset α)
        ((Equiv.symm Finsupp.equivFunOnFinite : (a : α → ℕ) → α →₀ ℕ) P)) =
    Multiset.count a
      (Multiset.sum
        (Multiset.map
          (fun (a : α) ↦
            HSMul.hSMul (β := Multiset α) ((↑(Subtype.mk (p := fun (P : α → ℕ) ↦ ∑ i : α, P i = n) P hP) : α → ℕ) a)
              {a})
          (val univ)))
have a₁ : Multiset.count a
    ((Finsupp.toMultiset : (a : α →₀ ℕ) → Multiset α)
      ((Equiv.symm Finsupp.equivFunOnFinite : (a : α → ℕ) → α →₀ ℕ) P)) =
  Multiset.sum
    (Multiset.map
      (fun (b : α) ↦
        Multiset.count a
          (HSMul.hSMul (β := Multiset α) ((↑(Subtype.mk (p := fun (P : α → ℕ) ↦ ∑ i : α, P i = n) P hP) : α → ℕ) b)
            {b}))
      (val univ))
Tactic: rw [Multiset.count_sum]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
⊢ Eq (α := α →₀ M) (some 0) 0
have h : ∀ (a : α), Eq.{u_2 + 1} (α := M) ((some 0 : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : AddZeroClass M
f g : Finsupp.{u_1, u_2} (Option α) M
⊢ (f + g).some = f.some + g.some
have h : ∀ (a : α), Eq.{u_2 + 1} (α := M) (((f + g).some : (a : α) → M) a : M) ((f.some + g.some : (a : α) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
m : M
⊢ Eq (α := α →₀ M) (some (single none m)) 0
have h : ∀ (a : α), Eq.{u_2 + 1} (α := M) ((some (single none m) : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
a : α
m : M
⊢ Eq (α := α →₀ M) (some (single (Option.some a) m)) (single a m)
have h : ∀ (b : α),
  Eq.{u_2 + 1} (α := M) ((some (single (Option.some a) m) : (a : α) → M) b : M) ((single a m : (a : α) → M) b : M)
Tactic: ext b
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
a : α
m : M
⊢ Eq (α := α →₀ M) (some (single (Option.some a) m)) (single a m)
have h : ∀ (b : α),
  Eq.{u_2 + 1} (α := M) ((some (single (Option.some a) m) : (a : α) → M) b : M) ((single a m : (a : α) → M) b : M)
Tactic: classical
    ext b
    simp [single_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
⊢ (embDomain Embedding.some f).some = f
have h : ∀ (a : α), Eq.{u_2 + 1} (α := M) (((embDomain Embedding.some f).some : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
a : α
⊢ Eq.{u_2 + 1} (α := M) (((embDomain Embedding.some f).some : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
have h : Eq.{u_2 + 1} (α := M) ((embDomain Embedding.some f : (a : Option α) → M) (Option.some a) : M) ((f : (a : α) → M) a : M)
Tactic: rw [some_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : Finsupp.{u_1, u_2} (Option α) M
a : M
⊢ (f.update none a).some = f.some
have h : ∀ (a_1 : α), Eq.{u_2 + 1} (α := M) (((f.update none a).some : (a : α) → M) a_1 : M) ((f.some : (a : α) → M) a_1 : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst : Zero M
P : Finsupp.{u_1, u_2} (Option α) M
⊢ (fun (P : M × (α →₀ M)) ↦ (embDomain Embedding.some P.2).update none P.1)
      ((fun (P : Finsupp.{u_1, u_2} (Option α) M) ↦ (((P : (a : Option α) → M) none, P.some) : M × (α →₀ M))) P) =
    P
have h : Eq.{u_2 + 1} (α := M)
  (((fun (P : M × (α →₀ M)) ↦ (embDomain Embedding.some P.2).update none P.1)
          ((fun (P : Finsupp.{u_1, u_2} (Option α) M) ↦ (((P : (a : Option α) → M) none, P.some) : M × (α →₀ M))) P) :
        (a : Option α) → M)
      none :
    M)
  ((P : (a : Option α) → M) none : M)
Tactic: ext (_ | a)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst : Zero M
P : Finsupp.{u_1, u_2} (Option α) M
h :
  Eq.{u_2 + 1} (α := M)
    (((fun (P : M × (α →₀ M)) ↦ (embDomain Embedding.some P.2).update none P.1)
            ((fun (P : Finsupp.{u_1, u_2} (Option α) M) ↦ (((P : (a : Option α) → M) none, P.some) : M × (α →₀ M))) P) :
          (a : Option α) → M)
        none :
      M)
    ((P : (a : Option α) → M) none : M)
⊢ (fun (P : M × (α →₀ M)) ↦ (embDomain Embedding.some P.2).update none P.1)
      ((fun (P : Finsupp.{u_1, u_2} (Option α) M) ↦ (((P : (a : Option α) → M) none, P.some) : M × (α →₀ M))) P) =
    P
have h₁ : ∀ (a : α),
  Eq.{u_2 + 1} (α := M)
    (((fun (P : M × (α →₀ M)) ↦ (embDomain Embedding.some P.2).update none P.1)
            ((fun (P : Finsupp.{u_1, u_2} (Option α) M) ↦ (((P : (a : Option α) → M) none, P.some) : M × (α →₀ M))) P) :
          (a : Option α) → M)
        (Option.some a) :
      M)
    ((P : (a : Option α) → M) (Option.some a) : M)
Tactic: ext (_ | a)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst : Zero M
P : M × (α →₀ M)
⊢ (fun (P : Finsupp.{u_1, u_2} (Option α) M) ↦ (((P : (a : Option α) → M) none, P.some) : M × (α →₀ M)))
      ((fun (P : M × (α →₀ M)) ↦ (embDomain Embedding.some P.2).update none P.1) P) =
    P
have fst : ((fun (P : Finsupp.{u_1, u_2} (Option α) M) ↦ (((P : (a : Option α) → M) none, P.some) : M × (α →₀ M)))
      ((fun (P : M × (α →₀ M)) ↦ (embDomain Embedding.some P.2).update none P.1) P)).1 =
  P.1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst : Zero M
P : M × (α →₀ M)
fst :
  ((fun (P : Finsupp.{u_1, u_2} (Option α) M) ↦ (((P : (a : Option α) → M) none, P.some) : M × (α →₀ M)))
        ((fun (P : M × (α →₀ M)) ↦ (embDomain Embedding.some P.2).update none P.1) P)).1 =
    P.1
⊢ (fun (P : Finsupp.{u_1, u_2} (Option α) M) ↦ (((P : (a : Option α) → M) none, P.some) : M × (α →₀ M)))
      ((fun (P : M × (α →₀ M)) ↦ (embDomain Embedding.some P.2).update none P.1) P) =
    P
have snd : ∀ (a : α),
  Eq.{u_2 + 1} (α := M)
    ((((fun (P : Finsupp.{u_1, u_2} (Option α) M) ↦ (((P : (a : Option α) → M) none, P.some) : M × (α →₀ M)))
              ((fun (P : M × (α →₀ M)) ↦ (embDomain Embedding.some P.2).update none P.1) P)).2 :
          (a : α) → M)
        a :
      M)
    ((P.2 : (a : α) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
a : Option α
⊢ (optionElim y f : (a : Option α) → M) a = a.elim y (⇑f : (a : α) → M)
have none : (optionElim y f : (a : Option α) → M) none = Option.elim.{u_1, u_2 + 1} (α := α) none y (⇑f : (a : α) → M)
Tactic: cases a with
  | none => exact optionElim_apply_none y f
  | some x => simp only [optionElim_apply_some, Option.elim_some]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
a : Option α
none :
  (optionElim y f : (a : Option α) → M) Option.none =
    Option.elim.{u_1, u_2 + 1} (α := α) Option.none y (⇑f : (a : α) → M)
⊢ (optionElim y f : (a : Option α) → M) a = a.elim y (⇑f : (a : α) → M)
have some : ∀ (x : α), (optionElim y f : (a : Option α) → M) (Option.some x) = (Option.some x).elim y (⇑f : (a : α) → M)
Tactic: cases a with
  | none => exact optionElim_apply_none y f
  | some x => simp only [optionElim_apply_some, Option.elim_some]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
a : Option α
⊢ (optionElim y f : (a : Option α) → M) a = Option.elim' y (⇑f : (a : α) → M) a
have rw : a.elim y (⇑f : (a : α) → M) = Option.elim' y (⇑f : (a : α) → M) a
Tactic: rw [optionElim_apply_eq_elim, Option.elim'_eq_elim]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
a : Option α
rw : a.elim y (⇑f : (a : α) → M) = Option.elim' y (⇑f : (a : α) → M) a
⊢ (optionElim y f : (a : Option α) → M) a = Option.elim' y (⇑f : (a : α) → M) a
have rw₁ : a.elim y (⇑f : (a : α) → M) = a.elim y (⇑f : (a : α) → M)
Tactic: rw [optionElim_apply_eq_elim, Option.elim'_eq_elim]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
⊢ (optionElim y f).some = f
have h : ∀ (a : α), Eq.{u_2 + 1} (α := M) (((optionElim y f).some : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : Finsupp.{u_1, u_2} (Option α) M
⊢ optionElim ((f : (a : Option α) → M) none) f.some = f
have h : ∀ (a : Option α),
  Eq.{u_2 + 1} (α := M)
    (((optionElim ((f : (a : Option α) → M) none) f.some : Finsupp.{u_1, u_2} (Option α) M) : (a : Option α) → M) a : M)
    ((f : (a : Option α) → M) a : M)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : Finsupp.{u_1, u_2} (Option α) M
a : Option α
⊢ Eq.{u_2 + 1} (α := M)
    (((optionElim ((f : (a : Option α) → M) none) f.some : Finsupp.{u_1, u_2} (Option α) M) : (a : Option α) → M) a : M)
    ((f : (a : Option α) → M) a : M)
have h : Eq.{u_2 + 1} (α := M)
  (((optionElim ((f : (a : Option α) → M) none) f.some : Finsupp.{u_1, u_2} (Option α) M) : (a : Option α) → M) none :
    M)
  ((f : (a : Option α) → M) none : M)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : Finsupp.{u_1, u_2} (Option α) M
a : Option α
h :
  Eq.{u_2 + 1} (α := M)
    (((optionElim ((f : (a : Option α) → M) none) f.some : Finsupp.{u_1, u_2} (Option α) M) : (a : Option α) → M) none :
      M)
    ((f : (a : Option α) → M) none : M)
⊢ Eq.{u_2 + 1} (α := M)
    (((optionElim ((f : (a : Option α) → M) none) f.some : Finsupp.{u_1, u_2} (Option α) M) : (a : Option α) → M) a : M)
    ((f : (a : Option α) → M) a : M)
have h₁ : ∀ (val : α),
  Eq.{u_2 + 1} (α := M)
    (((optionElim ((f : (a : Option α) → M) none) f.some : Finsupp.{u_1, u_2} (Option α) M) : (a : Option α) → M)
        (Option.some val) :
      M)
    ((f : (a : Option α) → M) (Option.some val) : M)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : Finsupp.{u_1, u_2} (Option α) M
⊢ Eq.{u_2 + 1} (α := M)
    (((optionElim ((f : (a : Option α) → M) none) f.some : Finsupp.{u_1, u_2} (Option α) M) : (a : Option α) → M) none :
      M)
    ((f : (a : Option α) → M) none : M)
have h : Eq.{u_2 + 1} (α := M) ((f : (a : Option α) → M) none : M) ((f : (a : Option α) → M) none : M)
Tactic: rw [optionElim_apply_none]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
⊢ Eq (α := Finsupp.{u_1, u_2} (Option α) M) (optionElim y 0) (single none y)
have h : ∀ (a : Option α),
  Eq.{u_2 + 1} (α := M) ((optionElim y 0 : (a : Option α) → M) a : M) ((single none y : (a : Option α) → M) a : M)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
a : Option α
⊢ Eq.{u_2 + 1} (α := M) ((optionElim y 0 : (a : Option α) → M) a : M) ((single none y : (a : Option α) → M) a : M)
have h : Eq.{u_2 + 1} (α := M) ((optionElim y 0 : (a : Option α) → M) none : M) ((single none y : (a : Option α) → M) none : M)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
a : Option α
h :
  Eq.{u_2 + 1} (α := M) ((optionElim y 0 : (a : Option α) → M) none : M) ((single none y : (a : Option α) → M) none : M)
⊢ Eq.{u_2 + 1} (α := M) ((optionElim y 0 : (a : Option α) → M) a : M) ((single none y : (a : Option α) → M) a : M)
have h₁ : ∀ (val : α),
  Eq.{u_2 + 1} (α := M) ((optionElim y 0 : (a : Option α) → M) (Option.some val) : M)
    ((single none y : (a : Option α) → M) (Option.some val) : M)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
h : y ≠ 0
⊢ optionElim y f ≠ 0
have contrapose : ∀ (c : optionElim y f = 0), y = 0
Tactic: contrapose h with c
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
⊢ Eq.{u_2 + 1} (α := M) ((optionElim y f : (a : Option α) → M) none : M) ((0 : (a : Option α) → M) none : M)
have rw : Eq.{u_2 + 1} (α := M) ((0 : (a : Option α) → M) none : M) ((0 : (a : Option α) → M) none : M)
Tactic: rw [c]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (hypothesis)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
⊢ y = 0
have this : Eq.{u_2 + 1} (α := M) ((optionElim y f : (a : Option α) → M) none : M) ((0 : (a : Option α) → M) none : M)
Tactic: have : f.optionElim y none = (0 : Option α →₀ M) none := by
    rw [c]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
h : f ≠ 0
⊢ optionElim y f ≠ 0
have contrapose : ∀ (c : optionElim y f = 0), f = 0
Tactic: contrapose h with c
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
⊢ f = 0
have h : ∀ (a : α), Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
a : α
⊢ Eq.{u_2 + 1} (α := M) ((optionElim y f : (a : Option α) → M) (Option.some a) : M)
    ((0 : (a : Option α) → M) (Option.some a) : M)
have rw : Eq.{u_2 + 1} (α := M) ((0 : (a : Option α) → M) (Option.some a) : M) ((0 : (a : Option α) → M) (Option.some a) : M)
Tactic: rw [c]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (hypothesis)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
a : α
⊢ Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)
have this : Eq.{u_2 + 1} (α := M) ((optionElim y f : (a : Option α) → M) (Option.some a) : M)
  ((0 : (a : Option α) → M) (Option.some a) : M)
Tactic: have : f.optionElim y (Option.some a) = (0 : Option α →₀ M) (Option.some a) := by
    rw [c]