Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Simon Hudon, Yury Kudryashov

! This file was ported from Lean 3 source module algebra.free_monoid.basic
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.List.BigOperators.Basic

/-!
# Free monoid over a given alphabet

## Main definitions

* `FreeMonoid α`: free monoid over alphabet `α`; defined as a synonym for `List α`
with multiplication given by `(++)`.
* `FreeMonoid.of`: embedding `α → FreeMonoid α` sending each element `x` to `[x]`;
* `FreeMonoid.lift`: natural equivalence between `α → M` and `FreeMonoid α →* M`
* `FreeMonoid.map`: embedding of `α → β` into `FreeMonoid α →* FreeMonoid β` given by `List.map`.
-/

variable {α: Type ?u.16741α : Type _: Type (?u.5665+1)Type _} {β: Type ?u.5β : Type _: Type (?u.12678+1)Type _} {γ: Type ?u.1625γ : Type _: Type (?u.29+1)Type _} {M: Type ?u.11M : Type _: Type (?u.11+1)Type _} [Monoid: Type ?u.14 → Type ?u.14Monoid M: Type ?u.11M] {N: Type ?u.38N : Type _: Type (?u.55103+1)Type _} [Monoid: Type ?u.16759 → Type ?u.16759Monoid N: Type ?u.43329N]

/-- Free monoid over a given alphabet. -/
def FreeMonoid: (α : ?m.44) → ?m.48 αFreeMonoid (α: ?m.44α) := List: Type ?u.51 → Type ?u.51List α: ?m.44α
#align free_monoid FreeMonoid: Type u_1 → Type u_1FreeMonoid

namespace FreeMonoid

-- Porting note: TODO. Check this is still needed
instance: {α : Type u_1} → [inst : DecidableEq α] → DecidableEq (FreeMonoid α)instance [DecidableEq: Sort ?u.84 → Sort (max1?u.84)DecidableEq α: Type ?u.63α] : DecidableEq: Sort ?u.93 → Sort (max1?u.93)DecidableEq (FreeMonoid: Type ?u.94 → Type ?u.94FreeMonoid α: Type ?u.63α) := instDecidableEqList: {α : Type ?u.104} → [inst : DecidableEq α] → DecidableEq (List α)instDecidableEqList

/-- The identity equivalence between `FreeMonoid α` and `List α`. -/
def toList: FreeMonoid α ≃ List αtoList : FreeMonoid: Type ?u.405 → Type ?u.405FreeMonoid α: Type ?u.382α ≃ List: Type ?u.406 → Type ?u.406List α: Type ?u.382α := Equiv.refl: (α : Sort ?u.408) → α ≃ αEquiv.refl _: Sort ?u.408_
#align free_monoid.to_list FreeMonoid.toList: {α : Type u_1} → FreeMonoid α ≃ List αFreeMonoid.toList

/-- The identity equivalence between `List α` and `FreeMonoid α`. -/
def ofList: {α : Type u_1} → List α ≃ FreeMonoid αofList : List: Type ?u.503 → Type ?u.503List α: Type ?u.480α ≃ FreeMonoid: Type ?u.504 → Type ?u.504FreeMonoid α: Type ?u.480α := Equiv.refl: (α : Sort ?u.506) → α ≃ αEquiv.refl _: Sort ?u.506_
#align free_monoid.of_list FreeMonoid.ofList: {α : Type u_1} → List α ≃ FreeMonoid αFreeMonoid.ofList

theorem toList_symm: ∀ {α : Type u_1}, toList.symm = ofListtoList_symm : (@toList: {α : Type ?u.597} → FreeMonoid α ≃ List αtoList α: Type ?u.575α).symm: {α : Sort ?u.599} → {β : Sort ?u.598} → α ≃ β → β ≃ αsymm = ofList: {α : Type ?u.607} → List α ≃ FreeMonoid αofList := rfl: ∀ {α : Sort ?u.646} {a : α}, a = arfl
#align free_monoid.to_list_symm FreeMonoid.toList_symm: ∀ {α : Type u_1}, toList.symm = ofListFreeMonoid.toList_symm

theorem ofList_symm: ∀ {α : Type u_1}, ofList.symm = toListofList_symm : (@ofList: {α : Type ?u.711} → List α ≃ FreeMonoid αofList α: Type ?u.689α).symm: {α : Sort ?u.713} → {β : Sort ?u.712} → α ≃ β → β ≃ αsymm = toList: {α : Type ?u.721} → FreeMonoid α ≃ List αtoList := rfl: ∀ {α : Sort ?u.760} {a : α}, a = arfl
#align free_monoid.of_list_symm FreeMonoid.ofList_symm: ∀ {α : Type u_1}, ofList.symm = toListFreeMonoid.ofList_symm

theorem toList_ofList: ∀ (l : List α), ↑toList (↑ofList l) = ltoList_ofList (l: List αl : List: Type ?u.824 → Type ?u.824List α: Type ?u.803α) : toList: {α : Type ?u.828} → FreeMonoid α ≃ List αtoList (ofList: {α : Type ?u.906} → List α ≃ FreeMonoid αofList l: List αl) = l: List αl := rfl: ∀ {α : Sort ?u.992} {a : α}, a = arfl
#align free_monoid.to_list_of_list FreeMonoid.toList_ofList: ∀ {α : Type u_1} (l : List α), ↑toList (↑ofList l) = lFreeMonoid.toList_ofList

theorem ofList_toList: ∀ (xs : FreeMonoid α), ↑ofList (↑toList xs) = xsofList_toList (xs: FreeMonoid αxs : FreeMonoid: Type ?u.1079 → Type ?u.1079FreeMonoid α: Type ?u.1058α) : ofList: {α : Type ?u.1083} → List α ≃ FreeMonoid αofList (toList: {α : Type ?u.1161} → FreeMonoid α ≃ List αtoList xs: FreeMonoid αxs) = xs: FreeMonoid αxs := rfl: ∀ {α : Sort ?u.1247} {a : α}, a = arfl
#align free_monoid.of_list_to_list FreeMonoid.ofList_toList: ∀ {α : Type u_1} (xs : FreeMonoid α), ↑ofList (↑toList xs) = xsFreeMonoid.ofList_toList

theorem toList_comp_ofList: ↑toList ∘ ↑ofList = idtoList_comp_ofList : @toList: {α : Type ?u.1341} → FreeMonoid α ≃ List αtoList α: Type ?u.1313α ∘ ofList: {α : Type ?u.1422} → List α ≃ FreeMonoid αofList = id: {α : Sort ?u.1504} → α → αid := rfl: ∀ {α : Sort ?u.1545} {a : α}, a = arfl
#align free_monoid.to_list_comp_of_list FreeMonoid.toList_comp_ofList: ∀ {α : Type u_1}, ↑toList ∘ ↑ofList = idFreeMonoid.toList_comp_ofList

theorem ofList_comp_toList: ↑ofList ∘ ↑toList = idofList_comp_toList : @ofList: {α : Type ?u.1647} → List α ≃ FreeMonoid αofList α: Type ?u.1619α ∘ toList: {α : Type ?u.1728} → FreeMonoid α ≃ List αtoList = id: {α : Sort ?u.1810} → α → αid := rfl: ∀ {α : Sort ?u.1852} {a : α}, a = arfl
#align free_monoid.of_list_comp_to_list FreeMonoid.ofList_comp_toList: ∀ {α : Type u_1}, ↑ofList ∘ ↑toList = idFreeMonoid.ofList_comp_toList

instance: {α : Type u_1} → CancelMonoid (FreeMonoid α)instance : CancelMonoid: Type ?u.1947 → Type ?u.1947CancelMonoid (FreeMonoid: Type ?u.1948 → Type ?u.1948FreeMonoid α: Type ?u.1926α)
where
one := ofList: {α : Type ?u.3073} → List α ≃ FreeMonoid αofList []: List ?m.3152[]
mul x: ?m.1966x y: ?m.1969y := ofList: {α : Type ?u.1971} → List α ≃ FreeMonoid αofList (toList: {α : Type ?u.2052} → FreeMonoid α ≃ List αtoList x: ?m.1966x ++ toList: {α : Type ?u.2132} → FreeMonoid α ≃ List αtoList y: ?m.1969y)
mul_one := List.append_nil: ∀ {α : Type ?u.3192} (as : List α), as ++ [] = asList.append_nil
one_mul := List.nil_append: ∀ {α : Type ?u.3155} (as : List α), [] ++ as = asList.nil_append
mul_assoc := List.append_assoc: ∀ {α : Type ?u.2277} (as bs cs : List α), as ++ bs ++ cs = as ++ (bs ++ cs)List.append_assoc
mul_left_cancel _: ?m.2807_ _: ?m.2810_ _: ?m.2813_ := List.append_left_cancel: ∀ {α : Type ?u.2815} {s t₁ t₂ : List α}, s ++ t₁ = s ++ t₂ → t₁ = t₂List.append_left_cancel
mul_right_cancel _: ?m.3265_ _: ?m.3268_ _: ?m.3271_ := List.append_right_cancel: ∀ {α : Type ?u.3273} {s₁ s₂ t : List α}, s₁ ++ t = s₂ ++ t → s₁ = s₂List.append_right_cancel

instance: {α : Type u_1} → Inhabited (FreeMonoid α)instance : Inhabited: Sort ?u.4709 → Sort (max1?u.4709)Inhabited (FreeMonoid: Type ?u.4710 → Type ?u.4710FreeMonoid α: Type ?u.4688α) := ⟨1: ?m.47181⟩

