awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Multiset.Functor (goal)
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
p : a ≈ b
⊢ ofList <$> Traversable.traverse f a = ofList <$> Traversable.traverse f b
have nil : ofList <$> Traversable.traverse f [] = ofList <$> Traversable.traverse f []
Tactic: induction p with
  | nil => rfl
  | @cons x l₁ l₂ _ h =>
    have :
      Multiset.cons <$> f x <*> ofList <$> Traversable.traverse f l₁ =
        Multiset.cons <$> f x <*> ofList <$> Traversable.traverse f l₂ := by
      rw [h]
    simpa [functor_norm] using this
  | swap x y l =>
    have :
      (fun a b (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) <$> f y <*> f x =
        (fun a b l ↦ ↑(a :: b :: l)) <$> f x <*> f y := by
      rw [CommApplicative.commutative_map]
      congr 2
      funext a b l
      simpa [flip] using Perm.swap a b l
    simp [Function.comp_def, this, functor_norm]
  | trans => simp [*]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.Multiset.Functor (goal)
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
p : a ≈ b
nil : ofList <$> Traversable.traverse f [] = ofList <$> Traversable.traverse f []
⊢ ofList <$> Traversable.traverse f a = ofList <$> Traversable.traverse f b
have cons : ∀ (x : α') {l₁ l₂ : List α'},
  l₁ ~ l₂ →
    ∀ (h : ofList <$> Traversable.traverse f l₁ = ofList <$> Traversable.traverse f l₂),
      ofList <$> Traversable.traverse f (x :: l₁) = ofList <$> Traversable.traverse f (x :: l₂)
Tactic: induction p with
  | nil => rfl
  | @cons x l₁ l₂ _ h =>
    have :
      Multiset.cons <$> f x <*> ofList <$> Traversable.traverse f l₁ =
        Multiset.cons <$> f x <*> ofList <$> Traversable.traverse f l₂ := by
      rw [h]
    simpa [functor_norm] using this
  | swap x y l =>
    have :
      (fun a b (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) <$> f y <*> f x =
        (fun a b l ↦ ↑(a :: b :: l)) <$> f x <*> f y := by
      rw [CommApplicative.commutative_map]
      congr 2
      funext a b l
      simpa [flip] using Perm.swap a b l
    simp [Function.comp_def, this, functor_norm]
  | trans => simp [*]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.Multiset.Functor (goal)
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
p : a ≈ b
nil : ofList <$> Traversable.traverse f [] = ofList <$> Traversable.traverse f []
cons :
  ∀ (x : α') {l₁ l₂ : List α'},
    l₁ ~ l₂ →
      ∀ (h : ofList <$> Traversable.traverse f l₁ = ofList <$> Traversable.traverse f l₂),
        ofList <$> Traversable.traverse f (x :: l₁) = ofList <$> Traversable.traverse f (x :: l₂)
⊢ ofList <$> Traversable.traverse f a = ofList <$> Traversable.traverse f b
have swap : ∀ (x y : α') (l : List α'),
  ofList <$> Traversable.traverse f (y :: x :: l) = ofList <$> Traversable.traverse f (x :: y :: l)
Tactic: induction p with
  | nil => rfl
  | @cons x l₁ l₂ _ h =>
    have :
      Multiset.cons <$> f x <*> ofList <$> Traversable.traverse f l₁ =
        Multiset.cons <$> f x <*> ofList <$> Traversable.traverse f l₂ := by
      rw [h]
    simpa [functor_norm] using this
  | swap x y l =>
    have :
      (fun a b (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) <$> f y <*> f x =
        (fun a b l ↦ ↑(a :: b :: l)) <$> f x <*> f y := by
      rw [CommApplicative.commutative_map]
      congr 2
      funext a b l
      simpa [flip] using Perm.swap a b l
    simp [Function.comp_def, this, functor_norm]
  | trans => simp [*]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.Multiset.Functor (goal)
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
p : a ≈ b
nil : ofList <$> Traversable.traverse f [] = ofList <$> Traversable.traverse f []
cons :
  ∀ (x : α') {l₁ l₂ : List α'},
    l₁ ~ l₂ →
      ∀ (h : ofList <$> Traversable.traverse f l₁ = ofList <$> Traversable.traverse f l₂),
        ofList <$> Traversable.traverse f (x :: l₁) = ofList <$> Traversable.traverse f (x :: l₂)
swap :
  ∀ (x y : α') (l : List α'),
    ofList <$> Traversable.traverse f (y :: x :: l) = ofList <$> Traversable.traverse f (x :: y :: l)
⊢ ofList <$> Traversable.traverse f a = ofList <$> Traversable.traverse f b
have trans : ∀ {l₁ l₂ l₃ : List α'},
  l₁ ~ l₂ →
    l₂ ~ l₃ →
      ofList <$> Traversable.traverse f l₁ = ofList <$> Traversable.traverse f l₂ →
        ofList <$> Traversable.traverse f l₂ = ofList <$> Traversable.traverse f l₃ →
          ofList <$> Traversable.traverse f l₁ = ofList <$> Traversable.traverse f l₃
Tactic: induction p with
  | nil => rfl
  | @cons x l₁ l₂ _ h =>
    have :
      Multiset.cons <$> f x <*> ofList <$> Traversable.traverse f l₁ =
        Multiset.cons <$> f x <*> ofList <$> Traversable.traverse f l₂ := by
      rw [h]
    simpa [functor_norm] using this
  | swap x y l =>
    have :
      (fun a b (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) <$> f y <*> f x =
        (fun a b l ↦ ↑(a :: b :: l)) <$> f x <*> f y := by
      rw [CommApplicative.commutative_map]
      congr 2
      funext a b l
      simpa [flip] using Perm.swap a b l
    simp [Function.comp_def, this, functor_norm]
  | trans => simp [*]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.Multiset.Functor (goal)
Goal:
α β : Type u_1
h : α → β
⊢ Functor.map h ∘ ofList = ofList ∘ Functor.map h
have h₁ : ∀ (x : List α), (Functor.map h ∘ ofList) x = (ofList ∘ Functor.map h) x
Tactic: funext
-- Lean 4 proof step from Mathlib.Data.Multiset.Functor (goal)
Goal:
α : Type u_1
x : Multiset α
⊢ Eq (α := Id (Multiset α)) (traverse pure x) (pure x)
have h : ∀ (a : List α), Eq (α := Id (Multiset α)) (traverse pure ⟦a⟧) (pure ⟦a⟧)
Tactic: induction x using Quotient.inductionOn
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Multiset.Functor (goal)
Goal:
G H : Type u_1 → Type u_1
inst : Applicative G
inst_1 : Applicative H
inst_2 : CommApplicative G
inst_3 : CommApplicative H
α β γ : Type u_1
g : α → G β
h : β → H γ
x : Multiset α
⊢ traverse (Comp.mk ∘ Functor.map h ∘ g) x = Comp.mk (traverse h <$> traverse g x)
have h₁ : ∀ (a : List α), traverse (Comp.mk ∘ Functor.map h ∘ g) ⟦a⟧ = Comp.mk (traverse h <$> traverse g ⟦a⟧)
Tactic: induction x using Quotient.inductionOn
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Multiset.Functor (goal)
Goal:
G : Type u_1 → Type u_1
inst : Applicative G
inst_1 : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
x : Multiset α
⊢ Functor.map h <$> traverse g x = traverse (Functor.map h ∘ g) x
have h₁ : ∀ (a : List α), Functor.map h <$> traverse g ⟦a⟧ = traverse (Functor.map h ∘ g) ⟦a⟧
Tactic: induction x using Quotient.inductionOn
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Multiset.Functor (goal)
Goal:
G : Type u_1 → Type u_1
inst : Applicative G
inst_1 : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
a : List α
⊢ Functor.map h <$> traverse g ⟦a⟧ = traverse (Functor.map h ∘ g) ⟦a⟧
have h₁ : (fun (a : List β) ↦ h <$> (↑a : Multiset β)) <$> Traversable.traverse g a =
  ofList <$> Traversable.traverse (Functor.map h ∘ g) a
Tactic: simp only [traverse, quot_mk_to_coe, lift_coe, Function.comp_apply, Functor.map_map]
-- Lean 4 proof step from Mathlib.Data.Multiset.Functor (goal)
Goal:
G : Type u_1 → Type u_1
inst : Applicative G
inst_1 : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
a : List α
⊢ (fun (a : List β) ↦ h <$> (↑a : Multiset β)) <$> Traversable.traverse g a =
    ofList <$> Traversable.traverse (Functor.map h ∘ g) a
have h₁ : (fun (a : List β) ↦ h <$> (↑a : Multiset β)) <$> Traversable.traverse g a =
  ofList <$> (Functor.map (Functor.map h) ∘ Traversable.traverse g) a
Tactic: rw [Traversable.map_traverse']
-- Lean 4 proof step from Mathlib.Data.Multiset.Functor (goal)
Goal:
G : Type u_1 → Type u_1
inst : Applicative G
inst_1 : CommApplicative G
α β γ : Type u_1
g : α → β
h : β → G γ
x : Multiset α
⊢ traverse h (map g x) = traverse (h ∘ g) x
have h₁ : ∀ (a : List α), traverse h (map g ⟦a⟧) = traverse (h ∘ g) ⟦a⟧
Tactic: induction x using Quotient.inductionOn
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Multiset.Functor (goal)
Goal:
G : Type u_1 → Type u_1
inst : Applicative G
inst_1 : CommApplicative G
α β γ : Type u_1
g : α → β
h : β → G γ
a : List α
⊢ traverse h (map g ⟦a⟧) = traverse (h ∘ g) ⟦a⟧
have h₁ : ofList <$> Traversable.traverse h (List.map g a) = ofList <$> Traversable.traverse (h ∘ g) a
Tactic: simp only [traverse, quot_mk_to_coe, map_coe, lift_coe, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Multiset.Functor (goal)
Goal:
G : Type u_1 → Type u_1
inst : Applicative G
inst_1 : CommApplicative G
α β γ : Type u_1
g : α → β
h : β → G γ
a : List α
⊢ ofList <$> Traversable.traverse h (List.map g a) = ofList <$> Traversable.traverse (h ∘ g) a
have h₁ : ofList <$> Traversable.traverse h (List.map g a) = ofList <$> Traversable.traverse h (g <$> a)
Tactic: rw [← Traversable.traverse_map h g, List.map_eq_map]
-- Lean 4 proof step from Mathlib.Data.Multiset.Functor (goal)
Goal:
G : Type u_1 → Type u_1
inst : Applicative G
inst_1 : CommApplicative G
α β γ : Type u_1
g : α → β
h : β → G γ
a : List α
h₁ : ofList <$> Traversable.traverse h (List.map g a) = ofList <$> Traversable.traverse h (g <$> a)
⊢ ofList <$> Traversable.traverse h (List.map g a) = ofList <$> Traversable.traverse (h ∘ g) a
have h₂ : ofList <$> Traversable.traverse h (List.map g a) = ofList <$> Traversable.traverse h (List.map g a)
Tactic: rw [← Traversable.traverse_map h g, List.map_eq_map]
-- Lean 4 proof step from Mathlib.Data.Multiset.Functor (goal)
Goal:
G H : Type u_1 → Type u_1
inst : Applicative G
inst_1 : Applicative H
inst_2 : CommApplicative G
inst_3 : CommApplicative H
eta : ApplicativeTransformation G H
α β : Type u_1
f : α → G β
x : Multiset α
⊢ Eq (α := H (Multiset β)) ((fun {α : Type u_1} ↦ eta.app α) (traverse f x))
    (traverse ((fun {α : Type u_1} ↦ eta.app α) ∘ f) x)
have h : ∀ (a : List α),
  Eq (α := H (Multiset β)) ((fun {α : Type u_1} ↦ eta.app α) (traverse f ⟦a⟧))
    (traverse ((fun {α : Type u_1} ↦ eta.app α) ∘ f) ⟦a⟧)
Tactic: induction x using Quotient.inductionOn
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Multiset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ #(Finset.Icc s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)
have simp_rw : Finset.card.{u_1} (α := Multiset α)
    (Finset.map (Equiv.toEmbedding (Equiv.symm (AddEquiv.toEquiv equivDFinsupp)))
      (Finset.Icc ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s)
        ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t))) =
  ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)
Tactic: simp_rw [Icc_eq, Finset.card_map, DFinsupp.card_Icc, Nat.card_Icc, Multiset.toDFinsupp_apply,
    toDFinsupp_support]
-- Lean 4 proof step from Mathlib.Data.Multiset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
simp_rw :
  Finset.card.{u_1} (α := Multiset α)
      (Finset.map (Equiv.toEmbedding (Equiv.symm (AddEquiv.toEquiv equivDFinsupp)))
        (Finset.Icc ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s)
          ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t))) =
    ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)
⊢ #(Finset.Icc s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)
have simp_rw₁ : Finset.card (α := Π₀ (x : α), ℕ)
    (Finset.Icc ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s)
        ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t) :
      Finset (Π₀ (x : α), ℕ)) =
  ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)
