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: Kenny Lau

! This file was ported from Lean 3 source module algebra.free
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Hom.Group
import Mathlib.Algebra.Hom.Equiv.Basic
import Mathlib.Control.Applicative
import Mathlib.Control.Traversable.Basic
import Mathlib.Logic.Equiv.Defs
import Mathlib.Data.List.Basic

/-!
# Free constructions

## Main definitions

* `FreeMagma α`: free magma (structure with binary operation without any axioms) over alphabet `α`,
defined inductively, with traversable instance and decidable equality.
* `MagmaAssocQuotient α`: quotient of a magma `α` by the associativity equivalence relation.
* `FreeSemigroup α`: free semigroup over alphabet `α`, defined as a structure with two fields
`head : α` and `tail : List α` (i.e. nonempty lists), with traversable instance and decidable
equality.
* `FreeMagmaAssocQuotientEquiv α`: isomorphism between `MagmaAssocQuotient (FreeMagma α)` and
`FreeSemigroup α`.
* `FreeMagma.lift`: the universal property of the free magma, expressing its adjointness.
-/

universe u v l

/-- Free nonabelian additive magma over a given alphabet. -/
inductive FreeAddMagma: Type u → Type uFreeAddMagma (α: Type uα : Type u: Type (u+1)Type u) : Type u: Type (u+1)Type u
| of: {α : Type u} → α → FreeAddMagma αof : α: Type uα → FreeAddMagma: Type u → Type uFreeAddMagma α: Type uα
deriving DecidableEq: Sort u → Sort (max1u)DecidableEq

/-- Free magma over a given alphabet. -/
inductive FreeMagma: Type u → Type uFreeMagma (α: Type uα : Type u: Type (u+1)Type u) : Type u: Type (u+1)Type u
| of: {α : Type u} → α → FreeMagma αof : α: Type uα → FreeMagma: Type u → Type uFreeMagma α: Type uα
| mul: {α : Type u} → FreeMagma α → FreeMagma α → FreeMagma αmul : FreeMagma: Type u → Type uFreeMagma α: Type uα → FreeMagma: Type u → Type uFreeMagma α: Type uα → FreeMagma: Type u → Type uFreeMagma α: Type uα
deriving DecidableEq: Sort u → Sort (max1u)DecidableEq
#align free_magma FreeMagma: Type u → Type uFreeMagma
compile_inductive% FreeMagma: Type u → Type uFreeMagma

namespace FreeMagma

variable {α: Type uα : Type u: Type (u+1)Type u}

instance: {α : Type u} → [inst : Inhabited α] → Inhabited (FreeMagma α)instance [Inhabited: Sort ?u.5896 → Sort (max1?u.5896)Inhabited α: Type uα] : Inhabited: Sort ?u.5899 → Sort (max1?u.5899)Inhabited (FreeMagma: Type ?u.5900 → Type ?u.5900FreeMagma α: Type uα) := ⟨of: {α : Type ?u.5908} → α → FreeMagma αof default: {α : Sort ?u.5911} → [self : Inhabited α] → αdefault⟩

instance: {α : Type u} → Mul (FreeMagma α)instance : Mul: Type ?u.6138 → Type ?u.6138Mul (FreeMagma: Type ?u.6139 → Type ?u.6139FreeMagma α: Type uα) := ⟨FreeMagma.mul: {α : Type ?u.6146} → FreeMagma α → FreeMagma α → FreeMagma αFreeMagma.mul⟩

-- Porting note: invalid attribute 'match_pattern', declaration is in an imported module
-- attribute [match_pattern] Mul.mul

theorem mul_eq: ∀ {α : Type u} (x y : FreeMagma α), mul x y = x * ymul_eq (x: FreeMagma αx y: FreeMagma αy : FreeMagma: Type ?u.6251 → Type ?u.6251FreeMagma α: Type uα) : mul: {α : Type ?u.6255} → FreeMagma α → FreeMagma α → FreeMagma αmul x: FreeMagma αx y: FreeMagma αy = x: FreeMagma αx * y: FreeMagma αy := rfl: ∀ {α : Sort ?u.6316} {a : α}, a = arfl
#align free_magma.mul_eq FreeMagma.mul_eq: ∀ {α : Type u} (x y : FreeMagma α), mul x y = x * yFreeMagma.mul_eq

/- Porting note: these lemmas are autogenerated by the inductive definition and due to
the existence of mul_eq not in simp normal form -/
attribute [nolint simpNF: Std.Tactic.Lint.LintersimpNF] FreeMagma.mul.sizeOf_spec: ∀ {α : Type u} [inst : SizeOf α] (a a_1 : FreeMagma α), sizeOf (mul a a_1) = 1 + sizeOf a + sizeOf a_1FreeMagma.mul.sizeOf_spec
attribute [nolint simpNF: Std.Tactic.Lint.LintersimpNF] FreeAddMagma.add.injEq: ∀ {α : Type u} (a a_1 a_2 a_3 : FreeAddMagma α),
attribute [nolint simpNF: Std.Tactic.Lint.LintersimpNF] FreeMagma.mul.injEq: ∀ {α : Type u} (a a_1 a_2 a_3 : FreeMagma α), (mul a a_1 = mul a_2 a_3) = (a = a_2 ∧ a_1 = a_3)FreeMagma.mul.injEq