theorem toList_one: ↑toList 1 = []toList_one : toList: {α : Type ?u.5213} → FreeMonoid α ≃ List αtoList (1: ?m.52941 : FreeMonoid: Type ?u.5292 → Type ?u.5292FreeMonoid α: Type ?u.5191α) = []: List ?m.5575[] := rfl: ∀ {α : Sort ?u.5610} {a : α}, a = arfl
#align free_monoid.to_list_one FreeMonoid.toList_one: ∀ {α : Type u_1}, ↑toList 1 = []FreeMonoid.toList_one

theorem ofList_nil: ↑ofList [] = 1ofList_nil : ofList: {α : Type ?u.5687} → List α ≃ FreeMonoid αofList ([]: List ?m.5768[] : List: Type ?u.5766 → Type ?u.5766List α: Type ?u.5665α) = 1: ?m.57711 := rfl: ∀ {α : Sort ?u.6139} {a : α}, a = arfl
#align free_monoid.of_list_nil FreeMonoid.ofList_nil: ∀ {α : Type u_1}, ↑ofList [] = 1FreeMonoid.ofList_nil

theorem toList_mul: ∀ (xs ys : FreeMonoid α), ↑toList (xs * ys) = ↑toList xs ++ ↑toList ystoList_mul (xs: FreeMonoid αxs ys: FreeMonoid αys : FreeMonoid: Type ?u.6211 → Type ?u.6211FreeMonoid α: Type ?u.6190α) : toList: {α : Type ?u.6218} → FreeMonoid α ≃ List αtoList (xs: FreeMonoid αxs * ys: FreeMonoid αys) = toList: {α : Type ?u.6724} → FreeMonoid α ≃ List αtoList xs: FreeMonoid αxs ++ toList: {α : Type ?u.6803} → FreeMonoid α ≃ List αtoList ys: FreeMonoid αys := rfl: ∀ {α : Sort ?u.6941} {a : α}, a = arfl
#align free_monoid.to_list_mul FreeMonoid.toList_mul: ∀ {α : Type u_1} (xs ys : FreeMonoid α), ↑toList (xs * ys) = ↑toList xs ++ ↑toList ysFreeMonoid.toList_mul

