awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Multiset.Antidiagonal (goal)
Goal:
α : Type u_1
s : Multiset α
this : s.powerset.card = HPow.hPow (α := ℕ) 2 s.card
rwa :
  ∀ (this : (map Prod.fst s.antidiagonal).card = HPow.hPow (α := ℕ) 2 s.card),
    s.antidiagonal.card = HPow.hPow (α := ℕ) 2 s.card
⊢ s.antidiagonal.card = HPow.hPow (α := ℕ) 2 s.card
have rwa₁ : ∀ (this : s.antidiagonal.card = HPow.hPow (α := ℕ) 2 s.card), s.antidiagonal.card = HPow.hPow (α := ℕ) 2 s.card
Tactic: rwa [← antidiagonal_map_fst, card_map] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Multiset.Basic (goal)
Goal:
α : Type u_1
s : Multiset α
⊢ s.toList = [] ↔ s = 0
have rw : (↑s.toList : Multiset α) = 0 ↔ s = 0
Tactic: rw [← coe_eq_zero, coe_toList]
-- Lean 4 proof step from Mathlib.Data.Multiset.Basic (goal)
Goal:
α : Type u_1
s : Multiset α
rw : (↑s.toList : Multiset α) = 0 ↔ s = 0
⊢ s.toList = [] ↔ s = 0
have rw₁ : s = 0 ↔ s = 0
Tactic: rw [← coe_eq_zero, coe_toList]
-- Lean 4 proof step from Mathlib.Data.Multiset.Basic (goal)
Goal:
α : Type u_1
a : α
s : Multiset α
⊢ a ∈ s.toList ↔ a ∈ s
have rw : a ∈ (↑s.toList : Multiset α) ↔ a ∈ s
Tactic: rw [← mem_coe, coe_toList]
-- Lean 4 proof step from Mathlib.Data.Multiset.Basic (goal)
Goal:
α : Type u_1
a : α
s : Multiset α
rw : a ∈ (↑s.toList : Multiset α) ↔ a ∈ s
⊢ a ∈ s.toList ↔ a ∈ s
have rw₁ : a ∈ s ↔ a ∈ s
Tactic: rw [← mem_coe, coe_toList]
-- Lean 4 proof step from Mathlib.Data.Multiset.Basic (goal)
Goal:
α : Type u_1
a : α
m : Multiset α
⊢ m.toList = [a] ↔ m = {a}
have rw : m.toList ~ [a] ↔ m = {a}
Tactic: rw [← perm_singleton, ← coe_eq_coe, coe_toList, coe_singleton]
-- Lean 4 proof step from Mathlib.Data.Multiset.Basic (goal)
Goal:
α : Type u_1
a : α
m : Multiset α
rw : m.toList ~ [a] ↔ m = {a}
⊢ m.toList = [a] ↔ m = {a}
have rw₁ : (↑m.toList : Multiset α) = (↑[a] : Multiset α) ↔ m = {a}
Tactic: rw [← perm_singleton, ← coe_eq_coe, coe_toList, coe_singleton]
-- Lean 4 proof step from Mathlib.Data.Multiset.Basic (goal)
Goal:
α : Type u_1
a : α
m : Multiset α
rw : m.toList ~ [a] ↔ m = {a}
rw₁ : (↑m.toList : Multiset α) = (↑[a] : Multiset α) ↔ m = {a}
⊢ m.toList = [a] ↔ m = {a}
have rw₂ : m = (↑[a] : Multiset α) ↔ m = {a}
Tactic: rw [← perm_singleton, ← coe_eq_coe, coe_toList, coe_singleton]
-- Lean 4 proof step from Mathlib.Data.Multiset.Basic (goal)
Goal:
α : Type u_1
a : α
m : Multiset α
rw : m.toList ~ [a] ↔ m = {a}
rw₁ : (↑m.toList : Multiset α) = (↑[a] : Multiset α) ↔ m = {a}
rw₂ : m = (↑[a] : Multiset α) ↔ m = {a}
⊢ m.toList = [a] ↔ m = {a}
have rw₃ : m = {a} ↔ m = {a}
Tactic: rw [← perm_singleton, ← coe_eq_coe, coe_toList, coe_singleton]
-- Lean 4 proof step from Mathlib.Data.Multiset.Basic (goal)
Goal:
α : Type u_1
s : Multiset α
⊢ s.toList.length = s.card
have rw : (↑s.toList : Multiset α).card = s.card
Tactic: rw [← coe_card, coe_toList]
-- Lean 4 proof step from Mathlib.Data.Multiset.Basic (goal)
Goal:
α : Type u_1
s : Multiset α
rw : (↑s.toList : Multiset α).card = s.card
⊢ s.toList.length = s.card
have rw₁ : s.card = s.card
Tactic: rw [← coe_card, coe_toList]
-- Lean 4 proof step from Mathlib.Data.Multiset.Basic (goal)
Goal:
α : Type u_1
p : Multiset α → Sort u_3
s : Multiset α
H : (s : Multiset α) → ((t : Multiset α) → t < s → p t) → p s
⊢ s.strongInductionOn (p := p) H = H s fun (t : Multiset α) (_h : t < s) ↦ t.strongInductionOn (p := p) H
have rw : (H s fun (t : Multiset α) (_h : t < s) ↦ t.strongInductionOn (p := p) H) =
  H s fun (t : Multiset α) (_h : t < s) ↦ t.strongInductionOn (p := p) H
