awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Multiset.Functor
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x : α'
l₁ l₂ : List α'
h_1 : l₁ ~ l₂
h : ofList <$> Traversable.traverse f l₁ = ofList <$> Traversable.traverse f l₂
rw rw₁ : cons <$> f x <*> ofList <$> Traversable.traverse f l₂ = cons <$> f x <*> ofList <$> Traversable.traverse f l₂
⊢ cons <$> f x <*> ofList <$> Traversable.traverse f l₁ = cons <$> f x <*> ofList <$> Traversable.traverse f l₂

Tactic:
rw [h]
-- Module: Mathlib.Data.Multiset.Functor
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x : α'
l₁ l₂ : List α'
h_1 : l₁ ~ l₂
h : ofList <$> Traversable.traverse f l₁ = ofList <$> Traversable.traverse f l₂
⊢ cons <$> f x <*> ofList <$> Traversable.traverse f l₁ = cons <$> f x <*> ofList <$> Traversable.traverse f l₂

Tactic:
have :
      Multiset.cons <$> f x <*> ofList <$> Traversable.traverse f l₁ =
        Multiset.cons <$> f x <*> ofList <$> Traversable.traverse f l₂ := by
      rw [h]
-- Module: Mathlib.Data.Multiset.Functor
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x : α'
l₁ l₂ : List α'
h_1 : l₁ ~ l₂
h : ofList <$> Traversable.traverse f l₁ = ofList <$> Traversable.traverse f l₂
this : cons <$> f x <*> ofList <$> Traversable.traverse f l₁ = cons <$> f x <*> ofList <$> Traversable.traverse f l₂
⊢ ofList <$> Traversable.traverse f (x :: l₁) = ofList <$> Traversable.traverse f (x :: l₂)

