awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 β)
this : f = fun (a : α) ↦ (↑(f' a) : Multiset β)
⊢ (s.bind f).Nodup ↔ (∀ (a : α), a ∈ s → (f a).Nodup) ∧ Pairwise (Disjoint on f) s
have hd : Symmetric fun (a b : α) ↦ (f' a).Disjoint (f' b)
Tactic: have hd : Symmetric fun a b ↦ List.Disjoint (f' a) (f' b) := fun a b h ↦ h.symm
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
s : Multiset α
f : α → Multiset β
⊢ (s.dedup.bind f).dedup = (s.bind f).dedup
have a : ∀ (x : β), count x (s.dedup.bind f).dedup = count x (s.bind f).dedup
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
s : Multiset α
f : α → Multiset β
x : β
⊢ count x (s.dedup.bind f).dedup = count x (s.bind f).dedup
have a : Eq (α := ℕ) (if x ∈ s.dedup.bind f then 1 else 0) (if x ∈ s.bind f then 1 else 0)
Tactic: simp_rw [count_dedup]
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
s : Multiset α
f : α → Multiset β
x : β
⊢ Eq (α := ℕ) (if x ∈ s.dedup.bind f then 1 else 0) (if x ∈ s.bind f then 1 else 0)
have a : (x ∈ s.dedup.bind f) = (x ∈ s.bind f)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
⊢ fold op (fold op b₀ (map b 0)) (bind 0 t) = fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) 0)
have empty : fold op (fold op b₀ (map b 0)) 0 = fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) 0)
Tactic: rw [zero_bind, map_zero, map_zero, fold_zero]
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
empty : fold op (fold op b₀ (map b 0)) 0 = fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) 0)
⊢ fold op (fold op b₀ (map b 0)) (bind 0 t) = fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) 0)
have empty₁ : fold op (fold op b₀ 0) 0 = fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) 0)
Tactic: rw [zero_bind, map_zero, map_zero, fold_zero]
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
empty : fold op (fold op b₀ (map b 0)) 0 = fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) 0)
empty₁ : fold op (fold op b₀ 0) 0 = fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) 0)
⊢ fold op (fold op b₀ (map b 0)) (bind 0 t) = fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) 0)
have empty₂ : fold op (fold op b₀ 0) 0 = fold op b₀ 0
Tactic: rw [zero_bind, map_zero, map_zero, fold_zero]
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
empty : fold op (fold op b₀ (map b 0)) 0 = fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) 0)
empty₁ : fold op (fold op b₀ 0) 0 = fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) 0)
empty₂ : fold op (fold op b₀ 0) 0 = fold op b₀ 0
⊢ fold op (fold op b₀ (map b 0)) (bind 0 t) = fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) 0)
have empty₃ : fold op b₀ 0 = fold op b₀ 0
Tactic: rw [zero_bind, map_zero, map_zero, fold_zero]
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha_1 : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
a : ι
ha : Multiset ι
ih : fold op (fold op b₀ (map b ha)) (ha.bind t) = fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) ha)
⊢ fold op (fold op b₀ (map b (a ::ₘ ha))) ((a ::ₘ ha).bind t) =
    fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) (a ::ₘ ha))
have cons : fold op (fold op b₀ (map b (a ::ₘ ha))) (t a + ha.bind t) =
  fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) (a ::ₘ ha))
Tactic: rw [cons_bind, map_cons, map_cons, fold_cons_left, fold_cons_left, fold_add, ih]
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha_1 : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
a : ι
ha : Multiset ι
ih : fold op (fold op b₀ (map b ha)) (ha.bind t) = fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) ha)
cons :
  fold op (fold op b₀ (map b (a ::ₘ ha))) (t a + ha.bind t) =
    fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) (a ::ₘ ha))
⊢ fold op (fold op b₀ (map b (a ::ₘ ha))) ((a ::ₘ ha).bind t) =
    fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) (a ::ₘ ha))
have cons₁ : fold op (fold op b₀ (b a ::ₘ map b ha)) (t a + ha.bind t) =
  fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) (a ::ₘ ha))
