awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
p : Multiset α → Sort u_3
n : ℕ
H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁
s : Multiset α
rw rw₁ :
  (H s fun {t : Multiset α} (ht : t.card ≤ n) (_h : s < t) ↦ strongDownwardInduction (p := p) H t ht) =
    H s fun {t₂ : Multiset α} (ht : t₂.card ≤ n) (_hst : s < t₂) ↦ strongDownwardInduction (p := p) H t₂ ht
⊢ strongDownwardInduction (p := p) H s =
    H s fun {t₂ : Multiset α} (ht : t₂.card ≤ n) (_hst : s < t₂) ↦ strongDownwardInduction (p := p) H t₂ ht

Tactic:
rw [strongDownwardInduction]

Premises used: Multiset.strongDownwardInduction
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
p : Multiset α → Sort u_3
s : Multiset α
n : ℕ
H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁
dsimp :
  (fun (a : s.card ≤ n) ↦ strongDownwardInduction (p := fun (x : Multiset α) ↦ p x) H s a) =
    H s fun {t : Multiset α} (ht : t.card ≤ n) (_h : s < t) ↦
      strongDownwardInduction (p := fun (x : Multiset α) ↦ p x) H t ht
⊢ (fun (a : s.card ≤ n) ↦ s.strongDownwardInductionOn (p := fun (x : Multiset α) ↦ p x) H a) =
    H s fun {t : Multiset α} (ht : t.card ≤ n) (_h : s < t) ↦
      t.strongDownwardInductionOn (p := fun (x : Multiset α) ↦ p x) H ht

Tactic:
dsimp only [strongDownwardInductionOn]
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
p : Multiset α → Sort u_3
s : Multiset α
n : ℕ
H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁
rw rw₁ :
  (fun (a : s.card ≤ n) ↦
      H s
        (fun {t : Multiset α} (ht : t.card ≤ n) (_h : s < t) ↦
          strongDownwardInduction (p := fun (x : Multiset α) ↦ p x) H t ht)
        a) =
    H s fun {t : Multiset α} (ht : t.card ≤ n) (_h : s < t) ↦
      strongDownwardInduction (p := fun (x : Multiset α) ↦ p x) H t ht
⊢ (fun (a : s.card ≤ n) ↦ strongDownwardInduction (p := fun (x : Multiset α) ↦ p x) H s a) =
    H s fun {t : Multiset α} (ht : t.card ≤ n) (_h : s < t) ↦
      strongDownwardInduction (p := fun (x : Multiset α) ↦ p x) H t ht

Tactic:
rw [strongDownwardInduction]

