awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
α : Type u_1
⊢ LT.lt (α := ℕ) ((degree : (a : Fin 2 →₀ ℕ) → ℕ) (HAdd.hAdd (α := Fin 2 →₀ ℕ) (single 0 1) (single 1 1)) : ℕ)
      ((degree : (a : Fin 2 →₀ ℕ) → ℕ)
          ((ofDegLex : (a : DegLex (Fin 2 →₀ ℕ)) → Fin 2 →₀ ℕ)
              ((toDegLex : (a : Fin 2 →₀ ℕ) → DegLex (Fin 2 →₀ ℕ)) (single 0 2)) :
            Fin 2 →₀ ℕ) :
        ℕ) ∨
    Eq (α := ℕ) ((degree : (a : Fin 2 →₀ ℕ) → ℕ) (HAdd.hAdd (α := Fin 2 →₀ ℕ) (single 0 1) (single 1 1)) : ℕ)
        ((degree : (a : Fin 2 →₀ ℕ) → ℕ)
            ((ofDegLex : (a : DegLex (Fin 2 →₀ ℕ)) → Fin 2 →₀ ℕ)
                ((toDegLex : (a : Fin 2 →₀ ℕ) → DegLex (Fin 2 →₀ ℕ)) (single 0 2)) :
              Fin 2 →₀ ℕ) :
          ℕ) ∧
      LT.lt (α := Lex (Fin 2 →₀ ℕ))
        ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (HAdd.hAdd (α := Fin 2 →₀ ℕ) (single 0 1) (single 1 1)) :
          Lex (Fin 2 →₀ ℕ))
        ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ))
            ((ofDegLex : (a : DegLex (Fin 2 →₀ ℕ)) → Fin 2 →₀ ℕ)
              ((toDegLex : (a : Fin 2 →₀ ℕ) → DegLex (Fin 2 →₀ ℕ)) (single 0 2))) :
          Lex (Fin 2 →₀ ℕ))
have simp : HAdd.hAdd (α := Lex (Fin 2 →₀ ℕ)) (β := Lex (Fin 2 →₀ ℕ))
    ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 0 1) : Lex (Fin 2 →₀ ℕ))
    ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 1 1) : Lex (Fin 2 →₀ ℕ)) <
  (toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 0 2)
Tactic: simp only [Fin.isValue, map_add, degree_single, Nat.reduceAdd, ofDegLex_toDegLex,
    lt_self_iff_false, toLex_add, true_and, false_or]
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
α : Type u_1
⊢ HAdd.hAdd (α := Lex (Fin 2 →₀ ℕ)) (β := Lex (Fin 2 →₀ ℕ))
      ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 0 1) : Lex (Fin 2 →₀ ℕ))
      ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 1 1) : Lex (Fin 2 →₀ ℕ)) <
    (toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 0 2)
have h : (∀ (j : Fin 2),
    (fun (x1 x2 : Fin 2) ↦ x1 < x2) j 0 →
      Eq (α := (@fun {i : Fin 2} ↦ ℕ) j)
        ((((ofLex : (a : Lex (Fin 2 →₀ ℕ)) → Fin 2 →₀ ℕ)
                  (HAdd.hAdd (α := Lex (Fin 2 →₀ ℕ)) (β := Lex (Fin 2 →₀ ℕ))
                    ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 0 1) : Lex (Fin 2 →₀ ℕ))
                    ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 1 1) : Lex (Fin 2 →₀ ℕ))) :
                Fin 2 →₀ ℕ) :
              (a : Fin 2) → ℕ)
            j :
          ℕ)
        ((((ofLex : (a : Lex (Fin 2 →₀ ℕ)) → Fin 2 →₀ ℕ) ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 0 2)) :
                Fin 2 →₀ ℕ) :
              (a : Fin 2) → ℕ)
            j :
          ℕ)) ∧
  (@fun {i : Fin 2} (x1 x2 : ℕ) ↦ x1 < x2) 0
    ((((ofLex : (a : Lex (Fin 2 →₀ ℕ)) → Fin 2 →₀ ℕ)
            (HAdd.hAdd (α := Lex (Fin 2 →₀ ℕ)) (β := Lex (Fin 2 →₀ ℕ))
              ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 0 1) : Lex (Fin 2 →₀ ℕ))
              ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 1 1) : Lex (Fin 2 →₀ ℕ))) :
          Fin 2 →₀ ℕ) :
        (a : Fin 2) → ℕ)
      0)
    ((((ofLex : (a : Lex (Fin 2 →₀ ℕ)) → Fin 2 →₀ ℕ) ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 0 2)) :
          Fin 2 →₀ ℕ) :
        (a : Fin 2) → ℕ)
      0)
