awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Multiset.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m_1 m : Multiset α
f : α → β
l : List α
a : α
s : List α
x_1 :
  { v : Equiv.{u_1 + 1, u_2 + 1} (ToType ⟦s⟧) (map f ⟦s⟧).ToType //
    ∀ (a : ToType ⟦s⟧),
      Sigma.fst (β := fun (x : β) ↦ Fin (count x (map f ⟦s⟧))) ((v : (a : ToType ⟦s⟧) → (map f ⟦s⟧).ToType) a) =
        f (a.fst (β := fun (x : α) ↦ Fin (count x ⟦s⟧))) }
v : Equiv.{u_1 + 1, u_2 + 1} (ToType ⟦s⟧) (map f ⟦s⟧).ToType
hv :
  ∀ (a : ToType ⟦s⟧),
    Sigma.fst (β := fun (x : β) ↦ Fin (count x (map f ⟦s⟧))) ((v : (a : ToType ⟦s⟧) → (map f ⟦s⟧).ToType) a) =
      f (a.fst (β := fun (x : α) ↦ Fin (count x ⟦s⟧)))
x : ToType ⟦a :: s⟧
⊢ Sigma.fst (β := fun (x : β) ↦ Fin (count x (map f ⟦a :: s⟧)))
      (((Equiv.trans (Equiv.trans (Equiv.trans consEquiv v.optionCongr) (Equiv.symm consEquiv)) (Equiv.symm (cast ⋯)) :
            Equiv.{u_1 + 1, u_2 + 1} (a ::ₘ ⟦s⟧).ToType (map f ⟦a :: s⟧).ToType) :
          (a_1 : ToType ⟦a :: s⟧) → (map f ⟦a :: s⟧).ToType)
        x) =
    f (x.fst (β := fun (x : α) ↦ Fin (count x ⟦a :: s⟧)))
have simp : Sigma.fst (β := fun (x : β) ↦ Fin (count x (map f ⟦a :: s⟧)))
    ((Equiv.symm (cast sorry) : (a_1 : (f a ::ₘ map f ⟦s⟧).ToType) → (map f ⟦a :: s⟧).ToType)
      (Option.elim
        (Option.map.{u_1, u_2} (α := ToType ⟦s⟧) (⇑v : (a : ToType ⟦s⟧) → (map f ⟦s⟧).ToType)
          (if h :
              x.fst (β := fun (x : α) ↦ Fin (count x (a ::ₘ ⟦s⟧))) = a ∧
                (↑(x.snd (β := fun (x : α) ↦ Fin (count x (a ::ₘ ⟦s⟧)))) : ℕ) = count a ⟦s⟧ then
            none
          else
            some
              (Sigma.mk (β := fun (x : α) ↦ Fin (count x ⟦s⟧)) (x.fst (β := fun (x : α) ↦ Fin (count x (a ::ₘ ⟦s⟧))))
                ⟨(↑(x.snd (β := fun (x : α) ↦ Fin (count x (a ::ₘ ⟦s⟧)))) : ℕ), sorry⟩)))
        (Sigma.mk (β := fun (x : β) ↦ Fin (count x (f a ::ₘ map f ⟦s⟧))) (f a)
          (⟨count (f a) (map f ⟦s⟧), sorry⟩ : Fin (count (f a) (f a ::ₘ map f ⟦s⟧))))
        fun (x : (map f ⟦s⟧).ToType) ↦
        Sigma.mk (β := fun (x : β) ↦ Fin (count x (f a ::ₘ map f ⟦s⟧)))
          (x.fst (β := fun (x : β) ↦ Fin (count x (map f ⟦s⟧))))
          (Fin.castLE sorry (x.snd (β := fun (x : β) ↦ Fin (count x (map f ⟦s⟧))))))) =
  f (x.fst (β := fun (x : α) ↦ Fin (count x ⟦a :: s⟧)))
Tactic: simp only [consEquiv, Equiv.trans_apply, Equiv.coe_fn_mk, Equiv.optionCongr_apply,
            Equiv.coe_fn_symm_mk]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m_1 m : Multiset α