Tactic: rw [strongInductionOn]
-- Lean 4 proof step from Mathlib.Data.Multiset.Basic (hypothesis)
Goal:
α : Type u_1
n : ℕ
s t : Multiset α
ht : t.card ≤ n
_h : s < t
⊢ n - t.card < n - s.card
have this : s.card < t.card
Tactic: have := (card_lt_card _h)
-- Lean 4 proof step from Mathlib.Data.Multiset.Basic (goal)
Goal:
α : Type u_1
n : ℕ
s t : Multiset α
ht : t.card ≤ n
_h : s < t
⊢ n - t.card < n - s.card
have decreasing_by : ∀ (this : s.card < t.card), n - t.card < n - s.card
Tactic: decreasing_by have := (card_lt_card _h); lia
-- Lean 4 proof step from Mathlib.Data.Multiset.Basic (goal)
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 α
⊢ strongDownwardInduction (p := p) H s =
    H s fun {t₂ : Multiset α} (ht : t₂.card ≤ n) (_hst : s < t₂) ↦ strongDownwardInduction (p := p) H t₂ ht
have 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
Tactic: rw [strongDownwardInduction]
-- Lean 4 proof step from Mathlib.Data.Multiset.Basic (goal)
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₁
⊢ (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
have 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
Tactic: dsimp only [strongDownwardInductionOn]
-- Lean 4 proof step from Mathlib.Data.Multiset.Basic (goal)
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₁
⊢ (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
have 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
Tactic: rw [strongDownwardInduction]
-- Lean 4 proof step from Mathlib.Data.Multiset.Basic (goal)
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 ⋯
have 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 sorry) sorry hp =
    List.chooseX p b sorry
Tactic: funext hp
-- Lean 4 proof step from Mathlib.Data.Multiset.Basic (goal)
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
⊢ 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 ⋯
have h : ∀ (x y : { t : α // t ∈ b ∧ p t }), x = y
Tactic: suffices all_equal : ∀ x y : { t // t ∈ b ∧ p t }, x = y by
        apply all_equal
-- Lean 4 proof step from Mathlib.Data.Multiset.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rcases hp with ⟨z, ⟨_z_mem_l, _pz⟩, z_unique⟩
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Data.Multiset.Basic (goal)
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
⊢ 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)
have h : x = y
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
S : Multiset (Multiset α)
⊢ map f S.join = (map (map f) S).join
have empty : map f (join 0) = (map (map f) 0).join
Tactic: induction S using Multiset.induction with
  | empty => simp
  | cons _ _ ih => simp [ih]
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
S : Multiset (Multiset α)
empty : map f (join 0) = (map (map f) 0).join
⊢ map f S.join = (map (map f) S).join
have 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
Tactic: induction S using Multiset.induction with
  | empty => simp
  | cons _ _ ih => simp [ih]
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
inst : CommMonoid α
S : Multiset (Multiset α)
⊢ S.join.prod = (map prod S).prod
have empty : Eq.{u_1 + 1} (α := α) (prod (join 0)) (prod (map prod 0))
Tactic: induction S using Multiset.induction with
  | empty => simp
  | cons _ _ ih => simp [ih]
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
inst : CommMonoid α
S : Multiset (Multiset α)
empty : Eq.{u_1 + 1} (α := α) (prod (join 0)) (prod (map prod 0))
⊢ S.join.prod = (map prod S).prod
have cons : ∀ (a : Multiset α) (s : Multiset (Multiset α)) (ih : s.join.prod = (map prod s).prod),
  (a ::ₘ s).join.prod = (map prod (a ::ₘ s)).prod
Tactic: induction S using Multiset.induction with
  | empty => simp
  | cons _ _ ih => simp [ih]
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
h : Rel (Rel r) s t
⊢ Rel r s.join t.join
have zero : Rel r (join 0) (join 0)
Tactic: induction h with
  | zero => simp
  | cons hab hst ih => simpa using hab.add ih
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
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)
⊢ Rel r s.join t.join
have 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
Tactic: induction h with
  | zero => simp
  | cons hab hst ih => simpa using hab.add ih
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
S : Multiset (Multiset α)
p : α → Prop
inst : DecidablePred p
⊢ filter p S.join = (map (filter p) S).join
have empty : filter p (join 0) = (map (filter p) 0).join
Tactic: induction S using Multiset.induction with
  | empty => simp
  | cons _ _ ih => simp [ih]
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
S : Multiset (Multiset α)
p : α → Prop
inst : DecidablePred p
empty : filter p (join 0) = (map (filter p) 0).join
⊢ filter p S.join = (map (filter p) S).join
have 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
Tactic: induction S using Multiset.induction with
  | empty => simp
  | cons _ _ ih => simp [ih]
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
S : Multiset (Multiset α)
f : α → Option β
⊢ filterMap f S.join = (map (filterMap f) S).join
have empty : filterMap f (join 0) = (map (filterMap f) 0).join
Tactic: induction S using Multiset.induction with
  | empty => simp
  | cons _ _ ih => simp [ih]
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
S : Multiset (Multiset α)
f : α → Option β
empty : filterMap f (join 0) = (map (filterMap f) 0).join
⊢ filterMap f S.join = (map (filterMap f) S).join
have 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
Tactic: induction S using Multiset.induction with
  | empty => simp
  | cons _ _ ih => simp [ih]
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
l : List α
f : α → List β
⊢ ((↑l : Multiset α).bind fun (a : α) ↦ (↑(f a) : Multiset β)) = (↑(List.flatMap f l) : Multiset β)
have rw : ((↑l : Multiset α).bind fun (a : α) ↦ (↑(f a) : Multiset β)) = (↑(List.map (ofList ∘ f) l) : Multiset (Multiset β)).join
Tactic: rw [List.flatMap, ← coe_join, List.map_map]
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ (bind 0 fun (x : α) ↦ {f x}) = map f 0
have rw : 0 = map f 0
Tactic: rw [zero_bind, map_zero]
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
rw : 0 = map f 0
⊢ (bind 0 fun (x : α) ↦ {f x}) = map f 0
have rw₁ : Eq.{v + 1} (α := Multiset β) 0 0
Tactic: rw [zero_bind, map_zero]
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β β' : Type v
m : Multiset α
f : α → Multiset β
f' : α → Multiset β'
h : β = β'
hf : ∀ (a : α), a ∈ m → f a ≍ f' a
⊢ m.bind f ≍ m.bind f'
have subst : ∀ {f' : α → Multiset β} (hf : ∀ (a : α), a ∈ m → f a ≍ f' a), m.bind f ≍ m.bind f'
Tactic: subst h
Cleared hypotheses: β', f', h, hf
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (hypothesis)
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'
have hf₁ : ∀ (a : α), a ∈ m → f a = f' a
Tactic: simp only [heq_eq_eq] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
m : Multiset α
p : α → Prop
inst : DecidablePred p
⊢ filter p m = m.bind fun (a : α) ↦ if p a then {a} else 0
have empty : filter p 0 = bind 0 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]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
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
⊢ filter p m = m.bind fun (a : α) ↦ if p a then {a} else 0
have 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
Tactic: induction m using Multiset.induction with
  | empty => simp
  | cons a m ih => simp [filter_cons, ih]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst : DecidablePred p
⊢ (filter p m).bind f = m.bind fun (a : α) ↦ if p a then f a else 0
have 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)
Tactic: simp only [filter_eq_bind, bind_assoc]
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst : DecidablePred p
⊢ 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)
have a : ∀ (a : α), a ∈ m → bind (if p a then {a} else 0) f = if p a then f a else 0
Tactic: apply Multiset.bind_congr
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst : DecidablePred p
a : α
ham : a ∈ m
⊢ bind (if p a then {a} else 0) f = if p a then f a else 0
have pos : p a → bind {a} f = f a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst : DecidablePred p
a : α
ham : a ∈ m
pos : p a → bind {a} f = f a
⊢ bind (if p a then {a} else 0) f = if p a then f a else 0
have neg : ¬p a → bind 0 f = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
m : Multiset α
f : α → Option β
⊢ filterMap f m = m.bind fun (a : α) ↦ Option.getD (Option.map singleton (f a)) 0
have empty : filterMap f 0 = bind 0 fun (a : α) ↦ Option.getD (Option.map singleton (f a)) 0
Tactic: induction m using Multiset.induction with
  | empty => simp
  | cons a m ih => simp [filterMap_cons, ih]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