Tactic: use 0
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
a : α
n : ℕ
⊢ (toMultiset : (a : α →₀ ℕ) → Multiset α) (single a n) = HSMul.hSMul (β := Multiset α) n {a}
have rw : HSMul.hSMul (α := ℕ) (β := Multiset α) 0 {a} = 0
Tactic: rw [toMultiset_apply, sum_single_index]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
ι : Type u_3
s : Finset ι
n : ℕ
⊢ (toMultiset : (a : ι →₀ ℕ) → Multiset ι) (∑ i ∈ s, single i n) = n • s.val
have simp_rw : ∑ i ∈ s, (toMultiset : (a : ι →₀ ℕ) → Multiset ι) (single i n) = n • s.val
Tactic: simp_rw [toMultiset_sum, Finsupp.toMultiset_single, Finset.sum_nsmul, sum_multiset_singleton]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
ι : Type u_3
s : Finset ι
n : ℕ
simp_rw : ∑ i ∈ s, (toMultiset : (a : ι →₀ ℕ) → Multiset ι) (single i n) = n • s.val
⊢ (toMultiset : (a : ι →₀ ℕ) → Multiset ι) (∑ i ∈ s, single i n) = n • s.val
have simp_rw₁ : ∑ x ∈ s, HSMul.hSMul (β := Multiset ι) n {x} = n • s.val
Tactic: simp_rw [toMultiset_sum, Finsupp.toMultiset_single, Finset.sum_nsmul, sum_multiset_singleton]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
ι : Type u_3
s : Finset ι
n : ℕ
simp_rw : ∑ i ∈ s, (toMultiset : (a : ι →₀ ℕ) → Multiset ι) (single i n) = n • s.val
simp_rw₁ : ∑ x ∈ s, HSMul.hSMul (β := Multiset ι) n {x} = n • s.val
⊢ (toMultiset : (a : ι →₀ ℕ) → Multiset ι) (∑ i ∈ s, single i n) = n • s.val
have simp_rw₂ : HSMul.hSMul (β := Multiset ι) n (∑ x ∈ s, {x}) = n • s.val
Tactic: simp_rw [toMultiset_sum, Finsupp.toMultiset_single, Finset.sum_nsmul, sum_multiset_singleton]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
β : Type u_2
f : α →₀ ℕ
g : α → β
⊢ Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) = (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g f)
have refine_1 : Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) 0) = (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g 0)
Tactic: refine f.induction ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
β : Type u_2
f : α →₀ ℕ
g : α → β
refine_1 :
  Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) 0) = (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g 0)
⊢ Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) = (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g f)
have refine_2 : ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
  a ∉ f.support →
    b ≠ 0 →
      Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) =
          (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g f) →
        Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) (single a b + f)) =
          (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g (single a b + f))
Tactic: refine f.induction ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
β : Type u_2
f : α →₀ ℕ
g : α → β
⊢ Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) 0) = (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g 0)
have refine_1 : Multiset.map g 0 = (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g 0)
Tactic: rw [toMultiset_zero, Multiset.map_zero, mapDomain_zero, toMultiset_zero]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
β : Type u_2
f : α →₀ ℕ
g : α → β
refine_1 : Multiset.map g 0 = (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g 0)
⊢ Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) 0) = (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g 0)
have refine_1₁ : Eq (α := Multiset β) (0 : Multiset β) ((toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g 0) : Multiset β)
Tactic: rw [toMultiset_zero, Multiset.map_zero, mapDomain_zero, toMultiset_zero]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
β : Type u_2
f : α →₀ ℕ
g : α → β
refine_1 : Multiset.map g 0 = (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g 0)
refine_1₁ :
  Eq (α := Multiset β) (0 : Multiset β) ((toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g 0) : Multiset β)