Tactic:
simpa [functor_norm] using this
-- Module: Mathlib.Data.Multiset.Functor
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
rw :
  Eq (α := F ((l : List β') → Multiset β'))
    ((flip fun (a b : β') (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) <$> f x <*> f y)
    ((fun (a b : β') (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) <$> f x <*> f y)
⊢ Eq (α := F ((l : List β') → Multiset β'))
    ((fun (a b : β') (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) <$> f y <*> f x)
    ((fun (a b : β') (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) <$> f x <*> f y)

Tactic:
rw [CommApplicative.commutative_map]

Premises used: CommApplicative.commutative_map
-- Module: Mathlib.Data.Multiset.Functor
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
e_a :
  Eq.{u + 1} (α := β' → β' → (l : List β') → Multiset β')
    (flip fun (a b : β') (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) fun (a b : β') (l : List β') ↦
    (↑(a :: b :: l) : Multiset β')
⊢ Eq (α := F ((l : List β') → Multiset β'))
    ((flip fun (a b : β') (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) <$> f x <*> f y)
    ((fun (a b : β') (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) <$> f x <*> f y)

Tactic:
congr 2
-- Module: Mathlib.Data.Multiset.Functor
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
e_a :
  ∀ (a b : β') (l : List β'),
    flip (fun (a b : β') (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) a b l = (↑(a :: b :: l) : Multiset β')
⊢ Eq.{u + 1} (α := β' → β' → (l : List β') → Multiset β')
    (flip fun (a b : β') (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) fun (a b : β') (l : List β') ↦
    (↑(a :: b :: l) : Multiset β')

Tactic:
funext a b l
-- Module: Mathlib.Data.Multiset.Functor
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : CommApplicative F
α' β' : Type u
f : α' → F β'
a_1 b_1 : List α'
x y : α'
l_1 : List α'
a b : β'
l : List β'
⊢ flip (fun (a b : β') (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) a b l = (↑(a :: b :: l) : Multiset β')

Tactic:
simpa [flip] using Perm.swap a b l

Premises used: flip, List.Perm.swap
-- Module: Mathlib.Data.Multiset.Functor
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
⊢ Eq (α := F ((l : List β') → Multiset β'))
    ((fun (a b : β') (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) <$> f y <*> f x)
    ((fun (a b : β') (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) <$> f x <*> f y)

Tactic:
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
-- Module: Mathlib.Data.Multiset.Functor
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
this :
  Eq (α := F ((l : List β') → Multiset β'))
    ((fun (a b : β') (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) <$> f y <*> f x)
    ((fun (a b : β') (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) <$> f x <*> f y)
⊢ ofList <$> Traversable.traverse f (y :: x :: l) = ofList <$> Traversable.traverse f (x :: y :: l)

Tactic:
simp [Function.comp_def, this, functor_norm]

Premises used: Function.comp_def
-- Module: Mathlib.Data.Multiset.Functor
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : CommApplicative F
α' β' : Type u
f : α' → F β'
a b l₁ l₂ l₃ : List α'
h : l₁ ~ l₂
h_1 : l₂ ~ l₃
a_ih : ofList <$> Traversable.traverse f l₁ = ofList <$> Traversable.traverse f l₂
a_ih_1 : ofList <$> Traversable.traverse f l₂ = ofList <$> Traversable.traverse f l₃
⊢ ofList <$> Traversable.traverse f l₁ = ofList <$> Traversable.traverse f l₃

Tactic:
simp [*]
-- Module: Mathlib.Data.Multiset.Functor
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)
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₃
⊢ ofList <$> Traversable.traverse f a = ofList <$> Traversable.traverse f b

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 [*]

Premises used: Multiset.cons, Function.comp_def, List.nil
-- Module: Mathlib.Data.Multiset.Functor
Goal:
α : Type u_1
⊢ Eq (α := α → Multiset α) pure singleton

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Multiset.Functor
Goal:
α β : Type u_1
⊢ Eq.{u_1 + 1} (α := Multiset α → (α → Multiset β) → Multiset β)
    (fun (x1 : Multiset α) (x2 : α → Multiset β) ↦ x1 >>= x2) bind

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Multiset.Functor
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : CommApplicative F
α' β' : Type u
f : α' → F β'
α : Type u_1
x : Multiset α
⊢ id <$> x = x

Tactic:
simp only [fmap_def, id_eq, map_id']

Premises used: Multiset.fmap_def, Multiset.map_id', id_eq
-- Module: Mathlib.Data.Multiset.Functor
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : CommApplicative F
α' β' : Type u
f : α' → F β'
α β : Type u_1
x : α
x_1 : α → Multiset β
⊢ pure x >>= x_1 = x_1 x

Tactic:
simp only [pure_def, bind_def, singleton_bind]

Premises used: Multiset.singleton_bind, Multiset.bind_def, Multiset.pure_def
-- Module: Mathlib.Data.Multiset.Functor
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : CommApplicative F
α' β' : Type u
f : α' → F β'
α β : Type u_1
x : α → β
x_1 : Multiset α
⊢ (do
      let y ← x_1
      pure (x y)) =
    x <$> x_1

Tactic:
simp only [pure_def, bind_def, bind_singleton, fmap_def]

Premises used: Multiset.fmap_def, Multiset.bind_singleton, Multiset.bind_def, Multiset.pure_def
-- Module: Mathlib.Data.Multiset.Functor
Goal:
α β : Type u_1
h : α → β
h₁ : ∀ (x : List α), (Functor.map h ∘ ofList) x = (ofList ∘ Functor.map h) x
⊢ Functor.map h ∘ ofList = ofList ∘ Functor.map h

Tactic:
funext
-- Module: Mathlib.Data.Multiset.Functor
Goal:
α β : Type u_1
h : α → β
x : List α
⊢ (Functor.map h ∘ ofList) x = (ofList ∘ Functor.map h) x

Tactic:
simp only [Function.comp_apply, fmap_def, map_coe, List.map_eq_map]

Premises used: Multiset.fmap_def, List.map_eq_map, Function.comp_apply, Multiset.map_coe
-- Module: Mathlib.Data.Multiset.Functor
Goal:
α : Type u_1
x : Multiset α
h : ∀ (a : List α), Eq (α := Id (Multiset α)) (traverse pure ⟦a⟧) (pure ⟦a⟧)
⊢ Eq (α := Id (Multiset α)) (traverse pure x) (pure x)

Tactic:
induction x using Quotient.inductionOn
-- Module: Mathlib.Data.Multiset.Functor
Goal:
α : Type u_1
a : List α
⊢ Eq (α := Id (Multiset α)) (traverse pure ⟦a⟧) (pure ⟦a⟧)

Tactic:
simp [traverse]

Premises used: Multiset.traverse
-- Module: Mathlib.Data.Multiset.Functor
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 α
h₁ : ∀ (a : List α), traverse (Comp.mk ∘ Functor.map h ∘ g) ⟦a⟧ = Comp.mk (traverse h <$> traverse g ⟦a⟧)
⊢ traverse (Comp.mk ∘ Functor.map h ∘ g) x = Comp.mk (traverse h <$> traverse g x)

Tactic:
induction x using Quotient.inductionOn
-- Module: Mathlib.Data.Multiset.Functor
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 γ
a : List α
⊢ traverse (Comp.mk ∘ Functor.map h ∘ g) ⟦a⟧ = Comp.mk (traverse h <$> traverse g ⟦a⟧)

Tactic:
simp only [traverse, quot_mk_to_coe, lift_coe, Function.comp_apply, Functor.map_map, functor_norm]

Premises used: Multiset.traverse, Multiset.quot_mk_to_coe, Function.comp_apply, Multiset.lift_coe, Functor.map_map
-- Module: Mathlib.Data.Multiset.Functor
Goal:
G : Type u_1 → Type u_1
inst : Applicative G
inst_1 : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
x : Multiset α
h₁ : ∀ (a : List α), Functor.map h <$> traverse g ⟦a⟧ = traverse (Functor.map h ∘ g) ⟦a⟧
⊢ Functor.map h <$> traverse g x = traverse (Functor.map h ∘ g) x

Tactic:
induction x using Quotient.inductionOn
-- Module: Mathlib.Data.Multiset.Functor
Goal:
G : Type u_1 → Type u_1
inst : Applicative G
inst_1 : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
a : List α
h₁ :
  (fun (a : List β) ↦ h <$> (↑a : Multiset β)) <$> Traversable.traverse g a =
    ofList <$> Traversable.traverse (Functor.map h ∘ g) a
⊢ Functor.map h <$> traverse g ⟦a⟧ = traverse (Functor.map h ∘ g) ⟦a⟧

Tactic:
simp only [traverse, quot_mk_to_coe, lift_coe, Function.comp_apply, Functor.map_map]

Premises used: Multiset.traverse, Multiset.quot_mk_to_coe, Function.comp_apply, Multiset.lift_coe, Functor.map_map
-- Module: Mathlib.Data.Multiset.Functor
Goal:
G : Type u_1 → Type u_1
inst : Applicative G
inst_1 : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
a : List α
h₁ :
  (fun (a : List β) ↦ h <$> (↑a : Multiset β)) <$> Traversable.traverse g a =
    ofList <$> (Functor.map (Functor.map h) ∘ Traversable.traverse g) a
⊢ (fun (a : List β) ↦ h <$> (↑a : Multiset β)) <$> Traversable.traverse g a =
    ofList <$> Traversable.traverse (Functor.map h ∘ g) a

Tactic:
rw [Traversable.map_traverse']

Premises used: Traversable.map_traverse'
-- Module: Mathlib.Data.Multiset.Functor
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 <$> (Functor.map (Functor.map h) ∘ Traversable.traverse g) a

Tactic:
simp only [fmap_def, Function.comp_apply, Functor.map_map, List.map_eq_map, map_coe]

Premises used: Multiset.fmap_def, List.map_eq_map, Function.comp_apply, Multiset.map_coe, Functor.map_map
-- Module: Mathlib.Data.Multiset.Functor
Goal:
G : Type u_1 → Type u_1
inst : Applicative G
inst_1 : CommApplicative G
α β γ : Type u_1
g : α → β
h : β → G γ
x : Multiset α
h₁ : ∀ (a : List α), traverse h (map g ⟦a⟧) = traverse (h ∘ g) ⟦a⟧
⊢ traverse h (map g x) = traverse (h ∘ g) x

Tactic:
induction x using Quotient.inductionOn
-- Module: Mathlib.Data.Multiset.Functor
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
⊢ traverse h (map g ⟦a⟧) = traverse (h ∘ g) ⟦a⟧

Tactic:
simp only [traverse, quot_mk_to_coe, map_coe, lift_coe, Function.comp_apply]

Premises used: Multiset.traverse, Multiset.quot_mk_to_coe, Function.comp_apply, Multiset.lift_coe, Multiset.map_coe
-- Module: Mathlib.Data.Multiset.Functor
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)
h₂ h₃ : ofList <$> Traversable.traverse h (List.map g a) = ofList <$> Traversable.traverse h (List.map g a)
⊢ 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]

Premises used: List.map_eq_map, Traversable.traverse_map
-- Module: Mathlib.Data.Multiset.Functor
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 α
h :
  ∀ (a : List α),
    Eq (α := H (Multiset β)) ((fun {α : Type u_1} ↦ eta.app α) (traverse f ⟦a⟧))
      (traverse ((fun {α : Type u_1} ↦ eta.app α) ∘ f) ⟦a⟧)
⊢ Eq (α := H (Multiset β)) ((fun {α : Type u_1} ↦ eta.app α) (traverse f x))
    (traverse ((fun {α : Type u_1} ↦ eta.app α) ∘ f) x)

Tactic:
induction x using Quotient.inductionOn
-- Module: Mathlib.Data.Multiset.Functor
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 β
a : List α
⊢ Eq (α := H (Multiset β)) ((fun {α : Type u_1} ↦ eta.app α) (traverse f ⟦a⟧))
    (traverse ((fun {α : Type u_1} ↦ eta.app α) ∘ f) ⟦a⟧)

Tactic:
simp only [quot_mk_to_coe, traverse, lift_coe, Function.comp_apply,
    ApplicativeTransformation.preserves_map, LawfulTraversable.naturality]

Premises used: Multiset.traverse, Multiset.quot_mk_to_coe, LawfulTraversable.naturality, ApplicativeTransformation.preserves_map, Function.comp_apply, Multiset.lift_coe
-- Module: Mathlib.Data.Multiset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t_1 s t x : Multiset α
⊢ Membership.mem (γ := Finset (Multiset α))
      ((fun (s t : Multiset α) ↦
          (Finset.map (Equiv.toEmbedding (Equiv.symm (AddEquiv.toEquiv equivDFinsupp)))
              (Finset.Icc ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s)
                ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t)) :
            Finset (Multiset α)))
        s t)
      x ↔
    s ≤ x ∧ x ≤ t

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ Finset.Icc s t =
    Finset.map (Equiv.toEmbedding (Equiv.symm (AddEquiv.toEquiv equivDFinsupp)))
      (Finset.Icc ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s)
        ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t))

Tactic:
rfl

Premises used: Finset.map, Finset.Icc, rfl
-- Module: Mathlib.Data.Multiset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ Eq.{u_1 + 1} (α := Finset (Multiset α))
    (Finset.map (Equiv.toEmbedding (Equiv.symm (AddEquiv.toEquiv equivDFinsupp)))
      (Finset.Icc ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) (s ⊓ t))
        ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) (s ⊔ t))))
    (Finset.map (Equiv.toEmbedding (Equiv.symm (AddEquiv.toEquiv equivDFinsupp)))
      (uIcc ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t)))

Tactic:
simp [uIcc]

Premises used: Finset.uIcc
-- Module: Mathlib.Data.Multiset.Interval
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))
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))
⊢ #(Finset.Icc s 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]

Premises used: Multiset.toDFinsupp_support, Multiset.Icc_eq, Multiset.toDFinsupp_apply, Finset.card_map, Nat.card_Icc, DFinsupp.card_Icc
-- Module: Mathlib.Data.Multiset.Interval
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
rw₁ 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
⊢ #(Finset.Ico s t) = 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]

Premises used: Finset.card_Ico_eq_card_Icc_sub_one, Multiset.card_Icc
-- Module: Mathlib.Data.Multiset.Interval
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
rw₁ 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
⊢ #(Finset.Ioc s t) = 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]

Premises used: Finset.card_Ioc_eq_card_Icc_sub_one, Multiset.card_Icc
-- Module: Mathlib.Data.Multiset.Interval
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
rw₁ 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
⊢ #(Finset.Ioo s t) = 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]

Premises used: Finset.card_Ioo_eq_card_Icc_sub_two, Multiset.card_Icc
-- Module: Mathlib.Data.Multiset.Interval
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)
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))
simp_rw₃ :
  Eq (α := ℕ)
    (∏
      x ∈
        DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s) ∪
          DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t),
      ((HSub.hSub (α := ℤ)
            (↑((((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t : Π₀ (x : α), ℕ) : (a : α) → ℕ) x) : ℤ)
            (↑((((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s : Π₀ (x : α), ℕ) : (a : α) → ℕ) x) : ℤ)).natAbs +
        1))
    (∏ i ∈ s.toFinset ∪ t.toFinset, ((HSub.hSub (α := ℤ) (↑(count i t) : ℤ) (↑(count i s) : ℤ)).natAbs + 1))
simp_rw₄ :
  Eq (α := ℕ)
    (∏
      x ∈
        DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s) ∪
          DFinsupp.support (β := fun (i : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t),
      ((HSub.hSub (α := ℤ) (↑(count x t) : ℤ) (↑(count x s) : ℤ)).natAbs + 1))
    (∏ x ∈ s.toFinset ∪ t.toFinset, ((HSub.hSub (α := ℤ) (↑(count x t) : ℤ) (↑(count x s) : ℤ)).natAbs + 1))
⊢ #(uIcc s 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]

Premises used: Multiset.toDFinsupp_support, Multiset.toDFinsupp_apply, Finset.card_map, Multiset.uIcc_eq, DFinsupp.card_uIcc, Nat.card_uIcc