Tactic: simp_rw [Icc_eq, Finset.card_map, DFinsupp.card_Icc, Nat.card_Icc, Multiset.toDFinsupp_apply,
    toDFinsupp_support]
-- Lean 4 proof step from Mathlib.Data.Multiset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
simp_rw :
  Finset.card.{u_1} (α := Multiset α)
      (Finset.map (Equiv.toEmbedding (Equiv.symm (AddEquiv.toEquiv equivDFinsupp)))
        (Finset.Icc ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s)
          ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t))) =
    ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)
simp_rw₁ :
  Finset.card (α := Π₀ (x : α), ℕ)
      (Finset.Icc ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s)
          ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t) :
        Finset (Π₀ (x : α), ℕ)) =
    ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)
⊢ #(Finset.Icc s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)
have simp_rw₂ : Eq (α := ℕ)
  (∏
    i ∈
      DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s) ∪
        DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t),
    #(Finset.Icc ((((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s : Π₀ (x : α), ℕ) : (a : α) → ℕ) i)
        ((((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t : Π₀ (x : α), ℕ) : (a : α) → ℕ) i)))
  (∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s))
Tactic: simp_rw [Icc_eq, Finset.card_map, DFinsupp.card_Icc, Nat.card_Icc, Multiset.toDFinsupp_apply,
    toDFinsupp_support]