f : α → β
l : List α
a : α
s : List α
x_1 :
  { v : Equiv.{u_1 + 1, u_2 + 1} (ToType ⟦s⟧) (map f ⟦s⟧).ToType //
    ∀ (a : ToType ⟦s⟧),
      Sigma.fst (β := fun (x : β) ↦ Fin (count x (map f ⟦s⟧))) ((v : (a : ToType ⟦s⟧) → (map f ⟦s⟧).ToType) a) =
        f (a.fst (β := fun (x : α) ↦ Fin (count x ⟦s⟧))) }
v : Equiv.{u_1 + 1, u_2 + 1} (ToType ⟦s⟧) (map f ⟦s⟧).ToType
hv :
  ∀ (a : ToType ⟦s⟧),
    Sigma.fst (β := fun (x : β) ↦ Fin (count x (map f ⟦s⟧))) ((v : (a : ToType ⟦s⟧) → (map f ⟦s⟧).ToType) a) =
      f (a.fst (β := fun (x : α) ↦ Fin (count x ⟦s⟧)))
x : ToType ⟦a :: s⟧
⊢ Sigma.fst (β := fun (x : β) ↦ Fin (count x (map f ⟦a :: s⟧)))
      ((Equiv.symm (cast ⋯) : (a_1 : (f a ::ₘ map f ⟦s⟧).ToType) → (map f ⟦a :: s⟧).ToType)
        (Option.elim
          (Option.map.{u_1, u_2} (α := ToType ⟦s⟧) (⇑v : (a : ToType ⟦s⟧) → (map f ⟦s⟧).ToType)
            (if h :
                x.fst (β := fun (x : α) ↦ Fin (count x (a ::ₘ ⟦s⟧))) = a ∧
                  (↑(x.snd (β := fun (x : α) ↦ Fin (count x (a ::ₘ ⟦s⟧)))) : ℕ) = count a ⟦s⟧ then
              none
            else
              some
                (Sigma.mk (β := fun (x : α) ↦ Fin (count x ⟦s⟧)) (x.fst (β := fun (x : α) ↦ Fin (count x (a ::ₘ ⟦s⟧))))
                  ⟨(↑(x.snd (β := fun (x : α) ↦ Fin (count x (a ::ₘ ⟦s⟧)))) : ℕ), ⋯⟩)))
          (Sigma.mk (β := fun (x : β) ↦ Fin (count x (f a ::ₘ map f ⟦s⟧))) (f a)
            (⟨count (f a) (map f ⟦s⟧), ⋯⟩ : Fin (count (f a) (f a ::ₘ map f ⟦s⟧))))
          fun (x : (map f ⟦s⟧).ToType) ↦
          Sigma.mk (β := fun (x : β) ↦ Fin (count x (f a ::ₘ map f ⟦s⟧)))
            (x.fst (β := fun (x : β) ↦ Fin (count x (map f ⟦s⟧))))
            (Fin.castLE ⋯ (x.snd (β := fun (x : β) ↦ Fin (count x (map f ⟦s⟧))))))) =
    f (x.fst (β := fun (x : α) ↦ Fin (count x ⟦a :: s⟧)))
have isTrue : x.fst (β := fun (x : α) ↦ Fin (count x (a ::ₘ ⟦s⟧))) = a ∧
    (↑(x.snd (β := fun (x : α) ↦ Fin (count x (a ::ₘ ⟦s⟧)))) : ℕ) = count a ⟦s⟧ →
  Sigma.fst (β := fun (x : β) ↦ Fin (count x (map f ⟦a :: s⟧)))
      ((Equiv.symm (cast sorry) : (a_1 : (f a ::ₘ map f ⟦s⟧).ToType) → (map f ⟦a :: s⟧).ToType)
        (Option.elim (Option.map.{u_1, u_2} (α := ToType ⟦s⟧) (⇑v : (a : ToType ⟦s⟧) → (map f ⟦s⟧).ToType) none)
          (Sigma.mk (β := fun (x : β) ↦ Fin (count x (f a ::ₘ map f ⟦s⟧))) (f a)
            (⟨count (f a) (map f ⟦s⟧), sorry⟩ : Fin (count (f a) (f a ::ₘ map f ⟦s⟧))))
          fun (x : (map f ⟦s⟧).ToType) ↦
          Sigma.mk (β := fun (x : β) ↦ Fin (count x (f a ::ₘ map f ⟦s⟧)))
            (x.fst (β := fun (x : β) ↦ Fin (count x (map f ⟦s⟧))))
            (Fin.castLE sorry (x.snd (β := fun (x : β) ↦ Fin (count x (map f ⟦s⟧))))))) =
    f (x.fst (β := fun (x : α) ↦ Fin (count x ⟦a :: s⟧)))