@[to_additive: ∀ {α : Type u_1} (xs ys : List α),
theorem ofList_append: ∀ {α : Type u_1} (xs ys : List α), ↑ofList (xs ++ ys) = ↑ofList xs * ↑ofList ysofList_append (xs: List αxs ys: List αys : List: Type ?u.7082 → Type ?u.7082List α: Type ?u.7058α) : ofList: {α : Type ?u.7086} → List α ≃ FreeMonoid αofList (xs: List αxs ++ ys: List αys) = ofList: {α : Type ?u.7220} → List α ≃ FreeMonoid αofList xs: List αxs * ofList: {α : Type ?u.7299} → List α ≃ FreeMonoid αofList ys: List αys := rfl: ∀ {α : Sort ?u.8291} {a : α}, a = arfl
#align free_monoid.of_list_append FreeMonoid.ofList_append: ∀ {α : Type u_1} (xs ys : List α), ↑ofList (xs ++ ys) = ↑ofList xs * ↑ofList ysFreeMonoid.ofList_append
#align free_add_monoid.of_list_append FreeAddMonoid.ofList_append: ∀ {α : Type u_1} (xs ys : List α),

theorem toList_prod: ∀ {α : Type u_1} (xs : List (FreeMonoid α)), ↑toList (List.prod xs) = List.join (List.map (↑toList) xs)toList_prod (xs: List (FreeMonoid α)xs : List: Type ?u.8396 → Type ?u.8396List (FreeMonoid: Type ?u.8397 → Type ?u.8397FreeMonoid α: Type ?u.8375α)) : toList: {α : Type ?u.8401} → FreeMonoid α ≃ List αtoList xs: List (FreeMonoid α)xs.prod: {α : Type ?u.8479} → [inst : Mul α] → [inst : One α] → List α → αprod = (xs: List (FreeMonoid α)xs.map: {α : Type ?u.9084} → {β : Type ?u.9083} → (α → β) → List α → List βmap toList: {α : Type ?u.9091} → FreeMonoid α ≃ List αtoList).join: {α : Type ?u.9171} → List (List α) → List αjoin := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.8378γ: Type ?u.8381M: Type ?u.8384inst✝¹: Monoid MN: Type ?u.8390inst✝: Monoid Nxs: List (FreeMonoid α)↑toList (List.prod xs) = List.join (List.map (↑toList) xs)induction xs: List (FreeMonoid α)xsα: Type u_1β: Type ?u.8378γ: Type ?u.8381M: Type ?u.8384inst✝¹: Monoid MN: Type ?u.8390inst✝: Monoid Nnil↑toList (List.prod []) = List.join (List.map ↑toList [])α: Type u_1β: Type ?u.8378γ: Type ?u.8381M: Type ?u.8384inst✝¹: Monoid MN: Type ?u.8390inst✝: Monoid Nhead✝: FreeMonoid αtail✝: List (FreeMonoid α)tail_ih✝: ↑toList (List.prod tail✝) = List.join (List.map (↑toList) tail✝)cons↑toList (List.prod (head✝ :: tail✝)) = List.join (List.map (↑toList) (head✝ :: tail✝)) α: Type u_1β: Type ?u.8378γ: Type ?u.8381M: Type ?u.8384inst✝¹: Monoid MN: Type ?u.8390inst✝: Monoid Nxs: List (FreeMonoid α)↑toList (List.prod xs) = List.join (List.map (↑toList) xs)<;>α: Type u_1β: Type ?u.8378γ: Type ?u.8381M: Type ?u.8384inst✝¹: Monoid MN: Type ?u.8390inst✝: Monoid Nnil↑toList (List.prod []) = List.join (List.map ↑toList [])α: Type u_1β: Type ?u.8378γ: Type ?u.8381M: Type ?u.8384inst✝¹: Monoid MN: Type ?u.8390inst✝: Monoid Nhead✝: FreeMonoid αtail✝: List (FreeMonoid α)tail_ih✝: ↑toList (List.prod tail✝) = List.join (List.map (↑toList) tail✝)cons↑toList (List.prod (head✝ :: tail✝)) = List.join (List.map (↑toList) (head✝ :: tail✝)) α: Type u_1β: Type ?u.8378γ: Type ?u.8381M: Type ?u.8384inst✝¹: Monoid MN: Type ?u.8390inst✝: Monoid Nxs: List (FreeMonoid α)↑toList (List.prod xs) = List.join (List.map (↑toList) xs)simp [*, List.join: {α : Type ?u.10257} → List (List α) → List αList.join]Goals accomplished! 🐙
#align free_monoid.to_list_prod FreeMonoid.toList_prod: ∀ {α : Type u_1} (xs : List (FreeMonoid α)), ↑toList (List.prod xs) = List.join (List.map (↑toList) xs)FreeMonoid.toList_prod

@[to_additive: ∀ {α : Type u_1} (xs : List (List α)),
theorem ofList_join: ∀ (xs : List (List α)), ↑ofList (List.join xs) = List.prod (List.map (↑ofList) xs)ofList_join (xs: List (List α)xs : List: Type ?u.10913 → Type ?u.10913List (List: Type ?u.10914 → Type ?u.10914List α: Type ?u.10892α)) : ofList: {α : Type ?u.10918} → List α ≃ FreeMonoid αofList xs: List (List α)xs.join: {α : Type ?u.10996} → List (List α) → List αjoin = (xs: List (List α)xs.map: {α : Type ?u.11003} → {β : Type ?u.11002} → (α → β) → List α → List βmap ofList: {α : Type ?u.11010} → List α ≃ FreeMonoid αofList).prod: {α : Type ?u.11090} → [inst : Mul α] → [inst : One α] → List α → αprod :=
toList: {α : Type ?u.11695} → FreeMonoid α ≃ List αtoList.injective: ∀ {α : Sort ?u.11698} {β : Sort ?u.11697} (e : α ≃ β), Function.Injective ↑einjective <| byGoals accomplished! 🐙 α: Type u_1β: Type ?u.10895γ: Type ?u.10898M: Type ?u.10901inst✝¹: Monoid MN: Type ?u.10907inst✝: Monoid Nxs: List (List α)↑toList (↑ofList (List.join xs)) = ↑toList (List.prod (List.map (↑ofList) xs))simpGoals accomplished! 🐙
#align free_monoid.of_list_join FreeMonoid.ofList_join: ∀ {α : Type u_1} (xs : List (List α)), ↑ofList (List.join xs) = List.prod (List.map (↑ofList) xs)FreeMonoid.ofList_join
#align free_add_monoid.of_list_join FreeAddMonoid.ofList_join: ∀ {α : Type u_1} (xs : List (List α)),

/-- Embeds an element of `α` into `FreeMonoid α` as a singleton list. -/
def of: {α : Type u_1} → α → FreeMonoid αof (x: αx : α: Type ?u.12090α) : FreeMonoid: Type ?u.12113 → Type ?u.12113FreeMonoid α: Type ?u.12090α := ofList: {α : Type ?u.12117} → List α ≃ FreeMonoid αofList [x: αx]
#align free_monoid.of FreeMonoid.of: {α : Type u_1} → α → FreeMonoid αFreeMonoid.of

theorem toList_of: ∀ (x : α), ↑toList (of x) = [x]toList_of (x: αx : α: Type ?u.12359α) : toList: {α : Type ?u.12383} → FreeMonoid α ≃ List αtoList (of: {α : Type ?u.12461} → α → FreeMonoid αof x: αx) = [x: αx] := rfl: ∀ {α : Sort ?u.12474} {a : α}, a = arfl
#align free_monoid.to_list_of FreeMonoid.toList_of: ∀ {α : Type u_1} (x : α), ↑toList (of x) = [x]FreeMonoid.toList_of

theorem ofList_singleton: ∀ {α : Type u_1} (x : α), ↑ofList [x] = of xofList_singleton (x: αx : α: Type ?u.12536α) : ofList: {α : Type ?u.12560} → List α ≃ FreeMonoid αofList [x: αx] = of: {α : Type ?u.12644} → α → FreeMonoid αof x: αx := rfl: ∀ {α : Sort ?u.12651} {a : α}, a = arfl
#align free_monoid.of_list_singleton FreeMonoid.ofList_singleton: ∀ {α : Type u_1} (x : α), ↑ofList [x] = of xFreeMonoid.ofList_singleton

theorem ofList_cons: ∀ (x : α) (xs : List α), ↑ofList (x :: xs) = of x * ↑ofList xsofList_cons (x: αx : α: Type ?u.12675α) (xs: List αxs : List: Type ?u.12698 → Type ?u.12698List α: Type ?u.12675α) : ofList: {α : Type ?u.12702} → List α ≃ FreeMonoid αofList (x: αx :: xs: List αxs) = of: {α : Type ?u.12787} → α → FreeMonoid αof x: αx * ofList: {α : Type ?u.12789} → List α ≃ FreeMonoid αofList xs: List αxs := rfl: ∀ {α : Sort ?u.13676} {a : α}, a = arfl
#align free_monoid.of_list_cons FreeMonoid.ofList_cons: ∀ {α : Type u_1} (x : α) (xs : List α), ↑ofList (x :: xs) = of x * ↑ofList xsFreeMonoid.ofList_cons

@[to_additive: ∀ {α : Type u_1} (x : α) (xs : FreeAddMonoid α),
theorem toList_of_mul: ∀ (x : α) (xs : FreeMonoid α), ↑toList (of x * xs) = x :: ↑toList xstoList_of_mul (x: αx : α: Type ?u.13768α) (xs: FreeMonoid αxs : FreeMonoid: Type ?u.13791 → Type ?u.13791FreeMonoid α: Type ?u.13768α) : toList: {α : Type ?u.13795} → FreeMonoid α ≃ List αtoList (of: {α : Type ?u.13876} → α → FreeMonoid αof x: αx * xs: FreeMonoid αxs) = x: αx :: toList: {α : Type ?u.14302} → FreeMonoid α ≃ List αtoList xs: FreeMonoid αxs := rfl: ∀ {α : Sort ?u.14387} {a : α}, a = arfl
#align free_monoid.to_list_of_mul FreeMonoid.toList_of_mul: ∀ {α : Type u_1} (x : α) (xs : FreeMonoid α), ↑toList (of x * xs) = x :: ↑toList xsFreeMonoid.toList_of_mul

theorem of_injective: ∀ {α : Type u_1}, Function.Injective ofof_injective : Function.Injective: {α : Sort ?u.14455} → {β : Sort ?u.14454} → (α → β) → PropFunction.Injective (@of: {α : Type ?u.14458} → α → FreeMonoid αof α: Type ?u.14433α) := List.singleton_injective: ∀ {α : Type ?u.14463}, Function.Injective fun a => [a]List.singleton_injective
#align free_monoid.of_injective FreeMonoid.of_injective: ∀ {α : Type u_1}, Function.Injective ofFreeMonoid.of_injective

/-- Recursor for `FreeMonoid` using `1` and `FreeMonoid.of x * xs` instead of `[]` and `x :: xs`. -/
@[to_additive: {α : Type u_1} →
{C : FreeAddMonoid α → Sort u_2} →
(xs : FreeAddMonoid α) → C 0 → ((x : α) → (xs : FreeAddMonoid α) → C xs → C (FreeAddMonoid.of x + xs)) → C xsto_additive (attr := elab_as_elim) "Recursor for `FreeAddMonoid` using `0` and
-- Porting note: change from `List.recOn` to `List.rec` since only the latter is computable
def recOn: {C : FreeMonoid α → Sort ?u.14504} →
(xs : FreeMonoid α) → C 1 → ((x : α) → (xs : FreeMonoid α) → C xs → C (of x * xs)) → C xsrecOn {C: FreeMonoid α → Sort ?u.14504C : FreeMonoid: Type ?u.14502 → Type ?u.14502FreeMonoid α: Type ?u.14480α → Sort _: Type ?u.14504SortSort _: Type ?u.14504 _} (xs: FreeMonoid αxs : FreeMonoid: Type ?u.14507 → Type ?u.14507FreeMonoid α: Type ?u.14480α) (h0: C 1h0 : C: FreeMonoid α → Sort ?u.14504C 1: ?m.145111)
(ih: (x : ?m.14793) → (xs : FreeMonoid α) → C xs → C (of x * xs)ih : ∀ x: ?m.14793x xs: ?m.14796xs, C: FreeMonoid α → Sort ?u.14504C xs: ?m.14796xs → C: FreeMonoid α → Sort ?u.14504C (of: {α : Type ?u.14804} → α → FreeMonoid αof x: ?m.14793x * xs: ?m.14796xs)) : C: FreeMonoid α → Sort ?u.14504C xs: FreeMonoid αxs := List.rec: {α : Type ?u.15210} →
{motive : List α → Sort ?u.15211} →
motive [] → ((head : α) → (tail : List α) → motive tail → motive (head :: tail)) → (t : List α) → motive tList.rec h0: C 1h0 ih: (x : α) → (xs : FreeMonoid α) → C xs → C (of x * xs)ih xs: FreeMonoid αxs
#align free_monoid.rec_on FreeMonoid.recOn: {α : Type u_1} →
{C : FreeMonoid α → Sort u_2} →
(xs : FreeMonoid α) → C 1 → ((x : α) → (xs : FreeMonoid α) → C xs → C (of x * xs)) → C xsFreeMonoid.recOn
{C : FreeAddMonoid α → Sort u_2} →
(xs : FreeAddMonoid α) → C 0 → ((x : α) → (xs : FreeAddMonoid α) → C xs → C (FreeAddMonoid.of x + xs)) → C xsFreeAddMonoid.recOn

@[to_additive: ∀ {α : Type u_1} {C : FreeAddMonoid α → Sort u_2} (h0 : C 0)
(ih : (x : α) → (xs : FreeAddMonoid α) → C xs → C (FreeAddMonoid.of x + xs)), FreeAddMonoid.recOn 0 h0 ih = h0to_additive (attr := simp)]
theorem recOn_one: ∀ {C : FreeMonoid α → Sort u_2} (h0 : C 1) (ih : (x : α) → (xs : FreeMonoid α) → C xs → C (of x * xs)),
recOn 1 h0 ih = h0recOn_one {C: FreeMonoid α → Sort u_2C : FreeMonoid: Type ?u.15615 → Type ?u.15615FreeMonoid α: Type ?u.15593α → Sort _: Type ?u.15617SortSort _: Type ?u.15617 _} (h0: C 1h0 : C: FreeMonoid α → Sort ?u.15617C 1: ?m.156211) (ih: (x : α) → (xs : FreeMonoid α) → C xs → C (of x * xs)ih : ∀ x: ?m.15903x xs: ?m.15906xs, C: FreeMonoid α → Sort ?u.15617C xs: ?m.15906xs → C: FreeMonoid α → Sort ?u.15617C (of: {α : Type ?u.15914} → α → FreeMonoid αof x: ?m.15903x * xs: ?m.15906xs)) :
@recOn: {α : Type ?u.15960} →
{C : FreeMonoid α → Sort ?u.15959} →
(xs : FreeMonoid α) → C 1 → ((x : α) → (xs : FreeMonoid α) → C xs → C (of x * xs)) → C xsrecOn α: Type ?u.15593α C: FreeMonoid α → Sort ?u.15617C 1: ?m.159651 h0: C 1h0 ih: (x : ?m.15903) → (xs : FreeMonoid α) → C xs → C (of x * xs)ih = h0: C 1h0 := rfl: ∀ {α : Sort ?u.16656} {a : α}, a = arfl
#align free_monoid.rec_on_one FreeMonoid.recOn_one: ∀ {α : Type u_1} {C : FreeMonoid α → Sort u_2} (h0 : C 1) (ih : (x : α) → (xs : FreeMonoid α) → C xs → C (of x * xs)),
recOn 1 h0 ih = h0FreeMonoid.recOn_one
#align free_add_monoid.rec_on_zero FreeAddMonoid.recOn_zero: ∀ {α : Type u_1} {C : FreeAddMonoid α → Sort u_2} (h0 : C 0)
(ih : (x : α) → (xs : FreeAddMonoid α) → C xs → C (FreeAddMonoid.of x + xs)), FreeAddMonoid.recOn 0 h0 ih = h0FreeAddMonoid.recOn_zero

@[to_additive: ∀ {α : Type u_1} {C : FreeAddMonoid α → Sort u_2} (x : α) (xs : FreeAddMonoid α) (h0 : C 0)
(ih : (x : α) → (xs : FreeAddMonoid α) → C xs → C (FreeAddMonoid.of x + xs)),
theorem recOn_of_mul: ∀ {C : FreeMonoid α → Sort u_2} (x : α) (xs : FreeMonoid α) (h0 : C 1)
(ih : (x : α) → (xs : FreeMonoid α) → C xs → C (of x * xs)), recOn (of x * xs) h0 ih = ih x xs (recOn xs h0 ih)recOn_of_mul {C: FreeMonoid α → Sort u_2C : FreeMonoid: Type ?u.16763 → Type ?u.16763FreeMonoid α: Type ?u.16741α → Sort _: Type ?u.16765SortSort _: Type ?u.16765 _} (x: αx : α: Type ?u.16741α) (xs: FreeMonoid αxs : FreeMonoid: Type ?u.16770 → Type ?u.16770FreeMonoid α: Type ?u.16741α) (h0: C 1h0 : C: FreeMonoid α → Sort ?u.16765C 1: ?m.167741)
(ih: (x : ?m.17056) → (xs : FreeMonoid α) → C xs → C (of x * xs)ih : ∀ x: ?m.17056x xs: ?m.17059xs, C: FreeMonoid α → Sort ?u.16765C xs: ?m.17059xs → C: FreeMonoid α → Sort ?u.16765C (of: {α : Type ?u.17067} → α → FreeMonoid αof x: ?m.17056x * xs: ?m.17059xs)) : @recOn: {α : Type ?u.17113} →
{C : FreeMonoid α → Sort ?u.17112} →
(xs : FreeMonoid α) → C 1 → ((x : α) → (xs : FreeMonoid α) → C xs → C (of x * xs)) → C xsrecOn α: Type ?u.16741α C: FreeMonoid α → Sort ?u.16765C (of: {α : Type ?u.17120} → α → FreeMonoid αof x: αx * xs: FreeMonoid αxs) h0: C 1h0 ih: (x : ?m.17056) → (xs : FreeMonoid α) → C xs → C (of x * xs)ih = ih: (x : ?m.17056) → (xs : FreeMonoid α) → C xs → C (of x * xs)ih x: αx xs: FreeMonoid αxs (recOn: {α : Type ?u.18114} →
{C : FreeMonoid α → Sort ?u.18113} →
(xs : FreeMonoid α) → C 1 → ((x : α) → (xs : FreeMonoid α) → C xs → C (of x * xs)) → C xsrecOn xs: FreeMonoid αxs h0: C 1h0 ih: (x : ?m.17056) → (xs : FreeMonoid α) → C xs → C (of x * xs)ih) :=
rfl: ∀ {α : Sort ?u.18157} {a : α}, a = arfl
#align free_monoid.rec_on_of_mul FreeMonoid.recOn_of_mul: ∀ {α : Type u_1} {C : FreeMonoid α → Sort u_2} (x : α) (xs : FreeMonoid α) (h0 : C 1)
(ih : (x : α) → (xs : FreeMonoid α) → C xs → C (of x * xs)), recOn (of x * xs) h0 ih = ih x xs (recOn xs h0 ih)FreeMonoid.recOn_of_mul
(ih : (x : α) → (xs : FreeAddMonoid α) → C xs → C (FreeAddMonoid.of x + xs)),

/-- A version of `List.cases_on` for `FreeMonoid` using `1` and `FreeMonoid.of x * xs` instead of
`[]` and `x :: xs`. -/
@[to_additive: {α : Type u_1} →
{C : FreeAddMonoid α → Sort u_2} →
(xs : FreeAddMonoid α) → C 0 → ((x : α) → (xs : FreeAddMonoid α) → C (FreeAddMonoid.of x + xs)) → C xsto_additive (attr := elab_as_elim) "A version of `List.casesOn` for `FreeAddMonoid` using `0` and
def casesOn: {α : Type u_1} →
{C : FreeMonoid α → Sort u_2} → (xs : FreeMonoid α) → C 1 → ((x : α) → (xs : FreeMonoid α) → C (of x * xs)) → C xscasesOn {C: FreeMonoid α → Sort ?u.18335C : FreeMonoid: Type ?u.18333 → Type ?u.18333FreeMonoid α: Type ?u.18311α → Sort _: Type ?u.18335SortSort _: Type ?u.18335 _} (xs: FreeMonoid αxs : FreeMonoid: Type ?u.18338 → Type ?u.18338FreeMonoid α: Type ?u.18311α) (h0: C 1h0 : C: FreeMonoid α → Sort ?u.18335C 1: ?m.183421)
(ih: (x : α) → (xs : FreeMonoid α) → C (of x * xs)ih : ∀ x: ?m.18624x xs: ?m.18627xs, C: FreeMonoid α → Sort ?u.18335C (of: {α : Type ?u.18633} → α → FreeMonoid αof x: ?m.18624x * xs: ?m.18627xs)) : C: FreeMonoid α → Sort ?u.18335C xs: FreeMonoid αxs := List.casesOn: {α : Type ?u.19043} →
{motive : List α → Sort ?u.19044} →
(t : List α) → motive [] → ((head : α) → (tail : List α) → motive (head :: tail)) → motive tList.casesOn xs: FreeMonoid αxs h0: C 1h0 ih: (x : α) → (xs : FreeMonoid α) → C (of x * xs)ih
#align free_monoid.cases_on FreeMonoid.casesOn: {α : Type u_1} →
{C : FreeMonoid α → Sort u_2} → (xs : FreeMonoid α) → C 1 → ((x : α) → (xs : FreeMonoid α) → C (of x * xs)) → C xsFreeMonoid.casesOn
{C : FreeAddMonoid α → Sort u_2} →
(xs : FreeAddMonoid α) → C 0 → ((x : α) → (xs : FreeAddMonoid α) → C (FreeAddMonoid.of x + xs)) → C xsFreeAddMonoid.casesOn

@[to_additive: ∀ {α : Type u_1} {C : FreeAddMonoid α → Sort u_2} (h0 : C 0)
(ih : (x : α) → (xs : FreeAddMonoid α) → C (FreeAddMonoid.of x + xs)), FreeAddMonoid.casesOn 0 h0 ih = h0to_additive (attr := simp)]
theorem casesOn_one: ∀ {C : FreeMonoid α → Sort u_2} (h0 : C 1) (ih : (x : α) → (xs : FreeMonoid α) → C (of x * xs)), casesOn 1 h0 ih = h0casesOn_one {C: FreeMonoid α → Sort u_2C : FreeMonoid: Type ?u.19408 → Type ?u.19408FreeMonoid α: Type ?u.19386α → Sort _: Type ?u.19410SortSort _: Type ?u.19410 _} (h0: C 1h0 : C: FreeMonoid α → Sort ?u.19410C 1: ?m.194141) (ih: (x : ?m.19696) → (xs : ?m.19747 x) → C (of x * xs)ih : ∀ x: ?m.19696x xs: ?m.19699xs, C: FreeMonoid α → Sort ?u.19410C (of: {α : Type ?u.19705} → α → FreeMonoid αof x: ?m.19696x * xs: ?m.19699xs)) :
@casesOn: {α : Type ?u.19753} →
{C : FreeMonoid α → Sort ?u.19752} →
(xs : FreeMonoid α) → C 1 → ((x : α) → (xs : FreeMonoid α) → C (of x * xs)) → C xscasesOn α: Type ?u.19386α C: FreeMonoid α → Sort ?u.19410C 1: ?m.197581 h0: C 1h0 ih: (x : ?m.19696) → (xs : ?m.19747 x) → C (of x * xs)ih = h0: C 1h0 := rfl: ∀ {α : Sort ?u.20448} {a : α}, a = arfl
#align free_monoid.cases_on_one FreeMonoid.casesOn_one: ∀ {α : Type u_1} {C : FreeMonoid α → Sort u_2} (h0 : C 1) (ih : (x : α) → (xs : FreeMonoid α) → C (of x * xs)),
casesOn 1 h0 ih = h0FreeMonoid.casesOn_one
#align free_add_monoid.cases_on_zero FreeAddMonoid.casesOn_zero: ∀ {α : Type u_1} {C : FreeAddMonoid α → Sort u_2} (h0 : C 0)

@[to_additive: ∀ {α : Type u_1} {C : FreeAddMonoid α → Sort u_2} (x : α) (xs : FreeAddMonoid α) (h0 : C 0)
(ih : (x : α) → (xs : FreeAddMonoid α) → C (FreeAddMonoid.of x + xs)),
theorem casesOn_of_mul: ∀ {α : Type u_1} {C : FreeMonoid α → Sort u_2} (x : α) (xs : FreeMonoid α) (h0 : C 1)
(ih : (x : α) → (xs : FreeMonoid α) → C (of x * xs)), casesOn (of x * xs) h0 ih = ih x xscasesOn_of_mul {C: FreeMonoid α → Sort u_2C : FreeMonoid: Type ?u.20549 → Type ?u.20549FreeMonoid α: Type ?u.20527α → Sort _: Type ?u.20551SortSort _: Type ?u.20551 _} (x: αx : α: Type ?u.20527α) (xs: FreeMonoid αxs : FreeMonoid: Type ?u.20556 → Type ?u.20556FreeMonoid α: Type ?u.20527α) (h0: C 1h0 : C: FreeMonoid α → Sort ?u.20551C 1: ?m.205601)
(ih: (x : ?m.20842) → (xs : ?m.20893 x) → C (of x * xs)ih : ∀ x: ?m.20842x xs: ?m.20845xs, C: FreeMonoid α → Sort ?u.20551C (of: {α : Type ?u.20851} → α → FreeMonoid αof x: ?m.20842x * xs: ?m.20845xs)) : @casesOn: {α : Type ?u.20899} →
{C : FreeMonoid α → Sort ?u.20898} →
(xs : FreeMonoid α) → C 1 → ((x : α) → (xs : FreeMonoid α) → C (of x * xs)) → C xscasesOn α: Type ?u.20527α C: FreeMonoid α → Sort ?u.20551C (of: {α : Type ?u.20906} → α → FreeMonoid αof x: αx * xs: FreeMonoid αxs) h0: C 1h0 ih: (x : ?m.20842) → (xs : ?m.20893 x) → C (of x * xs)ih = ih: (x : ?m.20842) → (xs : ?m.20893 x) → C (of x * xs)ih x: αx xs: FreeMonoid αxs := rfl: ∀ {α : Sort ?u.21905} {a : α}, a = arfl
#align free_monoid.cases_on_of_mul FreeMonoid.casesOn_of_mul: ∀ {α : Type u_1} {C : FreeMonoid α → Sort u_2} (x : α) (xs : FreeMonoid α) (h0 : C 1)
(ih : (x : α) → (xs : FreeMonoid α) → C (of x * xs)), casesOn (of x * xs) h0 ih = ih x xsFreeMonoid.casesOn_of_mul
(ih : (x : α) → (xs : FreeAddMonoid α) → C (FreeAddMonoid.of x + xs)),

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : AddMonoid M] ⦃f g : FreeAddMonoid α →+ M⦄,
(∀ (x : α), ↑f (FreeAddMonoid.of x) = ↑g (FreeAddMonoid.of x)) → f = gto_additive (attr := ext)]
theorem hom_eq: ∀ ⦃f g : FreeMonoid α →* M⦄, (∀ (x : α), ↑f (of x) = ↑g (of x)) → f = ghom_eq ⦃f: FreeMonoid α →* Mf g: FreeMonoid α →* Mg : FreeMonoid: Type ?u.22553 → Type ?u.22553FreeMonoid α: Type ?u.22028α →* M: Type ?u.22037M⦄ (h: ∀ (x : α), ↑f (of x) = ↑g (of x)h : ∀ x: ?m.22559x, f: FreeMonoid α →* Mf (of: {α : Type ?u.22861} → α → FreeMonoid αof x: ?m.22559x) = g: FreeMonoid α →* Mg (of: {α : Type ?u.23137} → α → FreeMonoid αof x: ?m.22559x)) : f: FreeMonoid α →* Mf = g: FreeMonoid α →* Mg :=
MonoidHom.ext: ∀ {M : Type ?u.23149} {N : Type ?u.23150} [inst : MulOneClass M] [inst_1 : MulOneClass N] ⦃f g : M →* N⦄,
(∀ (x : M), ↑f x = ↑g x) → f = gMonoidHom.ext fun l: ?m.23189l ↦ recOn: ∀ {α : Type ?u.23192} {C : FreeMonoid α → Sort ?u.23191} (xs : FreeMonoid α),
C 1 → (∀ (x : α) (xs : FreeMonoid α), C xs → C (of x * xs)) → C xsrecOn l: ?m.23189l (f: FreeMonoid α →* Mf.map_one: ∀ {M : Type ?u.23722} {N : Type ?u.23723} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N), ↑f 1 = 1map_one.trans: ∀ {α : Sort ?u.23732} {a b c : α}, a = b → b = c → a = ctrans g: FreeMonoid α →* Mg.map_one: ∀ {M : Type ?u.23745} {N : Type ?u.23746} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N), ↑f 1 = 1map_one.symm: ∀ {α : Sort ?u.23751} {a b : α}, a = b → b = asymm)
(fun x: ?m.23762x xs: ?m.23765xs hxs: ?m.23768hxs ↦ byGoals accomplished! 🐙  α: Type u_1β: Type ?u.22031γ: Type ?u.22034M: Type u_2inst✝¹: Monoid MN: Type ?u.22043inst✝: Monoid Nf, g: FreeMonoid α →* Mh: ∀ (x : α), ↑f (of x) = ↑g (of x)l: FreeMonoid αx: αxs: FreeMonoid αhxs: ↑f xs = ↑g xs↑f (of x * xs) = ↑g (of x * xs)simp only [h: ∀ (x : α), ↑f (of x) = ↑g (of x)h, hxs: ↑f xs = ↑g xshxs, MonoidHom.map_mul: ∀ {M : Type ?u.23810} {N : Type ?u.23811} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N) (a b : M),
↑f (a * b) = ↑f a * ↑f bMonoidHom.map_mul]Goals accomplished! 🐙)
#align free_monoid.hom_eq FreeMonoid.hom_eq: ∀ {α : Type u_1} {M : Type u_2} [inst : Monoid M] ⦃f g : FreeMonoid α →* M⦄, (∀ (x : α), ↑f (of x) = ↑g (of x)) → f = gFreeMonoid.hom_eq
#align free_add_monoid.hom_eq FreeAddMonoid.hom_eq: ∀ {α : Type u_1} {M : Type u_2} [inst : AddMonoid M] ⦃f g : FreeAddMonoid α →+ M⦄,

/-- A variant of `List.prod` that has `[x].prod = x` true definitionally.
The purpose is to make `FreeMonoid.lift_eval_of` true by `rfl`. -/
@[to_additive: {M : Type u_1} → [inst : AddMonoid M] → List M → Mto_additive "A variant of `List.sum` that has `[x].sum = x` true definitionally.
The purpose is to make `FreeAddMonoid.lift_eval_of` true by `rfl`."]
def prodAux: {M : Type ?u.24210} → [inst : Monoid M] → List M → MprodAux {M: Type ?u.24210M} [Monoid: Type ?u.24210 → Type ?u.24210Monoid M: ?m.24207M] : List: Type ?u.24214 → Type ?u.24214List M: ?m.24207M → M: ?m.24207M
| []  => 1: ?m.242331
| (x: Mx :: xs: List Mxs) => List.foldl: {α : Type ?u.24574} → {β : Type ?u.24573} → (α → β → α) → α → List β → αList.foldl (· * ·): M → M → M(· * ·) x: Mx xs: List Mxs
#align free_monoid.prod_aux FreeMonoid.prodAux: {M : Type u_1} → [inst : Monoid M] → List M → MFreeMonoid.prodAux

lemma prodAux_eq: ∀ {M : Type u_1} [inst : Monoid M] (l : List M), prodAux l = List.prod lprodAux_eq : ∀ l: List Ml : List: Type ?u.25679 → Type ?u.25679List M: Type ?u.25666M, FreeMonoid.prodAux: {M : Type ?u.25683} → [inst : Monoid M] → List M → MFreeMonoid.prodAux l: List Ml = l: List Ml.prod: {α : Type ?u.25696} → [inst : Mul α] → [inst : One α] → List α → αprod
| []  => rfl: ∀ {α : Sort ?u.26301} {a : α}, a = arfl
| (_ :: xs: List Mxs) => congr_arg: ∀ {α : Sort ?u.26348} {β : Sort ?u.26347} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂congr_arg (fun x: ?m.26354x => List.foldl: {α : Type ?u.26357} → {β : Type ?u.26356} → (α → β → α) → α → List β → αList.foldl (· * ·): M → M → M(· * ·) x: ?m.26354x xs: List Mxs) (one_mul: ∀ {M : Type ?u.26789} [inst : MulOneClass M] (a : M), 1 * a = aone_mul _: ?m.26790_).symm: ∀ {α : Sort ?u.26804} {a b : α}, a = b → b = asymm
#align free_monoid.prod_aux_eq FreeMonoid.prodAux_eq: ∀ {M : Type u_1} [inst : Monoid M] (l : List M), prodAux l = List.prod lFreeMonoid.prodAux_eq

/-- Equivalence between maps `α → M` and monoid homomorphisms `FreeMonoid α →* M`. -/
@[to_additive: {α : Type u_1} → {M : Type u_2} → [inst : AddMonoid M] → (α → M) ≃ (FreeAddMonoid α →+ M)to_additive "Equivalence between maps `α → A` and additive monoid homomorphisms
def lift: (α → M) ≃ (FreeMonoid α →* M)lift : (α: Type ?u.27396α → M: Type ?u.27405M) ≃ (FreeMonoid: Type ?u.27424 → Type ?u.27424FreeMonoid α: Type ?u.27396α →* M: Type ?u.27405M) where
toFun f: ?m.27931f :=
{ toFun := fun l: ?m.28443l ↦ prodAux: {M : Type ?u.28445} → [inst : Monoid M] → List M → MprodAux ((toList: {α : Type ?u.28462} → FreeMonoid α ≃ List αtoList l: ?m.28443l).map: {α : Type ?u.28543} → {β : Type ?u.28542} → (α → β) → List α → List βmap f: ?m.27931f)
map_one' := rfl: ∀ {α : Sort ?u.28563} {a : α}, a = arfl
map_mul' := fun _: ?m.28600_ _: ?m.28603_ ↦ byGoals accomplished! 🐙 α: Type ?u.27396β: Type ?u.27399γ: Type ?u.27402M: Type ?u.27405inst✝¹: Monoid MN: Type ?u.27411inst✝: Monoid Nf: α → Mx✝¹, x✝: FreeMonoid αOneHom.toFun
{ toFun := fun l => prodAux (List.map f (↑toList l)),
map_one' := (_ : (fun l => prodAux (List.map f (↑toList l))) 1 = (fun l => prodAux (List.map f (↑toList l))) 1) }
(x✝¹ * x✝) =   OneHom.toFun
{ toFun := fun l => prodAux (List.map f (↑toList l)),
map_one' :=
(_ : (fun l => prodAux (List.map f (↑toList l))) 1 = (fun l => prodAux (List.map f (↑toList l))) 1) }
x✝¹ *     OneHom.toFun
{ toFun := fun l => prodAux (List.map f (↑toList l)),
map_one' :=
(_ : (fun l => prodAux (List.map f (↑toList l))) 1 = (fun l => prodAux (List.map f (↑toList l))) 1) }
x✝simp only [prodAux_eq: ∀ {M : Type ?u.29565} [inst : Monoid M] (l : List M), prodAux l = List.prod lprodAux_eq, toList_mul: ∀ {α : Type ?u.29576} (xs ys : FreeMonoid α), ↑toList (xs * ys) = ↑toList xs ++ ↑toList ystoList_mul, List.map_append: ∀ {α : Type ?u.29603} {β : Type ?u.29604} (f : α → β) (l₁ l₂ : List α),
List.map f (l₁ ++ l₂) = List.map f l₁ ++ List.map f l₂List.map_append, List.prod_append: ∀ {M : Type ?u.29627} [inst : Monoid M] {l₁ l₂ : List M}, List.prod (l₁ ++ l₂) = List.prod l₁ * List.prod l₂List.prod_append]Goals accomplished! 🐙 }
invFun f: ?m.28615f x: ?m.28618x := f: ?m.28615f (of: {α : Type ?u.28914} → α → FreeMonoid αof x: ?m.28618x)
left_inv f: ?m.28921f := rfl: ∀ {α : Sort ?u.28924} {a : α}, a = arfl
right_inv f: ?m.29057f := hom_eq: ∀ {α : Type ?u.29059} {M : Type ?u.29060} [inst : Monoid M] ⦃f g : FreeMonoid α →* M⦄,
(∀ (x : α), ↑f (of x) = ↑g (of x)) → f = ghom_eq fun x: ?m.29089x ↦ rfl: ∀ {α : Sort ?u.29091} {a : α}, a = arfl
#align free_monoid.lift FreeMonoid.lift: {α : Type u_1} → {M : Type u_2} → [inst : Monoid M] → (α → M) ≃ (FreeMonoid α →* M)FreeMonoid.lift

-- porting note: new
@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : AddMonoid M] (f : α → M) (l : List α),
theorem lift_ofList: ∀ (f : α → M) (l : List α), ↑(↑lift f) (↑ofList l) = List.prod (List.map f l)lift_ofList (f: α → Mf : α: Type ?u.30499α → M: Type ?u.30508M) (l: List αl : List: Type ?u.30524 → Type ?u.30524List α: Type ?u.30499α) : lift: {α : Type ?u.30529} → {M : Type ?u.30528} → [inst : Monoid M] → (α → M) ≃ (FreeMonoid α →* M)lift f: α → Mf (ofList: {α : Type ?u.30978} → List α ≃ FreeMonoid αofList l: List αl) = (l: List αl.map: {α : Type ?u.31060} → {β : Type ?u.31059} → (α → β) → List α → List βmap f: α → Mf).prod: {α : Type ?u.31070} → [inst : Mul α] → [inst : One α] → List α → αprod :=
prodAux_eq: ∀ {M : Type ?u.31661} [inst : Monoid M] (l : List M), prodAux l = List.prod lprodAux_eq _: List ?m.31662_

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : AddMonoid M] (f : FreeAddMonoid α →+ M),
theorem lift_symm_apply: ∀ {α : Type u_1} {M : Type u_2} [inst : Monoid M] (f : FreeMonoid α →* M), ↑lift.symm f = ↑f ∘ oflift_symm_apply (f: FreeMonoid α →* Mf : FreeMonoid: Type ?u.31994 → Type ?u.31994FreeMonoid α: Type ?u.31971α →* M: Type ?u.31980M) : lift: {α : Type ?u.32496} → {M : Type ?u.32495} → [inst : Monoid M] → (α → M) ≃ (FreeMonoid α →* M)lift.symm: {α : Sort ?u.32515} → {β : Sort ?u.32514} → α ≃ β → β ≃ αsymm f: FreeMonoid α →* Mf = f: FreeMonoid α →* Mf ∘ of: {α : Type ?u.32949} → α → FreeMonoid αof := rfl: ∀ {α : Sort ?u.32966} {a : α}, a = arfl
#align free_monoid.lift_symm_apply FreeMonoid.lift_symm_apply: ∀ {α : Type u_1} {M : Type u_2} [inst : Monoid M] (f : FreeMonoid α →* M), ↑lift.symm f = ↑f ∘ ofFreeMonoid.lift_symm_apply

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : AddMonoid M] (f : α → M) (l : FreeAddMonoid α),
theorem lift_apply: ∀ {α : Type u_1} {M : Type u_2} [inst : Monoid M] (f : α → M) (l : FreeMonoid α),
↑(↑lift f) l = List.prod (List.map f (↑toList l))lift_apply (f: α → Mf : α: Type ?u.33071α → M: Type ?u.33080M) (l: FreeMonoid αl : FreeMonoid: Type ?u.33096 → Type ?u.33096FreeMonoid α: Type ?u.33071α) : lift: {α : Type ?u.33101} → {M : Type ?u.33100} → [inst : Monoid M] → (α → M) ≃ (FreeMonoid α →* M)lift f: α → Mf l: FreeMonoid αl = ((toList: {α : Type ?u.33551} → FreeMonoid α ≃ List αtoList l: FreeMonoid αl).map: {α : Type ?u.33631} → {β : Type ?u.33630} → (α → β) → List α → List βmap f: α → Mf).prod: {α : Type ?u.33642} → [inst : Mul α] → [inst : One α] → List α → αprod :=
prodAux_eq: ∀ {M : Type ?u.34233} [inst : Monoid M] (l : List M), prodAux l = List.prod lprodAux_eq _: List ?m.34234_
#align free_monoid.lift_apply FreeMonoid.lift_apply: ∀ {α : Type u_1} {M : Type u_2} [inst : Monoid M] (f : α → M) (l : FreeMonoid α),
↑(↑lift f) l = List.prod (List.map f (↑toList l))FreeMonoid.lift_apply
#align free_add_monoid.lift_apply FreeAddMonoid.lift_apply: ∀ {α : Type u_1} {M : Type u_2} [inst : AddMonoid M] (f : α → M) (l : FreeAddMonoid α),

theorem lift_comp_of: ∀ (f : α → M), ↑(↑lift f) ∘ of = flift_comp_of (f: α → Mf : α: Type ?u.34438α → M: Type ?u.34447M) : lift: {α : Type ?u.34471} → {M : Type ?u.34470} → [inst : Monoid M] → (α → M) ≃ (FreeMonoid α →* M)lift f: α → Mf ∘ of: {α : Type ?u.34922} → α → FreeMonoid αof = f: α → Mf := rfl: ∀ {α : Sort ?u.34934} {a : α}, a = arfl
#align free_monoid.lift_comp_of FreeMonoid.lift_comp_of: ∀ {α : Type u_1} {M : Type u_2} [inst : Monoid M] (f : α → M), ↑(↑lift f) ∘ of = fFreeMonoid.lift_comp_of

@[to_additive: ∀ {α : Type u_2} {M : Type u_1} [inst : AddMonoid M] (f : α → M) (x : α),
theorem lift_eval_of: ∀ (f : α → M) (x : α), ↑(↑lift f) (of x) = f xlift_eval_of (f: α → Mf : α: Type ?u.35024α → M: Type ?u.35033M) (x: αx : α: Type ?u.35024α) : lift: {α : Type ?u.35053} → {M : Type ?u.35052} → [inst : Monoid M] → (α → M) ≃ (FreeMonoid α →* M)lift f: α → Mf (of: {α : Type ?u.35502} → α → FreeMonoid αof x: αx) = f: α → Mf x: αx := rfl: ∀ {α : Sort ?u.35510} {a : α}, a = arfl
#align free_monoid.lift_eval_of FreeMonoid.lift_eval_of: ∀ {α : Type u_2} {M : Type u_1} [inst : Monoid M] (f : α → M) (x : α), ↑(↑lift f) (of x) = f xFreeMonoid.lift_eval_of
#align free_add_monoid.lift_eval_of FreeAddMonoid.lift_eval_of: ∀ {α : Type u_2} {M : Type u_1} [inst : AddMonoid M] (f : α → M) (x : α),

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : AddMonoid M] (f : FreeAddMonoid α →+ M),
theorem lift_restrict: ∀ {α : Type u_1} {M : Type u_2} [inst : Monoid M] (f : FreeMonoid α →* M), ↑lift (↑f ∘ of) = flift_restrict (f: FreeMonoid α →* Mf : FreeMonoid: Type ?u.35698 → Type ?u.35698FreeMonoid α: Type ?u.35675α →* M: Type ?u.35684M) : lift: {α : Type ?u.36200} → {M : Type ?u.36199} → [inst : Monoid M] → (α → M) ≃ (FreeMonoid α →* M)lift (f: FreeMonoid α →* Mf ∘ of: {α : Type ?u.36622} → α → FreeMonoid αof) = f: FreeMonoid α →* Mf := lift: {α : Type ?u.36642} → {M : Type ?u.36641} → [inst : Monoid M] → (α → M) ≃ (FreeMonoid α →* M)lift.apply_symm_apply: ∀ {α : Sort ?u.36661} {β : Sort ?u.36660} (e : α ≃ β) (x : β), ↑e (↑e.symm x) = xapply_symm_apply f: FreeMonoid α →* Mf
#align free_monoid.lift_restrict FreeMonoid.lift_restrict: ∀ {α : Type u_1} {M : Type u_2} [inst : Monoid M] (f : FreeMonoid α →* M), ↑lift (↑f ∘ of) = fFreeMonoid.lift_restrict

@[to_additive: ∀ {α : Type u_3} {M : Type u_1} [inst : AddMonoid M] {N : Type u_2} [inst_1 : AddMonoid N] (g : M →+ N) (f : α → M),
theorem comp_lift: ∀ {α : Type u_3} {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] (g : M →* N) (f : α → M),
MonoidHom.comp g (↑lift f) = ↑lift (↑g ∘ f)comp_lift (g: M →* Ng : M: Type ?u.36843M →* N: Type ?u.36849N) (f: α → Mf : α: Type ?u.36834α → M: Type ?u.36843M) : g: M →* Ng.comp: {M : Type ?u.37296} →
{N : Type ?u.37295} →
{P : Type ?u.37294} →
[inst : MulOneClass M] → [inst_1 : MulOneClass N] → [inst_2 : MulOneClass P] → (N →* P) → (M →* N) → M →* Pcomp (lift: {α : Type ?u.37316} → {M : Type ?u.37315} → [inst : Monoid M] → (α → M) ≃ (FreeMonoid α →* M)lift f: α → Mf) = lift: {α : Type ?u.37729} → {M : Type ?u.37728} → [inst : Monoid M] → (α → M) ≃ (FreeMonoid α →* M)lift (g: M →* Ng ∘ f: α → Mf) :=
-- Porting note: replace ext by FreeMonoid.hom_eq
FreeMonoid.hom_eq: ∀ {α : Type ?u.38167} {M : Type ?u.38168} [inst : Monoid M] ⦃f g : FreeMonoid α →* M⦄,
(∀ (x : α), ↑f (of x) = ↑g (of x)) → f = gFreeMonoid.hom_eq (byGoals accomplished! 🐙 α: Type u_3β: Type ?u.36837γ: Type ?u.36840M: Type u_1inst✝¹: Monoid MN: Type u_2inst✝: Monoid Ng: M →* Nf: α → M∀ (x : α), ↑(MonoidHom.comp g (↑lift f)) (of x) = ↑(↑lift (↑g ∘ f)) (of x)simpGoals accomplished! 🐙)
#align free_monoid.comp_lift FreeMonoid.comp_lift: ∀ {α : Type u_3} {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] (g : M →* N) (f : α → M),
MonoidHom.comp g (↑lift f) = ↑lift (↑g ∘ f)FreeMonoid.comp_lift
#align free_add_monoid.comp_lift FreeAddMonoid.comp_lift: ∀ {α : Type u_3} {M : Type u_1} [inst : AddMonoid M] {N : Type u_2} [inst_1 : AddMonoid N] (g : M →+ N) (f : α → M),

@[to_additive: ∀ {α : Type u_3} {M : Type u_1} [inst : AddMonoid M] {N : Type u_2} [inst_1 : AddMonoid N] (g : M →+ N) (f : α → M)
theorem hom_map_lift: ∀ {α : Type u_3} {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] (g : M →* N) (f : α → M)
(x : FreeMonoid α), ↑g (↑(↑lift f) x) = ↑(↑lift (↑g ∘ f)) xhom_map_lift (g: M →* Ng : M: Type ?u.40724M →* N: Type ?u.40730N) (f: α → Mf : α: Type ?u.40715α → M: Type ?u.40724M) (x: FreeMonoid αx : FreeMonoid: Type ?u.41174 → Type ?u.41174FreeMonoid α: Type ?u.40715α) : g: M →* Ng (lift: {α : Type ?u.41477} → {M : Type ?u.41476} → [inst : Monoid M] → (α → M) ≃ (FreeMonoid α →* M)lift f: α → Mf x: FreeMonoid αx) = lift: {α : Type ?u.41923} → {M : Type ?u.41922} → [inst : Monoid M] → (α → M) ≃ (FreeMonoid α →* M)lift (g: M →* Ng ∘ f: α → Mf) x: FreeMonoid αx :=
FunLike.ext_iff: ∀ {F : Sort ?u.42670} {α : Sort ?u.42672} {β : α → Sort ?u.42671} [i : FunLike F α β] {f g : F},
f = g ↔ ∀ (x : α), ↑f x = ↑g xFunLike.ext_iff.1: ∀ {a b : Prop}, (a ↔ b) → a → b1 (comp_lift: ∀ {α : Type ?u.42716} {M : Type ?u.42714} [inst : Monoid M] {N : Type ?u.42715} [inst_1 : Monoid N] (g : M →* N)
(f : α → M), MonoidHom.comp g (↑lift f) = ↑lift (↑g ∘ f)comp_lift g: M →* Ng f: α → Mf) x: FreeMonoid αx
#align free_monoid.hom_map_lift FreeMonoid.hom_map_lift: ∀ {α : Type u_3} {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] (g : M →* N) (f : α → M)
(x : FreeMonoid α), ↑g (↑(↑lift f) x) = ↑(↑lift (↑g ∘ f)) xFreeMonoid.hom_map_lift
#align free_add_monoid.hom_map_lift FreeAddMonoid.hom_map_lift: ∀ {α : Type u_3} {M : Type u_1} [inst : AddMonoid M] {N : Type u_2} [inst_1 : AddMonoid N] (g : M →+ N) (f : α → M)

/-- Define a multiplicative action of `FreeMonoid α` on `β`. -/
def mkMulAction: (α → β → β) → MulAction (FreeMonoid α) βmkMulAction (f: α → β → βf : α: Type ?u.43314α → β: Type ?u.43317β → β: Type ?u.43317β) : MulAction: (α : Type ?u.43342) → Type ?u.43341 → [inst : Monoid α] → Type (max?u.43342?u.43341)MulAction (FreeMonoid: Type ?u.43343 → Type ?u.43343FreeMonoid α: Type ?u.43314α) β: Type ?u.43317β where
smul l: ?m.43614l b: ?m.43617b := l: ?m.43614l.toList: {α : Type ?u.43619} → FreeMonoid α ≃ List αtoList.foldr: {α : Type ?u.43699} → {β : Type ?u.43698} → (α → β → β) → β → List α → βfoldr f: α → β → βf b: ?m.43617b
one_smul _: ?m.43719_ := rfl: ∀ {α : Sort ?u.43721} {a : α}, a = arfl
mul_smul _: ?m.43751_ _: ?m.43754_ _: ?m.43757_ := List.foldr_append: ∀ {α : Type ?u.43759} {β : Type ?u.43760} (f : α → β → β) (b : β) (l l' : List α),
List.foldr f b (l ++ l') = List.foldr f (List.foldr f b l') lList.foldr_append _: ?m.43761 → ?m.43762 → ?m.43762_ _: ?m.43762_ _: List ?m.43761_ _: List ?m.43761_
#align free_monoid.mk_mul_action FreeMonoid.mkMulAction: {α : Type u_1} → {β : Type u_2} → (α → β → β) → MulAction (FreeMonoid α) βFreeMonoid.mkMulAction

@[to_additive: ∀ {α : Type u_1} {β : Type u_2} (f : α → β → β) (l : FreeAddMonoid α) (b : β),
theorem smul_def: ∀ {α : Type u_1} {β : Type u_2} (f : α → β → β) (l : FreeMonoid α) (b : β), l • b = List.foldr f b (↑toList l)smul_def (f: α → β → βf : α: Type ?u.44637α → β: Type ?u.44640β → β: Type ?u.44640β) (l: FreeMonoid αl : FreeMonoid: Type ?u.44664 → Type ?u.44664FreeMonoid α: Type ?u.44637α) (b: βb : β: Type ?u.44640β) :
haveI := mkMulAction: {α : Type ?u.44672} → {β : Type ?u.44671} → (α → β → β) → MulAction (FreeMonoid α) βmkMulAction f: α → β → βf
l: FreeMonoid αl • b: βb = l: FreeMonoid αl.toList: {α : Type ?u.45569} → FreeMonoid α ≃ List αtoList.foldr: {α : Type ?u.45648} → {β : Type ?u.45647} → (α → β → β) → β → List α → βfoldr f: α → β → βf b: βb := rfl: ∀ {α : Sort ?u.45668} {a : α}, a = arfl
#align free_monoid.smul_def FreeMonoid.smul_def: ∀ {α : Type u_1} {β : Type u_2} (f : α → β → β) (l : FreeMonoid α) (b : β), l • b = List.foldr f b (↑toList l)FreeMonoid.smul_def

@[to_additive: ∀ {α : Type u_1} {β : Type u_2} (f : α → β → β) (l : List α) (b : β), ↑FreeAddMonoid.ofList l +ᵥ b = List.foldr f b lto_additive]
theorem ofList_smul: ∀ {α : Type u_1} {β : Type u_2} (f : α → β → β) (l : List α) (b : β), ↑ofList l • b = List.foldr f b lofList_smul (f: α → β → βf : α: Type ?u.45710α → β: Type ?u.45713β → β: Type ?u.45713β) (l: List αl : List: Type ?u.45737 → Type ?u.45737List α: Type ?u.45710α) (b: βb : β: Type ?u.45713β) :
haveI := mkMulAction: {α : Type ?u.45745} → {β : Type ?u.45744} → (α → β → β) → MulAction (FreeMonoid α) βmkMulAction f: α → β → βf
ofList: {α : Type ?u.45767} → List α ≃ FreeMonoid αofList l: List αl • b: βb = l: List αl.foldr: {α : Type ?u.46836} → {β : Type ?u.46835} → (α → β → β) → β → List α → βfoldr f: α → β → βf b: βb := rfl: ∀ {α : Sort ?u.46855} {a : α}, a = arfl
#align free_monoid.of_list_smul FreeMonoid.ofList_smul: ∀ {α : Type u_1} {β : Type u_2} (f : α → β → β) (l : List α) (b : β), ↑ofList l • b = List.foldr f b lFreeMonoid.ofList_smul

@[to_additive: ∀ {α : Type u_2} {β : Type u_1} (f : α → β → β) (x : α) (y : β), FreeAddMonoid.of x +ᵥ y = f x yto_additive (attr := simp)]
theorem of_smul: ∀ (f : α → β → β) (x : α) (y : β), of x • y = f x yof_smul (f: α → β → βf : α: Type ?u.46908α → β: Type ?u.46911β → β: Type ?u.46911β) (x: αx : α: Type ?u.46908α) (y: βy : β: Type ?u.46911β) :
(haveI := mkMulAction: {α : Type ?u.46947} → {β : Type ?u.46946} → (α → β → β) → MulAction (FreeMonoid α) βmkMulAction f: α → β → βf
of: {α : Type ?u.46968} → α → FreeMonoid αof x: αx • y: βy) = f: α → β → βf x: αx y: βy := rfl: ∀ {α : Sort ?u.47849} {a : α}, a = arfl
#align free_monoid.of_smul FreeMonoid.of_smul: ∀ {α : Type u_2} {β : Type u_1} (f : α → β → β) (x : α) (y : β), of x • y = f x yFreeMonoid.of_smul

/-- The unique monoid homomorphism `FreeMonoid α →* FreeMonoid β` that sends
each `of x` to `of (f x)`. -/
that sends each `of x` to `of (f x)`."]
def map: {α : Type u_1} → {β : Type u_2} → (α → β) → FreeMonoid α →* FreeMonoid βmap (f: α → βf : α: Type ?u.47942α → β: Type ?u.47945β) : FreeMonoid: Type ?u.47969 → Type ?u.47969FreeMonoid α: Type ?u.47942α →* FreeMonoid: Type ?u.47970 → Type ?u.47970FreeMonoid β: Type ?u.47945β
where
toFun l: ?m.48990l := ofList: {α : Type ?u.48992} → List α ≃ FreeMonoid αofList <| l: ?m.48990l.toList: {α : Type ?u.49070} → FreeMonoid α ≃ List αtoList.map: {α : Type ?u.49150} → {β : Type ?u.49149} → (α → β) → List α → List βmap f: α → βf
map_one' := rfl: ∀ {α : Sort ?u.49166} {a : α}, a = arfl
map_mul' _: ?m.49191_ _: ?m.49194_ := List.map_append: ∀ {α : Type ?u.49196} {β : Type ?u.49197} (f : α → β) (l₁ l₂ : List α),
List.map f (l₁ ++ l₂) = List.map f l₁ ++ List.map f l₂List.map_append _: ?m.49198 → ?m.49199_ _: List ?m.49198_ _: List ?m.49198_
#align free_monoid.map FreeMonoid.map: {α : Type u_1} → {β : Type u_2} → (α → β) → FreeMonoid α →* FreeMonoid βFreeMonoid.map

@[to_additive: ∀ {α : Type u_2} {β : Type u_1} (f : α → β) (x : α),
theorem map_of: ∀ (f : α → β) (x : α), ↑(map f) (of x) = of (f x)map_of (f: α → βf : α: Type ?u.51259α → β: Type ?u.51262β) (x: αx : α: Type ?u.51259α) : map: {α : Type ?u.51288} → {β : Type ?u.51287} → (α → β) → FreeMonoid α →* FreeMonoid βmap f: α → βf (of: {α : Type ?u.51594} → α → FreeMonoid αof x: αx) = of: {α : Type ?u.51597} → α → FreeMonoid αof (f: α → βf x: αx) := rfl: ∀ {α : Sort ?u.51605} {a : α}, a = arfl
#align free_monoid.map_of FreeMonoid.map_of: ∀ {α : Type u_2} {β : Type u_1} (f : α → β) (x : α), ↑(map f) (of x) = of (f x)FreeMonoid.map_of
#align free_add_monoid.map_of FreeAddMonoid.map_of: ∀ {α : Type u_2} {β : Type u_1} (f : α → β) (x : α),

@[to_additive: ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (xs : FreeAddMonoid α),
theorem toList_map: ∀ (f : α → β) (xs : FreeMonoid α), ↑toList (↑(map f) xs) = List.map f (↑toList xs)toList_map (f: α → βf : α: Type ?u.51717α → β: Type ?u.51720β) (xs: FreeMonoid αxs : FreeMonoid: Type ?u.51742 → Type ?u.51742FreeMonoid α: Type ?u.51717α) : toList: {α : Type ?u.51746} → FreeMonoid α ≃ List αtoList (map: {α : Type ?u.51825} → {β : Type ?u.51824} → (α → β) → FreeMonoid α →* FreeMonoid βmap f: α → βf xs: FreeMonoid αxs) = xs: FreeMonoid αxs.toList: {α : Type ?u.52134} → FreeMonoid α ≃ List αtoList.map: {α : Type ?u.52213} → {β : Type ?u.52212} → (α → β) → List α → List βmap f: α → βf := rfl: ∀ {α : Sort ?u.52230} {a : α}, a = arfl
#align free_monoid.to_list_map FreeMonoid.toList_map: ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (xs : FreeMonoid α), ↑toList (↑(map f) xs) = List.map f (↑toList xs)FreeMonoid.toList_map
#align free_add_monoid.to_list_map FreeAddMonoid.toList_map: ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (xs : FreeAddMonoid α),

@[to_additive: ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (xs : List α),
theorem ofList_map: ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (xs : List α), ↑ofList (List.map f xs) = ↑(map f) (↑ofList xs)ofList_map (f: α → βf : α: Type ?u.52319α → β: Type ?u.52322β) (xs: List αxs : List: Type ?u.52344 → Type ?u.52344List α: Type ?u.52319α) : ofList: {α : Type ?u.52348} → List α ≃ FreeMonoid αofList (xs: List αxs.map: {α : Type ?u.52427} → {β : Type ?u.52426} → (α → β) → List α → List βmap f: α → βf) = map: {α : Type ?u.52441} → {β : Type ?u.52440} → (α → β) → FreeMonoid α →* FreeMonoid βmap f: α → βf (ofList: {α : Type ?u.52747} → List α ≃ FreeMonoid αofList xs: List αxs) := rfl: ∀ {α : Sort ?u.52832} {a : α}, a = arfl
#align free_monoid.of_list_map FreeMonoid.ofList_map: ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (xs : List α), ↑ofList (List.map f xs) = ↑(map f) (↑ofList xs)FreeMonoid.ofList_map
#align free_add_monoid.of_list_map FreeAddMonoid.ofList_map: ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (xs : List α),

theorem lift_of_comp_eq_map: ∀ {α : Type u_1} {β : Type u_2} (f : α → β), (↑lift fun x => of (f x)) = map flift_of_comp_eq_map (f: α → βf : α: Type ?u.52881α → β: Type ?u.52884β) : (lift: {α : Type ?u.52908} → {M : Type ?u.52907} → [inst : Monoid M] → (α → M) ≃ (FreeMonoid α →* M)lift fun x: ?m.53023x ↦ of: {α : Type ?u.53025} → α → FreeMonoid αof (f: α → βf x: ?m.53023x)) = map: {α : Type ?u.53284} → {β : Type ?u.53283} → (α → β) → FreeMonoid α →* FreeMonoid βmap f: α → βf := hom_eq: ∀ {α : Type ?u.53299} {M : Type ?u.53300} [inst : Monoid M] ⦃f g : FreeMonoid α →* M⦄,
(∀ (x : α), ↑f (of x) = ↑g (of x)) → f = ghom_eq fun _: ?m.53332_ ↦ rfl: ∀ {α : Sort ?u.53334} {a : α}, a = arfl
#align free_monoid.lift_of_comp_eq_map FreeMonoid.lift_of_comp_eq_map: ∀ {α : Type u_1} {β : Type u_2} (f : α → β), (↑lift fun x => of (f x)) = map fFreeMonoid.lift_of_comp_eq_map

@[to_additive: ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_2} (g : β → γ) (f : α → β),
theorem map_comp: ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_2} (g : β → γ) (f : α → β), map (g ∘ f) = MonoidHom.comp (map g) (map f)map_comp (g: β → γg : β: Type ?u.53726β → γ: Type ?u.53729γ) (f: α → βf : α: Type ?u.53723α → β: Type ?u.53726β) : map: {α : Type ?u.53754} → {β : Type ?u.53753} → (α → β) → FreeMonoid α →* FreeMonoid βmap (g: β → γg ∘ f: α → βf) = (map: {α : Type ?u.53775} → {β : Type ?u.53774} → (α → β) → FreeMonoid α →* FreeMonoid βmap g: β → γg).comp: {M : Type ?u.53783} →
{N : Type ?u.53782} →
{P : Type ?u.53781} →
[inst : MulOneClass M] → [inst_1 : MulOneClass N] → [inst_2 : MulOneClass P] → (N →* P) → (M →* N) → M →* Pcomp (map: {α : Type ?u.53805} → {β : Type ?u.53804} → (α → β) → FreeMonoid α →* FreeMonoid βmap f: α → βf) := hom_eq: ∀ {α : Type ?u.54669} {M : Type ?u.54670} [inst : Monoid M] ⦃f g : FreeMonoid α →* M⦄,
(∀ (x : α), ↑f (of x) = ↑g (of x)) → f = ghom_eq fun _: ?m.54702_ ↦ rfl: ∀ {α : Sort ?u.54704} {a : α}, a = arfl
#align free_monoid.map_comp FreeMonoid.map_comp: ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_2} (g : β → γ) (f : α → β), map (g ∘ f) = MonoidHom.comp (map g) (map f)FreeMonoid.map_comp
#align free_add_monoid.map_comp FreeAddMonoid.map_comp: ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_2} (g : β → γ) (f : α → β),