Tactic: rw [cons_bind, map_cons, map_cons, fold_cons_left, fold_cons_left, fold_add, ih]
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha_1 : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
a : ι
ha : Multiset ι
ih : fold op (fold op b₀ (map b ha)) (ha.bind t) = fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) ha)
cons :
  fold op (fold op b₀ (map b (a ::ₘ ha))) (t a + ha.bind t) =
    fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) (a ::ₘ ha))
cons₁ :
  fold op (fold op b₀ (b a ::ₘ map b ha)) (t a + ha.bind t) =
    fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) (a ::ₘ ha))
⊢ fold op (fold op b₀ (map b (a ::ₘ ha))) ((a ::ₘ ha).bind t) =
    fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) (a ::ₘ ha))
have cons₂ : fold op (fold op b₀ (b a ::ₘ map b ha)) (t a + ha.bind t) =
  fold op b₀ (fold op (b a) (t a) ::ₘ map (fun (i : ι) ↦ fold op (b i) (t i)) ha)
Tactic: rw [cons_bind, map_cons, map_cons, fold_cons_left, fold_cons_left, fold_add, ih]
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha_1 : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
a : ι
ha : Multiset ι
ih : fold op (fold op b₀ (map b ha)) (ha.bind t) = fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) ha)
cons :
  fold op (fold op b₀ (map b (a ::ₘ ha))) (t a + ha.bind t) =
    fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) (a ::ₘ ha))
cons₁ :
  fold op (fold op b₀ (b a ::ₘ map b ha)) (t a + ha.bind t) =
    fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) (a ::ₘ ha))
cons₂ :
  fold op (fold op b₀ (b a ::ₘ map b ha)) (t a + ha.bind t) =
    fold op b₀ (fold op (b a) (t a) ::ₘ map (fun (i : ι) ↦ fold op (b i) (t i)) ha)
⊢ fold op (fold op b₀ (map b (a ::ₘ ha))) ((a ::ₘ ha).bind t) =
    fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) (a ::ₘ ha))
have cons₃ : fold op (op (b a) (fold op b₀ (map b ha))) (t a + ha.bind t) =
  fold op b₀ (fold op (b a) (t a) ::ₘ map (fun (i : ι) ↦ fold op (b i) (t i)) ha)
Tactic: rw [cons_bind, map_cons, map_cons, fold_cons_left, fold_cons_left, fold_add, ih]
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha_1 : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
a : ι
ha : Multiset ι
ih : fold op (fold op b₀ (map b ha)) (ha.bind t) = fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) ha)
cons :
  fold op (fold op b₀ (map b (a ::ₘ ha))) (t a + ha.bind t) =
    fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) (a ::ₘ ha))
cons₁ :
  fold op (fold op b₀ (b a ::ₘ map b ha)) (t a + ha.bind t) =
    fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) (a ::ₘ ha))
cons₂ :
  fold op (fold op b₀ (b a ::ₘ map b ha)) (t a + ha.bind t) =
    fold op b₀ (fold op (b a) (t a) ::ₘ map (fun (i : ι) ↦ fold op (b i) (t i)) ha)
cons₃ :
  fold op (op (b a) (fold op b₀ (map b ha))) (t a + ha.bind t) =
    fold op b₀ (fold op (b a) (t a) ::ₘ map (fun (i : ι) ↦ fold op (b i) (t i)) ha)
⊢ fold op (fold op b₀ (map b (a ::ₘ ha))) ((a ::ₘ ha).bind t) =
    fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) (a ::ₘ ha))
have cons₄ : fold op (op (b a) (fold op b₀ (map b ha))) (t a + ha.bind t) =
  op (fold op (b a) (t a)) (fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) ha))
Tactic: rw [cons_bind, map_cons, map_cons, fold_cons_left, fold_cons_left, fold_add, ih]
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha_1 : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
a : ι
ha : Multiset ι
ih : fold op (fold op b₀ (map b ha)) (ha.bind t) = fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) ha)
cons :
  fold op (fold op b₀ (map b (a ::ₘ ha))) (t a + ha.bind t) =
    fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) (a ::ₘ ha))
cons₁ :
  fold op (fold op b₀ (b a ::ₘ map b ha)) (t a + ha.bind t) =
    fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) (a ::ₘ ha))