Tactic: split
-- Lean 4 proof step from Mathlib.Data.Multiset.Fold (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b a : α
s : Multiset α
⊢ fold op b (a ::ₘ s) = fold op (op b a) s
have rw : foldl op b (a ::ₘ s) = fold op (op b a) s
Tactic: rw [fold_eq_foldl, foldl_cons, ← fold_eq_foldl]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fold (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b a : α
s : Multiset α
rw : foldl op b (a ::ₘ s) = fold op (op b a) s
⊢ fold op b (a ::ₘ s) = fold op (op b a) s
have rw₁ : foldl op (op b a) s = fold op (op b a) s
Tactic: rw [fold_eq_foldl, foldl_cons, ← fold_eq_foldl]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fold (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b a : α
s : Multiset α
rw : foldl op b (a ::ₘ s) = fold op (op b a) s
rw₁ : foldl op (op b a) s = fold op (op b a) s
⊢ fold op b (a ::ₘ s) = fold op (op b a) s
have rw₂ : fold op (op b a) s = fold op (op b a) s
Tactic: rw [fold_eq_foldl, foldl_cons, ← fold_eq_foldl]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fold (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b a : α
s : Multiset α
⊢ fold op b (a ::ₘ s) = fold op (op a b) s
have rw : fold op (op b a) s = fold op (op a b) s
Tactic: rw [fold_cons'_right, hc.comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fold (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b a : α
s : Multiset α
rw : fold op (op b a) s = fold op (op a b) s
⊢ fold op b (a ::ₘ s) = fold op (op a b) s
have rw₁ : fold op (op a b) s = fold op (op a b) s
Tactic: rw [fold_cons'_right, hc.comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fold (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b₁ b₂ : α
s₁ s₂ : Multiset α
⊢ fold op (op b₁ b₂) (s₁ + 0) = op (fold op b₁ s₁) (fold op b₂ 0)
have rw : fold op (op b₁ b₂) s₁ = op (fold op b₁ s₁) (fold op b₂ 0)
Tactic: rw [Multiset.add_zero, fold_zero, ← fold_cons'_right, ← fold_cons_right op]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fold (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b₁ b₂ : α
s₁ s₂ : Multiset α
rw : fold op (op b₁ b₂) s₁ = op (fold op b₁ s₁) (fold op b₂ 0)
⊢ fold op (op b₁ b₂) (s₁ + 0) = op (fold op b₁ s₁) (fold op b₂ 0)
have rw₁ : fold op (op b₁ b₂) s₁ = op (fold op b₁ s₁) b₂
Tactic: rw [Multiset.add_zero, fold_zero, ← fold_cons'_right, ← fold_cons_right op]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fold (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b₁ b₂ : α
s₁ s₂ : Multiset α
rw : fold op (op b₁ b₂) s₁ = op (fold op b₁ s₁) (fold op b₂ 0)
rw₁ : fold op (op b₁ b₂) s₁ = op (fold op b₁ s₁) b₂
⊢ fold op (op b₁ b₂) (s₁ + 0) = op (fold op b₁ s₁) (fold op b₂ 0)
have rw₂ : fold op b₁ (b₂ ::ₘ s₁) = op (fold op b₁ s₁) b₂
Tactic: rw [Multiset.add_zero, fold_zero, ← fold_cons'_right, ← fold_cons_right op]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fold (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b₁ b₂ : α
s₁ s₂ : Multiset α
rw : fold op (op b₁ b₂) s₁ = op (fold op b₁ s₁) (fold op b₂ 0)
rw₁ : fold op (op b₁ b₂) s₁ = op (fold op b₁ s₁) b₂
rw₂ : fold op b₁ (b₂ ::ₘ s₁) = op (fold op b₁ s₁) b₂
⊢ fold op (op b₁ b₂) (s₁ + 0) = op (fold op b₁ s₁) (fold op b₂ 0)
have rw₃ : fold op b₁ (b₂ ::ₘ s₁) = fold op b₁ (b₂ ::ₘ s₁)
Tactic: rw [Multiset.add_zero, fold_zero, ← fold_cons'_right, ← fold_cons_right op]
-- Lean 4 proof step from Mathlib.Data.Multiset.Fold (goal)
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b₁ b₂ : α
s₁ s₂ : Multiset α
a : α
b : Multiset α
h : fold op (op b₁ b₂) (s₁ + b) = op (fold op b₁ s₁) (fold op b₂ b)
⊢ fold op (op b₁ b₂) (s₁ + a ::ₘ b) = op (fold op b₁ s₁) (fold op b₂ (a ::ₘ b))
have rw : fold op (op b₁ b₂) (s₁ + a ::ₘ b) = op (fold op b₁ s₁) (op a (fold op b₂ b))
Tactic: rw [fold_cons_left, add_cons, fold_cons_left, h, ← ha.assoc, hc.comm 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
b₁ b₂ : α
s₁ s₂ : Multiset α
a : α
b : Multiset α
h : fold op (op b₁ b₂) (s₁ + b) = op (fold op b₁ s₁) (fold op b₂ b)
rw : fold op (op b₁ b₂) (s₁ + a ::ₘ b) = op (fold op b₁ s₁) (op a (fold op b₂ b))
⊢ fold op (op b₁ b₂) (s₁ + a ::ₘ b) = op (fold op b₁ s₁) (fold op b₂ (a ::ₘ b))
have rw₁ : fold op (op b₁ b₂) (a ::ₘ (s₁ + b)) = op (fold op b₁ s₁) (op a (fold op b₂ b))
Tactic: rw [fold_cons_left, add_cons, fold_cons_left, h, ← ha.assoc, hc.comm 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
b₁ b₂ : α
s₁ s₂ : Multiset α
a : α
b : Multiset α
h : fold op (op b₁ b₂) (s₁ + b) = op (fold op b₁ s₁) (fold op b₂ b)
rw : fold op (op b₁ b₂) (s₁ + a ::ₘ b) = op (fold op b₁ s₁) (op a (fold op b₂ b))
rw₁ : fold op (op b₁ b₂) (a ::ₘ (s₁ + b)) = op (fold op b₁ s₁) (op a (fold op b₂ b))
⊢ fold op (op b₁ b₂) (s₁ + a ::ₘ b) = op (fold op b₁ s₁) (fold op b₂ (a ::ₘ b))
have rw₂ : op a (fold op (op b₁ b₂) (s₁ + b)) = op (fold op b₁ s₁) (op a (fold op b₂ b))
Tactic: rw [fold_cons_left, add_cons, fold_cons_left, h, ← ha.assoc, hc.comm 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
b₁ b₂ : α
s₁ s₂ : Multiset α
a : α
b : Multiset α
h : fold op (op b₁ b₂) (s₁ + b) = op (fold op b₁ s₁) (fold op b₂ b)
rw : fold op (op b₁ b₂) (s₁ + a ::ₘ b) = op (fold op b₁ s₁) (op a (fold op b₂ b))
rw₁ : fold op (op b₁ b₂) (a ::ₘ (s₁ + b)) = op (fold op b₁ s₁) (op a (fold op b₂ b))
rw₂ : op a (fold op (op b₁ b₂) (s₁ + b)) = op (fold op b₁ s₁) (op a (fold op b₂ b))
⊢ fold op (op b₁ b₂) (s₁ + a ::ₘ b) = op (fold op b₁ s₁) (fold op b₂ (a ::ₘ b))
have rw₃ : op a (op (fold op b₁ s₁) (fold op b₂ b)) = op (fold op b₁ s₁) (op a (fold op b₂ b))
Tactic: rw [fold_cons_left, add_cons, fold_cons_left, h, ← ha.assoc, hc.comm 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
b₁ b₂ : α
s₁ s₂ : Multiset α
a : α
b : Multiset α
h : fold op (op b₁ b₂) (s₁ + b) = op (fold op b₁ s₁) (fold op b₂ b)
rw : fold op (op b₁ b₂) (s₁ + a ::ₘ b) = op (fold op b₁ s₁) (op a (fold op b₂ b))
rw₁ : fold op (op b₁ b₂) (a ::ₘ (s₁ + b)) = op (fold op b₁ s₁) (op a (fold op b₂ b))
rw₂ : op a (fold op (op b₁ b₂) (s₁ + b)) = op (fold op b₁ s₁) (op a (fold op b₂ b))
rw₃ : op a (op (fold op b₁ s₁) (fold op b₂ b)) = op (fold op b₁ s₁) (op a (fold op b₂ b))
⊢ fold op (op b₁ b₂) (s₁ + a ::ₘ b) = op (fold op b₁ s₁) (fold op b₂ (a ::ₘ b))
have rw₄ : op (op a (fold op b₁ s₁)) (fold op b₂ b) = op (fold op b₁ s₁) (op a (fold op b₂ b))
Tactic: rw [fold_cons_left, add_cons, fold_cons_left, h, ← ha.assoc, hc.comm 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
b₁ b₂ : α
s₁ s₂ : Multiset α
a : α
b : Multiset α
h : fold op (op b₁ b₂) (s₁ + b) = op (fold op b₁ s₁) (fold op b₂ b)
rw : fold op (op b₁ b₂) (s₁ + a ::ₘ b) = op (fold op b₁ s₁) (op a (fold op b₂ b))
rw₁ : fold op (op b₁ b₂) (a ::ₘ (s₁ + b)) = op (fold op b₁ s₁) (op a (fold op b₂ b))
rw₂ : op a (fold op (op b₁ b₂) (s₁ + b)) = op (fold op b₁ s₁) (op a (fold op b₂ b))
rw₃ : op a (op (fold op b₁ s₁) (fold op b₂ b)) = op (fold op b₁ s₁) (op a (fold op b₂ b))
rw₄ : op (op a (fold op b₁ s₁)) (fold op b₂ b) = op (fold op b₁ s₁) (op a (fold op b₂ b))
⊢ fold op (op b₁ b₂) (s₁ + a ::ₘ b) = op (fold op b₁ s₁) (fold op b₂ (a ::ₘ b))
have rw₅ : op (op (fold op b₁ s₁) a) (fold op b₂ b) = op (fold op b₁ s₁) (op a (fold op b₂ b))
Tactic: rw [fold_cons_left, add_cons, fold_cons_left, h, ← ha.assoc, hc.comm 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
b₁ b₂ : α
s₁ s₂ : Multiset α
a : α
b : Multiset α
h : fold op (op b₁ b₂) (s₁ + b) = op (fold op b₁ s₁) (fold op b₂ b)
rw : fold op (op b₁ b₂) (s₁ + a ::ₘ b) = op (fold op b₁ s₁) (op a (fold op b₂ b))
rw₁ : fold op (op b₁ b₂) (a ::ₘ (s₁ + b)) = op (fold op b₁ s₁) (op a (fold op b₂ b))
rw₂ : op a (fold op (op b₁ b₂) (s₁ + b)) = op (fold op b₁ s₁) (op a (fold op b₂ b))
rw₃ : op a (op (fold op b₁ s₁) (fold op b₂ b)) = op (fold op b₁ s₁) (op a (fold op b₂ b))
rw₄ : op (op a (fold op b₁ s₁)) (fold op b₂ b) = op (fold op b₁ s₁) (op a (fold op b₂ b))
rw₅ : op (op (fold op b₁ s₁) a) (fold op b₂ b) = op (fold op b₁ s₁) (op a (fold op b₂ b))
⊢ fold op (op b₁ b₂) (s₁ + a ::ₘ b) = op (fold op b₁ s₁) (fold op b₂ (a ::ₘ b))
have rw₆ : op (fold op b₁ s₁) (op a (fold op b₂ b)) = op (fold op b₁ s₁) (op a (fold op b₂ b))
Tactic: rw [fold_cons_left, add_cons, fold_cons_left, h, ← ha.assoc, hc.comm 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))
⊢ 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 : 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)))
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)))
⊢ 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 (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)))
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)))
⊢ 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 (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)))
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)))
⊢ 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 (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)))
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)))
⊢ 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 (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)))
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)))
⊢ 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 (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))
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))
⊢ 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 (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))
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]