⊢ Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) 0) = (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g 0)
have refine_1₂ : Eq.{u_2 + 1} (α := Multiset β) 0 ((toMultiset : (a : β →₀ ℕ) → Multiset β) 0)
Tactic: rw [toMultiset_zero, Multiset.map_zero, mapDomain_zero, toMultiset_zero]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
β : Type u_2
f : α →₀ ℕ
g : α → β
refine_1 : Multiset.map g 0 = (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g 0)
refine_1₁ :
  Eq (α := Multiset β) (0 : Multiset β) ((toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g 0) : Multiset β)
refine_1₂ : Eq.{u_2 + 1} (α := Multiset β) 0 ((toMultiset : (a : β →₀ ℕ) → Multiset β) 0)
⊢ Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) 0) = (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g 0)
have refine_1₃ : Eq.{u_2 + 1} (α := Multiset β) 0 0
Tactic: rw [toMultiset_zero, Multiset.map_zero, mapDomain_zero, toMultiset_zero]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
β : Type u_2
f_1 : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
h : a ∉ f.support
h_1 : n ≠ 0
ih :
  Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) = (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g f)
⊢ Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) (single a n + f)) =
    (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g (single a n + f))
have refine_2 : HAdd.hAdd (β := Multiset β)
    (HSMul.hSMul (β := Multiset β) n ((Multiset.mapAddMonoidHom g : (a : Multiset α) → Multiset β) {a} : Multiset β))
    ((toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g f) : Multiset β) =
  HAdd.hAdd (β := Multiset β) (HSMul.hSMul (β := Multiset β) n {g a})
    ((toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g f) : Multiset β)
Tactic: rw [toMultiset_add, Multiset.map_add, ih, mapDomain_add, mapDomain_single,
      toMultiset_single, toMultiset_add, toMultiset_single, ← Multiset.coe_mapAddMonoidHom,
      (Multiset.mapAddMonoidHom g).map_nsmul]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoid α
f : α →₀ ℕ
⊢ Eq (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) f)) (f.prod fun (a : α) (n : ℕ) ↦ a ^ n)
have refine_1 : Eq.{u_1 + 1} (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) 0)) (prod 0 fun (a : α) (n : ℕ) ↦ a ^ n)
Tactic: refine f.induction ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoid α
f : α →₀ ℕ
refine_1 :
  Eq.{u_1 + 1} (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) 0))
    (prod 0 fun (a : α) (n : ℕ) ↦ a ^ n)
⊢ Eq (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) f)) (f.prod fun (a : α) (n : ℕ) ↦ a ^ n)
have refine_2 : ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
  a ∉ f.support →
    b ≠ 0 →
      Eq (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) f)) (f.prod fun (a : α) (n : ℕ) ↦ a ^ n) →
        Eq (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) (single a b + f)))
          ((single a b + f).prod fun (a : α) (n : ℕ) ↦ a ^ n)
Tactic: refine f.induction ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoid α
f : α →₀ ℕ
⊢ Eq.{u_1 + 1} (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) 0))
    (prod 0 fun (a : α) (n : ℕ) ↦ a ^ n)
have refine_1 : Eq.{u_1 + 1} (α := α) (Multiset.prod 0) (prod 0 fun (a : α) (n : ℕ) ↦ a ^ n)
Tactic: rw [toMultiset_zero, Multiset.prod_zero, Finsupp.prod_zero_index]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoid α
f : α →₀ ℕ
refine_1 : Eq.{u_1 + 1} (α := α) (Multiset.prod 0) (prod 0 fun (a : α) (n : ℕ) ↦ a ^ n)
⊢ Eq.{u_1 + 1} (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) 0))
    (prod 0 fun (a : α) (n : ℕ) ↦ a ^ n)