cons₂ :
  fold op (fold op b₀ (b a ::ₘ map b ha)) (t a + ha.bind t) =
    fold op b₀ (fold op (b a) (t a) ::ₘ map (fun (i : ι) ↦ fold op (b i) (t i)) ha)
cons₃ :
  fold op (op (b a) (fold op b₀ (map b ha))) (t a + ha.bind t) =
    fold op b₀ (fold op (b a) (t a) ::ₘ map (fun (i : ι) ↦ fold op (b i) (t i)) ha)
cons₄ :
  fold op (op (b a) (fold op b₀ (map b ha))) (t a + ha.bind t) =
    op (fold op (b a) (t a)) (fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) ha))
⊢ fold op (fold op b₀ (map b (a ::ₘ ha))) ((a ::ₘ ha).bind t) =
    fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) (a ::ₘ ha))
have cons₅ : op (fold op (b a) (t a)) (fold op (fold op b₀ (map b ha)) (ha.bind t)) =
  op (fold op (b a) (t a)) (fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) ha))
Tactic: rw [cons_bind, map_cons, map_cons, fold_cons_left, fold_cons_left, fold_add, ih]
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha_1 : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
a : ι
ha : Multiset ι
ih : fold op (fold op b₀ (map b ha)) (ha.bind t) = fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) ha)
cons :
  fold op (fold op b₀ (map b (a ::ₘ ha))) (t a + ha.bind t) =
    fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) (a ::ₘ ha))
cons₁ :
  fold op (fold op b₀ (b a ::ₘ map b ha)) (t a + ha.bind t) =
    fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) (a ::ₘ ha))
cons₂ :
  fold op (fold op b₀ (b a ::ₘ map b ha)) (t a + ha.bind t) =
    fold op b₀ (fold op (b a) (t a) ::ₘ map (fun (i : ι) ↦ fold op (b i) (t i)) ha)
cons₃ :
  fold op (op (b a) (fold op b₀ (map b ha))) (t a + ha.bind t) =
    fold op b₀ (fold op (b a) (t a) ::ₘ map (fun (i : ι) ↦ fold op (b i) (t i)) ha)
cons₄ :
  fold op (op (b a) (fold op b₀ (map b ha))) (t a + ha.bind t) =
    op (fold op (b a) (t a)) (fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) ha))
cons₅ :
  op (fold op (b a) (t a)) (fold op (fold op b₀ (map b ha)) (ha.bind t)) =
    op (fold op (b a) (t a)) (fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) ha))
⊢ fold op (fold op b₀ (map b (a ::ₘ ha))) ((a ::ₘ ha).bind t) =
    fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) (a ::ₘ ha))
have cons₆ : op (fold op (b a) (t a)) (fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) ha)) =
  op (fold op (b a) (t a)) (fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) ha))
Tactic: rw [cons_bind, map_cons, map_cons, fold_cons_left, fold_cons_left, fold_add, ih]
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
ι : Type u_4
s : Multiset ι
t : ι → Multiset α
b : ι → α
b₀ : α
⊢ fold op (fold op b₀ (map b s)) (s.bind t) = fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) s)
have empty : fold op (fold op b₀ (map b 0)) (bind 0 t) = fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) 0)
Tactic: induction s using Multiset.induction_on with
  | empty => rw [zero_bind, map_zero, map_zero, fold_zero]
  | cons a ha ih => rw [cons_bind, map_cons, map_cons, fold_cons_left, fold_cons_left, fold_add, ih]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
ι : Type u_4
s : Multiset ι
t : ι → Multiset α
b : ι → α
b₀ : α
empty : fold op (fold op b₀ (map b 0)) (bind 0 t) = fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) 0)
⊢ fold op (fold op b₀ (map b s)) (s.bind t) = fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) s)
have cons : ∀ (a : ι) (ha_1 : Multiset ι)
  (ih : fold op (fold op b₀ (map b ha_1)) (ha_1.bind t) = fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) ha_1)),
  fold op (fold op b₀ (map b (a ::ₘ ha_1))) ((a ::ₘ ha_1).bind t) =
    fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) (a ::ₘ ha_1))
Tactic: induction s using Multiset.induction_on with
  | empty => rw [zero_bind, map_zero, map_zero, fold_zero]
  | cons a ha ih => rw [cons_bind, map_cons, map_cons, fold_cons_left, fold_cons_left, fold_add, ih]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
