awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m : Multiset α
v : α
x : (v ::ₘ m).ToType
hx : x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) ≠ v
⊢ count (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) (v ::ₘ m) =
    count (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) m

Tactic:
simp [hx]
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
v : α
x : (v ::ₘ m).ToType
hx : x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) ≠ v
simp :
  Eq (α := m.ToType)
    (Sigma.mk (β := fun (x : α) ↦ Fin (count x m)) (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))))
      (⟨(↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ), ⋯⟩ :
        Fin (count (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) m)))
    (Sigma.mk (β := fun (x : α) ↦ Fin (count x m)) (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))))
      (Fin.cast ⋯ (x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))))))
⊢ Eq (α := Option m.ToType) ((consEquiv : (a : (v ::ₘ m).ToType) → Option m.ToType) x : Option m.ToType)
    (some
        (Sigma.mk (β := fun (x : α) ↦ Fin (count x m)) (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))))
          (Fin.cast ⋯ (x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))))) :
      Option m.ToType)

Tactic:
simp [consEquiv, hx]

Premises used: Multiset.consEquiv
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
v : α
x : (v ::ₘ m).ToType
hx : x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) ≠ v
⊢ Eq (α := m.ToType)
    (Sigma.mk (β := fun (x : α) ↦ Fin (count x m)) (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))))
      (⟨(↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ), ⋯⟩ :
        Fin (count (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) m)))
    (Sigma.mk (β := fun (x : α) ↦ Fin (count x m)) (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))))
      (Fin.cast ⋯ (x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))))))

Tactic:
rfl
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
v : α
x : (v ::ₘ m).ToType
hx : x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) = v
hx2 : (↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) = count v m
⊢ Eq (α := Option m.ToType) ((consEquiv : (a : (v ::ₘ m).ToType) → Option m.ToType) x : Option m.ToType)
    (none : Option m.ToType)

Tactic:
simp [consEquiv, hx, hx2]

Premises used: Multiset.consEquiv
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m : Multiset α
v : α
x : (v ::ₘ m).ToType
hx : x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) = v
hx2 : (↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) < count v m
⊢ (↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) <
    count (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) m

Tactic:
simpa [hx]
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
v : α
x : (v ::ₘ m).ToType
hx : x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) = v
hx2 : (↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) < count v m
⊢ Eq (α := Option m.ToType) ((consEquiv : (a : (v ::ₘ m).ToType) → Option m.ToType) x : Option m.ToType)
    (some
        (Sigma.mk (β := fun (x : α) ↦ Fin (count x m)) (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))))
          (⟨(↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ), ⋯⟩ :
            Fin (count (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) m))) :
      Option m.ToType)

Tactic:
simp [consEquiv, hx, hx2.ne]

Premises used: Multiset.consEquiv, LT.lt.ne
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m_1 m : Multiset α
f : α → β
l : List α
⊢ IsEmpty.{u_1 + 1} (ToType (α := α) 0)

Tactic:
infer_instance
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m_1 m : Multiset α
f : α → β
l : List α
⊢ IsEmpty.{u_2 + 1} (ToType (α := β) 0)

Tactic:
infer_instance
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m_1 m : Multiset α
f : α → β
l : List α
⊢ ∀ (a : ToType ⟦[]⟧),
    Sigma.fst (β := fun (x : β) ↦ Fin (count x (map f ⟦[]⟧)))
        ((Equiv.equivOfIsEmpty (ToType ⟦[]⟧) (map f ⟦[]⟧).ToType : (a : ToType ⟦[]⟧) → (map f ⟦[]⟧).ToType) a) =
      f (a.fst (β := fun (x : α) ↦ Fin (count x ⟦[]⟧)))

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Fintype
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⟧
simp :
  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⟧)))
⊢ 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⟧)))

Tactic:
simp only [consEquiv, Equiv.trans_apply, Equiv.coe_fn_mk, Equiv.optionCongr_apply,
            Equiv.coe_fn_symm_mk]

Premises used: Equiv.coe_fn_symm_mk, Equiv.trans_apply, Multiset.consEquiv, Equiv.optionCongr_apply, Equiv.coe_fn_mk
-- Module: Mathlib.Data.Multiset.Fintype
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⟧
h :
  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 ⋯) : (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⟧), ⋯⟩ : 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⟧)))

