awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Multiset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
f g : β → α
u₁ u₂ : α
s : Multiset β
a : β
b : Multiset β
h : fold op (op u₁ u₂) (map (fun (x : β) ↦ op (f x) (g x)) b) = op (fold op u₁ (map f b)) (fold op u₂ (map g b))
rw :
  fold op (op u₁ u₂) (op (f a) (g a) ::ₘ map (fun (x : β) ↦ op (f x) (g x)) b) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
rw₁ :
  op (op (f a) (g a)) (fold op (op u₁ u₂) (map (fun (x : β) ↦ op (f x) (g x)) b)) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
rw₂ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
rw₃ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (fold op u₁ (f a ::ₘ map f b)) (fold op u₂ (map g (a ::ₘ b)))
rw₄ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (fold op u₂ (map g (a ::ₘ b)))
rw₅ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (fold op u₂ (g a ::ₘ map g b))
rw₆ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
⊢ fold op (op u₁ u₂) (map (fun (x : β) ↦ op (f x) (g x)) (a ::ₘ b)) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
have rw₇ : op (f a) (op (g a) (op (fold op u₁ (map f b)) (fold op u₂ (map g b)))) =
  op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
Tactic: rw [map_cons, fold_cons_left, h, map_cons, fold_cons_left, map_cons,
      fold_cons_right, ha.assoc, ← ha.assoc (g a), hc.comm (g a),
      ha.assoc, hc.comm (g a), ha.assoc]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
f g : β → α
u₁ u₂ : α
s : Multiset β
a : β
b : Multiset β
h : fold op (op u₁ u₂) (map (fun (x : β) ↦ op (f x) (g x)) b) = op (fold op u₁ (map f b)) (fold op u₂ (map g b))
rw :
  fold op (op u₁ u₂) (op (f a) (g a) ::ₘ map (fun (x : β) ↦ op (f x) (g x)) b) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
rw₁ :
  op (op (f a) (g a)) (fold op (op u₁ u₂) (map (fun (x : β) ↦ op (f x) (g x)) b)) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