-- Lean 4 proof step from Mathlib.Data.Multiset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
simp_rw :
  Finset.card.{u_1} (α := Multiset α)
      (Finset.map (Equiv.toEmbedding (Equiv.symm (AddEquiv.toEquiv equivDFinsupp)))
        (Finset.Icc ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s)
          ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t))) =
    ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)
simp_rw₁ :
  Finset.card (α := Π₀ (x : α), ℕ)
      (Finset.Icc ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s)
          ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t) :
        Finset (Π₀ (x : α), ℕ)) =
    ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)
simp_rw₂ :
  Eq (α := ℕ)
    (∏
      i ∈
        DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s) ∪
          DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t),
      #(Finset.Icc ((((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s : Π₀ (x : α), ℕ) : (a : α) → ℕ) i)
          ((((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t : Π₀ (x : α), ℕ) : (a : α) → ℕ) i)))
    (∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s))
⊢ #(Finset.Icc s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)
have simp_rw₃ : Eq (α := ℕ)
  (∏
    x ∈
      DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s) ∪
        DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t),
    ((((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t : Π₀ (x : α), ℕ) : (a : α) → ℕ) x + 1 -
      (((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s : Π₀ (x : α), ℕ) : (a : α) → ℕ) x))
  (∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s))
Tactic: simp_rw [Icc_eq, Finset.card_map, DFinsupp.card_Icc, Nat.card_Icc, Multiset.toDFinsupp_apply,
    toDFinsupp_support]