l₁ : List α
l₂ : List β
⊢ (↑l₁ : Multiset α).product (↑l₂ : Multiset β) = (↑(l₁.product l₂) : Multiset (α × β))
have rw : Eq (α := Multiset (α × β)) ((↑l₁ : Multiset α).bind fun (a : α) ↦ map (Prod.mk a) (↑l₂ : Multiset β))
  ((↑l₁ : Multiset α).bind fun (a : α) ↦ (↑(List.map (Prod.mk a) l₂) : Multiset (α × β)))
Tactic: rw [product, List.product, ← coe_bind]
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
s_1 : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : Multiset β), s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
t u : Multiset β
⊢ (a ::ₘ s) ×ˢ (t + u) = (a ::ₘ s) ×ˢ t + (a ::ₘ s) ×ˢ u
have rw : map (Prod.mk a) (t + u) + (s ×ˢ t + s ×ˢ u) = (a ::ₘ s) ×ˢ t + (a ::ₘ s) ×ˢ u
Tactic: rw [cons_product, IH]
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
s : Multiset α
t : Multiset β
⊢ map Prod.swap (s ×ˢ t) = t ×ˢ s
have empty : map Prod.swap (SProd.sprod (α := Multiset α) 0 t) = SProd.sprod (β := Multiset α) t 0
Tactic: induction s using Multiset.induction
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
s : Multiset α
t : Multiset β
empty : map Prod.swap (SProd.sprod (α := Multiset α) 0 t) = SProd.sprod (β := Multiset α) t 0
⊢ map Prod.swap (s ×ˢ t) = t ×ˢ s
have cons : ∀ (a : α) (s : Multiset α), map Prod.swap (s ×ˢ t) = t ×ˢ s → map Prod.swap ((a ::ₘ s) ×ˢ t) = t ×ˢ (a ::ₘ s)
Tactic: induction s using Multiset.induction
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
M : Type u_4
inst : CommMonoid M
s : Multiset α
t : Multiset β
f : α × β → M
⊢ (map f (s ×ˢ t)).prod = prod (map (fun (i : α) ↦ prod (map (fun (j : β) ↦ f (i, j)) t)) s)
have empty : (map f (SProd.sprod (α := Multiset α) 0 t)).prod = prod (map (fun (i : α) ↦ prod (map (fun (j : β) ↦ f (i, j)) t)) 0)
Tactic: induction s using Multiset.induction
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
β : Type v
M : Type u_4
inst : CommMonoid M
s : Multiset α
t : Multiset β
f : α × β → M
empty :
  (map f (SProd.sprod (α := Multiset α) 0 t)).prod = prod (map (fun (i : α) ↦ prod (map (fun (j : β) ↦ f (i, j)) t)) 0)
⊢ (map f (s ×ˢ t)).prod = prod (map (fun (i : α) ↦ prod (map (fun (j : β) ↦ f (i, j)) t)) s)
have cons : ∀ (a : α) (s : Multiset α),
  (map f (s ×ˢ t)).prod = prod (map (fun (i : α) ↦ prod (map (fun (j : β) ↦ f (i, j)) t)) s) →
    (map f ((a ::ₘ s) ×ˢ t)).prod = prod (map (fun (i : α) ↦ prod (map (fun (j : β) ↦ f (i, j)) t)) (a ::ₘ s))
Tactic: induction s using Multiset.induction
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
σ : α → Type u_4
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ ((↑l₁ : Multiset α).sigma (σ := σ) fun (a : α) ↦ (↑(l₂ a) : Multiset (σ a))) =
    (↑(l₁.sigma (σ := σ) l₂) : Multiset ((a : α) × σ a))
have rw : Eq (α := Multiset ((a : α) × σ a))
  ((↑l₁ : Multiset α).bind fun (a : α) ↦ map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (↑(l₂ a) : Multiset (σ a)))
  ((↑l₁ : Multiset α).bind fun (a : α) ↦
    (↑(List.map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (l₂ a)) : Multiset ((a : α) × σ a)))