have refine_1₁ : Eq.{u_1 + 1} (α := α) 1 (prod 0 fun (a : α) (n : ℕ) ↦ a ^ n)
Tactic: rw [toMultiset_zero, Multiset.prod_zero, Finsupp.prod_zero_index]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoid α
f : α →₀ ℕ
refine_1 : Eq.{u_1 + 1} (α := α) (Multiset.prod 0) (prod 0 fun (a : α) (n : ℕ) ↦ a ^ n)
refine_1₁ : Eq.{u_1 + 1} (α := α) 1 (prod 0 fun (a : α) (n : ℕ) ↦ a ^ n)
⊢ Eq.{u_1 + 1} (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) 0))
    (prod 0 fun (a : α) (n : ℕ) ↦ a ^ n)
have refine_1₂ : Eq.{u_1 + 1} (α := α) 1 1
Tactic: rw [toMultiset_zero, Multiset.prod_zero, Finsupp.prod_zero_index]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : CommMonoid α
f_1 : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
h : a ∉ f.support
h_1 : n ≠ 0
ih : Eq (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) f)) (f.prod fun (a : α) (n : ℕ) ↦ a ^ n)
⊢ Eq (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) (single a n + f)))
    ((single a n + f).prod fun (a : α) (n : ℕ) ↦ a ^ n)
have refine_2 : HPow.hPow (β := ℕ) a 0 = 1
Tactic: rw [toMultiset_add, Multiset.prod_add, ih, toMultiset_single, Multiset.prod_nsmul,
      Finsupp.prod_add_index' pow_zero pow_add, Finsupp.prod_single_index, Multiset.prod_singleton]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
f : α →₀ ℕ
⊢ Multiset.toFinset ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) = f.support
have refine_1 : Eq.{u_1 + 1} (α := Finset α) (Multiset.toFinset ((toMultiset : (a : α →₀ ℕ) → Multiset α) 0)) (support (M := ℕ) 0)
Tactic: refine f.induction ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
f : α →₀ ℕ
refine_1 :
  Eq.{u_1 + 1} (α := Finset α) (Multiset.toFinset ((toMultiset : (a : α →₀ ℕ) → Multiset α) 0)) (support (M := ℕ) 0)
⊢ Multiset.toFinset ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) = f.support
have refine_2 : ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
  a ∉ f.support →
    b ≠ 0 →
      Multiset.toFinset ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) = f.support →
        Multiset.toFinset ((toMultiset : (a : α →₀ ℕ) → Multiset α) (single a b + f)) = (single a b + f).support