Tactic:
simp_all
-- Module: Mathlib.Data.Multiset.Fintype
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⟧
h :
  ¬(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 ⋯) : (a_1 : (f a ::ₘ map f ⟦s⟧).ToType) → (map f ⟦a :: s⟧).ToType)
        (Option.elim
          (Option.map (α := ToType ⟦s⟧) (⇑v : (a : ToType ⟦s⟧) → (map f ⟦s⟧).ToType)
            (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⟧)))

Tactic:
simp_all
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
s : Multiset α
f : α → β
v : s.ToType
⊢ Sigma.fst (β := fun (x : β) ↦ Fin (count x (map f s)))
      (((s.mapEquiv f : Equiv.{u_1 + 1, u_2 + 1} s.ToType (map f s).ToType) : (a : s.ToType) → (map f s).ToType) v) =
    f (v.fst (β := fun (x : α) ↦ Fin (count x s)))

Tactic:
(Multiset.mapEquiv_aux s f).out.2 v

Premises used: Quotient.out, Multiset.mapEquiv_aux, Subtype.property
-- Module: Mathlib.Data.Multiset.Fold
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b : α
s : Multiset α
⊢ fold op b s = foldr op b s

Tactic:
rfl

Premises used: rfl, Multiset.fold
-- Module: Mathlib.Data.Multiset.Fold
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b : α
l : List α
⊢ fold op b (↑l : Multiset α) = List.foldr op b l

Tactic:
rfl

Premises used: Multiset.foldr, rfl, Multiset.fold
-- Module: Mathlib.Data.Multiset.Fold
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b : α
l : List α
⊢ List.foldl (fun (x y : α) ↦ op y x) b l = List.foldl op b l

Tactic:
simp [hc.comm]

Premises used: Std.Commutative.comm
-- Module: Mathlib.Data.Multiset.Fold
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b : α
s : Multiset α
⊢ fold op b s = foldl op b s

Tactic:
Quot.inductionOn s fun _ => coe_fold_l _ _ _

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.Fold
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b : α
⊢ fold op b 0 = b

Tactic:
rfl

Premises used: Multiset.foldr, List.foldr, rfl, Multiset.fold
-- Module: Mathlib.Data.Multiset.Fold
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
⊢ ∀ (b a : α) (s : Multiset α), fold op b (a ::ₘ s) = op a (fold op b s)

Tactic:
foldr_cons _

Premises used: Multiset.foldr_cons, Multiset.fold
-- Module: Mathlib.Data.Multiset.Fold
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b a : α
s : Multiset α
⊢ fold op b (a ::ₘ s) = op (fold op b s) a

Tactic:
simp [hc.comm]

Premises used: Std.Commutative.comm
-- Module: Mathlib.Data.Multiset.Fold
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
rw₂ rw₃ : fold op (op b a) s = fold op (op b a) s
⊢ fold op b (a ::ₘ s) = fold op (op b a) s

Tactic:
rw [fold_eq_foldl, foldl_cons, ← fold_eq_foldl]

Premises used: Multiset.fold_eq_foldl, Multiset.foldl_cons
-- Module: Mathlib.Data.Multiset.Fold
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
rw₁ rw₂ : fold op (op a b) s = fold op (op a b) s
⊢ fold op b (a ::ₘ s) = fold op (op a b) s

Tactic:
rw [fold_cons'_right, hc.comm]

Premises used: Std.Commutative.comm, Multiset.fold_cons'_right
-- Module: Mathlib.Data.Multiset.Fold
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₂
rw₃ rw₄ : fold op b₁ (b₂ ::ₘ s₁) = fold op b₁ (b₂ ::ₘ s₁)
⊢ fold op (op b₁ b₂) (s₁ + 0) = op (fold op b₁ s₁) (fold op b₂ 0)

Tactic:
rw [Multiset.add_zero, fold_zero, ← fold_cons'_right, ← fold_cons_right op]

Premises used: Multiset.add_zero, Multiset.fold_zero, Multiset.fold_cons'_right, Multiset.fold_cons_right
-- Module: Mathlib.Data.Multiset.Fold
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))
rw₆ rw₇ : op (fold op b₁ s₁) (op 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))

Tactic:
rw [fold_cons_left, add_cons, fold_cons_left, h, ← ha.assoc, hc.comm a,
      ha.assoc]

Premises used: Multiset.fold_cons_left, Std.Associative.assoc, Multiset.add_cons, Std.Commutative.comm
-- Module: Mathlib.Data.Multiset.Fold
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b a : α
⊢ fold op b {a} = op a b

Tactic:
foldr_singleton _ _ _