Tactic: rw [Multiset.sigma, List.sigma, ← coe_bind]
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
σ : α → Type u_4
s_1 : Multiset α
a : α
s : Multiset α
IH :
  ∀ (t u : (a : α) → Multiset (σ a)),
    (s.sigma (σ := σ) fun (a : α) ↦ t a + u a) = s.sigma (σ := σ) t + s.sigma (σ := σ) u
t u : (a : α) → Multiset (σ a)
⊢ ((a ::ₘ s).sigma (σ := σ) fun (a : α) ↦ t a + u a) = (a ::ₘ s).sigma (σ := σ) t + (a ::ₘ s).sigma (σ := σ) u
have rw : map (Sigma.mk (β := σ) a) (t a + u a) + (s.sigma (σ := σ) t + s.sigma (σ := σ) u) =
  (a ::ₘ s).sigma (σ := σ) t + (a ::ₘ s).sigma (σ := σ) u
Tactic: rw [cons_sigma, IH]
-- Lean 4 proof step from Mathlib.Data.Multiset.Bind (goal)
Goal:
α : Type u_1
s : Multiset α
σ : α → Type u_5
t : (a : α) → Multiset (σ a)
l₁ : List α
⊢ Nodup (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l₁) →
    (∀ (a : α), (t a).Nodup) →
      (Multiset.sigma (σ := σ) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l₁) t).Nodup
have choose : ∀ (f : (a : α) → List (σ a)) (hf : ∀ (a : α), ⟦f a⟧ = t a),
  Nodup (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l₁) →
    (∀ (a : α), (t a).Nodup) →
      (Multiset.sigma (σ := σ) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l₁) t).Nodup