rw₂ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
rw₃ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (fold op u₁ (f a ::ₘ map f b)) (fold op u₂ (map g (a ::ₘ b)))
rw₄ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (fold op u₂ (map g (a ::ₘ b)))
rw₅ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (fold op u₂ (g a ::ₘ map g b))
rw₆ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
rw₇ :
  op (f a) (op (g a) (op (fold op u₁ (map f b)) (fold op u₂ (map g b)))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
⊢ fold op (op u₁ u₂) (map (fun (x : β) ↦ op (f x) (g x)) (a ::ₘ b)) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
have rw₈ : op (f a) (op (op (g a) (fold op u₁ (map f b))) (fold op u₂ (map g b))) =
  op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
Tactic: rw [map_cons, fold_cons_left, h, map_cons, fold_cons_left, map_cons,
      fold_cons_right, ha.assoc, ← ha.assoc (g a), hc.comm (g a),
      ha.assoc, hc.comm (g a), ha.assoc]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
f g : β → α
u₁ u₂ : α
s : Multiset β
a : β
b : Multiset β
h : fold op (op u₁ u₂) (map (fun (x : β) ↦ op (f x) (g x)) b) = op (fold op u₁ (map f b)) (fold op u₂ (map g b))
rw :
  fold op (op u₁ u₂) (op (f a) (g a) ::ₘ map (fun (x : β) ↦ op (f x) (g x)) b) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
rw₁ :
  op (op (f a) (g a)) (fold op (op u₁ u₂) (map (fun (x : β) ↦ op (f x) (g x)) b)) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
rw₂ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
rw₃ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (fold op u₁ (f a ::ₘ map f b)) (fold op u₂ (map g (a ::ₘ b)))
rw₄ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (fold op u₂ (map g (a ::ₘ b)))
rw₅ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (fold op u₂ (g a ::ₘ map g b))
rw₆ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
rw₇ :
  op (f a) (op (g a) (op (fold op u₁ (map f b)) (fold op u₂ (map g b)))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
rw₈ :
  op (f a) (op (op (g a) (fold op u₁ (map f b))) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
⊢ fold op (op u₁ u₂) (map (fun (x : β) ↦ op (f x) (g x)) (a ::ₘ b)) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
have rw₉ : op (f a) (op (op (fold op u₁ (map f b)) (g a)) (fold op u₂ (map g b))) =
  op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
Tactic: rw [map_cons, fold_cons_left, h, map_cons, fold_cons_left, map_cons,
      fold_cons_right, ha.assoc, ← ha.assoc (g a), hc.comm (g a),
      ha.assoc, hc.comm (g a), ha.assoc]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
f g : β → α
u₁ u₂ : α
s : Multiset β
a : β
b : Multiset β
h : fold op (op u₁ u₂) (map (fun (x : β) ↦ op (f x) (g x)) b) = op (fold op u₁ (map f b)) (fold op u₂ (map g b))
rw :
  fold op (op u₁ u₂) (op (f a) (g a) ::ₘ map (fun (x : β) ↦ op (f x) (g x)) b) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
rw₁ :
  op (op (f a) (g a)) (fold op (op u₁ u₂) (map (fun (x : β) ↦ op (f x) (g x)) b)) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
rw₂ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
rw₃ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (fold op u₁ (f a ::ₘ map f b)) (fold op u₂ (map g (a ::ₘ b)))
rw₄ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (fold op u₂ (map g (a ::ₘ b)))
rw₅ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (fold op u₂ (g a ::ₘ map g b))
rw₆ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
rw₇ :
  op (f a) (op (g a) (op (fold op u₁ (map f b)) (fold op u₂ (map g b)))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
rw₈ :
  op (f a) (op (op (g a) (fold op u₁ (map f b))) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
rw₉ :
  op (f a) (op (op (fold op u₁ (map f b)) (g a)) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
⊢ fold op (op u₁ u₂) (map (fun (x : β) ↦ op (f x) (g x)) (a ::ₘ b)) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
have rw₁₀ : op (f a) (op (fold op u₁ (map f b)) (op (g a) (fold op u₂ (map g b)))) =
  op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
Tactic: rw [map_cons, fold_cons_left, h, map_cons, fold_cons_left, map_cons,
      fold_cons_right, ha.assoc, ← ha.assoc (g a), hc.comm (g a),
      ha.assoc, hc.comm (g a), ha.assoc]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
f g : β → α
u₁ u₂ : α
s : Multiset β
a : β
b : Multiset β
h : fold op (op u₁ u₂) (map (fun (x : β) ↦ op (f x) (g x)) b) = op (fold op u₁ (map f b)) (fold op u₂ (map g b))
rw :
  fold op (op u₁ u₂) (op (f a) (g a) ::ₘ map (fun (x : β) ↦ op (f x) (g x)) b) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
rw₁ :
  op (op (f a) (g a)) (fold op (op u₁ u₂) (map (fun (x : β) ↦ op (f x) (g x)) b)) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
rw₂ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
rw₃ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (fold op u₁ (f a ::ₘ map f b)) (fold op u₂ (map g (a ::ₘ b)))
rw₄ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (fold op u₂ (map g (a ::ₘ b)))
rw₅ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (fold op u₂ (g a ::ₘ map g b))
rw₆ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
rw₇ :
  op (f a) (op (g a) (op (fold op u₁ (map f b)) (fold op u₂ (map g b)))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
rw₈ :
  op (f a) (op (op (g a) (fold op u₁ (map f b))) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
rw₉ :
  op (f a) (op (op (fold op u₁ (map f b)) (g a)) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
rw₁₀ :
  op (f a) (op (fold op u₁ (map f b)) (op (g a) (fold op u₂ (map g b)))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
⊢ fold op (op u₁ u₂) (map (fun (x : β) ↦ op (f x) (g x)) (a ::ₘ b)) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
have rw₁₁ : op (f a) (op (fold op u₁ (map f b)) (op (fold op u₂ (map g b)) (g a))) =
  op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
Tactic: rw [map_cons, fold_cons_left, h, map_cons, fold_cons_left, map_cons,
      fold_cons_right, ha.assoc, ← ha.assoc (g a), hc.comm (g a),
      ha.assoc, hc.comm (g a), ha.assoc]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
f g : β → α
u₁ u₂ : α
s : Multiset β
a : β
b : Multiset β
h : fold op (op u₁ u₂) (map (fun (x : β) ↦ op (f x) (g x)) b) = op (fold op u₁ (map f b)) (fold op u₂ (map g b))
rw :
  fold op (op u₁ u₂) (op (f a) (g a) ::ₘ map (fun (x : β) ↦ op (f x) (g x)) b) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
rw₁ :
  op (op (f a) (g a)) (fold op (op u₁ u₂) (map (fun (x : β) ↦ op (f x) (g x)) b)) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
rw₂ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
rw₃ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (fold op u₁ (f a ::ₘ map f b)) (fold op u₂ (map g (a ::ₘ b)))
rw₄ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (fold op u₂ (map g (a ::ₘ b)))
rw₅ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (fold op u₂ (g a ::ₘ map g b))
rw₆ :
  op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
rw₇ :
  op (f a) (op (g a) (op (fold op u₁ (map f b)) (fold op u₂ (map g b)))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
rw₈ :
  op (f a) (op (op (g a) (fold op u₁ (map f b))) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
rw₉ :
  op (f a) (op (op (fold op u₁ (map f b)) (g a)) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
rw₁₀ :
  op (f a) (op (fold op u₁ (map f b)) (op (g a) (fold op u₂ (map g b)))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
rw₁₁ :
  op (f a) (op (fold op u₁ (map f b)) (op (fold op u₂ (map g b)) (g a))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
⊢ fold op (op u₁ u₂) (map (fun (x : β) ↦ op (f x) (g x)) (a ::ₘ b)) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
have rw₁₂ : op (f a) (op (fold op u₁ (map f b)) (op (fold op u₂ (map g b)) (g a))) =
  op (f a) (op (fold op u₁ (map f b)) (op (fold op u₂ (map g b)) (g a)))
Tactic: rw [map_cons, fold_cons_left, h, map_cons, fold_cons_left, map_cons,
      fold_cons_right, ha.assoc, ← ha.assoc (g a), hc.comm (g a),
      ha.assoc, hc.comm (g a), ha.assoc]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fold (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst : DecidableEq α
s₁ s₂ : Multiset α
b₁ b₂ : α
⊢ op (fold op b₁ (s₁ ∪ s₂)) (fold op b₂ (s₁ ∩ s₂)) = op (fold op b₁ s₁) (fold op b₂ s₂)
have rw : fold op (op b₁ b₂) (s₁ ∪ s₂ + s₁ ∩ s₂) = op (fold op b₁ s₁) (fold op b₂ s₂)
Tactic: rw [← fold_add op, union_add_inter, fold_add op]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fold (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst : DecidableEq α
s₁ s₂ : Multiset α
b₁ b₂ : α
rw : fold op (op b₁ b₂) (s₁ ∪ s₂ + s₁ ∩ s₂) = op (fold op b₁ s₁) (fold op b₂ s₂)
⊢ op (fold op b₁ (s₁ ∪ s₂)) (fold op b₂ (s₁ ∩ s₂)) = op (fold op b₁ s₁) (fold op b₂ s₂)
have rw₁ : fold op (op b₁ b₂) (s₁ + s₂) = op (fold op b₁ s₁) (fold op b₂ s₂)
Tactic: rw [← fold_add op, union_add_inter, fold_add op]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fold (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst : DecidableEq α
s₁ s₂ : Multiset α
b₁ b₂ : α
rw : fold op (op b₁ b₂) (s₁ ∪ s₂ + s₁ ∩ s₂) = op (fold op b₁ s₁) (fold op b₂ s₂)
rw₁ : fold op (op b₁ b₂) (s₁ + s₂) = op (fold op b₁ s₁) (fold op b₂ s₂)
⊢ op (fold op b₁ (s₁ ∪ s₂)) (fold op b₂ (s₁ ∩ s₂)) = op (fold op b₁ s₁) (fold op b₂ s₂)
have rw₂ : op (fold op b₁ s₁) (fold op b₂ s₂) = op (fold op b₁ s₁) (fold op b₂ s₂)
Tactic: rw [← fold_add op, union_add_inter, fold_add op]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fold (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst : DecidableEq α
hi : Std.IdempotentOp op
s_1 : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)
have pos : ∀ (h : a ∈ s), fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Data.Multiset.Fold (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst : DecidableEq α
hi : Std.IdempotentOp op
s_1 : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
pos : ∀ (h : a ∈ s), fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)
have neg : ∀ (h : ¬a ∈ s), fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Data.Multiset.Fold (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst : DecidableEq α
hi : Std.IdempotentOp op
s_1 : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : a ∈ s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)
have pos : fold op b s = op a (fold op b s)
Tactic: simp only [h, dedup_cons_of_mem, IH, fold_cons_left]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fold (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst : DecidableEq α
hi : Std.IdempotentOp op
s_1 : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : a ∈ s
⊢ fold op b s = op a (fold op b s)
have pos : fold op b (a ::ₘ s.erase a) = op a (fold op b (a ::ₘ s.erase a))
Tactic: rw [← cons_erase h, fold_cons_left, ← ha.assoc, hi.idempotent]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fold (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst : DecidableEq α
hi : Std.IdempotentOp op
s_1 : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : a ∈ s
pos : fold op b (a ::ₘ s.erase a) = op a (fold op b (a ::ₘ s.erase a))
⊢ fold op b s = op a (fold op b s)
have pos₁ : op a (fold op b (s.erase a)) = op a (op a (fold op b (s.erase a)))
Tactic: rw [← cons_erase h, fold_cons_left, ← ha.assoc, hi.idempotent]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fold (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst : DecidableEq α
hi : Std.IdempotentOp op
s_1 : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : a ∈ s
pos : fold op b (a ::ₘ s.erase a) = op a (fold op b (a ::ₘ s.erase a))
pos₁ : op a (fold op b (s.erase a)) = op a (op a (fold op b (s.erase a)))
⊢ fold op b s = op a (fold op b s)
have pos₂ : op a (fold op b (s.erase a)) = op (op a a) (fold op b (s.erase a))
Tactic: rw [← cons_erase h, fold_cons_left, ← ha.assoc, hi.idempotent]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fold (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst : DecidableEq α
hi : Std.IdempotentOp op
s_1 : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : a ∈ s
pos : fold op b (a ::ₘ s.erase a) = op a (fold op b (a ::ₘ s.erase a))
pos₁ : op a (fold op b (s.erase a)) = op a (op a (fold op b (s.erase a)))
pos₂ : op a (fold op b (s.erase a)) = op (op a a) (fold op b (s.erase a))
⊢ fold op b s = op a (fold op b s)
have pos₃ : op a (fold op b (s.erase a)) = op a (fold op b (s.erase a))
Tactic: rw [← cons_erase h, fold_cons_left, ← ha.assoc, hi.idempotent]
-- Lean 4 proof step from Mathlib.Data.Multiset.Functor (goal)
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : CommApplicative F
α' β' : Type u
f : α' → F β'
⊢ Multiset α' → F (Multiset β')
have refine : ∀ (a b : List α'),
  a ≈ b → (Functor.map ofList ∘ Traversable.traverse f) a = (Functor.map ofList ∘ Traversable.traverse f) b
Tactic: refine Quotient.lift (Functor.map ofList ∘ Traversable.traverse f) ?_
-- Lean 4 proof step from Mathlib.Data.Multiset.Functor (goal)
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
p : a ≈ b
⊢ (Functor.map ofList ∘ Traversable.traverse f) a = (Functor.map ofList ∘ Traversable.traverse f) b
have unfold : ofList <$> Traversable.traverse f a = ofList <$> Traversable.traverse f b
Tactic: unfold Function.comp
-- Lean 4 proof step from Mathlib.Data.Multiset.Functor (goal)
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
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₂
have rw : cons <$> f x <*> ofList <$> Traversable.traverse f l₂ = cons <$> f x <*> ofList <$> Traversable.traverse f l₂
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Multiset.Functor (hypothesis)
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₂
⊢ ofList <$> Traversable.traverse f (x :: l₁) = ofList <$> Traversable.traverse f (x :: l₂)
have this : 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]
-- Lean 4 proof step from Mathlib.Data.Multiset.Functor (goal)
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
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)
have 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)
Tactic: rw [CommApplicative.commutative_map]
-- Lean 4 proof step from Mathlib.Data.Multiset.Functor (goal)
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
⊢ 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)
have 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 β')
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Data.Multiset.Functor (goal)
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
⊢ 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 β')
have e_a : ∀ (a b : β') (l : List β'),
  flip (fun (a b : β') (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) a b l = (↑(a :: b :: l) : Multiset β')
Tactic: funext a b l
-- Lean 4 proof step from Mathlib.Data.Multiset.Functor (hypothesis)
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
⊢ ofList <$> Traversable.traverse f (y :: x :: l) = ofList <$> Traversable.traverse f (x :: y :: l)
have 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)
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