Tactic: refine f.induction ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
f : α →₀ ℕ
⊢ Eq.{u_1 + 1} (α := Finset α) (Multiset.toFinset ((toMultiset : (a : α →₀ ℕ) → Multiset α) 0)) (support (M := ℕ) 0)
have refine_1 : Eq.{u_1 + 1} (α := Finset α) (Multiset.toFinset 0) (support (M := ℕ) 0)
Tactic: rw [toMultiset_zero, Multiset.toFinset_zero, support_zero]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
f : α →₀ ℕ
refine_1 : Eq.{u_1 + 1} (α := Finset α) (Multiset.toFinset 0) (support (M := ℕ) 0)
⊢ Eq.{u_1 + 1} (α := Finset α) (Multiset.toFinset ((toMultiset : (a : α →₀ ℕ) → Multiset α) 0)) (support (M := ℕ) 0)
have refine_1₁ : Eq.{u_1 + 1} (α := Finset α) ∅ (support (M := ℕ) 0)
Tactic: rw [toMultiset_zero, Multiset.toFinset_zero, support_zero]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
f : α →₀ ℕ
refine_1 : Eq.{u_1 + 1} (α := Finset α) (Multiset.toFinset 0) (support (M := ℕ) 0)
refine_1₁ : Eq.{u_1 + 1} (α := Finset α) ∅ (support (M := ℕ) 0)
⊢ Eq.{u_1 + 1} (α := Finset α) (Multiset.toFinset ((toMultiset : (a : α →₀ ℕ) → Multiset α) 0)) (support (M := ℕ) 0)
have refine_1₂ : Eq.{u_1 + 1} (α := Finset α) ∅ ∅
Tactic: rw [toMultiset_zero, Multiset.toFinset_zero, support_zero]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
f_1 : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : a ∉ f.support
hn : n ≠ 0
ih : Multiset.toFinset ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) = f.support
⊢ Multiset.toFinset ((toMultiset : (a : α →₀ ℕ) → Multiset α) (single a n + f)) = (single a n + f).support
have refine_2 : Disjoint (support (single a n)) f.support
Tactic: rw [toMultiset_add, Multiset.toFinset_add, ih, toMultiset_single, support_add_eq,
      support_single _ hn, Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
f_1 : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : a ∉ f.support
hn : n ≠ 0
ih : Multiset.toFinset ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) = f.support
⊢ Disjoint (support (single a n)) f.support
have refine_2 : Disjoint {a} f.support
Tactic: refine Disjoint.mono_left support_single_subset ?_
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
f : α →₀ ℕ
a : α
⊢ Multiset.count a ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) =
    f.sum fun (x : α) (n : ℕ) ↦ Multiset.count a (HSMul.hSMul (β := Multiset α) n {x})
have rw : Multiset.count a (f.sum fun (a : α) (n : ℕ) ↦ HSMul.hSMul (β := Multiset α) n {a}) =
  f.sum fun (x : α) (n : ℕ) ↦ Multiset.count a (HSMul.hSMul (β := Multiset α) n {x})