m : Multiset α
f : α → Option β
empty : filterMap f 0 = bind 0 fun (a : α) ↦ Option.getD (Option.map singleton (f a)) 0
⊢ filterMap f m = m.bind fun (a : α) ↦ Option.getD (Option.map singleton (f a)) 0
have cons : ∀ (a : α) (m : Multiset α) (ih : filterMap f m = m.bind fun (a : α) ↦ Option.getD (Option.map singleton (f a)) 0),
  filterMap f (a ::ₘ m) = (a ::ₘ m).bind fun (a : α) ↦ Option.getD (Option.map singleton (f a)) 0
Tactic: induction m using Multiset.induction with
  | empty => simp
  | cons a m ih => simp [filterMap_cons, ih]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
f : α → Option β
g : β → Multiset γ
⊢ (filterMap f m).bind g = m.bind fun (a : α) ↦ (Option.map g (f a)).getD 0
have simp : Eq.{u_2 + 1} (α := Multiset γ) (m.bind fun (a : α) ↦ bind (Option.getD (Option.map singleton (f a)) 0) g)
  (m.bind fun (a : α) ↦ (Option.map g (f a)).getD 0)
Tactic: simp only [filterMap_eq_bind, Multiset.bind_assoc]
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
f : α → Option β
g : β → Multiset γ
⊢ Eq.{u_2 + 1} (α := Multiset γ) (m.bind fun (a : α) ↦ bind (Option.getD (Option.map singleton (f a)) 0) g)
    (m.bind fun (a : α) ↦ (Option.map g (f a)).getD 0)