Premises used: Multiset.foldr_singleton, Multiset.fold
-- Module: Mathlib.Data.Multiset.Fold
Goal:
α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
f g : β → α
u₁ u₂ : α
s : Multiset β
⊢ fold op (op u₁ u₂) (map (fun (x : β) ↦ op (f x) (g x)) 0) = op (fold op u₁ (map f 0)) (fold op u₂ (map g 0))

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Fold
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))
rw₁₂ 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)))
⊢ 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)))

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]

Premises used: Multiset.fold_cons_left, Multiset.map_cons, Std.Associative.assoc, Std.Commutative.comm, Multiset.fold_cons_right
-- Module: Mathlib.Data.Multiset.Fold
Goal:
α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
op' : β → β → β
inst : Std.Commutative op'
inst_1 : Std.Associative op'
m : α → β
hm : ∀ (x y : α), m (op x y) = op' (m x) (m y)
b : α
s : Multiset α
⊢ fold op' (m b) (map m 0) = m (fold op b 0)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Fold
Goal:
α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
op' : β → β → β
inst : Std.Commutative op'
inst_1 : Std.Associative op'
m : α → β
hm : ∀ (x y : α), m (op x y) = op' (m x) (m y)
b : α
s : Multiset α
⊢ ∀ (a : α) (s : Multiset α),
    fold op' (m b) (map m s) = m (fold op b s) → fold op' (m b) (map m (a ::ₘ s)) = m (fold op b (a ::ₘ s))

Tactic:
simp +contextual [hm]
-- Module: Mathlib.Data.Multiset.Fold
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₂)
rw₂ rw₃ : op (fold op b₁ s₁) (fold op b₂ 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₂)

Tactic:
rw [← fold_add op, union_add_inter, fold_add op]

Premises used: Multiset.fold_add, Multiset.union_add_inter
-- Module: Mathlib.Data.Multiset.Fold
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst : DecidableEq α
hi : Std.IdempotentOp op
s : Multiset α
b : α
⊢ fold op b (dedup 0) = fold op b 0

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Fold
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)
neg : ∀ (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)

Tactic:
by_cases h : a ∈ s
-- Module: Mathlib.Data.Multiset.Fold
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)

Tactic:
simp [IH, h]
-- Module: Mathlib.Data.Multiset.Fold
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 s = op a (fold op b s)
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)

Tactic:
simp only [h, dedup_cons_of_mem, IH, fold_cons_left]

Premises used: Multiset.fold_cons_left, Multiset.dedup_cons_of_mem
-- Module: Mathlib.Data.Multiset.Fold
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))
pos₃ pos₄ : op a (fold op b (s.erase a)) = op a (fold op b (s.erase a))
⊢ fold op b s = op a (fold op b s)

Tactic:
rw [← cons_erase h, fold_cons_left, ← ha.assoc, hi.idempotent]

Premises used: Multiset.fold_cons_left, Std.Associative.assoc, Std.IdempotentOp.idempotent, Multiset.cons_erase
-- Module: Mathlib.Data.Multiset.Functor
Goal:
α' β' : Type u_1
s : Multiset α'
f : α' → β'
⊢ f <$> s = map f s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Multiset.Functor
Goal:
⊢ ∀ {α : Type u_1} (x : Multiset α), id <$> x = x

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Functor
Goal:
⊢ ∀ {α β γ : Type u_1} (g : α → β) (h : β → γ) (x : Multiset α), (h ∘ g) <$> x = h <$> g <$> x

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Functor
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : CommApplicative F
α' β' : Type u
f : α' → F β'
refine :
  ∀ (a b : List α'),
    a ≈ b → (Functor.map ofList ∘ Traversable.traverse f) a = (Functor.map ofList ∘ Traversable.traverse f) b
⊢ Multiset α' → F (Multiset β')

Tactic:
refine Quotient.lift (Functor.map ofList ∘ Traversable.traverse f) ?_

Premises used: Function.comp, Multiset.ofList, Traversable.traverse, Quotient.lift, Functor.map
-- Module: Mathlib.Data.Multiset.Functor
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
p : a ≈ b
unfold : ofList <$> Traversable.traverse f a = ofList <$> Traversable.traverse f b
⊢ (Functor.map ofList ∘ Traversable.traverse f) a = (Functor.map ofList ∘ Traversable.traverse f) b

Tactic:
unfold Function.comp

Premises used: Function.comp
-- Module: Mathlib.Data.Multiset.Functor
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
⊢ ofList <$> Traversable.traverse f [] = ofList <$> Traversable.traverse f []

Tactic:
rfl