Tactic: choose f hf using fun a => Quotient.exists_rep (t a)
-- Lean 4 proof step from Mathlib.Data.Multiset.Count (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
l : List α
⊢ countP (fun (a : { a : α // a ∈ ⟦l⟧ }) ↦ p (↑a : α)) (attach ⟦l⟧) = countP p ⟦l⟧
have simp : countP (fun (a : { a : α // a ∈ (↑l : Multiset α) }) ↦ p (↑a : α)) (↑l.attach : Multiset { x : α // x ∈ l }) =
  List.countP (fun (a : { x : α // x ∈ l }) ↦ decide (p (↑a : α))) l.attach
Tactic: simp only [quot_mk_to_coe, coe_countP, coe_attach, coe_countP, ← List.countP_attach (l := l)]
-- Lean 4 proof step from Mathlib.Data.Multiset.Count (goal)
Goal:
α : Type u_1
s s' : Multiset α
hs : s = s'
p p' : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred p'
hp : ∀ (x : α), x ∈ s → p x = p' x
⊢ countP p s = countP p' s'
have revert : ∀ (hs : s = s') (hp : ∀ (x : α), x ∈ s → p x = p' x), countP p s = countP p' s'
Tactic: revert hs hp
Cleared hypotheses: hs, hp
-- Lean 4 proof step from Mathlib.Data.Multiset.Count (hypothesis)
Goal:
α : Type u_1
s s' : Multiset α
p p' : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred p'
l l' : List α
hs :
  Eq (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l)
    (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l')
hp : ∀ (x : α), Membership.mem (γ := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) x → p x = p' x
⊢ countP p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) =
    countP p' (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l')
have hs₁ : l ~ l'
Tactic: simp only [quot_mk_to_coe'', coe_eq_coe] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Multiset.Count (goal)
Goal:
α : Type u_1
s s' : Multiset α
p p' : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred p'
l l' : List α
hp : ∀ (x : α), Membership.mem (γ := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) x → p x = p' x
hs : l ~ l'
⊢ countP p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) =
    countP p' (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l')
have apply : ∀ (x : α), x ∈ l → decide (p x) = decide (p' x)
Tactic: apply hs.countP_congr
-- Lean 4 proof step from Mathlib.Data.Multiset.Count (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
⊢ count a (↑l : Multiset α) = List.count a l
have simp_rw : List.countP (fun (b : α) ↦ decide (b = a)) l = List.countP (fun (x : α) ↦ x == a) l
Tactic: simp_rw [count, List.count, coe_countP (a = ·) l, @eq_comm _ a]
-- Lean 4 proof step from Mathlib.Data.Multiset.Count (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
⊢ 1 ≤ count a s ↔ a ∈ s
have rw : 0 < count a s ↔ a ∈ s
Tactic: rw [succ_le_iff, count_pos]
-- Lean 4 proof step from Mathlib.Data.Multiset.Count (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
rw : 0 < count a s ↔ a ∈ s
⊢ 1 ≤ count a s ↔ a ∈ s
have rw₁ : a ∈ s ↔ a ∈ s
Tactic: rw [succ_le_iff, count_pos]
-- Lean 4 proof step from Mathlib.Data.Multiset.Count (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
_l₁ _l₂ : List α
⊢ (isSetoid α : List α → List α → Prop) _l₁ _l₂ ↔ ∀ (a : α), count a ⟦_l₁⟧ = count a ⟦_l₂⟧
have simp : (isSetoid α : List α → List α → Prop) _l₁ _l₂ ↔ ∀ (a : α), List.count a _l₁ = List.count a _l₂
Tactic: simp only [quot_mk_to_coe, coe_count]
-- Lean 4 proof step from Mathlib.Data.Multiset.Count (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Symm r
x : α
inst_2 : DecidablePred (r x)
t : Multiset α
h : Rel r 0 t
⊢ countP (r x) 0 = countP (r x) t
have empty : countP (r x) 0 = countP (r x) 0
Tactic: rw [rel_zero_left.mp h]
-- Lean 4 proof step from Mathlib.Data.Multiset.Count (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Symm r
x : α
inst_2 : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α} (h : Rel r s t), countP (r x) s = countP (r x) t
t : Multiset α
h : Rel r (y ::ₘ s) t
⊢ countP (r x) (y ::ₘ s) = countP (r x) t
have cons : ∀ (b : α) (bs : Multiset α) (hb1 : r y b) (hb2 : Rel r s bs) (h : Rel r (y ::ₘ s) (b ::ₘ bs)),
  countP (r x) (y ::ₘ s) = countP (r x) (b ::ₘ bs)
Tactic: obtain ⟨b, bs, hb1, hb2, rfl⟩ := rel_cons_left.mp h
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Data.Multiset.Count (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Symm r
x : α
inst_2 : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α} (h : Rel r s t), countP (r x) s = countP (r x) t
b : α
bs : Multiset α
hb1 : r y b
hb2 : Rel r s bs
h : Rel r (y ::ₘ s) (b ::ₘ bs)
⊢ countP (r x) (y ::ₘ s) = countP (r x) (b ::ₘ bs)
have cons : (countP (r x) bs + if r x y then 1 else 0) = countP (r x) bs + if r x b then 1 else 0
Tactic: rw [countP_cons, countP_cons, ih hb2]
-- Lean 4 proof step from Mathlib.Data.Multiset.Count (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Symm r
x : α
inst_2 : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α} (h : Rel r s t), countP (r x) s = countP (r x) t
b : α
bs : Multiset α
hb1 : r y b
hb2 : Rel r s bs
h : Rel r (y ::ₘ s) (b ::ₘ bs)
⊢ (countP (r x) bs + if r x y then 1 else 0) = countP (r x) bs + if r x b then 1 else 0
have cons : Eq (α := ℕ) (if r x y then 1 else 0) (if r x b then 1 else 0)
Tactic: simp only [Nat.add_right_inj]
-- Lean 4 proof step from Mathlib.Data.Multiset.Count (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Symm r
s t : Multiset α
x : α
inst_2 : DecidablePred (r x)
h : Rel r s t
⊢ countP (r x) s = countP (r x) t
have empty : ∀ {t : Multiset α} (h : Rel r 0 t), countP (r x) 0 = countP (r x) t
Tactic: induction s using Multiset.induction_on generalizing t with
  | empty => rw [rel_zero_left.mp h]
  | cons y s ih =>
    obtain ⟨b, bs, hb1, hb2, rfl⟩ := rel_cons_left.mp h
    rw [countP_cons, countP_cons, ih hb2]
    simp only [Nat.add_right_inj]
    exact (if_congr ⟨fun h => _root_.trans h hb1, fun h => _root_.trans h (symm hb1)⟩ rfl rfl)
Cleared hypotheses: s, t, h