-- Lean 4 proof step from Mathlib.Data.Multiset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
simp_rw :
  Finset.card.{u_1} (α := Multiset α)
      (Finset.map (Equiv.toEmbedding (Equiv.symm (AddEquiv.toEquiv equivDFinsupp)))
        (Finset.Icc ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s)
          ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t))) =
    ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)
simp_rw₁ :
  Finset.card (α := Π₀ (x : α), ℕ)
      (Finset.Icc ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s)
          ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t) :
        Finset (Π₀ (x : α), ℕ)) =
    ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)
simp_rw₂ :
  Eq (α := ℕ)
    (∏
      i ∈
        DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s) ∪
          DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t),
      #(Finset.Icc ((((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s : Π₀ (x : α), ℕ) : (a : α) → ℕ) i)
          ((((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t : Π₀ (x : α), ℕ) : (a : α) → ℕ) i)))
    (∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s))
simp_rw₃ :
  Eq (α := ℕ)
    (∏
      x ∈
        DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s) ∪
          DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t),
      ((((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t : Π₀ (x : α), ℕ) : (a : α) → ℕ) x + 1 -
        (((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s : Π₀ (x : α), ℕ) : (a : α) → ℕ) x))
    (∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s))
⊢ #(Finset.Icc s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)
have simp_rw₄ : Eq (α := ℕ)
  (∏
    x ∈
      DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s) ∪
        DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t),
    (count x t + 1 - count x s))
  (∏ x ∈ s.toFinset ∪ t.toFinset, (count x t + 1 - count x s))