have a : ∀ (a : α), a ∈ m → bind (Option.getD (Option.map singleton (f a)) 0) g = (Option.map g (f a)).getD 0
Tactic: apply Multiset.bind_congr
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
f : α → Option β
g : β → Multiset γ
a : α
ham : a ∈ m
⊢ bind (Option.getD (Option.map singleton (f a)) 0) g = (Option.map g (f a)).getD 0
have a₁ : ∀ (x : Option β), bind (Option.getD (Option.map singleton x) 0) g = (Option.map g x).getD 0
Tactic: cases f a with
  | none => simp
  | some b => simp
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
γ : Type u_2
δ : Type u_3
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel p (s.bind f) (t.bind g)
have h₁ : Rel (Rel p) (map f s) (map g t)
Tactic: apply rel_join
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
γ : Type u_2
δ : Type u_3
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel (Rel p) (map f s) (map g t)
have h₁ : Rel (fun (a : α) (b : β) ↦ Rel p (f a) (g b)) s t
Tactic: rw [rel_map]
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
⊢ f x ≤ S.bind f
have refine : ∀ (a : β), count a (f x) ≤ count a (S.bind f)
Tactic: refine le_iff_count.2 fun a ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
⊢ count a (f x) ≤ count a (S.bind f)
have obtain : ∀ (m' : Multiset ℕ) (hm' : map (fun (b : α) ↦ count a (f b)) S = (fun (b : α) ↦ count a (f b)) x ::ₘ m'),
  count a (f x) ≤ count a (S.bind f)
Tactic: obtain ⟨m', hm'⟩ := exists_cons_of_mem <| mem_map_of_mem (fun b ↦ count a (f b)) hx
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
m' : Multiset ℕ
hm' : map (fun (b : α) ↦ count a (f b)) S = (fun (b : α) ↦ count a (f b)) x ::ₘ m'
⊢ count a (f x) ≤ count a (S.bind f)
have rw : count a (f x) ≤ (fun (b : α) ↦ count a (f b)) x + m'.sum
Tactic: rw [count_bind, hm', sum_cons]
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
⊢ f x ≤ S.bind f
have refine : ∀ (a : β), count a (f x) ≤ count a (S.bind f)
Tactic: classical
  refine le_iff_count.2 fun a ↦ ?_
  obtain ⟨m', hm'⟩ := exists_cons_of_mem <| mem_map_of_mem (fun b ↦ count a (f b)) hx
  rw [count_bind, hm', sum_cons]
  exact Nat.le_add_right _ _
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
refine : ∀ (a : β), count a (f x) ≤ count a (S.bind f)
⊢ f x ≤ S.bind f
have refine₁ : ∀ (a : β) (m' : Multiset ℕ) (hm' : map (fun (b : α) ↦ count a (f b)) S = (fun (b : α) ↦ count a (f b)) x ::ₘ m'),
  count a (f x) ≤ count a (S.bind f)
Tactic: classical
  refine le_iff_count.2 fun a ↦ ?_
  obtain ⟨m', hm'⟩ := exists_cons_of_mem <| mem_map_of_mem (fun b ↦ count a (f b)) hx
  rw [count_bind, hm', sum_cons]
  exact Nat.le_add_right _ _
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
refine : ∀ (a : β), count a (f x) ≤ count a (S.bind f)
refine₁ :
  ∀ (a : β) (m' : Multiset ℕ) (hm' : map (fun (b : α) ↦ count a (f b)) S = (fun (b : α) ↦ count a (f b)) x ::ₘ m'),
    count a (f x) ≤ count a (S.bind f)
⊢ f x ≤ S.bind f
have refine₂ : ∀ (a : β) (m' : Multiset ℕ) (hm' : map (fun (b : α) ↦ count a (f b)) S = (fun (b : α) ↦ count a (f b)) x ::ₘ m'),
  count a (f x) ≤ (fun (b : α) ↦ count a (f b)) x + m'.sum
Tactic: classical
  refine le_iff_count.2 fun a ↦ ?_
  obtain ⟨m', hm'⟩ := exists_cons_of_mem <| mem_map_of_mem (fun b ↦ count a (f b)) hx
  rw [count_bind, hm', sum_cons]
  exact Nat.le_add_right _ _
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (hypothesis)
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
⊢ (s.bind f).Nodup ↔ (∀ (a : α), a ∈ s → (f a).Nodup) ∧ Pairwise (Disjoint on f) s
have this : ∀ (a : α), ∃ (l : List β), f a = (↑l : Multiset β)
Tactic: have : ∀ a, ∃ l : List β, f a = l := fun a => Quot.induction_on (f a) fun l => ⟨l, rfl⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
this : ∀ (a : α), ∃ (l : List β), f a = (↑l : Multiset β)
⊢ (s.bind f).Nodup ↔ (∀ (a : α), a ∈ s → (f a).Nodup) ∧ Pairwise (Disjoint on f) s
have choose : ∀ (f' : (a : α) → List β) (h' : ∀ (a : α), f a = (↑(f' a) : Multiset β)),
  (s.bind f).Nodup ↔ (∀ (a : α), a ∈ s → (f a).Nodup) ∧ Pairwise (Disjoint on f) s
Tactic: choose f' h' using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (hypothesis)
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
f' : (a : α) → List β
h' : ∀ (a : α), f a = (↑(f' a) : Multiset β)
⊢ (s.bind f).Nodup ↔ (∀ (a : α), a ∈ s → (f a).Nodup) ∧ Pairwise (Disjoint on f) s
have this : f = fun (a : α) ↦ (↑(f' a) : Multiset β)
Tactic: have : f = fun a ↦ ofList (f' a) := funext h'