Tactic: rw [toMultiset_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
f : α →₀ ℕ
a : α
⊢ HMul.hMul (α := ℕ) ((f : (a : α) → ℕ) a : ℕ) (Multiset.count a {a}) = (f : (a : α) → ℕ) a
have rw : HMul.hMul (α := ℕ) (β := ℕ) ((f : (a : α) → ℕ) a : ℕ) (1 : ℕ) = (f : (a : α) → ℕ) a
Tactic: rw [Multiset.count_singleton_self, mul_one]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
f : α →₀ ℕ
a : α
rw : HMul.hMul (α := ℕ) (β := ℕ) ((f : (a : α) → ℕ) a : ℕ) (1 : ℕ) = (f : (a : α) → ℕ) a
⊢ HMul.hMul (α := ℕ) ((f : (a : α) → ℕ) a : ℕ) (Multiset.count a {a}) = (f : (a : α) → ℕ) a
have rw₁ : Eq (α := ℕ) ((f : (a : α) → ℕ) a : ℕ) ((f : (a : α) → ℕ) a : ℕ)
Tactic: rw [Multiset.count_singleton_self, mul_one]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
f g : α →₀ ℕ
⊢ Eq (α := Multiset α) ((toMultiset : (a : α →₀ ℕ) → Multiset α) (f ⊔ g) : Multiset α)
    ((toMultiset : (a : α →₀ ℕ) → Multiset α) f ∪ (toMultiset : (a : α →₀ ℕ) → Multiset α) g : Multiset α)
have a : ∀ (a : α),
  Multiset.count a ((toMultiset : (a : α →₀ ℕ) → Multiset α) (f ⊔ g)) =
    Multiset.count a ((toMultiset : (a : α →₀ ℕ) → Multiset α) f ∪ (toMultiset : (a : α →₀ ℕ) → Multiset α) g)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
f g : α →₀ ℕ
a : α
⊢ Multiset.count a ((toMultiset : (a : α →₀ ℕ) → Multiset α) (f ⊔ g)) =
    Multiset.count a ((toMultiset : (a : α →₀ ℕ) → Multiset α) f ∪ (toMultiset : (a : α →₀ ℕ) → Multiset α) g)
have a : Multiset.count a ((toMultiset : (a : α →₀ ℕ) → Multiset α) (f ⊔ g)) =
  max (Multiset.count a ((toMultiset : (a : α →₀ ℕ) → Multiset α) f))
    (Multiset.count a ((toMultiset : (a : α →₀ ℕ) → Multiset α) g))
Tactic: simp_rw [Multiset.count_union, Finsupp.count_toMultiset, Finsupp.sup_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
f g : α →₀ ℕ
a_1 : α
a :
  Multiset.count a_1 ((toMultiset : (a : α →₀ ℕ) → Multiset α) (f ⊔ g)) =
    max (Multiset.count a_1 ((toMultiset : (a : α →₀ ℕ) → Multiset α) f))
      (Multiset.count a_1 ((toMultiset : (a : α →₀ ℕ) → Multiset α) g))
⊢ Multiset.count a_1 ((toMultiset : (a : α →₀ ℕ) → Multiset α) (f ⊔ g)) =
    Multiset.count a_1 ((toMultiset : (a : α →₀ ℕ) → Multiset α) f ∪ (toMultiset : (a : α →₀ ℕ) → Multiset α) g)
have a₁ : Eq (α := ℕ) ((f ⊔ g : (a : α) → ℕ) a_1 : ℕ) (max ((f : (a : α) → ℕ) a_1) ((g : (a : α) → ℕ) a_1) : ℕ)
Tactic: simp_rw [Multiset.count_union, Finsupp.count_toMultiset, Finsupp.sup_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
f g : α →₀ ℕ
⊢ Eq (α := Multiset α) ((toMultiset : (a : α →₀ ℕ) → Multiset α) (f ⊓ g) : Multiset α)
    ((toMultiset : (a : α →₀ ℕ) → Multiset α) f ∩ (toMultiset : (a : α →₀ ℕ) → Multiset α) g : Multiset α)
have a : ∀ (a : α),
  Multiset.count a ((toMultiset : (a : α →₀ ℕ) → Multiset α) (f ⊓ g)) =
    Multiset.count a ((toMultiset : (a : α →₀ ℕ) → Multiset α) f ∩ (toMultiset : (a : α →₀ ℕ) → Multiset α) g)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
f g : α →₀ ℕ
a : α
⊢ Multiset.count a ((toMultiset : (a : α →₀ ℕ) → Multiset α) (f ⊓ g)) =
    Multiset.count a ((toMultiset : (a : α →₀ ℕ) → Multiset α) f ∩ (toMultiset : (a : α →₀ ℕ) → Multiset α) g)
have a : Multiset.count a ((toMultiset : (a : α →₀ ℕ) → Multiset α) (f ⊓ g)) =
  min (Multiset.count a ((toMultiset : (a : α →₀ ℕ) → Multiset α) f))
    (Multiset.count a ((toMultiset : (a : α →₀ ℕ) → Multiset α) g))
Tactic: simp_rw [Multiset.count_inter, Finsupp.count_toMultiset, Finsupp.inf_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
f g : α →₀ ℕ
a_1 : α
a :
  Multiset.count a_1 ((toMultiset : (a : α →₀ ℕ) → Multiset α) (f ⊓ g)) =
    min (Multiset.count a_1 ((toMultiset : (a : α →₀ ℕ) → Multiset α) f))
      (Multiset.count a_1 ((toMultiset : (a : α →₀ ℕ) → Multiset α) g))
⊢ Multiset.count a_1 ((toMultiset : (a : α →₀ ℕ) → Multiset α) (f ⊓ g)) =
    Multiset.count a_1 ((toMultiset : (a : α →₀ ℕ) → Multiset α) f ∩ (toMultiset : (a : α →₀ ℕ) → Multiset α) g)
have a₁ : Eq (α := ℕ) ((f ⊓ g : (a : α) → ℕ) a_1 : ℕ) (min ((f : (a : α) → ℕ) a_1) ((g : (a : α) → ℕ) a_1) : ℕ)
Tactic: simp_rw [Multiset.count_inter, Finsupp.count_toMultiset, Finsupp.inf_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
f : α →₀ ℕ
i : α
⊢ Membership.mem (γ := Multiset α) ((toMultiset : (a : α →₀ ℕ) → Multiset α) f : Multiset α) i ↔ i ∈ f.support
have rw : Multiset.count i ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) ≠ 0 ↔ i ∈ f.support
Tactic: rw [← Multiset.count_ne_zero, Finsupp.count_toMultiset, Finsupp.mem_support_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
f : α →₀ ℕ
i : α
rw : Multiset.count i ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) ≠ 0 ↔ i ∈ f.support
⊢ Membership.mem (γ := Multiset α) ((toMultiset : (a : α →₀ ℕ) → Multiset α) f : Multiset α) i ↔ i ∈ f.support
have rw₁ : Ne (α := ℕ) ((f : (a : α) → ℕ) i : ℕ) (0 : ℕ) ↔ i ∈ f.support
Tactic: rw [← Multiset.count_ne_zero, Finsupp.count_toMultiset, Finsupp.mem_support_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
f : α →₀ ℕ
i : α
rw : Multiset.count i ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) ≠ 0 ↔ i ∈ f.support
rw₁ : Ne (α := ℕ) ((f : (a : α) → ℕ) i : ℕ) (0 : ℕ) ↔ i ∈ f.support
⊢ Membership.mem (γ := Multiset α) ((toMultiset : (a : α →₀ ℕ) → Multiset α) f : Multiset α) i ↔ i ∈ f.support
have rw₂ : Ne (α := ℕ) ((f : (a : α) → ℕ) i : ℕ) (0 : ℕ) ↔ Ne (α := ℕ) ((f : (a : α) → ℕ) i : ℕ) (0 : ℕ)
Tactic: rw [← Multiset.count_ne_zero, Finsupp.count_toMultiset, Finsupp.mem_support_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
f : α →₀ ℕ
i : α
⊢ Membership.mem (γ := Multiset α) ((toMultiset : (a : α →₀ ℕ) → Multiset α) f : Multiset α) i ↔ i ∈ f.support
have rw : Multiset.count i ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) ≠ 0 ↔ i ∈ f.support
Tactic: classical
  rw [← Multiset.count_ne_zero, Finsupp.count_toMultiset, Finsupp.mem_support_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
f : α →₀ ℕ
i : α
rw : Multiset.count i ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) ≠ 0 ↔ i ∈ f.support
⊢ Membership.mem (γ := Multiset α) ((toMultiset : (a : α →₀ ℕ) → Multiset α) f : Multiset α) i ↔ i ∈ f.support
have rw₁ : Ne (α := ℕ) ((f : (a : α) → ℕ) i : ℕ) (0 : ℕ) ↔ i ∈ f.support
Tactic: classical
  rw [← Multiset.count_ne_zero, Finsupp.count_toMultiset, Finsupp.mem_support_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Multiset (goal)
Goal:
α : Type u_1
f : α →₀ ℕ
i : α
rw : Multiset.count i ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) ≠ 0 ↔ i ∈ f.support
rw₁ : Ne (α := ℕ) ((f : (a : α) → ℕ) i : ℕ) (0 : ℕ) ↔ i ∈ f.support
⊢ Membership.mem (γ := Multiset α) ((toMultiset : (a : α →₀ ℕ) → Multiset α) f : Multiset α) i ↔ i ∈ f.support
have rw₂ : Ne (α := ℕ) ((f : (a : α) → ℕ) i : ℕ) (0 : ℕ) ↔ Ne (α := ℕ) ((f : (a : α) → ℕ) i : ℕ) (0 : ℕ)
Tactic: classical
  rw [← Multiset.count_ne_zero, Finsupp.count_toMultiset, Finsupp.mem_support_iff]