/-- Recursor for `FreeMagma` using `x * y` instead of `FreeMagma.mul x y`. -/
@[to_additive: {α : Type u} →
{C : FreeAddMagma α → Sort l} →
(x : FreeAddMagma α) → ((x : α) → C (FreeAddMagma.of x)) → ((x y : FreeAddMagma α) → C x → C y → C (x + y)) → C xto_additive (attr := elab_as_elim) "Recursor for `FreeAddMagma` using `x + y` instead of
def recOnMul: {α : Type u} →
{C : FreeMagma α → Sort l} →
(x : FreeMagma α) → ((x : α) → C (of x)) → ((x y : FreeMagma α) → C x → C y → C (x * y)) → C xrecOnMul {C: FreeMagma α → Sort lC : FreeMagma: Type ?u.6359 → Type ?u.6359FreeMagma α: Type uα → Sort l: Type lSortSort l: Type l l} (x: FreeMagma αx) (ih1: (x : α) → C (of x)ih1 : ∀ x: ?m.6367x, C: FreeMagma α → Sort lC (of: {α : Type ?u.6370} → α → FreeMagma αof x: ?m.6367x))
(ih2: (x y : FreeMagma α) → C x → C y → C (x * y)ih2 : ∀ x: ?m.6376x y: ?m.6379y, C: FreeMagma α → Sort lC x: ?m.6376x → C: FreeMagma α → Sort lC y: ?m.6379y → C: FreeMagma α → Sort lC (x: ?m.6376x * y: ?m.6379y)) : C: FreeMagma α → Sort lC x: ?m.6363x :=
FreeMagma.recOn: {α : Type ?u.6446} →
{motive : FreeMagma α → Sort ?u.6447} →
(t : FreeMagma α) →
((a : α) → motive (of a)) → ((a a_1 : FreeMagma α) → motive a → motive a_1 → motive (mul a a_1)) → motive tFreeMagma.recOn x: FreeMagma αx ih1: (x : α) → C (of x)ih1 ih2: (x y : FreeMagma α) → C x → C y → C (x * y)ih2
#align free_magma.rec_on_mul FreeMagma.recOnMul: {α : Type u} →
{C : FreeMagma α → Sort l} →
(x : FreeMagma α) → ((x : α) → C (of x)) → ((x y : FreeMagma α) → C x → C y → C (x * y)) → C xFreeMagma.recOnMul

theorem hom_ext: ∀ {α : Type u} {β : Type v} [inst : Mul β] {f g : FreeMagma α →ₙ* β}, ↑f ∘ of = ↑g ∘ of → f = ghom_ext {β: Type vβ : Type v: Type (v+1)Type v} [Mul: Type ?u.6836 → Type ?u.6836Mul β: Type vβ] {f: FreeMagma α →ₙ* βf g: FreeMagma α →ₙ* βg : FreeMagma: Type ?u.6871 → Type ?u.6871FreeMagma α: Type uα →ₙ* β: Type vβ} (h: ↑f ∘ of = ↑g ∘ ofh : f: FreeMagma α →ₙ* βf ∘ of: {α : Type ?u.7108} → α → FreeMagma αof = g: FreeMagma α →ₙ* βg ∘ of: {α : Type ?u.7319} → α → FreeMagma αof) : f: FreeMagma α →ₙ* βf = g: FreeMagma α →ₙ* βg :=
(FunLike.ext: ∀ {F : Sort ?u.7339} {α : Sort ?u.7340} {β : α → Sort ?u.7338} [i : FunLike F α β] (f g : F),
(∀ (x : α), ↑f x = ↑g x) → f = gFunLike.ext _: ?m.7341_ _: ?m.7341_) fun x: ?m.7382x ↦ recOnMul: ∀ {α : Type ?u.7385} {C : FreeMagma α → Sort ?u.7384} (x : FreeMagma α),
(∀ (x : α), C (of x)) → (∀ (x y : FreeMagma α), C x → C y → C (x * y)) → C xrecOnMul x: ?m.7382x (congr_fun: ∀ {α : Sort ?u.7629} {β : α → Sort ?u.7628} {f g : (x : α) → β x}, f = g → ∀ (a : α), f a = g acongr_fun h: ↑f ∘ of = ↑g ∘ ofh) <| byGoals accomplished! 🐙 α: Type uβ: Type vinst✝: Mul βf, g: FreeMagma α →ₙ* βh: ↑f ∘ of = ↑g ∘ ofx: FreeMagma α∀ (x y : FreeMagma α), ↑f x = ↑g x → ↑f y = ↑g y → ↑f (x * y) = ↑g (x * y)introsα: Type uβ: Type vinst✝: Mul βf, g: FreeMagma α →ₙ* βh: ↑f ∘ of = ↑g ∘ ofx, x✝, y✝: FreeMagma αa✝¹: ↑f x✝ = ↑g x✝a✝: ↑f y✝ = ↑g y✝↑f (x✝ * y✝) = ↑g (x✝ * y✝) α: Type uβ: Type vinst✝: Mul βf, g: FreeMagma α →ₙ* βh: ↑f ∘ of = ↑g ∘ ofx: FreeMagma α∀ (x y : FreeMagma α), ↑f x = ↑g x → ↑f y = ↑g y → ↑f (x * y) = ↑g (x * y);α: Type uβ: Type vinst✝: Mul βf, g: FreeMagma α →ₙ* βh: ↑f ∘ of = ↑g ∘ ofx, x✝, y✝: FreeMagma αa✝¹: ↑f x✝ = ↑g x✝a✝: ↑f y✝ = ↑g y✝↑f (x✝ * y✝) = ↑g (x✝ * y✝) α: Type uβ: Type vinst✝: Mul βf, g: FreeMagma α →ₙ* βh: ↑f ∘ of = ↑g ∘ ofx: FreeMagma α∀ (x y : FreeMagma α), ↑f x = ↑g x → ↑f y = ↑g y → ↑f (x * y) = ↑g (x * y)simp only [map_mul: ∀ {M : Type ?u.7671} {N : Type ?u.7672} {F : Type ?u.7670} [inst : Mul M] [inst_1 : Mul N] [inst_2 : MulHomClass F M N]
(f : F) (x y : M), ↑f (x * y) = ↑f x * ↑f ymap_mul, *]Goals accomplished! 🐙
#align free_magma.hom_ext FreeMagma.hom_ext: ∀ {α : Type u} {β : Type v} [inst : Mul β] {f g : FreeMagma α →ₙ* β}, ↑f ∘ of = ↑g ∘ of → f = gFreeMagma.hom_ext

end FreeMagma

/-- Lifts a function `α → β` to a magma homomorphism `FreeMagma α → β` given a magma `β`. -/
def FreeMagma.liftAux: {α : Type u} → {β : Type v} → [inst : Mul β] → (α → β) → FreeMagma α → βFreeMagma.liftAux {α: Type uα : Type u: Type (u+1)Type u} {β: Type vβ : Type v: Type (v+1)Type v} [Mul: Type ?u.8132 → Type ?u.8132Mul β: Type vβ] (f: α → βf : α: Type uα → β: Type vβ) : FreeMagma: Type ?u.8140 → Type ?u.8140FreeMagma α: Type uα → β: Type vβ
| FreeMagma.of: {α : Type ?u.8150} → α → FreeMagma αFreeMagma.of x: αx => f: α → βf x: αx
| x: FreeMagma αx * y: FreeMagma αy => liftAux: {α : Type u} → {β : Type v} → [inst : Mul β] → (α → β) → FreeMagma α → βliftAux f: α → βf x: FreeMagma αx * liftAux: {α : Type u} → {β : Type v} → [inst : Mul β] → (α → β) → FreeMagma α → βliftAux f: α → βf y: FreeMagma αy
#align free_magma.lift_aux FreeMagma.liftAux: {α : Type u} → {β : Type v} → [inst : Mul β] → (α → β) → FreeMagma α → βFreeMagma.liftAux

/-- Lifts a function `α → β` to an additive magma homomorphism `FreeAddMagma α → β` given
def FreeAddMagma.liftAux: {α : Type u} → {β : Type v} → [inst : Add β] → (α → β) → FreeAddMagma α → βFreeAddMagma.liftAux {α: Type uα : Type u: Type (u+1)Type u} {β: Type vβ : Type v: Type (v+1)Type v} [Add: Type ?u.8696 → Type ?u.8696Add β: Type vβ] (f: α → βf : α: Type uα → β: Type vβ) : FreeAddMagma: Type ?u.8704 → Type ?u.8704FreeAddMagma α: Type uα → β: Type vβ
| FreeAddMagma.of: {α : Type ?u.8714} → α → FreeAddMagma αFreeAddMagma.of x: αx => f: α → βf x: αx
| x: FreeAddMagma αx + y: FreeAddMagma αy => liftAux: {α : Type u} → {β : Type v} → [inst : Add β] → (α → β) → FreeAddMagma α → βliftAux f: α → βf x: FreeAddMagma αx + liftAux: {α : Type u} → {β : Type v} → [inst : Add β] → (α → β) → FreeAddMagma α → βliftAux f: α → βf y: FreeAddMagma αy

attribute [to_additive: {α : Type u} → {β : Type v} → [inst : Add β] → (α → β) → FreeAddMagma α → βto_additive existing] FreeMagma.liftAux: {α : Type u} → {β : Type v} → [inst : Mul β] → (α → β) → FreeMagma α → βFreeMagma.liftAux

namespace FreeMagma

section lift

variable {α: Type uα : Type u: Type (u+1)Type u} {β: Type vβ : Type v: Type (v+1)Type v} [Mul: Type ?u.10757 → Type ?u.10757Mul β: Type vβ] (f: α → βf : α: Type uα → β: Type vβ)

/-- The universal property of the free magma expressing its adjointness. -/
@[to_additive: {α : Type u} → {β : Type v} → [inst : Add β] → (α → β) ≃ AddHom (FreeAddMagma α) βto_additive (attr := simps symm_apply: ∀ {α : Type u} {β : Type v} [inst : Add β] (F : AddHom (FreeAddMagma α) β) (a : α),
def lift: (α → β) ≃ (FreeMagma α →ₙ* β)lift : (α: Type uα → β: Type vβ) ≃ (FreeMagma: Type ?u.9899 → Type ?u.9899FreeMagma α: Type uα →ₙ* β: Type vβ) where
toFun f: ?m.9933f :=
{ toFun := liftAux: {α : Type ?u.9946} → {β : Type ?u.9945} → [inst : Mul β] → (α → β) → FreeMagma α → βliftAux f: ?m.9933f
map_mul' := fun x: ?m.9984x y: ?m.9987y ↦ rfl: ∀ {α : Sort ?u.9989} {a : α}, a = arfl }
invFun F: ?m.10013F := F: ?m.10013F ∘ of: {α : Type ?u.10244} → α → FreeMagma αof
left_inv f: ?m.10255f := byGoals accomplished! 🐙 α: Type uβ: Type vinst✝: Mul βf✝, f: α → β(fun F => ↑F ∘ of)
((fun f => { toFun := liftAux f, map_mul' := (_ : ∀ (x y : FreeMagma α), liftAux f (x * y) = liftAux f (x * y)) })
f) =   frflGoals accomplished! 🐙
-- Porting note: replaced ext by FreeMagma.hom_ext
right_inv F: ?m.10261F := FreeMagma.hom_ext: ∀ {α : Type ?u.10264} {β : Type ?u.10263} [inst : Mul β] {f g : FreeMagma α →ₙ* β}, ↑f ∘ of = ↑g ∘ of → f = gFreeMagma.hom_ext (rfl: ∀ {α : Sort ?u.10304} {a : α}, a = arfl)
#align free_magma.lift FreeMagma.lift: {α : Type u} → {β : Type v} → [inst : Mul β] → (α → β) ≃ (FreeMagma α →ₙ* β)FreeMagma.lift

@[to_additive: ∀ {α : Type u} {β : Type v} [inst : Add β] (f : α → β) (x : α), ↑(↑FreeAddMagma.lift f) (FreeAddMagma.of x) = f xto_additive (attr := simp)]
theorem lift_of: ∀ (x : α), ↑(↑lift f) (of x) = f xlift_of (x: ?m.10764x) : lift: {α : Type ?u.10769} → {β : Type ?u.10768} → [inst : Mul β] → (α → β) ≃ (FreeMagma α →ₙ* β)lift f: α → βf (of: {α : Type ?u.11140} → α → FreeMagma αof x: ?m.10764x) = f: α → βf x: ?m.10764x := rfl: ∀ {α : Sort ?u.11146} {a : α}, a = arfl
#align free_magma.lift_of FreeMagma.lift_of: ∀ {α : Type u} {β : Type v} [inst : Mul β] (f : α → β) (x : α), ↑(↑lift f) (of x) = f xFreeMagma.lift_of

@[to_additive: ∀ {α : Type u} {β : Type v} [inst : Add β] (f : α → β), ↑(↑FreeAddMagma.lift f) ∘ FreeAddMagma.of = fto_additive (attr := simp)]
theorem lift_comp_of: ↑(↑lift f) ∘ of = flift_comp_of : lift: {α : Type ?u.11301} → {β : Type ?u.11300} → [inst : Mul β] → (α → β) ≃ (FreeMagma α →ₙ* β)lift f: α → βf ∘ of: {α : Type ?u.11674} → α → FreeMagma αof = f: α → βf := rfl: ∀ {α : Sort ?u.11685} {a : α}, a = arfl
#align free_magma.lift_comp_of FreeMagma.lift_comp_of: ∀ {α : Type u} {β : Type v} [inst : Mul β] (f : α → β), ↑(↑lift f) ∘ of = fFreeMagma.lift_comp_of

theorem lift_comp_of': ∀ {α : Type u} {β : Type v} [inst : Mul β] (f : FreeMagma α →ₙ* β), ↑lift (↑f ∘ of) = flift_comp_of' (f: FreeMagma α →ₙ* βf : FreeMagma: Type ?u.11841 → Type ?u.11841FreeMagma α: Type uα →ₙ* β: Type vβ) : lift: {α : Type ?u.11871} → {β : Type ?u.11870} → [inst : Mul β] → (α → β) ≃ (FreeMagma α →ₙ* β)lift (f: FreeMagma α →ₙ* βf ∘ of: {α : Type ?u.12228} → α → FreeMagma αof) = f: FreeMagma α →ₙ* βf := lift: {α : Type ?u.12242} → {β : Type ?u.12241} → [inst : Mul β] → (α → β) ≃ (FreeMagma α →ₙ* β)lift.apply_symm_apply: ∀ {α : Sort ?u.12271} {β : Sort ?u.12270} (e : α ≃ β) (x : β), ↑e (↑e.symm x) = xapply_symm_apply f: FreeMagma α →ₙ* βf
#align free_magma.lift_comp_of' FreeMagma.lift_comp_of': ∀ {α : Type u} {β : Type v} [inst : Mul β] (f : FreeMagma α →ₙ* β), ↑lift (↑f ∘ of) = fFreeMagma.lift_comp_of'

end lift

section Map

variable {α: Type uα : Type u: Type (u+1)Type u} {β: Type vβ : Type v: Type (v+1)Type v} (f: α → βf : α: Type uα → β: Type vβ)

/-- The unique magma homomorphism `FreeMagma α →ₙ* FreeMagma β` that sends
each `of x` to `of (f x)`. -/
each `of x` to `of (f x)`."]
def map: {α : Type u} → {β : Type v} → (α → β) → FreeMagma α →ₙ* FreeMagma βmap (f: α → βf : α: Type uα → β: Type vβ) : FreeMagma: Type ?u.12444 → Type ?u.12444FreeMagma α: Type uα →ₙ* FreeMagma: Type ?u.12445 → Type ?u.12445FreeMagma β: Type vβ := lift: {α : Type ?u.12477} → {β : Type ?u.12476} → [inst : Mul β] → (α → β) ≃ (FreeMagma α →ₙ* β)lift (of: {α : Type ?u.12610} → α → FreeMagma αof ∘ f: α → βf)
#align free_magma.map FreeMagma.map: {α : Type u} → {β : Type v} → (α → β) → FreeMagma α →ₙ* FreeMagma βFreeMagma.map

@[to_additive: ∀ {α : Type u} {β : Type v} (f : α → β) (x : α), ↑(FreeAddMagma.map f) (FreeAddMagma.of x) = FreeAddMagma.of (f x)to_additive (attr := simp)]
theorem map_of: ∀ {α : Type u} {β : Type v} (f : α → β) (x : α), ↑(map f) (of x) = of (f x)map_of (x: αx) : map: {α : Type ?u.12995} → {β : Type ?u.12994} → (α → β) → FreeMagma α →ₙ* FreeMagma βmap f: α → βf (of: {α : Type ?u.13225} → α → FreeMagma αof x: ?m.12990x) = of: {α : Type ?u.13228} → α → FreeMagma αof (f: α → βf x: ?m.12990x) := rfl: ∀ {α : Sort ?u.13234} {a : α}, a = arfl
#align free_magma.map_of FreeMagma.map_of: ∀ {α : Type u} {β : Type v} (f : α → β) (x : α), ↑(map f) (of x) = of (f x)FreeMagma.map_of

end Map

section Category

variable {α: Type uα β: Type uβ : Type u: Type (u+1)Type u}

instance: Monad FreeMagmainstance : Monad: (Type ?u.13345 → Type ?u.13344) → Type (max(?u.13345+1)?u.13344)Monad FreeMagma: Type ?u.13346 → Type ?u.13346FreeMagma where
pure := of: {α : Type ?u.13402} → α → FreeMagma αof
bind x: ?m.13495x f: ?m.13498f := lift: {α : Type ?u.13502} → {β : Type ?u.13501} → [inst : Mul β] → (α → β) ≃ (FreeMagma α →ₙ* β)lift f: ?m.13498f x: ?m.13495x

/-- Recursor on `FreeMagma` using `pure` instead of `of`. -/
@[to_additive: {α : Type u} →
{C : FreeAddMagma α → Sort l} →
(x : FreeAddMagma α) → ((x : α) → C (pure x)) → ((x y : FreeAddMagma α) → C x → C y → C (x + y)) → C xto_additive (attr := elab_as_elim) "Recursor on `FreeAddMagma` using `pure` instead of `of`."]
protected def recOnPure: {α : Type u} →
{C : FreeMagma α → Sort l} →
(x : FreeMagma α) → ((x : α) → C (pure x)) → ((x y : FreeMagma α) → C x → C y → C (x * y)) → C xrecOnPure {C: FreeMagma α → Sort lC : FreeMagma: Type ?u.16907 → Type ?u.16907FreeMagma α: Type uα → Sort l: Type lSortSort l: Type l l} (x: FreeMagma αx) (ih1: (x : α) → C (pure x)ih1 : ∀ x: ?m.16915x, C: FreeMagma α → Sort lC (pure: {f : Type ?u.16919 → Type ?u.16918} → [self : Pure f] → {α : Type ?u.16919} → α → f αpure x: ?m.16915x))
(ih2: (x y : FreeMagma α) → C x → C y → C (x * y)ih2 : ∀ x: ?m.16968x y: ?m.16971y, C: FreeMagma α → Sort lC x: ?m.16968x → C: FreeMagma α → Sort lC y: ?m.16971y → C: FreeMagma α → Sort lC (x: ?m.16968x * y: ?m.16971y)) : C: FreeMagma α → Sort lC x: ?m.16911x :=
FreeMagma.recOnMul: {α : Type ?u.17039} →
{C : FreeMagma α → Sort ?u.17038} →
(x : FreeMagma α) → ((x : α) → C (of x)) → ((x y : FreeMagma α) → C x → C y → C (x * y)) → C xFreeMagma.recOnMul x: FreeMagma αx ih1: (x : α) → C (pure x)ih1 ih2: (x y : FreeMagma α) → C x → C y → C (x * y)ih2
#align free_magma.rec_on_pure FreeMagma.recOnPure: {α : Type u} →
{C : FreeMagma α → Sort l} →
(x : FreeMagma α) → ((x : α) → C (pure x)) → ((x y : FreeMagma α) → C x → C y → C (x * y)) → C xFreeMagma.recOnPure

-- Porting note: dsimp can not prove this
@[to_additive: ∀ {α β : Type u} (f : α → β) (x : α), f <\$> pure x = pure (f x)to_additive (attr := simp, nolint simpNF: Std.Tactic.Lint.LintersimpNF)]
theorem map_pure: ∀ {α β : Type u} (f : α → β) (x : α), f <\$> pure x = pure (f x)map_pure (f: α → βf : α: Type uα → β: Type uβ) (x: αx) : (f: α → βf <\$> pure: {f : Type ?u.17462 → Type ?u.17461} → [self : Pure f] → {α : Type ?u.17462} → α → f αpure x: ?m.17427x : FreeMagma: Type ?u.17432 → Type ?u.17432FreeMagma β: Type uβ) = pure: {f : Type ?u.17535 → Type ?u.17534} → [self : Pure f] → {α : Type ?u.17535} → α → f αpure (f: α → βf x: ?m.17427x) := rfl: ∀ {α : Sort ?u.17566} {a : α}, a = arfl
#align free_magma.map_pure FreeMagma.map_pure: ∀ {α β : Type u} (f : α → β) (x : α), f <\$> pure x = pure (f x)FreeMagma.map_pure

@[to_additive: ∀ {α β : Type u} (f : α → β) (x y : FreeAddMagma α), f <\$> (x + y) = f <\$> x + f <\$> yto_additive (attr := simp)]
theorem map_mul': ∀ (f : α → β) (x y : FreeMagma α), f <\$> (x * y) = f <\$> x * f <\$> ymap_mul' (f: α → βf : α: Type uα → β: Type uβ) (x: FreeMagma αx y: FreeMagma αy : FreeMagma: Type ?u.17659 → Type ?u.17659FreeMagma α: Type uα) : f: α → βf <\$> (x: FreeMagma αx * y: FreeMagma αy) = f: α → βf <\$> x: FreeMagma αx * f: α → βf <\$> y: FreeMagma αy := rfl: ∀ {α : Sort ?u.17829} {a : α}, a = arfl
#align free_magma.map_mul' FreeMagma.map_mul': ∀ {α β : Type u} (f : α → β) (x y : FreeMagma α), f <\$> (x * y) = f <\$> x * f <\$> yFreeMagma.map_mul'

-- Porting note: dsimp can not prove this
@[to_additive: ∀ {α β : Type u} (f : α → FreeAddMagma β) (x : α), pure x >>= f = f xto_additive (attr := simp, nolint simpNF: Std.Tactic.Lint.LintersimpNF)]
theorem pure_bind: ∀ (f : α → FreeMagma β) (x : α), pure x >>= f = f xpure_bind (f: α → FreeMagma βf : α: Type uα → FreeMagma: Type ?u.17957 → Type ?u.17957FreeMagma β: Type uβ) (x: ?m.17960x) : pure: {f : Type ?u.17971 → Type ?u.17970} → [self : Pure f] → {α : Type ?u.17971} → α → f αpure x: ?m.17960x >>= f: α → FreeMagma βf = f: α → FreeMagma βf x: ?m.17960x := rfl: ∀ {α : Sort ?u.18058} {a : α}, a = arfl
#align free_magma.pure_bind FreeMagma.pure_bind: ∀ {α β : Type u} (f : α → FreeMagma β) (x : α), pure x >>= f = f xFreeMagma.pure_bind

@[to_additive: ∀ {α β : Type u} (f : α → FreeAddMagma β) (x y : FreeAddMagma α), x + y >>= f = (x >>= f) + (y >>= f)to_additive (attr := simp)]
theorem mul_bind: ∀ (f : α → FreeMagma β) (x y : FreeMagma α), x * y >>= f = (x >>= f) * (y >>= f)mul_bind (f: α → FreeMagma βf : α: Type uα → FreeMagma: Type ?u.18146 → Type ?u.18146FreeMagma β: Type uβ) (x: FreeMagma αx y: FreeMagma αy : FreeMagma: Type ?u.18152 → Type ?u.18152FreeMagma α: Type uα) : x: FreeMagma αx * y: FreeMagma αy >>= f: α → FreeMagma βf = (x: FreeMagma αx >>= f: α → FreeMagma βf) * (y: FreeMagma αy >>= f: α → FreeMagma βf) :=
rfl: ∀ {α : Sort ?u.18304} {a : α}, a = arfl
#align free_magma.mul_bind FreeMagma.mul_bind: ∀ {α β : Type u} (f : α → FreeMagma β) (x y : FreeMagma α), x * y >>= f = (x >>= f) * (y >>= f)FreeMagma.mul_bind

@[to_additive: ∀ {α β : Type u} {f : α → β} {x : FreeAddMagma α}, (Seq.seq (pure f) fun x_1 => x) = f <\$> xto_additive (attr := simp)]
theorem pure_seq: ∀ {α β : Type u} {f : α → β} {x : FreeMagma α}, (Seq.seq (pure f) fun x_1 => x) = f <\$> xpure_seq {α: Type uα β: Type uβ : Type u: Type (u+1)Type u} {f: α → βf : α: Type uα → β: Type uβ} {x: FreeMagma αx : FreeMagma: Type ?u.18438 → Type ?u.18438FreeMagma α: Type uα} : pure: {f : Type ?u.18449 → Type ?u.18448} → [self : Pure f] → {α : Type ?u.18449} → α → f αpure f: α → βf <*> x: FreeMagma αx = f: α → βf <\$> x: FreeMagma αx := rfl: ∀ {α : Sort ?u.18589} {a : α}, a = arfl
#align free_magma.pure_seq FreeMagma.pure_seq: ∀ {α β : Type u} {f : α → β} {x : FreeMagma α}, (Seq.seq (pure f) fun x_1 => x) = f <\$> xFreeMagma.pure_seq

@[to_additive: ∀ {α β : Type u} {f g : FreeAddMagma (α → β)} {x : FreeAddMagma α},
(Seq.seq (f + g) fun x_1 => x) = (Seq.seq f fun x_1 => x) + Seq.seq g fun x_1 => xto_additive (attr := simp)]
theorem mul_seq: ∀ {α β : Type u} {f g : FreeMagma (α → β)} {x : FreeMagma α},
(Seq.seq (f * g) fun x_1 => x) = (Seq.seq f fun x_1 => x) * Seq.seq g fun x_1 => xmul_seq {α: Type uα β: Type uβ : Type u: Type (u+1)Type u} {f: FreeMagma (α → β)f g: FreeMagma (α → β)g : FreeMagma: Type ?u.18713 → Type ?u.18713FreeMagma (α: Type uα → β: Type uβ)} {x: FreeMagma αx : FreeMagma: Type ?u.18719 → Type ?u.18719FreeMagma α: Type uα} :
f: FreeMagma (α → β)f * g: FreeMagma (α → β)g <*> x: FreeMagma αx = (f: FreeMagma (α → β)f <*> x: FreeMagma αx) * (g: FreeMagma (α → β)g <*> x: FreeMagma αx) := rfl: ∀ {α : Sort ?u.18895} {a : α}, a = arfl
#align free_magma.mul_seq FreeMagma.mul_seq: ∀ {α β : Type u} {f g : FreeMagma (α → β)} {x : FreeMagma α},
(Seq.seq (f * g) fun x_1 => x) = (Seq.seq f fun x_1 => x) * Seq.seq g fun x_1 => xFreeMagma.mul_seq

instance: LawfulMonad FreeMagmainstance : LawfulMonad: (m : Type ?u.19029 → Type ?u.19028) → [inst : Monad m] → PropLawfulMonad FreeMagma: Type u → Type uFreeMagma.{u} := LawfulMonad.mk': ∀ (m : Type ?u.19042 → Type ?u.19041) [inst : Monad m],
(∀ {α : Type ?u.19042} (x : m α), id <\$> x = x) →
(∀ {α β : Type ?u.19042} (x : α) (f : α → m β), pure x >>= f = f x) →
(∀ {α β γ : Type ?u.19042} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g) →
autoParam (∀ {α β : Type ?u.19042} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝ →
autoParam
(∀ {α β : Type ?u.19042} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝¹ →
autoParam
(∀ {α β : Type ?u.19042} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝² →
autoParam
(∀ {α β : Type ?u.19042} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =                       f <\$> x)
_auto✝³ →
autoParam
(∀ {α β : Type ?u.19042} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =                         Seq.seq f fun x_1 => x)
_auto✝⁴ →
(pure_bind := fun f: ?m.19159f x: ?m.19162x ↦ rfl: ∀ {α : Sort ?u.19165} {a : α}, a = arfl)
(bind_assoc := fun x: ?m.19199x f: ?m.19202f g: ?m.19206g ↦ FreeMagma.recOnPure: ∀ {α : Type ?u.19210} {C : FreeMagma α → Sort ?u.19209} (x : FreeMagma α),
(∀ (x : α), C (pure x)) → (∀ (x y : FreeMagma α), C x → C y → C (x * y)) → C xFreeMagma.recOnPure x: ?m.19199x (fun x: ?m.19305x ↦ rfl: ∀ {α : Sort ?u.19307} {a : α}, a = arfl) fun x: ?m.19407x y: ?m.19410y ih1: ?m.19413ih1 ih2: ?m.19416ih2 ↦ byGoals accomplished! 🐙
α, β, α✝, β✝, γ✝: Type ux✝: FreeMagma α✝f: α✝ → FreeMagma β✝g: β✝ → FreeMagma γ✝x, y: FreeMagma α✝ih1: x >>= f >>= g = x >>= fun x => f x >>= gih2: y >>= f >>= g = y >>= fun x => f x >>= gx * y >>= f >>= g = x * y >>= fun x => f x >>= grw [α, β, α✝, β✝, γ✝: Type ux✝: FreeMagma α✝f: α✝ → FreeMagma β✝g: β✝ → FreeMagma γ✝x, y: FreeMagma α✝ih1: x >>= f >>= g = x >>= fun x => f x >>= gih2: y >>= f >>= g = y >>= fun x => f x >>= gx * y >>= f >>= g = x * y >>= fun x => f x >>= gmul_bind: ∀ {α β : Type ?u.19520} (f : α → FreeMagma β) (x y : FreeMagma α), x * y >>= f = (x >>= f) * (y >>= f)mul_bind,α, β, α✝, β✝, γ✝: Type ux✝: FreeMagma α✝f: α✝ → FreeMagma β✝g: β✝ → FreeMagma γ✝x, y: FreeMagma α✝ih1: x >>= f >>= g = x >>= fun x => f x >>= gih2: y >>= f >>= g = y >>= fun x => f x >>= g(x >>= f) * (y >>= f) >>= g = x * y >>= fun x => f x >>= g α, β, α✝, β✝, γ✝: Type ux✝: FreeMagma α✝f: α✝ → FreeMagma β✝g: β✝ → FreeMagma γ✝x, y: FreeMagma α✝ih1: x >>= f >>= g = x >>= fun x => f x >>= gih2: y >>= f >>= g = y >>= fun x => f x >>= gx * y >>= f >>= g = x * y >>= fun x => f x >>= gmul_bind: ∀ {α β : Type ?u.19571} (f : α → FreeMagma β) (x y : FreeMagma α), x * y >>= f = (x >>= f) * (y >>= f)mul_bind,α, β, α✝, β✝, γ✝: Type ux✝: FreeMagma α✝f: α✝ → FreeMagma β✝g: β✝ → FreeMagma γ✝x, y: FreeMagma α✝ih1: x >>= f >>= g = x >>= fun x => f x >>= gih2: y >>= f >>= g = y >>= fun x => f x >>= g(x >>= f >>= g) * (y >>= f >>= g) = x * y >>= fun x => f x >>= g α, β, α✝, β✝, γ✝: Type ux✝: FreeMagma α✝f: α✝ → FreeMagma β✝g: β✝ → FreeMagma γ✝x, y: FreeMagma α✝ih1: x >>= f >>= g = x >>= fun x => f x >>= gih2: y >>= f >>= g = y >>= fun x => f x >>= gx * y >>= f >>= g = x * y >>= fun x => f x >>= gmul_bind: ∀ {α β : Type ?u.19585} (f : α → FreeMagma β) (x y : FreeMagma α), x * y >>= f = (x >>= f) * (y >>= f)mul_bind,α, β, α✝, β✝, γ✝: Type ux✝: FreeMagma α✝f: α✝ → FreeMagma β✝g: β✝ → FreeMagma γ✝x, y: FreeMagma α✝ih1: x >>= f >>= g = x >>= fun x => f x >>= gih2: y >>= f >>= g = y >>= fun x => f x >>= g(x >>= f >>= g) * (y >>= f >>= g) = (x >>= fun x => f x >>= g) * (y >>= fun x => f x >>= g) α, β, α✝, β✝, γ✝: Type ux✝: FreeMagma α✝f: α✝ → FreeMagma β✝g: β✝ → FreeMagma γ✝x, y: FreeMagma α✝ih1: x >>= f >>= g = x >>= fun x => f x >>= gih2: y >>= f >>= g = y >>= fun x => f x >>= gx * y >>= f >>= g = x * y >>= fun x => f x >>= gih1: x >>= f >>= g = x >>= fun x => f x >>= gih1,α, β, α✝, β✝, γ✝: Type ux✝: FreeMagma α✝f: α✝ → FreeMagma β✝g: β✝ → FreeMagma γ✝x, y: FreeMagma α✝ih1: x >>= f >>= g = x >>= fun x => f x >>= gih2: y >>= f >>= g = y >>= fun x => f x >>= g(x >>= fun x => f x >>= g) * (y >>= f >>= g) = (x >>= fun x => f x >>= g) * (y >>= fun x => f x >>= g) α, β, α✝, β✝, γ✝: Type ux✝: FreeMagma α✝f: α✝ → FreeMagma β✝g: β✝ → FreeMagma γ✝x, y: FreeMagma α✝ih1: x >>= f >>= g = x >>= fun x => f x >>= gih2: y >>= f >>= g = y >>= fun x => f x >>= gx * y >>= f >>= g = x * y >>= fun x => f x >>= gih2: y >>= f >>= g = y >>= fun x => f x >>= gih2α, β, α✝, β✝, γ✝: Type ux✝: FreeMagma α✝f: α✝ → FreeMagma β✝g: β✝ → FreeMagma γ✝x, y: FreeMagma α✝ih1: x >>= f >>= g = x >>= fun x => f x >>= gih2: y >>= f >>= g = y >>= fun x => f x >>= g(x >>= fun x => f x >>= g) * (y >>= fun x => f x >>= g) = (x >>= fun x => f x >>= g) * (y >>= fun x => f x >>= g)]Goals accomplished! 🐙)
(id_map := fun x: ?m.19110x ↦ FreeMagma.recOnPure: ∀ {α : Type ?u.19113} {C : FreeMagma α → Sort ?u.19112} (x : FreeMagma α),
(∀ (x : α), C (pure x)) → (∀ (x y : FreeMagma α), C x → C y → C (x * y)) → C xFreeMagma.recOnPure x: ?m.19110x (fun _: ?m.19271_ ↦ rfl: ∀ {α : Sort ?u.19273} {a : α}, a = arfl) fun x: ?m.19287x y: ?m.19290y ih1: ?m.19293ih1 ih2: ?m.19296ih2 ↦ byGoals accomplished! 🐙
α, β, α✝: Type ux✝, x, y: FreeMagma α✝ih1: id <\$> x = xih2: id <\$> y = yid <\$> (x * y) = x * yrw [α, β, α✝: Type ux✝, x, y: FreeMagma α✝ih1: id <\$> x = xih2: id <\$> y = yid <\$> (x * y) = x * ymap_mul': ∀ {α β : Type ?u.19482} (f : α → β) (x y : FreeMagma α), f <\$> (x * y) = f <\$> x * f <\$> ymap_mul',α, β, α✝: Type ux✝, x, y: FreeMagma α✝ih1: id <\$> x = xih2: id <\$> y = yid <\$> x * id <\$> y = x * y α, β, α✝: Type ux✝, x, y: FreeMagma α✝ih1: id <\$> x = xih2: id <\$> y = yid <\$> (x * y) = x * yih1: id <\$> x = xih1,α, β, α✝: Type ux✝, x, y: FreeMagma α✝ih1: id <\$> x = xih2: id <\$> y = yx * id <\$> y = x * y α, β, α✝: Type ux✝, x, y: FreeMagma α✝ih1: id <\$> x = xih2: id <\$> y = yid <\$> (x * y) = x * yih2: id <\$> y = yih2α, β, α✝: Type ux✝, x, y: FreeMagma α✝ih1: id <\$> x = xih2: id <\$> y = yx * y = x * y]Goals accomplished! 🐙)

end Category

end FreeMagma

/-- `FreeMagma` is traversable. -/
protected def FreeMagma.traverse: {m : Type u → Type u} → [inst : Applicative m] → {α β : Type u} → (α → m β) → FreeMagma α → m (FreeMagma β)FreeMagma.traverse {m: Type u → Type um : Type u: Type (u+1)Type u → Type u: Type (u+1)Type u} [Applicative: (Type ?u.19765 → Type ?u.19764) → Type (max(?u.19765+1)?u.19764)Applicative m: Type u → Type um] {α: Type uα β: Type uβ : Type u: Type (u+1)Type u}
(F: α → m βF : α: Type uα → m: Type u → Type um β: Type uβ) : FreeMagma: Type ?u.19780 → Type ?u.19780FreeMagma α: Type uα → m: Type u → Type um (FreeMagma: Type ?u.19782 → Type ?u.19782FreeMagma β: Type uβ)
| FreeMagma.of: {α : Type ?u.19792} → α → FreeMagma αFreeMagma.of x: αx => FreeMagma.of: {α : Type ?u.19832} → α → FreeMagma αFreeMagma.of <\$> F: α → m βF x: αx
| x: FreeMagma αx * y: FreeMagma αy => (· * ·): FreeMagma β → FreeMagma β → FreeMagma β(· * ·) <\$> x: FreeMagma αx.traverse: {m : Type u → Type u} → [inst : Applicative m] → {α β : Type u} → (α → m β) → FreeMagma α → m (FreeMagma β)traverse F: α → m βF <*> y: FreeMagma αy.traverse: {m : Type u → Type u} → [inst : Applicative m] → {α β : Type u} → (α → m β) → FreeMagma α → m (FreeMagma β)traverse F: α → m βF
#align free_magma.traverse FreeMagma.traverse: {m : Type u → Type u} → [inst : Applicative m] → {α β : Type u} → (α → m β) → FreeMagma α → m (FreeMagma β)FreeMagma.traverse

protected def FreeAddMagma.traverse: {m : Type u → Type u} → [inst : Applicative m] → {α β : Type u} → (α → m β) → FreeAddMagma α → m (FreeAddMagma β)FreeAddMagma.traverse {m: Type u → Type um : Type u: Type (u+1)Type u → Type u: Type (u+1)Type u} [Applicative: (Type ?u.20600 → Type ?u.20599) → Type (max(?u.20600+1)?u.20599)Applicative m: Type u → Type um] {α: Type uα β: Type uβ : Type u: Type (u+1)Type u}
(F: α → m βF : α: Type uα → m: Type u → Type um β: Type uβ) : FreeAddMagma: Type ?u.20615 → Type ?u.20615FreeAddMagma α: Type uα → m: Type u → Type um (FreeAddMagma: Type ?u.20617 → Type ?u.20617FreeAddMagma β: Type uβ)
| x: FreeAddMagma αx + y: FreeAddMagma αy => (· + ·): FreeAddMagma β → FreeAddMagma β → FreeAddMagma β(· + ·) <\$> x: FreeAddMagma αx.traverse: {m : Type u → Type u} → [inst : Applicative m] → {α β : Type u} → (α → m β) → FreeAddMagma α → m (FreeAddMagma β)traverse F: α → m βF <*> y: FreeAddMagma αy.traverse: {m : Type u → Type u} → [inst : Applicative m] → {α β : Type u} → (α → m β) → FreeAddMagma α → m (FreeAddMagma β)traverse F: α → m βF
#align free_add_magma.traverse FreeAddMagma.traverse: {m : Type u → Type u} → [inst : Applicative m] → {α β : Type u} → (α → m β) → FreeAddMagma α → m (FreeAddMagma β)FreeAddMagma.traverse

attribute [to_additive: {m : Type u → Type u} → [inst : Applicative m] → {α β : Type u} → (α → m β) → FreeAddMagma α → m (FreeAddMagma β)to_additive existing] FreeMagma.traverse: {m : Type u → Type u} → [inst : Applicative m] → {α β : Type u} → (α → m β) → FreeMagma α → m (FreeMagma β)FreeMagma.traverse

namespace FreeMagma

variable {α: Type uα : Type u: Type (u+1)Type u}

section Category

variable {β: Type uβ : Type u: Type (u+1)Type u}

instance: Traversable FreeMagmainstance : Traversable: (Type ?u.21836 → Type ?u.21836) → Type (?u.21836+1)Traversable FreeMagma: Type ?u.21837 → Type ?u.21837FreeMagma := ⟨@FreeMagma.traverse: {m : Type ?u.21869 → Type ?u.21869} →
[inst : Applicative m] → {α β : Type ?u.21869} → (α → m β) → FreeMagma α → m (FreeMagma β)FreeMagma.traverse⟩

variable {m: Type u → Type um : Type u: Type (u+1)Type u → Type u: Type (u+1)Type u} [Applicative: (Type ?u.22245 → Type ?u.22244) → Type (max(?u.22245+1)?u.22244)Applicative m: Type u → Type um] (F: α → m βF : α: Type uα → m: Type u → Type um β: Type uβ)

@[to_additive: ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β) (x : α), traverse F (pure x) = pure <\$> F xto_additive (attr := simp)]
theorem traverse_pure: ∀ (x : α), traverse F (pure x) = pure <\$> F xtraverse_pure (x: ?m.22274x) : traverse: {t : Type ?u.22278 → Type ?u.22278} →
[self : Traversable t] →
{m : Type ?u.22278 → Type ?u.22278} → [inst : Applicative m] → {α β : Type ?u.22278} → (α → m β) → t α → m (t β)traverse F: α → m βF (pure: {f : Type ?u.22292 → Type ?u.22291} → [self : Pure f] → {α : Type ?u.22292} → α → f αpure x: ?m.22274x : FreeMagma: Type ?u.22290 → Type ?u.22290FreeMagma α: Type uα) = pure: {f : Type ?u.22358 → Type ?u.22357} → [self : Pure f] → {α : Type ?u.22358} → α → f αpure <\$> F: α → m βF x: ?m.22274x := rfl: ∀ {α : Sort ?u.22447} {a : α}, a = arfl
#align free_magma.traverse_pure FreeMagma.traverse_pure: ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β) (x : α), traverse F (pure x) = pure <\$> F xFreeMagma.traverse_pure

@[to_additive: ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β), traverse F ∘ pure = fun x => pure <\$> F xto_additive (attr := simp)]
theorem traverse_pure': ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β), traverse F ∘ pure = fun x => pure <\$> F xtraverse_pure' : traverse: {t : Type ?u.22588 → Type ?u.22588} →
[self : Traversable t] →
{m : Type ?u.22588 → Type ?u.22588} → [inst : Applicative m] → {α β : Type ?u.22588} → (α → m β) → t α → m (t β)traverse F: α → m βF ∘ pure: {f : Type ?u.22656 → Type ?u.22655} → [self : Pure f] → {α : Type ?u.22656} → α → f αpure = fun x: ?m.22708x ↦ (pure: {f : Type ?u.22738 → Type ?u.22737} → [self : Pure f] → {α : Type ?u.22738} → α → f αpure <\$> F: α → m βF x: ?m.22708x : m: Type u → Type um (FreeMagma: Type ?u.22711 → Type ?u.22711FreeMagma β: Type uβ)) := rfl: ∀ {α : Sort ?u.22860} {a : α}, a = arfl
#align free_magma.traverse_pure' FreeMagma.traverse_pure': ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β), traverse F ∘ pure = fun x => pure <\$> F xFreeMagma.traverse_pure'

@[to_additive: ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β) (x y : FreeAddMagma α),
traverse F (x + y) = Seq.seq ((fun x x_1 => x + x_1) <\$> traverse F x) fun x => traverse F yto_additive (attr := simp)]
theorem traverse_mul: ∀ (x y : FreeMagma α), traverse F (x * y) = Seq.seq ((fun x x_1 => x * x_1) <\$> traverse F x) fun x => traverse F ytraverse_mul (x: FreeMagma αx y: FreeMagma αy : FreeMagma: Type ?u.23007 → Type ?u.23007FreeMagma α: Type uα) :
traverse: {t : Type ?u.23011 → Type ?u.23011} →
[self : Traversable t] →
{m : Type ?u.23011 → Type ?u.23011} → [inst : Applicative m] → {α β : Type ?u.23011} → (α → m β) → t α → m (t β)traverse F: α → m βF (x: FreeMagma αx * y: FreeMagma αy) = (· * ·): FreeMagma β → FreeMagma β → FreeMagma β(· * ·) <\$> traverse: {t : Type ?u.23150 → Type ?u.23150} →
[self : Traversable t] →
{m : Type ?u.23150 → Type ?u.23150} → [inst : Applicative m] → {α β : Type ?u.23150} → (α → m β) → t α → m (t β)traverse F: α → m βF x: FreeMagma αx <*> traverse: {t : Type ?u.23211 → Type ?u.23211} →
[self : Traversable t] →
{m : Type ?u.23211 → Type ?u.23211} → [inst : Applicative m] → {α β : Type ?u.23211} → (α → m β) → t α → m (t β)traverse F: α → m βF y: FreeMagma αy := rfl: ∀ {α : Sort ?u.23289} {a : α}, a = arfl
#align free_magma.traverse_mul FreeMagma.traverse_mul: ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β) (x y : FreeMagma α),
traverse F (x * y) = Seq.seq ((fun x x_1 => x * x_1) <\$> traverse F x) fun x => traverse F yFreeMagma.traverse_mul

@[to_additive: ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β),
Seq.seq ((fun x x_1 => x + x_1) <\$> traverse F x) fun x => traverse F yto_additive (attr := simp)]
theorem traverse_mul': ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β),
Function.comp (traverse F) ∘ Mul.mul = fun x y =>
Seq.seq ((fun x x_1 => x * x_1) <\$> traverse F x) fun x => traverse F ytraverse_mul' :
Function.comp: {α : Sort ?u.23456} → {β : Sort ?u.23455} → {δ : Sort ?u.23454} → (β → δ) → (α → β) → α → δFunction.comp (traverse: {t : Type ?u.23465 → Type ?u.23465} →
[self : Traversable t] →
{m : Type ?u.23465 → Type ?u.23465} → [inst : Applicative m] → {α β : Type ?u.23465} → (α → m β) → t α → m (t β)traverse F: α → m βF) ∘ @Mul.mul: {α : Type ?u.23540} → [self : Mul α] → α → α → αMul.mul (FreeMagma: Type ?u.23541 → Type ?u.23541FreeMagma α: Type uα) _ = fun x: ?m.23569x y: ?m.23572y ↦
(· * ·): FreeMagma β → FreeMagma β → FreeMagma β(· * ·) <\$> traverse: {t : Type ?u.23633 → Type ?u.23633} →
[self : Traversable t] →
{m : Type ?u.23633 → Type ?u.23633} → [inst : Applicative m] → {α β : Type ?u.23633} → (α → m β) → t α → m (t β)traverse F: α → m βF x: ?m.23569x <*> traverse: {t : Type ?u.23707 → Type ?u.23707} →
[self : Traversable t] →
{m : Type ?u.23707 → Type ?u.23707} → [inst : Applicative m] → {α β : Type ?u.23707} → (α → m β) → t α → m (t β)traverse F: α → m βF y: ?m.23572y := rfl: ∀ {α : Sort ?u.23893} {a : α}, a = arfl
#align free_magma.traverse_mul' FreeMagma.traverse_mul': ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β),
Function.comp (traverse F) ∘ Mul.mul = fun x y =>
Seq.seq ((fun x x_1 => x * x_1) <\$> traverse F x) fun x => traverse F yFreeMagma.traverse_mul'

@[to_additive: ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β) (x : FreeAddMagma α),
theorem traverse_eq: ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β) (x : FreeMagma α),
FreeMagma.traverse F x = traverse F xtraverse_eq (x: FreeMagma αx) : FreeMagma.traverse: {m : Type ?u.24073 → Type ?u.24073} →
[inst : Applicative m] → {α β : Type ?u.24073} → (α → m β) → FreeMagma α → m (FreeMagma β)FreeMagma.traverse F: α → m βF x: ?m.24069x = traverse: {t : Type ?u.24092 → Type ?u.24092} →
[self : Traversable t] →
{m : Type ?u.24092 → Type ?u.24092} → [inst : Applicative m] → {α β : Type ?u.24092} → (α → m β) → t α → m (t β)traverse F: α → m βF x: ?m.24069x := rfl: ∀ {α : Sort ?u.24113} {a : α}, a = arfl
#align free_magma.traverse_eq FreeMagma.traverse_eq: ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β) (x : FreeMagma α),
FreeMagma.traverse F x = traverse F xFreeMagma.traverse_eq

-- Porting note: dsimp can not prove this
@[to_additive: ∀ {α : Type u} (x y : FreeAddMagma α), (Seq.seq ((fun x x_1 => x + x_1) <\$> x) fun x => y) = x + yto_additive (attr := simp, nolint simpNF: Std.Tactic.Lint.LintersimpNF)]
theorem mul_map_seq: ∀ {α : Type u} (x y : FreeMagma α), (Seq.seq ((fun x x_1 => x * x_1) <\$> x) fun x => y) = x * ymul_map_seq (x: FreeMagma αx y: FreeMagma αy : FreeMagma: Type ?u.24220 → Type ?u.24220FreeMagma α: Type uα) :
((· * ·): FreeMagma α → FreeMagma α → FreeMagma α(· * ·) <\$> x: FreeMagma αx <*> y: FreeMagma αy : Id: Type ?u.24225 → Type ?u.24225Id (FreeMagma: Type ?u.24226 → Type ?u.24226FreeMagma α: Type uα)) = (x: FreeMagma αx * y: FreeMagma αy : FreeMagma: Type ?u.24386 → Type ?u.24386FreeMagma α: Type uα) := rfl: ∀ {α : Sort ?u.24422} {a : α}, a = arfl
#align free_magma.mul_map_seq FreeMagma.mul_map_seq: ∀ {α : Type u} (x y : FreeMagma α), (Seq.seq ((fun x x_1 => x * x_1) <\$> x) fun x => y) = x * yFreeMagma.mul_map_seq

instance: IsLawfulTraversable FreeMagmainstance : IsLawfulTraversable: (t : Type ?u.24536 → Type ?u.24536) → [inst : Traversable t] → Type (?u.24536+1)IsLawfulTraversable FreeMagma: Type u → Type uFreeMagma.{u} :=
id_traverse := fun x: ?m.24604x ↦
FreeMagma.recOnPure: ∀ {α : Type ?u.24607} {C : FreeMagma α → Sort ?u.24606} (x : FreeMagma α),
(∀ (x : α), C (pure x)) → (∀ (x y : FreeMagma α), C x → C y → C (x * y)) → C xFreeMagma.recOnPure x: ?m.24604x (fun x: ?m.24884x ↦ rfl: ∀ {α : Sort ?u.24886} {a : α}, a = arfl) fun x: ?m.24914x y: ?m.24917y ih1: ?m.24920ih1 ih2: ?m.24923ih2 ↦ byGoals accomplished! 🐙
α, β: Type um: Type u → Type uinst✝: Applicative mF: α → m βsrc✝:= instLawfulMonadFreeMagmaInstMonadFreeMagma: LawfulMonad FreeMagmaα✝: Type ux✝, x, y: FreeMagma α✝ih1: traverse pure x = xih2: traverse pure y = ytraverse pure (x * y) = x * yrw [α, β: Type um: Type u → Type uinst✝: Applicative mF: α → m βsrc✝:= instLawfulMonadFreeMagmaInstMonadFreeMagma: LawfulMonad FreeMagmaα✝: Type ux✝, x, y: FreeMagma α✝ih1: traverse pure x = xih2: traverse pure y = ytraverse pure (x * y) = x * ytraverse_mul: ∀ {α β : Type ?u.25033} {m : Type ?u.25033 → Type ?u.25033} [inst : Applicative m] (F : α → m β) (x y : FreeMagma α),
comp_traverse := fun f: ?m.24660f g: ?m.24664g x: ?m.24668x ↦
FreeMagma.recOnPure: ∀ {α : Type ?u.24671} {C : FreeMagma α → Sort ?u.24670} (x : FreeMagma α),
(∀ (x : α), C (pure x)) → (∀ (x y : FreeMagma α), C x → C y → C (x * y)) → C xFreeMagma.recOnPure x: ?m.24668x
(fun x: ?m.24932x ↦ byGoals accomplished! 🐙 α, β: Type um: Type u → Type uinst✝⁴: Applicative mF: α → m βsrc✝:= instLawfulMonadFreeMagmaInstMonadFreeMagma: LawfulMonad FreeMagmaF✝, G✝: Type u → Type uinst✝³: Applicative F✝inst✝²: Applicative G✝inst✝¹: LawfulApplicative F✝inst✝: LawfulApplicative G✝α✝, β✝, γ✝: Type uf: β✝ → F✝ γ✝g: α✝ → G✝ β✝x✝: FreeMagma α✝x: α✝traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (pure x) = Functor.Comp.mk (traverse f <\$> traverse g (pure x))simp only [(. ∘ .), traverse_pure: ∀ {α β : Type ?u.25200} {m : Type ?u.25200 → Type ?u.25200} [inst : Applicative m] (F : α → m β) (x : α),
traverse F (pure x) = pure <\$> F xtraverse_pure, traverse_pure': ∀ {α β : Type ?u.25219} {m : Type ?u.25219 → Type ?u.25219} [inst : Applicative m] (F : α → m β),
traverse F ∘ pure = fun x => pure <\$> F xtraverse_pure', functor_norm]Goals accomplished! 🐙)
(fun x: ?m.24938x y: ?m.24941y ih1: ?m.24944ih1 ih2: ?m.24947ih2 ↦ byGoals accomplished! 🐙
α, β: Type um: Type u → Type uinst✝⁴: Applicative mF: α → m βsrc✝:= instLawfulMonadFreeMagmaInstMonadFreeMagma: LawfulMonad FreeMagmaF✝, G✝: Type u → Type uinst✝³: Applicative F✝inst✝²: Applicative G✝inst✝¹: LawfulApplicative F✝inst✝: LawfulApplicative G✝α✝, β✝, γ✝: Type uf: β✝ → F✝ γ✝g: α✝ → G✝ β✝x✝, x, y: FreeMagma α✝ih1: traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <\$> traverse g x)ih2: traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <\$> traverse g y)traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (x * y) = Functor.Comp.mk (traverse f <\$> traverse g (x * y))rw [α, β: Type um: Type u → Type uinst✝⁴: Applicative mF: α → m βsrc✝:= instLawfulMonadFreeMagmaInstMonadFreeMagma: LawfulMonad FreeMagmaF✝, G✝: Type u → Type uinst✝³: Applicative F✝inst✝²: Applicative G✝inst✝¹: LawfulApplicative F✝inst✝: LawfulApplicative G✝α✝, β✝, γ✝: Type uf: β✝ → F✝ γ✝g: α✝ → G✝ β✝x✝, x, y: FreeMagma α✝ih1: traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <\$> traverse g x)ih2: traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <\$> traverse g y)traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (x * y) = Functor.Comp.mk (traverse f <\$> traverse g (x * y))traverse_mul: ∀ {α β : Type ?u.25672} {m : Type ?u.25672 → Type ?u.25672} [inst : Applicative m] (F : α → m β) (x y : FreeMagma α),
traverse F (x * y) = Seq.seq ((fun x x_1 => x * x_1) <\$> traverse F x) fun x => traverse F ytraverse_mul,α, β: Type um: Type u → Type uinst✝⁴: Applicative mF: α → m βsrc✝:= instLawfulMonadFreeMagmaInstMonadFreeMagma: LawfulMonad FreeMagmaF✝, G✝: Type u → Type uinst✝³: Applicative F✝inst✝²: Applicative G✝inst✝¹: LawfulApplicative F✝inst✝: LawfulApplicative G✝α✝, β✝, γ✝: Type uf: β✝ → F✝ γ✝g: α✝ → G✝ β✝x✝, x, y: FreeMagma α✝ih1: traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <\$> traverse g x)ih2: traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <\$> traverse g y)(Seq.seq ((fun x x_1 => x * x_1) <\$> traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x) fun x =>
traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y) =   Functor.Comp.mk (traverse f <\$> traverse g (x * y)) α, β: Type um: Type u → Type uinst✝⁴: Applicative mF: α → m βsrc✝:= instLawfulMonadFreeMagmaInstMonadFreeMagma: LawfulMonad FreeMagmaF✝, G✝: Type u → Type uinst✝³: Applicative F✝inst✝²: Applicative G✝inst✝¹: LawfulApplicative F✝inst✝: LawfulApplicative G✝α✝, β✝, γ✝: Type uf: β✝ → F✝ γ✝g: α✝ → G✝ β✝x✝, x, y: FreeMagma α✝ih1: traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <\$> traverse g x)ih2: traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <\$> traverse g y)traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (x * y) = Functor.Comp.mk (traverse f <\$> traverse g (x * y))ih1: traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <\$> traverse g x)ih1,α, β: Type um: Type u → Type uinst✝⁴: Applicative mF: α → m βsrc✝:= instLawfulMonadFreeMagmaInstMonadFreeMagma: LawfulMonad FreeMagmaF✝, G✝: Type u → Type uinst✝³: Applicative F✝inst✝²: Applicative G✝inst✝¹: LawfulApplicative F✝inst✝: LawfulApplicative G✝α✝, β✝, γ✝: Type uf: β✝ → F✝ γ✝g: α✝ → G✝ β✝x✝, x, y: FreeMagma α✝ih1: traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <\$> traverse g x)ih2: traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <\$> traverse g y)(Seq.seq ((fun x x_1 => x * x_1) <\$> Functor.Comp.mk (traverse f <\$> traverse g x)) fun x =>
traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y) =   Functor.Comp.mk (traverse f <\$> traverse g (x * y)) α, β: Type um: Type u → Type uinst✝⁴: Applicative mF: α → m βsrc✝:= instLawfulMonadFreeMagmaInstMonadFreeMagma: LawfulMonad FreeMagmaF✝, G✝: Type u → Type uinst✝³: Applicative F✝inst✝²: Applicative G✝inst✝¹: LawfulApplicative F✝inst✝: LawfulApplicative G✝α✝, β✝, γ✝: Type uf: β✝ → F✝ γ✝g: α✝ → G✝ β✝x✝, x, y: FreeMagma α✝ih1: traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <\$> traverse g x)ih2: traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <\$> traverse g y)traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (x * y) = Functor.Comp.mk (traverse f <\$> traverse g (x * y))ih2: traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <\$> traverse g y)ih2,α, β: Type um: Type u → Type uinst✝⁴: Applicative mF: α → m βsrc✝:= instLawfulMonadFreeMagmaInstMonadFreeMagma: LawfulMonad FreeMagmaF✝, G✝: Type u → Type uinst✝³: Applicative F✝inst✝²: Applicative G✝inst✝¹: LawfulApplicative F✝inst✝: LawfulApplicative G✝α✝, β✝, γ✝: Type uf: β✝ → F✝ γ✝g: α✝ → G✝ β✝x✝, x, y: FreeMagma α✝ih1: traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <\$> traverse g x)ih2: traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <\$> traverse g y)(Seq.seq ((fun x x_1 => x * x_1) <\$> Functor.Comp.mk (traverse f <\$> traverse g x)) fun x =>
Functor.Comp.mk (traverse f <\$> traverse g y)) =   Functor.Comp.mk (traverse f <\$> traverse g (x * y)) α, β: Type um: Type u → Type uinst✝⁴: Applicative mF: α → m βsrc✝:= instLawfulMonadFreeMagmaInstMonadFreeMagma: LawfulMonad FreeMagmaF✝, G✝: Type u → Type uinst✝³: Applicative F✝inst✝²: Applicative G✝inst✝¹: LawfulApplicative F✝inst✝: LawfulApplicative G✝α✝, β✝, γ✝: Type uf: β✝ → F✝ γ✝g: α✝ → G✝ β✝x✝, x, y: FreeMagma α✝ih1: traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <\$> traverse g x)ih2: traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <\$> traverse g y)traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (x * y) = Functor.Comp.mk (traverse f <\$> traverse g (x * y))traverse_mul: ∀ {α β : Type ?u.25738} {m : Type ?u.25738 → Type ?u.25738} [inst : Applicative m] (F : α → m β) (x y : FreeMagma α),
traverse F (x * y) = Seq.seq ((fun x x_1 => x * x_1) <\$> traverse F x) fun x => traverse F ytraverse_mulα, β: Type um: Type u → Type uinst✝⁴: Applicative mF: α → m βsrc✝:= instLawfulMonadFreeMagmaInstMonadFreeMagma: LawfulMonad FreeMagmaF✝, G✝: Type u → Type uinst✝³: Applicative F✝inst✝²: Applicative G✝inst✝¹: LawfulApplicative F✝inst✝: LawfulApplicative G✝α✝, β✝, γ✝: Type uf: β✝ → F✝ γ✝g: α✝ → G✝ β✝x✝, x, y: FreeMagma α✝ih1: traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <\$> traverse g x)ih2: traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <\$> traverse g y)(Seq.seq ((fun x x_1 => x * x_1) <\$> Functor.Comp.mk (traverse f <\$> traverse g x)) fun x =>
Functor.Comp.mk (traverse f <\$> traverse g y)) =   Functor.Comp.mk (traverse f <\$> Seq.seq ((fun x x_1 => x * x_1) <\$> traverse g x) fun x => traverse g y)]α, β: Type um: Type u → Type uinst✝⁴: Applicative mF: α → m βsrc✝:= instLawfulMonadFreeMagmaInstMonadFreeMagma: LawfulMonad FreeMagmaF✝, G✝: Type u → Type uinst✝³: Applicative F✝inst✝²: Applicative G✝inst✝¹: LawfulApplicative F✝inst✝: LawfulApplicative G✝α✝, β✝, γ✝: Type uf: β✝ → F✝ γ✝g: α✝ → G✝ β✝x✝, x, y: FreeMagma α✝ih1: traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <\$> traverse g x)ih2: traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <\$> traverse g y)(Seq.seq ((fun x x_1 => x * x_1) <\$> Functor.Comp.mk (traverse f <\$> traverse g x)) fun x =>
Functor.Comp.mk (traverse f <\$> traverse g y)) =   Functor.Comp.mk (traverse f <\$> Seq.seq ((fun x x_1 => x * x_1) <\$> traverse g x) fun x => traverse g y);α, β: Type um: Type u → Type uinst✝⁴: Applicative mF: α → m βsrc✝:= instLawfulMonadFreeMagmaInstMonadFreeMagma: LawfulMonad FreeMagmaF✝, G✝: Type u → Type uinst✝³: Applicative F✝inst✝²: Applicative G✝inst✝¹: LawfulApplicative F✝inst✝: LawfulApplicative G✝α✝, β✝, γ✝: Type uf: β✝ → F✝ γ✝g: α✝ → G✝ β✝x✝, x, y: FreeMagma α✝ih1: traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <\$> traverse g x)ih2: traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <\$> traverse g y)(Seq.seq ((fun x x_1 => x * x_1) <\$> Functor.Comp.mk (traverse f <\$> traverse g x)) fun x =>
Functor.Comp.mk (traverse f <\$> traverse g y)) =   Functor.Comp.mk (traverse f <\$> Seq.seq ((fun x x_1 => x * x_1) <\$> traverse g x) fun x => traverse g y)
α, β: Type um: Type u → Type uinst✝⁴: Applicative mF: α → m βsrc✝:= instLawfulMonadFreeMagmaInstMonadFreeMagma: LawfulMonad FreeMagmaF✝, G✝: Type u → Type uinst✝³: Applicative F✝inst✝²: Applicative G✝inst✝¹: LawfulApplicative F✝inst✝: LawfulApplicative G✝α✝, β✝, γ✝: Type uf: β✝ → F✝ γ✝g: α✝ → G✝ β✝x✝, x, y: FreeMagma α✝ih1: traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <\$> traverse g x)ih2: traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <\$> traverse g y)traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (x * y) = Functor.Comp.mk (traverse f <\$> traverse g (x * y))simp [Functor.Comp.map_mk: ∀ {F : Type ?u.25834 → Type ?u.25832} {G : Type ?u.25833 → Type ?u.25834} [inst : Functor F] [inst_1 : Functor G]
{α β : Type ?u.25833} (h : α → β) (x : F (G α)),
h <\$> Functor.Comp.mk x = Functor.Comp.mk ((fun x x_1 => x <\$> x_1) h <\$> x)Functor.Comp.map_mk, Functor.map_map: ∀ {α β γ : Type ?u.25867} {f : Type ?u.25867 → Type ?u.25866} [inst : Functor f] [inst_1 : LawfulFunctor f] (m : α → β)
(g : β → γ) (x : f α), g <\$> m <\$> x = (g ∘ m) <\$> xFunctor.map_map, (. ∘ .), Comp.seq_mk: ∀ {α β : Type ?u.25899} {f : Type ?u.25901 → Type ?u.25900} {g : Type ?u.25899 → Type ?u.25901} [inst : Applicative f]
[inst_1 : Applicative g] (h : f (g (α → β))) (x : f (g α)),
(Seq.seq (Functor.Comp.mk h) fun x_1 => Functor.Comp.mk x) =     Functor.Comp.mk (Seq.seq ((fun x x_1 => Seq.seq x fun x => x_1) <\$> h) fun x_1 => x)Comp.seq_mk, seq_map_assoc: ∀ {α β γ : Type ?u.25934} {F : Type ?u.25934 → Type ?u.25933} [inst : Applicative F] [inst_1 : LawfulApplicative F]
(x : F (α → β)) (f : γ → α) (y : F γ), (Seq.seq x fun x => f <\$> y) = Seq.seq ((fun x => x ∘ f) <\$> x) fun x => yseq_map_assoc,
map_seq: ∀ {α β γ : Type ?u.25964} {F : Type ?u.25964 → Type ?u.25963} [inst : Applicative F] [inst_1 : LawfulApplicative F]
(f : β → γ) (x : F (α → β)) (y : F α), (f <\$> Seq.seq x fun x => y) = Seq.seq ((fun x => f ∘ x) <\$> x) fun x => ymap_seq, traverse_mul: ∀ {α β : Type ?u.25984} {m : Type ?u.25984 → Type ?u.25984} [inst : Applicative m] (F : α → m β) (x y : FreeMagma α),
traverse F (x * y) = Seq.seq ((fun x x_1 => x * x_1) <\$> traverse F x) fun x => traverse F ytraverse_mul]Goals accomplished! 🐙)
naturality := fun η: ?m.24796η α: ?m.24799α β: ?m.24802β f: ?m.24805f x: ?m.24809x ↦
FreeMagma.recOnPure: ∀ {α : Type ?u.24812} {C : FreeMagma α → Sort ?u.24811} (x : FreeMagma α),
(∀ (x : α), C (pure x)) → (∀ (x y : FreeMagma α), C x → C y → C (x * y)) → C xFreeMagma.recOnPure x: ?m.24809x
(fun x: ?m.25003x ↦ byGoals accomplished! 🐙 α✝, β✝: Type um: Type u → Type uinst✝⁴: Applicative mF: α✝ → m β✝src✝:= instLawfulMonadFreeMagmaInstMonadFreeMagma: LawfulMonad FreeMagmaF✝, G✝: Type u → Type uinst✝³: Applicative F✝inst✝²: Applicative G✝inst✝¹: LawfulApplicative F✝inst✝: LawfulApplicative G✝η: ApplicativeTransformation F✝ G✝α, β: Type uf: α → F✝ βx✝: FreeMagma αx: α(fun {α} => ApplicativeTransformation.app η α) (traverse f (pure x)) =   traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) (pure x)simp only [traverse_pure: ∀ {α β : Type ?u.42295} {m : Type ?u.42295 → Type ?u.42295} [inst : Applicative m] (F : α → m β) (x : α),
traverse F (pure x) = pure <\$> F xtraverse_pure, functor_norm, Function.comp_apply: ∀ {β : Sort ?u.42309} {δ : Sort ?u.42310} {α : Sort ?u.42311} {f : β → δ} {g : α → β} {x : α}, (f ∘ g) x = f (g x)Function.comp_apply]Goals accomplished! 🐙)
(fun x: ?m.25009x y: ?m.25012y ih1: ?m.25015ih1 ih2: ?m.25018ih2 ↦ byGoals accomplished! 🐙 α✝, β✝: Type um: Type u → Type uinst✝⁴: Applicative mF: α✝ → m β✝src✝:= instLawfulMonadFreeMagmaInstMonadFreeMagma: LawfulMonad FreeMagmaF✝, G✝: Type u → Type uinst✝³: Applicative F✝inst✝²: Applicative G✝inst✝¹: LawfulApplicative F✝inst✝: LawfulApplicative G✝η: ApplicativeTransformation F✝ G✝α, β: Type uf: α → F✝ βx✝, x, y: FreeMagma αih1: (fun {α} => ApplicativeTransformation.app η α) (traverse f x) =   traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) xih2: (fun {α} => ApplicativeTransformation.app η α) (traverse f y) =   traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) y(fun {α} => ApplicativeTransformation.app η α) (traverse f (x * y)) =   traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) (x * y)simp only [traverse_mul: ∀ {α β : Type ?u.42516} {m : Type ?u.42516 → Type ?u.42516} [inst : Applicative m] (F : α → m β) (x y : FreeMagma α),
traverse F (x * y) = Seq.seq ((fun x x_1 => x * x_1) <\$> traverse F x) fun x => traverse F ytraverse_mul, functor_norm, ih1: (fun {α} => ApplicativeTransformation.app η α) (traverse f x) =   traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) xih1, ih2: (fun {α} => ApplicativeTransformation.app η α) (traverse f y) =   traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) yih2]Goals accomplished! 🐙)
traverse_eq_map_id := fun f: ?m.24737f x: ?m.24741x ↦
FreeMagma.recOnPure: ∀ {α : Type ?u.24744} {C : FreeMagma α → Sort ?u.24743} (x : FreeMagma α),
(∀ (x : α), C (pure x)) → (∀ (x y : FreeMagma α), C x → C y → C (x * y)) → C xFreeMagma.recOnPure x: ?m.24741x (fun _: ?m.24956_ ↦ rfl: ∀ {α : Sort ?u.24958} {a : α}, a = arfl) fun x: ?m.24985x y: ?m.24988y ih1: ?m.24991ih1 ih2: ?m.24994ih2 ↦ byGoals accomplished! 🐙
α, β: Type um: Type u → Type uinst✝: Applicative mF: α → m βsrc✝:= instLawfulMonadFreeMagmaInstMonadFreeMagma: LawfulMonad FreeMagmaα✝, β✝: Type uf: α✝ → β✝x✝, x, y: FreeMagma α✝ih1: traverse (pure ∘ f) x = id.mk (f <\$> x)ih2: traverse (pure ∘ f) y = id.mk (f <\$> y)traverse (pure ∘ f) (x * y) = id.mk (f <\$> (x * y))rw [α, β: Type um: Type u → Type uinst✝: Applicative mF: α → m βsrc✝:= instLawfulMonadFreeMagmaInstMonadFreeMagma: LawfulMonad FreeMagmaα✝, β✝: Type uf: α✝ → β✝x✝, x, y: FreeMagma α✝ih1: traverse (pure ∘ f) x = id.mk (f <\$> x)ih2: traverse (pure ∘ f) y = id.mk (f <\$> y)traverse (pure ∘ f) (x * y) = id.mk (f <\$> (x * y))traverse_mul: ∀ {α β : Type ?u.42151} {m : Type ?u.42151 → Type ?u.42151} [inst : Applicative m] (F : α → m β) (x y : FreeMagma α),

end Category

end FreeMagma

-- Porting note: changed String to Lean.Format
/-- Representation of an element of a free magma. -/
protected def FreeMagma.repr: {α : Type u} → [inst : Repr α] → FreeMagma α → Lean.FormatFreeMagma.repr {α: Type uα : Type u: Type (u+1)Type u} [Repr: Type ?u.43631 → Type ?u.43631Repr α: Type uα] : FreeMagma: Type ?u.43635 → Type ?u.43635FreeMagma α: Type uα → Lean.Format: TypeLean.Format
| FreeMagma.of: {α : Type ?u.43643} → α → FreeMagma αFreeMagma.of x: αx => repr: {α : Type ?u.43658} → [inst : Repr α] → α → Lean.Formatrepr x: αx
| x: FreeMagma αx * y: FreeMagma αy => "( ": String"( " ++ x: FreeMagma αx.repr: {α : Type u} → [inst : Repr α] → FreeMagma α → Lean.Formatrepr ++ " * ": String" * " ++ y: FreeMagma αy.repr: {α : Type u} → [inst : Repr α] → FreeMagma α → Lean.Formatrepr ++ " )": String" )"
#align free_magma.repr FreeMagma.repr: {α : Type u} → [inst : Repr α] → FreeMagma α → Lean.FormatFreeMagma.repr

/-- Representation of an element of a free additive magma. -/
protected def FreeAddMagma.repr: {α : Type u} → [inst : Repr α] → FreeAddMagma α → Lean.FormatFreeAddMagma.repr {α: Type uα : Type u: Type (u+1)Type u} [Repr: Type ?u.44607 → Type ?u.44607Repr α: Type uα] : FreeAddMagma: Type ?u.44611 → Type ?u.44611FreeAddMagma α: Type uα → Lean.Format: TypeLean.Format
| FreeAddMagma.of: {α : Type ?u.44619} → α → FreeAddMagma αFreeAddMagma.of x: αx => repr: {α : Type ?u.44634} → [inst : Repr α] → α → Lean.Formatrepr x: αx
| x: FreeAddMagma αx + y: FreeAddMagma αy => "( ": String"( " ++ x: FreeAddMagma αx.repr: {α : Type u} → [inst : Repr α] → FreeAddMagma α → Lean.Formatrepr ++ " + ": String" + " ++ y: FreeAddMagma αy.repr: {α : Type u} → [inst : Repr α] → FreeAddMagma α → Lean.Formatrepr ++ " )": String" )"

attribute [to_additive: {α : Type u} → [inst : Repr α] → FreeAddMagma α → Lean.Formatto_additive existing] FreeMagma.repr: {α : Type u} → [inst : Repr α] → FreeMagma α → Lean.FormatFreeMagma.repr

instance: {α : Type u} → [inst : Repr α] → Repr (FreeMagma α)instance {α: Type uα : Type u: Type (u+1)Type u} [Repr: Type ?u.45821 → Type ?u.45821Repr α: Type uα] : Repr: Type ?u.45824 → Type ?u.45824Repr (FreeMagma: Type ?u.45825 → Type ?u.45825FreeMagma α: Type uα) := ⟨fun o: ?m.45835o _: ?m.45838_ => FreeMagma.repr: {α : Type ?u.45840} → [inst : Repr α] → FreeMagma α → Lean.FormatFreeMagma.repr o: ?m.45835o⟩

/-- Length of an element of a free magma. -/
def FreeMagma.length: {α : Type u} → FreeMagma α → ℕFreeMagma.length {α: Type uα : Type u: Type (u+1)Type u} : FreeMagma: Type ?u.45983 → Type ?u.45983FreeMagma α: Type uα → ℕ: Typeℕ
| FreeMagma.of: {α : Type ?u.45990} → α → FreeMagma αFreeMagma.of _x: α_x => 1: ?m.460061
| x: FreeMagma αx * y: FreeMagma αy => x: FreeMagma αx.length: {α : Type u} → FreeMagma α → ℕlength + y: FreeMagma αy.length: {α : Type u} → FreeMagma α → ℕlength
#align free_magma.length FreeMagma.length: {α : Type u} → FreeMagma α → ℕFreeMagma.length

/-- Length of an element of a free additive magma. -/
def FreeAddMagma.length: {α : Type u} → FreeAddMagma α → ℕFreeAddMagma.length {α: Type uα : Type u: Type (u+1)Type u} : FreeAddMagma: Type ?u.46419 → Type ?u.46419FreeAddMagma α: Type uα → ℕ: Typeℕ
| x: FreeAddMagma αx + y: FreeAddMagma αy => x: FreeAddMagma αx.length: {α : Type u} → FreeAddMagma α → ℕlength + y: FreeAddMagma αy.length: {α : Type u} → FreeAddMagma α → ℕlength

attribute [to_additive: {α : Type u} → FreeAddMagma α → ℕto_additive existing (attr := simp)] FreeMagma.length: {α : Type u} → FreeMagma α → ℕFreeMagma.length

/-- Associativity relations for an additive magma. -/
inductive AddMagma.AssocRel: (α : Type u) → [inst : Add α] → α → α → PropAddMagma.AssocRel (α: Type uα : Type u: Type (u+1)Type u) [Add: Type ?u.47130 → Type ?u.47130Add α: Type uα] : α: Type uα → α: Type uα → Prop: TypeProp
| intro: ∀ {α : Type u} [inst : Add α] (x y z : α), AssocRel α (x + y + z) (x + (y + z))intro : ∀ x: ?m.47144x y: ?m.47147y z: ?m.47150z, AddMagma.AssocRel: (α : Type u) → [inst : Add α] → α → α → PropAddMagma.AssocRel α: Type uα (x: ?m.47144x + y: ?m.47147y + z: ?m.47150z) (x: ?m.47144x + (y: ?m.47147y + z: ?m.47150z))
| left: ∀ {α : Type u} [inst : Add α] (w x y z : α), AssocRel α (w + (x + y + z)) (w + (x + (y + z)))left : ∀ w: ?m.47282w x: ?m.47285x y: ?m.47288y z: ?m.47291z, AddMagma.AssocRel: (α : Type u) → [inst : Add α] → α → α → PropAddMagma.AssocRel α: Type uα (w: ?m.47282w + (x: ?m.47285x + y: ?m.47288y + z: ?m.47291z)) (w: ?m.47282w + (x: ?m.47285x + (y: ?m.47288y + z: ?m.47291z)))

/-- Associativity relations for a magma. -/
inductive Magma.AssocRel: (α : Type u) → [inst : Mul α] → α → α → PropMagma.AssocRel (α: Type uα : Type u: Type (u+1)Type u) [Mul: Type ?u.47493 → Type ?u.47493Mul α: Type uα] : α: Type uα → α: Type uα → Prop: TypeProp
| intro: ∀ {α : Type u} [inst : Mul α] (x y z : α), AssocRel α (x * y * z) (x * (y * z))intro : ∀ x: ?m.47507x y: ?m.47510y z: ?m.47513z, Magma.AssocRel: (α : Type u) → [inst : Mul α] → α → α → PropMagma.AssocRel α: Type uα (x: ?m.47507x * y: ?m.47510y * z: ?m.47513z) (x: ?m.47507x * (y: ?m.47510y * z: ?m.47513z))
| left: ∀ {α : Type u} [inst : Mul α] (w x y z : α), AssocRel α (w * (x * y * z)) (w * (x * (y * z)))left : ∀ w: ?m.47669w x: ?m.47672x y: ?m.47675y z: ?m.47678z, Magma.AssocRel: (α : Type u) → [inst : Mul α] → α → α → PropMagma.AssocRel α: Type uα (w: ?m.47669w * (x: ?m.47672x * y: ?m.47675y * z: ?m.47678z)) (w: ?m.47669w * (x: ?m.47672x * (y: ?m.47675y * z: ?m.47678z)))
#align magma.assoc_rel Magma.AssocRel: (α : Type u) → [inst : Mul α] → α → α → PropMagma.AssocRel

namespace Magma

/-- Semigroup quotient of a magma. -/
def AssocQuotient: (α : Type u) → [inst : Mul α] → Type uAssocQuotient (α: Type uα : Type u: Type (u+1)Type u) [Mul: Type ?u.47908 → Type ?u.47908Mul α: Type uα] : Type u: Type (u+1)Type u :=
Quot: {α : Sort ?u.47914} → (α → α → Prop) → Sort ?u.47914Quot <| AssocRel: (α : Type ?u.47916) → [inst : Mul α] → α → α → PropAssocRel α: Type uα
#align magma.assoc_quotient Magma.AssocQuotient: (α : Type u) → [inst : Mul α] → Type uMagma.AssocQuotient

namespace AssocQuotient

variable {α: Type uα : Type u: Type (u+1)Type u} [Mul: Type ?u.51434 → Type ?u.51434Mul α: Type uα]

@[to_additive: ∀ {α : Type u} [inst : Add α] (x y z : α),
Quot.mk (AddMagma.AssocRel α) (x + y + z) = Quot.mk (AddMagma.AssocRel α) (x + (y + z))to_additive]
theorem quot_mk_assoc: ∀ (x y z : α), Quot.mk (AssocRel α) (x * y * z) = Quot.mk (AssocRel α) (x * (y * z))quot_mk_assoc (x: αx y: αy z: αz : α: Type uα) : Quot.mk: {α : Sort ?u.47967} → (r : α → α → Prop) → α → Quot rQuot.mk (AssocRel: (α : Type ?u.47969) → [inst : Mul α] → α → α → PropAssocRel α: Type uα) (x: αx * y: αy * z: αz) = Quot.mk: {α : Sort ?u.48062} → (r : α → α → Prop) → α → Quot rQuot.mk _: ?m.48063 → ?m.48063 → Prop_ (x: αx * (y: αy * z: αz)) :=
Quot.sound: ∀ {α : Sort ?u.48157} {r : α → α → Prop} {a b : α}, r a b → Quot.mk r a = Quot.mk r bQuot.sound (AssocRel.intro: ∀ {α : Type ?u.48172} [inst : Mul α] (x y z : α), AssocRel α (x * y * z) (x * (y * z))AssocRel.intro _: ?m.48173_ _: ?m.48173_ _: ?m.48173_)
#align magma.assoc_quotient.quot_mk_assoc Magma.AssocQuotient.quot_mk_assoc: ∀ {α : Type u} [inst : Mul α] (x y z : α), Quot.mk (AssocRel α) (x * y * z) = Quot.mk (AssocRel α) (x * (y * z))Magma.AssocQuotient.quot_mk_assoc

@[to_additive: ∀ {α : Type u} [inst : Add α] (x y z w : α),
Quot.mk (AddMagma.AssocRel α) (x + (y + z + w)) = Quot.mk (AddMagma.AssocRel α) (x + (y + (z + w)))to_additive]
theorem quot_mk_assoc_left: ∀ (x y z w : α), Quot.mk (AssocRel α) (x * (y * z * w)) = Quot.mk (AssocRel α) (x * (y * (z * w)))quot_mk_assoc_left (x: αx y: αy z: αz w: αw : α: Type uα) :
Quot.mk: {α : Sort ?u.48252} → (r : α → α → Prop) → α → Quot rQuot.mk (AssocRel: (α : Type ?u.48254) → [inst : Mul α] → α → α → PropAssocRel α: Type uα) (x: αx * (y: αy * z: αz * w: αw)) = Quot.mk: {α : Sort ?u.48375} → (r : α → α → Prop) → α → Quot rQuot.mk _: ?m.48376 → ?m.48376 → Prop_ (x: αx * (y: αy * (z: αz * w: αw))) :=
Quot.sound: ∀ {α : Sort ?u.48499} {r : α → α → Prop} {a b : α}, r a b → Quot.mk r a = Quot.mk r bQuot.sound (AssocRel.left: ∀ {α : Type ?u.48514} [inst : Mul α] (w x y z : α), AssocRel α (w * (x * y * z)) (w * (x * (y * z)))AssocRel.left _: ?m.48515_ _: ?m.48515_ _: ?m.48515_ _: ?m.48515_)
#align magma.assoc_quotient.quot_mk_assoc_left Magma.AssocQuotient.quot_mk_assoc_left: ∀ {α : Type u} [inst : Mul α] (x y z w : α),
Quot.mk (AssocRel α) (x * (y * z * w)) = Quot.mk (AssocRel α) (x * (y * (z * w)))Magma.AssocQuotient.quot_mk_assoc_left

instance: {α : Type u} → [inst : Mul α] → Semigroup (AssocQuotient α)instance : Semigroup: Type ?u.48591 → Type ?u.48591Semigroup (AssocQuotient: (α : Type ?u.48592) → [inst : Mul α] → Type ?u.48592AssocQuotient α: Type uα) where
mul x: ?m.48611x y: ?m.48614y := byGoals accomplished! 🐙
α: Type uinst✝: Mul αx, y: AssocQuotient αAssocQuotient αrefine' Quot.liftOn₂: {α : Sort ?u.48802} →
{β : Sort ?u.48801} →
{γ : Sort ?u.48800} →
{r : α → α → Prop} →
{s : β → β → Prop} →
Quot r →
Quot s →
(f : α → β → γ) →
(∀ (a : α) (b₁ b₂ : β), s b₁ b₂ → f a b₁ = f a b₂) →
(∀ (a₁ a₂ : α) (b : β), r a₁ a₂ → f a₁ b = f a₂ b) → γQuot.liftOn₂ x: AssocQuotient αx y: AssocQuotient αy (fun x: ?m.48821x y: ?m.48824y ↦ Quot.mk: {α : Sort ?u.48826} → (r : α → α → Prop) → α → Quot rQuot.mk _: ?m.48827 → ?m.48827 → Prop_ (x: ?m.48821x * y: ?m.48824y)) _: ∀ (a : ?m.48803) (b₁ b₂ : ?m.48804),
?m.48807 b₁ b₂ → (fun x y => Quot.mk (AssocRel α) (x * y)) a b₁ = (fun x y => Quot.mk (AssocRel α) (x * y)) a b₂_ _: ∀ (a₁ a₂ : ?m.48803) (b : ?m.48804),
?m.48806 a₁ a₂ → (fun x y => Quot.mk (AssocRel α) (x * y)) a₁ b = (fun x y => Quot.mk (AssocRel α) (x * y)) a₂ b_α: Type uinst✝: Mul αx, y: AssocQuotient αrefine'_1∀ (a b₁ b₂ : α),
AssocRel α b₁ b₂ → (fun x y => Quot.mk (AssocRel α) (x * y)) a b₁ = (fun x y => Quot.mk (AssocRel α) (x * y)) a b₂α: Type uinst✝: Mul αx, y: AssocQuotient αrefine'_2∀ (a₁ a₂ b : α),
AssocRel α a₁ a₂ → (fun x y => Quot.mk (AssocRel α) (x * y)) a₁ b = (fun x y => Quot.mk (AssocRel α) (x * y)) a₂ b
α: Type uinst✝: Mul αx, y: AssocQuotient αAssocQuotient α·α: Type uinst✝: Mul αx, y: AssocQuotient αrefine'_1∀ (a b₁ b₂ : α),
AssocRel α b₁ b₂ → (fun x y => Quot.mk (AssocRel α) (x * y)) a b₁ = (fun x y => Quot.mk (AssocRel α) (x * y)) a b₂ α: Type uinst✝: Mul αx, y: AssocQuotient αrefine'_1∀ (a b₁ b₂ : α),
AssocRel α b₁ b₂ → (fun x y => Quot.mk (AssocRel α) (x * y)) a b₁ = (fun x y => Quot.mk (AssocRel α) (x * y)) a b₂α: Type uinst✝: Mul αx, y: AssocQuotient αrefine'_2∀ (a₁ a₂ b : α),
AssocRel α a₁ a₂ → (fun x y => Quot.mk (AssocRel α) (x * y)) a₁ b = (fun x y => Quot.mk (AssocRel α) (x * y)) a₂ brintro a: ?m.48803a b₁: ?m.48804b₁ b₂: ?m.48804b₂ (⟨c, d, e⟩ | ⟨c, d, e, f⟩): ?m.48807 b₁ b₂(⟨c, d, e⟩ | ⟨c, d, e, f⟩: ?m.48807 b₁ b₂⟨c: αc⟨c, d, e⟩ | ⟨c, d, e, f⟩: ?m.48807 b₁ b₂, d: αd⟨c, d, e⟩ | ⟨c, d, e, f⟩: ?m.48807 b₁ b₂, e: αe⟨c, d, e⟩ | ⟨c, d, e, f⟩: ?m.48807 b₁ b₂⟩ | ⟨c: αc⟨c, d, e⟩ | ⟨c, d, e, f⟩: ?m.48807 b₁ b₂, d: αd⟨c, d, e⟩ | ⟨c, d, e, f⟩: ?m.48807 b₁ b₂, e: αe⟨c, d, e⟩ | ⟨c, d, e, f⟩: ?m.48807 b₁ b₂, f: αf⟨c, d, e⟩ | ⟨c, d, e, f⟩: ?m.48807 b₁ b₂⟩(⟨c, d, e⟩ | ⟨c, d, e, f⟩): ?m.48807 b₁ b₂)α: Type uinst✝: Mul αx, y: AssocQuotient αa, c, d, e: αrefine'_1.intro(fun x y => Quot.mk (AssocRel α) (x * y)) a (c * d * e) = (fun x y => Quot.mk (AssocRel α) (x * y)) a (c * (d * e))α: Type uinst✝: Mul αx, y: AssocQuotient αa, c, d, e, f: αrefine'_1.left(fun x y => Quot.mk (AssocRel α) (x * y)) a (c * (d * e * f)) =   (fun x y => Quot.mk (AssocRel α) (x * y)) a (c * (d * (e * f))) α: Type uinst✝: Mul αx, y: AssocQuotient αrefine'_1∀ (a b₁ b₂ : α),
AssocRel α b₁ b₂ → (fun x y => Quot.mk (AssocRel α) (x * y)) a b₁ = (fun x y => Quot.mk (AssocRel α) (x * y)) a b₂<;>α: Type uinst✝: Mul αx, y: AssocQuotient αa, c, d, e: αrefine'_1.intro(fun x y => Quot.mk (AssocRel α) (x * y)) a (c * d * e) = (fun x y => Quot.mk (AssocRel α) (x * y)) a (c * (d * e))α: Type uinst✝: Mul αx, y: AssocQuotient αa, c, d, e, f: αrefine'_1.left(fun x y => Quot.mk (AssocRel α) (x * y)) a (c * (d * e * f)) =   (fun x y => Quot.mk (AssocRel α) (x * y)) a (c * (d * (e * f))) α: Type uinst✝: Mul αx, y: AssocQuotient αrefine'_1∀ (a b₁ b₂ : α),
AssocRel α b₁ b₂ → (fun x y => Quot.mk (AssocRel α) (x * y)) a b₁ = (fun x y => Quot.mk (AssocRel α) (x * y)) a b₂simp onlyα: Type uinst✝: Mul αx, y: AssocQuotient αa, c, d, e: αrefine'_1.introQuot.mk (AssocRel α) (a * (c * d * e)) = Quot.mk (AssocRel α) (a * (c * (d * e)))
α: Type uinst✝: Mul αx, y: AssocQuotient αrefine'_1∀ (a b₁ b₂ : α),
AssocRel α b₁ b₂ → (fun x y => Quot.mk (AssocRel α) (x * y)) a b₁ = (fun x y => Quot.mk (AssocRel α) (x * y)) a b₂·α: Type uinst✝: Mul αx, y: AssocQuotient αa, c, d, e: αrefine'_1.introQuot.mk (AssocRel α) (a * (c * d * e)) = Quot.mk (AssocRel α) (a * (c * (d * e))) α: Type uinst✝: Mul αx, y: AssocQuotient αa, c, d, e: αrefine'_1.introQuot.mk (AssocRel α) (a * (c * d * e)) = Quot.mk (AssocRel α) (a * (c * (d * e)))α: Type uinst✝: Mul αx, y: AssocQuotient αa, c, d, e, f: αrefine'_1.leftQuot.mk (AssocRel α) (a * (c * (d * e * ```