Premises used: Multiset.strongDownwardInduction
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
inst : DecidablePred p
l : Multiset α
a b : List α
_ :
  ∀ (p_1 : a ≈ b),
    Eq (α := (_hp : ∃! a : α, a ∈ ⟦b⟧ ∧ p a) → { a : α // a ∈ ⟦b⟧ ∧ p a })
      (Eq.ndrec (motive := fun (x : Multiset α) ↦ (_hp : ∃! a : α, a ∈ x ∧ p a) → { a : α // a ∈ x ∧ p a })
          (fun (ex_unique : ∃! a_1 : α, a_1 ∈ ⟦a⟧ ∧ p a_1) ↦ List.chooseX p a ⋯) ⋯ :
        (_hp : ∃! a : α, a ∈ ⟦b⟧ ∧ p a) → { a : α // a ∈ ⟦b⟧ ∧ p a })
      fun (ex_unique : ∃! a : α, a ∈ ⟦b⟧ ∧ p a) ↦ List.chooseX p b ⋯
⊢ ∀ (p_1 : a ≈ b),
    Eq (α := (_hp : ∃! a : α, a ∈ ⟦b⟧ ∧ p a) → { a : α // a ∈ ⟦b⟧ ∧ p a })
      (Eq.ndrec (motive := fun (x : Multiset α) ↦ (_hp : ∃! a : α, a ∈ x ∧ p a) → { a : α // a ∈ x ∧ p a })
          (fun (ex_unique : ∃! a_1 : α, a_1 ∈ ⟦a⟧ ∧ p a_1) ↦ List.chooseX p a ⋯) ⋯ :
        (_hp : ∃! a : α, a ∈ ⟦b⟧ ∧ p a) → { a : α // a ∈ ⟦b⟧ ∧ p a })
      fun (ex_unique : ∃! a : α, a ∈ ⟦b⟧ ∧ p a) ↦ List.chooseX p b ⋯

Tactic:
_
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
inst : DecidablePred p
l : Multiset α
a b : List α
p_1 : a ≈ b
h :
  ∀ (hp : ∃! a : α, a ∈ ⟦b⟧ ∧ p a),
    Eq.ndrec (motive := fun (x : Multiset α) ↦ (_hp : ∃! a : α, a ∈ x ∧ p a) → { a : α // a ∈ x ∧ p a })
        (fun (ex_unique : ∃! a_1 : α, a_1 ∈ ⟦a⟧ ∧ p a_1) ↦ List.chooseX p a ⋯) ⋯ hp =
      List.chooseX p b ⋯
⊢ Eq (α := (_hp : ∃! a : α, a ∈ ⟦b⟧ ∧ p a) → { a : α // a ∈ ⟦b⟧ ∧ p a })
    (Eq.ndrec (motive := fun (x : Multiset α) ↦ (_hp : ∃! a : α, a ∈ x ∧ p a) → { a : α // a ∈ x ∧ p a })
        (fun (ex_unique : ∃! a_1 : α, a_1 ∈ ⟦a⟧ ∧ p a_1) ↦ List.chooseX p a ⋯) ⋯ :
      (_hp : ∃! a : α, a ∈ ⟦b⟧ ∧ p a) → { a : α // a ∈ ⟦b⟧ ∧ p a })
    fun (ex_unique : ∃! a : α, a ∈ ⟦b⟧ ∧ p a) ↦ List.chooseX p b ⋯

Tactic:
funext hp
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
inst : DecidablePred p
l : Multiset α
a b : List α
p_1 : a ≈ b
hp : ∃! a : α, a ∈ ⟦b⟧ ∧ p a
all_equal : ∀ (x y : { t : α // t ∈ b ∧ p t }), x = y
⊢ Eq.ndrec (motive := fun (x : Multiset α) ↦ (_hp : ∃! a : α, a ∈ x ∧ p a) → { a : α // a ∈ x ∧ p a })
      (fun (ex_unique : ∃! a_1 : α, a_1 ∈ ⟦a⟧ ∧ p a_1) ↦ List.chooseX p a ⋯) ⋯ hp =
    List.chooseX p b ⋯

Tactic:
apply all_equal
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
inst : DecidablePred p
l : Multiset α
a b : List α
p_1 : a ≈ b
hp : ∃! a : α, a ∈ ⟦b⟧ ∧ p a
h : ∀ (x y : { t : α // t ∈ b ∧ p t }), x = y
⊢ Eq.ndrec (motive := fun (x : Multiset α) ↦ (_hp : ∃! a : α, a ∈ x ∧ p a) → { a : α // a ∈ x ∧ p a })
      (fun (ex_unique : ∃! a_1 : α, a_1 ∈ ⟦a⟧ ∧ p a_1) ↦ List.chooseX p a ⋯) ⋯ hp =
    List.chooseX p b ⋯

Tactic:
suffices all_equal : ∀ x y : { t // t ∈ b ∧ p t }, x = y by
        apply all_equal
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
inst : DecidablePred p
l : Multiset α
a b : List α
p_1 : a ≈ b
hp : ∃! a : α, a ∈ ⟦b⟧ ∧ p a
x : α
px : x ∈ b ∧ p x
y : α
py : y ∈ b ∧ p y
h :
  ∀ (z : α) (z_unique : ∀ (y : α), (fun (a : α) ↦ a ∈ ⟦b⟧ ∧ p a) y → y = z) (_z_mem_l : z ∈ ⟦b⟧) (_pz : p z),
    Eq (α := { t : α // t ∈ b ∧ p t }) (mk (p := fun (t : α) ↦ t ∈ b ∧ p t) x px)
      (mk (p := fun (t : α) ↦ t ∈ b ∧ p t) y py)
⊢ Eq (α := { t : α // t ∈ b ∧ p t }) (mk (p := fun (t : α) ↦ t ∈ b ∧ p t) x px)
    (mk (p := fun (t : α) ↦ t ∈ b ∧ p t) y py)

Tactic:
rcases hp with ⟨z, ⟨_z_mem_l, _pz⟩, z_unique⟩
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
inst : DecidablePred p
l : Multiset α
a b : List α
p_1 : a ≈ b
x : α
px : x ∈ b ∧ p x
y : α
py : y ∈ b ∧ p y
z : α
z_unique : ∀ (y : α), (fun (a : α) ↦ a ∈ ⟦b⟧ ∧ p a) y → y = z
_z_mem_l : z ∈ ⟦b⟧
_pz : p z
h : x = y
⊢ Eq (α := { t : α // t ∈ b ∧ p t }) (mk (p := fun (t : α) ↦ t ∈ b ∧ p t) x px)
    (mk (p := fun (t : α) ↦ t ∈ b ∧ p t) y py)

Tactic:
congr
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
inst : DecidablePred p
l : Multiset α
a b : List α
p_1 : a ≈ b
x : α
px : x ∈ b ∧ p x
y : α
py : y ∈ b ∧ p y
z : α
z_unique : ∀ (y : α), (fun (a : α) ↦ a ∈ ⟦b⟧ ∧ p a) y → y = z
_z_mem_l : z ∈ ⟦b⟧
_pz : p z
⊢ x = z

Tactic:
z_unique x px
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
inst : DecidablePred p
l : Multiset α
a b : List α
p_1 : a ≈ b
x : α
px : x ∈ b ∧ p x
y : α
py : y ∈ b ∧ p y
z : α
z_unique : ∀ (y : α), (fun (a : α) ↦ a ∈ ⟦b⟧ ∧ p a) y → y = z
_z_mem_l : z ∈ ⟦b⟧
_pz : p z
⊢ z = y

Tactic:
(z_unique y py).symm

Premises used: Eq.symm
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
inst : DecidablePred p
l : Multiset α
a b : List α
p_1 : a ≈ b
x : α
px : x ∈ b ∧ p x
y : α
py : y ∈ b ∧ p y
z : α
z_unique : ∀ (y : α), (fun (a : α) ↦ a ∈ ⟦b⟧ ∧ p a) y → y = z
_z_mem_l : z ∈ ⟦b⟧
_pz : p z
⊢ x = y

Tactic:
calc
        x = z := z_unique x px
        _ = y := (z_unique y py).symm

Premises used: Eq.symm
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
l : Multiset α
hp : ∃! a : α, a ∈ l ∧ p a
⊢ choose p l hp ∈ l ∧ p (choose p l hp)

Tactic:
(chooseX p l hp).property

Premises used: Multiset.chooseX, Multiset.choose, Subtype.property
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
l : Multiset α
hp : ∃! a : α, a ∈ l ∧ p a
⊢ choose p l hp ∈ l

Tactic:
(choose_spec _ _ _).1

Premises used: Multiset.choose_spec, And.left
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
l : Multiset α
hp : ∃! a : α, a ∈ l ∧ p a
⊢ p (choose p l hp)

Tactic:
(choose_spec _ _ _).2

Premises used: And.right, Multiset.choose_spec
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
inst : Subsingleton α
⊢ Eq (α := (a : List α) → Multiset α) (⇑(subsingletonEquiv α) : (a : List α) → Multiset α) ofList

Tactic:
rfl

Premises used: Multiset.ofList, rfl
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
l : List α
L : List (List α)
⊢ (↑(List.map ofList (l :: L)) : Multiset (Multiset α)).join = (↑(l :: L).flatten : Multiset α)

Tactic:
congr_arg (fun s : Multiset α => ↑l + s) (coe_join L)

Premises used: Multiset.sum, Multiset.add, Multiset.foldr, congr_arg, Multiset.ofList, HAdd.hAdd, Multiset.join, List.foldr, List.flatten
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
l : List α
L : List (List α)
⊢ (↑(List.map ofList (l :: L)) : Multiset (Multiset α)).join = (↑(l :: L).flatten : Multiset α)

Tactic:
exact congr_arg (fun s : Multiset α => ↑l + s) (coe_join L)

Premises used: congr_arg, HAdd.hAdd
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Multiset α) (join 0) 0

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Multiset.join, List.foldr, rfl
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
s : Multiset α
S : Multiset (Multiset α)
⊢ (s ::ₘ S).join = s + S.join

Tactic:
sum_cons _ _

Premises used: Multiset.join, Multiset.sum_cons
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
S T : Multiset (Multiset α)
⊢ (S + T).join = S.join + T.join

Tactic:
sum_add _ _

Premises used: Multiset.sum_add, Multiset.join
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
a : Multiset α
⊢ join {a} = a

Tactic:
sum_singleton _

Premises used: Multiset.sum_singleton, Multiset.join
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
a : α
S : Multiset (Multiset α)
⊢ Membership.mem (γ := Multiset α) (join 0) a ↔
    ∃ (s : Multiset α), Membership.mem (γ := Multiset (Multiset α)) 0 s ∧ a ∈ s

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
a : α
S : Multiset (Multiset α)
⊢ ∀ (a_1 : Multiset α) (s : Multiset (Multiset α)),
    (a ∈ s.join ↔ ∃ (s_1 : Multiset α), s_1 ∈ s ∧ a ∈ s_1) →
      (a ∈ (a_1 ::ₘ s).join ↔ ∃ (s_1 : Multiset α), s_1 ∈ a_1 ::ₘ s ∧ a ∈ s_1)

Tactic:
simp +contextual [or_and_right, exists_or]

Premises used: exists_or, or_and_right
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
S : Multiset (Multiset α)
⊢ card.{u_1} (α := α) (join 0) = (map.{0, u_1} (α := Multiset α) card 0).sum

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
S : Multiset (Multiset α)
⊢ ∀ (a : Multiset α) (s : Multiset (Multiset α)),
    s.join.card = (map card s).sum → (a ::ₘ s).join.card = (map card (a ::ₘ s)).sum

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
f : α → β
⊢ map f (join 0) = (map (map f) 0).join

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
f : α → β
a : Multiset α
s : Multiset (Multiset α)
ih : map f s.join = (map (map f) s).join
⊢ map f (a ::ₘ s).join = (map (map f) (a ::ₘ s)).join

Tactic:
simp [ih]
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
f : α → β
S : Multiset (Multiset α)
empty : map f (join 0) = (map (map f) 0).join
cons :
  ∀ (a : Multiset α) (s : Multiset (Multiset α)) (ih : map f s.join = (map (map f) s).join),
    map f (a ::ₘ s).join = (map (map f) (a ::ₘ s)).join
⊢ map f S.join = (map (map f) S).join

Tactic:
induction S using Multiset.induction with
  | empty => simp
  | cons _ _ ih => simp [ih]

Premises used: Multiset.cons
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
inst : CommMonoid α
⊢ Eq.{u_1 + 1} (α := α) (prod (join 0)) (prod (map prod 0))

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
inst : CommMonoid α
a : Multiset α
s : Multiset (Multiset α)
ih : s.join.prod = (map prod s).prod
⊢ (a ::ₘ s).join.prod = (map prod (a ::ₘ s)).prod

Tactic:
simp [ih]
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
inst : CommMonoid α
S : Multiset (Multiset α)
empty : Eq.{u_1 + 1} (α := α) (prod (join 0)) (prod (map prod 0))
cons :
  ∀ (a : Multiset α) (s : Multiset (Multiset α)) (ih : s.join.prod = (map prod s).prod),
    (a ::ₘ s).join.prod = (map prod (a ::ₘ s)).prod
⊢ S.join.prod = (map prod S).prod

Tactic:
induction S using Multiset.induction with
  | empty => simp
  | cons _ _ ih => simp [ih]

Premises used: Multiset.cons
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
⊢ Rel r (join 0) (join 0)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
a : Multiset α
b : Multiset β
as : Multiset (Multiset α)
bs : Multiset (Multiset β)
hab : Rel r a b
hst : Rel (Rel r) as bs
ih : Rel r as.join bs.join
⊢ Rel r (a ::ₘ as).join (b ::ₘ bs).join

Tactic:
simpa using hab.add ih

Premises used: Multiset.Rel.add
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
h : Rel (Rel r) s t
zero : Rel r (join 0) (join 0)
cons :
  ∀ {a : Multiset α} {b : Multiset β} {as : Multiset (Multiset α)} {bs : Multiset (Multiset β)} (hab : Rel r a b)
    (hst : Rel (Rel r) as bs) (ih : Rel r as.join bs.join), Rel r (a ::ₘ as).join (b ::ₘ bs).join
⊢ Rel r s.join t.join

Tactic:
induction h with
  | zero => simp
  | cons hab hst ih => simpa using hab.add ih

Premises used: Multiset.cons
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
⊢ filter p (join 0) = (map (filter p) 0).join

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
a : Multiset α
s : Multiset (Multiset α)
ih : filter p s.join = (map (filter p) s).join
⊢ filter p (a ::ₘ s).join = (map (filter p) (a ::ₘ s)).join

Tactic:
simp [ih]
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
S : Multiset (Multiset α)
p : α → Prop
inst : DecidablePred p
empty : filter p (join 0) = (map (filter p) 0).join
cons :
  ∀ (a : Multiset α) (s : Multiset (Multiset α)) (ih : filter p s.join = (map (filter p) s).join),
    filter p (a ::ₘ s).join = (map (filter p) (a ::ₘ s)).join
⊢ filter p S.join = (map (filter p) S).join

Tactic:
induction S using Multiset.induction with
  | empty => simp
  | cons _ _ ih => simp [ih]

Premises used: Multiset.cons
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
f : α → Option β
⊢ filterMap f (join 0) = (map (filterMap f) 0).join

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
f : α → Option β
a : Multiset α
s : Multiset (Multiset α)
ih : filterMap f s.join = (map (filterMap f) s).join
⊢ filterMap f (a ::ₘ s).join = (map (filterMap f) (a ::ₘ s)).join

Tactic:
simp [ih]
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
S : Multiset (Multiset α)
f : α → Option β
empty : filterMap f (join 0) = (map (filterMap f) 0).join
cons :
  ∀ (a : Multiset α) (s : Multiset (Multiset α)) (ih : filterMap f s.join = (map (filterMap f) s).join),
    filterMap f (a ::ₘ s).join = (map (filterMap f) (a ::ₘ s)).join
⊢ filterMap f S.join = (map (filterMap f) S).join

Tactic:
induction S using Multiset.induction with
  | empty => simp
  | cons _ _ ih => simp [ih]

Premises used: Multiset.cons
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
l : List α
f : α → List β
rw :
  ((↑l : Multiset α).bind fun (a : α) ↦ (↑(f a) : Multiset β)) =
    (↑(List.map (ofList ∘ f) l) : Multiset (Multiset β)).join
⊢ ((↑l : Multiset α).bind fun (a : α) ↦ (↑(f a) : Multiset β)) = (↑(List.flatMap f l) : Multiset β)

Tactic:
rw [List.flatMap, ← coe_join, List.map_map]

Premises used: List.map_map, List.flatMap, Multiset.coe_join
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
l : List α
f : α → List β
⊢ ((↑l : Multiset α).bind fun (a : α) ↦ (↑(f a) : Multiset β)) =
    (↑(List.map (ofList ∘ f) l) : Multiset (Multiset β)).join

Tactic:
rfl
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
f : α → Multiset β
⊢ bind 0 f = 0

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Multiset.join, List.foldr, Multiset.bind, rfl
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
a : α
s : Multiset α
f : α → Multiset β
⊢ (a ::ₘ s).bind f = f a + s.bind f

Tactic:
simp [bind]

Premises used: Multiset.bind
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
a : α
f : α → Multiset β
⊢ bind {a} f = f a

Tactic:
simp [bind]

Premises used: Multiset.bind
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
s t : Multiset α
f : α → Multiset β
⊢ (s + t).bind f = s.bind f + t.bind f

Tactic:
simp [bind]

Premises used: Multiset.bind
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
s : Multiset α
⊢ Eq.{v + 1} (α := Multiset β) (s.bind fun (x : α) ↦ 0) 0

Tactic:
simp [bind, join, nsmul_zero]

Premises used: nsmul_zero, Multiset.join, Multiset.bind
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
s : Multiset α
f g : α → Multiset β
⊢ (s.bind fun (a : α) ↦ f a + g a) = s.bind f + s.bind g

Tactic:
simp [bind, join]

Premises used: Multiset.join, Multiset.bind
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
g : α → Multiset β
⊢ (bind 0 fun (a : α) ↦ f a ::ₘ g a) = map f 0 + bind 0 g

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
g : α → Multiset β
⊢ ∀ (a : α) (s : Multiset α),
    (s.bind fun (a : α) ↦ f a ::ₘ g a) = map f s + s.bind g →
      ((a ::ₘ s).bind fun (a : α) ↦ f a ::ₘ g a) = map f (a ::ₘ s) + (a ::ₘ s).bind g

Tactic:
simp +contextual [add_comm, add_left_comm, add_assoc]

Premises used: add_left_comm, add_assoc, add_comm
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
rw : 0 = map f 0
rw₁ rw₂ : Eq.{v + 1} (α := Multiset β) 0 0
⊢ (bind 0 fun (x : α) ↦ {f x}) = map f 0

Tactic:
rw [zero_bind, map_zero]

Premises used: Multiset.map_zero, Multiset.zero_bind
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ ∀ (a : α) (s : Multiset α),
    (s.bind fun (x : α) ↦ {f x}) = map f s → ((a ::ₘ s).bind fun (x : α) ↦ {f x}) = map f (a ::ₘ s)

Tactic:
simp [singleton_add]

Premises used: Multiset.singleton_add
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
b : β
s : Multiset α
f : α → Multiset β
⊢ b ∈ s.bind f ↔ ∃ (a : α), a ∈ s ∧ b ∈ f a

Tactic:
simp [bind]

Premises used: Multiset.bind
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
⊢ (s.bind f).card = (map (card ∘ f) s).sum

Tactic:
simp [bind]

Premises used: Multiset.bind
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
f g : α → Multiset β
m : Multiset α
⊢ (∀ (a : α), a ∈ m → f a = g a) → m.bind f = m.bind g

Tactic:
simp +contextual [bind]

Premises used: Multiset.bind
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β β' : Type v
m : Multiset α
f : α → Multiset β
f' : α → Multiset β'
h : β = β'
hf : ∀ (a : α), a ∈ m → f a ≍ f' a
subst : ∀ {f' : α → Multiset β} (hf : ∀ (a : α), a ∈ m → f a ≍ f' a), m.bind f ≍ m.bind f'
⊢ m.bind f ≍ m.bind f'

Tactic:
subst h
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
m : Multiset α
f f' : α → Multiset β
hf : ∀ (a : α), a ∈ m → f a ≍ f' a
⊢ ∀ (a : α), a ∈ m → f a = f' a

Tactic:
simp only [heq_eq_eq] at hf

Premises used: heq_eq_eq
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
m : Multiset α
f f' : α → Multiset β
hf : ∀ (a : α), a ∈ m → f a = f' a
⊢ m.bind f ≍ m.bind f'

Tactic:
simp [bind_congr hf]

Premises used: Multiset.bind_congr
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
n : α → Multiset β
f : β → γ
⊢ map f (m.bind n) = m.bind fun (a : α) ↦ map f (n a)

Tactic:
simp [bind]

Premises used: Multiset.bind
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
n : β → Multiset γ
f : α → β
⊢ (map f 0).bind n = bind 0 fun (a : α) ↦ n (f a)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
n : β → Multiset γ
f : α → β
⊢ ∀ (a : α) (s : Multiset α),
    ((map f s).bind n = s.bind fun (a : α) ↦ n (f a)) → (map f (a ::ₘ s)).bind n = (a ::ₘ s).bind fun (a : α) ↦ n (f a)

Tactic:
simp +contextual
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
γ : Type u_2
s : Multiset α
f : α → Multiset β
g : β → Multiset γ
⊢ (bind 0 f).bind g = bind 0 fun (a : α) ↦ (f a).bind g

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
γ : Type u_2
s : Multiset α
f : α → Multiset β
g : β → Multiset γ
⊢ ∀ (a : α) (s : Multiset α),
    ((s.bind f).bind g = s.bind fun (a : α) ↦ (f a).bind g) →
      ((a ::ₘ s).bind f).bind g = (a ::ₘ s).bind fun (a : α) ↦ (f a).bind g

Tactic:
simp +contextual
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
n : Multiset β
f : α → β → Multiset γ
⊢ Eq.{u_2 + 1} (α := Multiset γ) (bind 0 fun (a : α) ↦ n.bind fun (b : β) ↦ f a b)
    (n.bind fun (b : β) ↦ bind 0 fun (a : α) ↦ f a b)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
n : Multiset β
f : α → β → Multiset γ
⊢ ∀ (a : α) (s : Multiset α),
    Eq.{u_2 + 1} (α := Multiset γ) (s.bind fun (a : α) ↦ n.bind fun (b : β) ↦ f a b)
        (n.bind fun (b : β) ↦ s.bind fun (a : α) ↦ f a b) →
      Eq.{u_2 + 1} (α := Multiset γ) ((a ::ₘ s).bind fun (a : α) ↦ n.bind fun (b : β) ↦ f a b)
        (n.bind fun (b : β) ↦ (a ::ₘ s).bind fun (a : α) ↦ f a b)

Tactic:
simp +contextual
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
n : Multiset β
f : α → β → γ
⊢ Eq.{u_2 + 1} (α := Multiset γ) (bind 0 fun (a : α) ↦ map (fun (b : β) ↦ f a b) n)
    (n.bind fun (b : β) ↦ map (fun (a : α) ↦ f a b) 0)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
n : Multiset β
f : α → β → γ
⊢ ∀ (a : α) (s : Multiset α),
    Eq.{u_2 + 1} (α := Multiset γ) (s.bind fun (a : α) ↦ map (fun (b : β) ↦ f a b) n)
        (n.bind fun (b : β) ↦ map (fun (a : α) ↦ f a b) s) →
      Eq.{u_2 + 1} (α := Multiset γ) ((a ::ₘ s).bind fun (a : α) ↦ map (fun (b : β) ↦ f a b) n)
        (n.bind fun (b : β) ↦ map (fun (a : α) ↦ f a b) (a ::ₘ s))

Tactic:
simp +contextual
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
⊢ filter p 0 = bind 0 fun (a : α) ↦ if p a then {a} else 0

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
a : α
m : Multiset α
ih : filter p m = m.bind fun (a : α) ↦ if p a then {a} else 0
⊢ filter p (a ::ₘ m) = (a ::ₘ m).bind fun (a : α) ↦ if p a then {a} else 0

Tactic:
simp [filter_cons, ih]

Premises used: Multiset.filter_cons
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
m : Multiset α
p : α → Prop
inst : DecidablePred p
empty : filter p 0 = bind 0 fun (a : α) ↦ if p a then {a} else 0
cons :
  ∀ (a : α) (m : Multiset α) (ih : filter p m = m.bind fun (a : α) ↦ if p a then {a} else 0),
    filter p (a ::ₘ m) = (a ::ₘ m).bind fun (a : α) ↦ if p a then {a} else 0
⊢ filter p m = m.bind fun (a : α) ↦ if p a then {a} else 0

Tactic:
induction m using Multiset.induction with
  | empty => simp
  | cons a m ih => simp [filter_cons, ih]

Premises used: Multiset.filter_cons, Multiset.cons
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst : DecidablePred p
simp :
  Eq.{v + 1} (α := Multiset β) (m.bind fun (a : α) ↦ bind (if p a then {a} else 0) f)
    (m.bind fun (a : α) ↦ if p a then f a else 0)
⊢ (filter p m).bind f = m.bind fun (a : α) ↦ if p a then f a else 0

Tactic:
simp only [filter_eq_bind, bind_assoc]

Premises used: Multiset.bind_assoc, Multiset.filter_eq_bind