Tactic: simp_rw [Icc_eq, Finset.card_map, DFinsupp.card_Icc, Nat.card_Icc, Multiset.toDFinsupp_apply,
    toDFinsupp_support]
-- Lean 4 proof step from Mathlib.Data.Multiset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ #(Finset.Ico s t) = HSub.hSub (α := ℕ) (∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)) 1
have rw : #(Finset.Icc s t) - 1 = HSub.hSub (α := ℕ) (∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)) 1
Tactic: rw [Finset.card_Ico_eq_card_Icc_sub_one, card_Icc]
-- Lean 4 proof step from Mathlib.Data.Multiset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
rw : #(Finset.Icc s t) - 1 = HSub.hSub (α := ℕ) (∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)) 1
⊢ #(Finset.Ico s t) = HSub.hSub (α := ℕ) (∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)) 1
have rw₁ : HSub.hSub (α := ℕ) (∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)) 1 =
  HSub.hSub (α := ℕ) (∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)) 1
Tactic: rw [Finset.card_Ico_eq_card_Icc_sub_one, card_Icc]
-- Lean 4 proof step from Mathlib.Data.Multiset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ #(Finset.Ioc s t) = HSub.hSub (α := ℕ) (∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)) 1
have rw : #(Finset.Icc s t) - 1 = HSub.hSub (α := ℕ) (∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)) 1
Tactic: rw [Finset.card_Ioc_eq_card_Icc_sub_one, card_Icc]
-- Lean 4 proof step from Mathlib.Data.Multiset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
rw : #(Finset.Icc s t) - 1 = HSub.hSub (α := ℕ) (∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)) 1
⊢ #(Finset.Ioc s t) = HSub.hSub (α := ℕ) (∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)) 1
have rw₁ : HSub.hSub (α := ℕ) (∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)) 1 =
  HSub.hSub (α := ℕ) (∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)) 1
Tactic: rw [Finset.card_Ioc_eq_card_Icc_sub_one, card_Icc]
-- Lean 4 proof step from Mathlib.Data.Multiset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ #(Finset.Ioo s t) = HSub.hSub (α := ℕ) (∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)) 2
have rw : #(Finset.Icc s t) - 2 = HSub.hSub (α := ℕ) (∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)) 2
Tactic: rw [Finset.card_Ioo_eq_card_Icc_sub_two, card_Icc]
-- Lean 4 proof step from Mathlib.Data.Multiset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
rw : #(Finset.Icc s t) - 2 = HSub.hSub (α := ℕ) (∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)) 2
⊢ #(Finset.Ioo s t) = HSub.hSub (α := ℕ) (∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)) 2
have rw₁ : HSub.hSub (α := ℕ) (∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)) 2 =
  HSub.hSub (α := ℕ) (∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)) 2
Tactic: rw [Finset.card_Ioo_eq_card_Icc_sub_two, card_Icc]
-- Lean 4 proof step from Mathlib.Data.Multiset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ #(uIcc s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, ((HSub.hSub (α := ℤ) (↑(count i t) : ℤ) (↑(count i s) : ℤ)).natAbs + 1)
have simp_rw : Finset.card.{u_1} (α := Multiset α)
    (Finset.map (Equiv.toEmbedding (Equiv.symm (AddEquiv.toEquiv equivDFinsupp)))
      (uIcc ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t))) =
  ∏ i ∈ s.toFinset ∪ t.toFinset, ((HSub.hSub (α := ℤ) (↑(count i t) : ℤ) (↑(count i s) : ℤ)).natAbs + 1)
Tactic: simp_rw [uIcc_eq, Finset.card_map, DFinsupp.card_uIcc, Nat.card_uIcc, Multiset.toDFinsupp_apply,
    toDFinsupp_support]
-- Lean 4 proof step from Mathlib.Data.Multiset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
simp_rw :
  Finset.card.{u_1} (α := Multiset α)
      (Finset.map (Equiv.toEmbedding (Equiv.symm (AddEquiv.toEquiv equivDFinsupp)))
        (uIcc ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s)
          ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t))) =
    ∏ i ∈ s.toFinset ∪ t.toFinset, ((HSub.hSub (α := ℤ) (↑(count i t) : ℤ) (↑(count i s) : ℤ)).natAbs + 1)
⊢ #(uIcc s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, ((HSub.hSub (α := ℤ) (↑(count i t) : ℤ) (↑(count i s) : ℤ)).natAbs + 1)
have simp_rw₁ : Finset.card (α := Π₀ (x : α), ℕ)
    (uIcc ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t) :
      Finset (Π₀ (x : α), ℕ)) =
  ∏ i ∈ s.toFinset ∪ t.toFinset, ((HSub.hSub (α := ℤ) (↑(count i t) : ℤ) (↑(count i s) : ℤ)).natAbs + 1)
Tactic: simp_rw [uIcc_eq, Finset.card_map, DFinsupp.card_uIcc, Nat.card_uIcc, Multiset.toDFinsupp_apply,
    toDFinsupp_support]
-- Lean 4 proof step from Mathlib.Data.Multiset.Interval (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
simp_rw :
  Finset.card.{u_1} (α := Multiset α)
      (Finset.map (Equiv.toEmbedding (Equiv.symm (AddEquiv.toEquiv equivDFinsupp)))
        (uIcc ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s)
          ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t))) =
    ∏ i ∈ s.toFinset ∪ t.toFinset, ((HSub.hSub (α := ℤ) (↑(count i t) : ℤ) (↑(count i s) : ℤ)).natAbs + 1)
simp_rw₁ :
  Finset.card (α := Π₀ (x : α), ℕ)
      (uIcc ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t) :
        Finset (Π₀ (x : α), ℕ)) =
    ∏ i ∈ s.toFinset ∪ t.toFinset, ((HSub.hSub (α := ℤ) (↑(count i t) : ℤ) (↑(count i s) : ℤ)).natAbs + 1)
⊢ #(uIcc s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, ((HSub.hSub (α := ℤ) (↑(count i t) : ℤ) (↑(count i s) : ℤ)).natAbs + 1)
have simp_rw₂ : Eq (α := ℕ)
  (∏
    i ∈
      DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s) ∪
        DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t),
    #(uIcc ((((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s : Π₀ (x : α), ℕ) : (a : α) → ℕ) i)
        ((((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t : Π₀ (x : α), ℕ) : (a : α) → ℕ) i)))
  (∏ i ∈ s.toFinset ∪ t.toFinset, ((HSub.hSub (α := ℤ) (↑(count i t) : ℤ) (↑(count i s) : ℤ)).natAbs + 1))
Tactic: simp_rw [uIcc_eq, Finset.card_map, DFinsupp.card_uIcc, Nat.card_uIcc, Multiset.toDFinsupp_apply,
    toDFinsupp_support]