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
Cmd instead of
Ctrl .
/-
Copyright (c) 2019 Kenny Lau. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kenny Lau
! This file was ported from Lean 3 source module algebra.free
! leanprover-community/mathlib commit 6d0adfa76594f304b4650d098273d4366edeb61b
! 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 u
| of : α → FreeAddMagma α
| add : FreeAddMagma α → FreeAddMagma α → FreeAddMagma α
deriving DecidableEq
#align free_add_magma FreeAddMagma
compile_inductive% FreeAddMagma
/-- Free magma over a given alphabet. -/
@[ to_additive ]
inductive FreeMagma ( α : Type u ) : Type u
| of : α → FreeMagma α
| mul : FreeMagma α → FreeMagma α → FreeMagma α
deriving DecidableEq
#align free_magma FreeMagma
compile_inductive% FreeMagma
namespace FreeMagma
variable { α : Type u }
@[ to_additive ]
instance [ Inhabited : Sort ?u.5896 → Sort (max1?u.5896) α ] : Inhabited : Sort ?u.5899 → Sort (max1?u.5899) ( FreeMagma α ) := ⟨ of default ⟩
@[ to_additive ]
instance : Mul ( FreeMagma α ) := ⟨ FreeMagma.mul ⟩
-- Porting note: invalid attribute 'match_pattern', declaration is in an imported module
-- attribute [match_pattern] Mul.mul
@[ to_additive ( attr := simp )]
theorem mul_eq ( x y : FreeMagma α ) : mul x y = x * y := rfl : ∀ {α : Sort ?u.6316} {a : α }, a = a
#align free_magma.mul_eq FreeMagma.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 ] FreeAddMagma.add.sizeOf_spec
attribute [ nolint simpNF ] FreeMagma.mul.sizeOf_spec
attribute [ nolint simpNF ] FreeAddMagma.add.injEq
attribute [ nolint simpNF ] FreeMagma.mul.injEq
/-- Recursor for `FreeMagma` using `x * y` instead of `FreeMagma.mul x y`. -/
@[ to_additive ( attr := elab_as_elim) "Recursor for `FreeAddMagma` using `x + y` instead of
`FreeAddMagma.add x y`."]
def recOnMul { C : FreeMagma α → Sort l } ( x ) ( ih1 : ∀ x , C ( of x ))
( ih2 : ∀ x y , C x → C y → C ( x * y )) : C x :=
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 t x ih1 ih2
#align free_magma.rec_on_mul FreeMagma.recOnMul
@[ to_additive ( attr := ext 1100)]
theorem hom_ext { β : Type v } [ Mul β ] { f g : FreeMagma α →ₙ* β } ( h : f ∘ of = g ∘ of ) : f = g :=
( FunLike.ext : ∀ {F : Sort ?u.7339} {α : Sort ?u.7340} {β : α → Sort ?u.7338i : FunLike F α β f g : F ),
(∀ (x : α ), ↑f x = ↑g x ) → f = g _ _ ) fun x ↦ recOnMul x ( congr_fun : ∀ {α : Sort ?u.7629} {β : α → Sort ?u.7628f g : (x : α ) → β x }, f = g ∀ (a : α ), f a = g a h ) <| by ∀ (x y : FreeMagma α ↑f x = ↑g x ↑f y = ↑g y ↑f (x * y = ↑g (x * y intros ↑f (x✝ * y✝ = ↑g (x✝ * y✝ ∀ (x y : FreeMagma α ↑f x = ↑g x ↑f y = ↑g y ↑f (x * y = ↑g (x * y ; ↑f (x✝ * y✝ = ↑g (x✝ * y✝ ∀ (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 y , *]
#align free_magma.hom_ext FreeMagma.hom_ext
end FreeMagma
/-- Lifts a function `α → β` to a magma homomorphism `FreeMagma α → β` given a magma `β`. -/
def FreeMagma.liftAux { α : Type u } { β : Type v } [ Mul β ] ( f : α → β ) : FreeMagma α → β
| FreeMagma.of x => f x
| x * y => liftAux f x * liftAux f y
#align free_magma.lift_aux FreeMagma.liftAux
/-- Lifts a function `α → β` to an additive magma homomorphism `FreeAddMagma α → β` given
an additive magma `β`. -/
def FreeAddMagma.liftAux { α : Type u } { β : Type v } [ Add β ] ( f : α → β ) : FreeAddMagma : Type ?u.8704 → Type ?u.8704 α → β
| FreeAddMagma.of x => f x
| x + y => liftAux f x + liftAux f y
#align free_add_magma.lift_aux FreeAddMagma.liftAux
attribute [ to_additive existing ] FreeMagma.liftAux
namespace FreeMagma
section lift
variable { α : Type u } { β : Type v } [ Mul β ] ( f : α → β )
/-- The universal property of the free magma expressing its adjointness. -/
@[ to_additive ( attr := simps symm_apply )
"The universal property of the free additive magma expressing its adjointness."]
def lift : ( α → β ) ≃ ( FreeMagma α →ₙ* β ) where
toFun f :=
{ toFun := liftAux f
map_mul' := fun x y ↦ rfl : ∀ {α : Sort ?u.9989} {a : α }, a = a }
invFun F := F ∘ of
left_inv f := by rfl
-- Porting note: replaced ext by FreeMagma.hom_ext
right_inv F := FreeMagma.hom_ext ( rfl : ∀ {α : Sort ?u.10304} {a : α }, a = a )
#align free_magma.lift FreeMagma.lift
@[ to_additive ( attr := simp )]
theorem lift_of : ∀ (x : α ), ↑(↑lift f ) (of x = f x lift_of ( x ) : lift f ( of x ) = f x := rfl : ∀ {α : Sort ?u.11146} {a : α }, a = a
#align free_magma.lift_of FreeMagma.lift_of : ∀ {α : Type u} {β : Type v} [inst : Mul β f : α → β x : α ), ↑(↑lift f ) (of x = f x
@[ to_additive : ∀ {α : Type u} {β : Type v} [inst : Add β f : α → β ↑(↑FreeAddMagma.lift f ) ∘ FreeAddMagma.of = f to_additive ( attr := simp )]
theorem lift_comp_of : ↑(↑lift f ) ∘ of = f lift_comp_of : lift f ∘ of = f := rfl : ∀ {α : Sort ?u.11685} {a : α }, a = a
#align free_magma.lift_comp_of FreeMagma.lift_comp_of : ∀ {α : Type u} {β : Type v} [inst : Mul β f : α → β ↑(↑lift f ) ∘ of = f
@[ to_additive ( attr := simp )]
theorem lift_comp_of' ( f : FreeMagma : Type ?u.11841 → Type ?u.11841 α →ₙ* β ) : lift ( f ∘ of ) = f := lift . apply_symm_apply : ∀ {α : Sort ?u.12271} {β : Sort ?u.12270} (e : α ≃ β x : β ), ↑e (↑e .symmx ) = x f
#align free_magma.lift_comp_of' FreeMagma.lift_comp_of'
end lift
section Map
variable { α : Type u } { β : Type v } ( f : α → β )
/-- The unique magma homomorphism `FreeMagma α →ₙ* FreeMagma β` that sends
each `of x` to `of (f x)`. -/
@[ to_additive "The unique additive magma homomorphism `FreeAddMagma α → FreeAddMagma β` that sends
each `of x` to `of (f x)`."]
def map ( f : α → β ) : FreeMagma : Type ?u.12444 → Type ?u.12444 α →ₙ* FreeMagma : Type ?u.12445 → Type ?u.12445 β := lift ( of ∘ f )
#align free_magma.map FreeMagma.map
@[ to_additive ( attr := simp )]
theorem map_of : ∀ {α : Type u} {β : Type v} (f : α → β x : α ), ↑(map f of x = of (f x map_of ( x ) : map f ( of x ) = of ( f x ) := rfl : ∀ {α : Sort ?u.13234} {a : α }, a = a
#align free_magma.map_of FreeMagma.map_of : ∀ {α : Type u} {β : Type v} (f : α → β x : α ), ↑(map f of x = of (f x
end Map
section Category
variable { α β : Type u }
@[ to_additive ]
instance : Monad : (Type ?u.13345 → Type ?u.13344Type (max(?u.13345+1)?u.13344) FreeMagma : Type ?u.13346 → Type ?u.13346 where
pure := of
bind x f := lift f x
/-- Recursor on `FreeMagma` using `pure` instead of `of`. -/
@[ to_additive ( attr := elab_as_elim) "Recursor on `FreeAddMagma` using `pure` instead of `of`."]
protected def recOnPure { C : FreeMagma : Type ?u.16907 → Type ?u.16907 α → Sort l } ( x ) ( ih1 : (x : α ) → C (pure x ih1 : ∀ x , C ( pure : {f : Type ?u.16919 → Type ?u.16918[self : Pure f {α : Type ?u.16919} → α → f α x ))
( ih2 : ∀ x y , C x → C y → C ( x * y )) : C x :=
FreeMagma.recOnMul x ih1 : (x : α ) → C (pure x ih1 ih2
#align free_magma.rec_on_pure FreeMagma.recOnPure
-- Porting note: dsimp can not prove this
@[ to_additive ( attr := simp , nolint simpNF )]
theorem map_pure ( f : α → β ) ( x ) : ( f <$> pure : {f : Type ?u.17462 → Type ?u.17461[self : Pure f {α : Type ?u.17462} → α → f α x : FreeMagma : Type ?u.17432 → Type ?u.17432 β ) = pure : {f : Type ?u.17535 → Type ?u.17534[self : Pure f {α : Type ?u.17535} → α → f α ( f x ) := rfl : ∀ {α : Sort ?u.17566} {a : α }, a = a
#align free_magma.map_pure FreeMagma.map_pure : ∀ {α β : Type u} (f : α → β x : α ), f <$> pure x = pure (f x
@[ to_additive ( attr := simp )]
theorem map_mul' ( f : α → β ) ( x y : FreeMagma : Type ?u.17659 → Type ?u.17659 α ) : f <$> ( x * y ) = f <$> x * f <$> y := rfl : ∀ {α : Sort ?u.17829} {a : α }, a = a
#align free_magma.map_mul' FreeMagma.map_mul'
-- Porting note: dsimp can not prove this
@[ to_additive ( attr := simp , nolint simpNF )]
theorem pure_bind ( f : α → FreeMagma : Type ?u.17957 → Type ?u.17957 β ) ( x ) : pure : {f : Type ?u.17971 → Type ?u.17970[self : Pure f {α : Type ?u.17971} → α → f α x >>= f = f x := rfl : ∀ {α : Sort ?u.18058} {a : α }, a = a
#align free_magma.pure_bind FreeMagma.pure_bind
@[ to_additive ( attr := simp )]
theorem mul_bind ( f : α → FreeMagma : Type ?u.18146 → Type ?u.18146 β ) ( x y : FreeMagma : Type ?u.18152 → Type ?u.18152 α ) : x * y >>= f = ( x >>= f ) * ( y >>= f ) :=
rfl : ∀ {α : Sort ?u.18304} {a : α }, a = a
#align free_magma.mul_bind FreeMagma.mul_bind
@[ to_additive ( attr := simp )]
theorem pure_seq { α β : Type u } { f : α → β } { x : FreeMagma : Type ?u.18438 → Type ?u.18438 α } : pure : {f : Type ?u.18449 → Type ?u.18448[self : Pure f {α : Type ?u.18449} → α → f α f <*> x = f <$> x := rfl : ∀ {α : Sort ?u.18589} {a : α }, a = a
#align free_magma.pure_seq FreeMagma.pure_seq
@[ to_additive ( attr := simp )]
theorem mul_seq { α β : Type u } { f g : FreeMagma : Type ?u.18713 → Type ?u.18713 ( α → β )} { x : FreeMagma : Type ?u.18719 → Type ?u.18719 α } :
f * g <*> x = ( f <*> x ) * ( g <*> x ) := rfl : ∀ {α : Sort ?u.18895} {a : α }, a = a
#align free_magma.mul_seq FreeMagma.mul_seq
@[ to_additive ]
instance : LawfulMonad FreeMagma .{u} := LawfulMonad.mk'
(pure_bind := fun f x ↦ rfl : ∀ {α : Sort ?u.19165} {a : α }, a = a )
(bind_assoc := fun x f g ↦ FreeMagma.recOnPure x ( fun x ↦ rfl : ∀ {α : Sort ?u.19307} {a : α }, a = a ) fun x y ih1 ih2 ↦ by
rw [ mul_bind , mul_bind , mul_bind , ih1 , ih2 ] )
(id_map := fun x ↦ FreeMagma.recOnPure x ( fun _ ↦ rfl : ∀ {α : Sort ?u.19273} {a : α }, a = a ) fun x y ih1 ih2 ↦ by
rw [ map_mul' , ih1 , ih2 ] )
end Category
end FreeMagma
/-- `FreeMagma` is traversable. -/
protected def FreeMagma.traverse { m : Type u → Type u } [ Applicative : (Type ?u.19765 → Type ?u.19764Type (max(?u.19765+1)?u.19764) m ] { α β : Type u }
( F : α → m β ) : FreeMagma : Type ?u.19780 → Type ?u.19780 α → m ( FreeMagma : Type ?u.19782 → Type ?u.19782 β )
| FreeMagma.of x => FreeMagma.of <$> F x
| x * y => (· * ·) <$> x . traverse F <*> y . traverse F
#align free_magma.traverse FreeMagma.traverse
/-- `FreeAddMagma` is traversable. -/
protected def FreeAddMagma.traverse { m : Type u → Type u } [ Applicative : (Type ?u.20600 → Type ?u.20599Type (max(?u.20600+1)?u.20599) m ] { α β : Type u }
( F : α → m β ) : FreeAddMagma : Type ?u.20615 → Type ?u.20615 α → m ( FreeAddMagma : Type ?u.20617 → Type ?u.20617 β )
| FreeAddMagma.of x => FreeAddMagma.of <$> F x
| x + y => (· + ·) <$> x . traverse F <*> y . traverse F
#align free_add_magma.traverse FreeAddMagma.traverse
attribute [ to_additive existing ] FreeMagma.traverse
namespace FreeMagma
variable { α : Type u }
section Category
variable { β : Type u }
@[ to_additive ]
instance : Traversable : (Type ?u.21836 → Type ?u.21836Type (?u.21836+1) FreeMagma : Type ?u.21837 → Type ?u.21837 := ⟨@ FreeMagma.traverse ⟩
variable { m : Type u → Type u } [ Applicative : (Type ?u.22245 → Type ?u.22244Type (max(?u.22245+1)?u.22244) m ] ( F : α → m β )
@[ to_additive ( attr := simp )]
theorem traverse_pure ( x ) : traverse F ( pure : {f : Type ?u.22292 → Type ?u.22291[self : Pure f {α : Type ?u.22292} → α → f α x : FreeMagma : Type ?u.22290 → Type ?u.22290 α ) = pure : {f : Type ?u.22358 → Type ?u.22357[self : Pure f {α : Type ?u.22358} → α → f α <$> F x := rfl : ∀ {α : Sort ?u.22447} {a : α }, a = a
#align free_magma.traverse_pure FreeMagma.traverse_pure
@[ to_additive ( attr := simp )]
theorem traverse_pure' : traverse F ∘ pure : {f : Type ?u.22656 → Type ?u.22655[self : Pure f {α : Type ?u.22656} → α → f α = fun x ↦ ( pure : {f : Type ?u.22738 → Type ?u.22737[self : Pure f {α : Type ?u.22738} → α → f α <$> F x : m ( FreeMagma : Type ?u.22711 → Type ?u.22711 β )) := rfl : ∀ {α : Sort ?u.22860} {a : α }, a = a
#align free_magma.traverse_pure' FreeMagma.traverse_pure'
@[ to_additive ( attr := simp )]
theorem traverse_mul ( x y : FreeMagma : Type ?u.23007 → Type ?u.23007 α ) :
traverse F ( x * y ) = (· * ·) <$> traverse F x <*> traverse F y := rfl : ∀ {α : Sort ?u.23289} {a : α }, a = a
#align free_magma.traverse_mul FreeMagma.traverse_mul
@[ to_additive ( attr := simp )]
theorem traverse_mul' :
Function.comp : {α : Sort ?u.23456} → {β : Sort ?u.23455} → {δ : Sort ?u.23454} → (β → δ (α → β α → δ ( traverse F ) ∘ @ Mul.mul : {α : Type ?u.23540} → [self : Mul α α → α → α ( FreeMagma : Type ?u.23541 → Type ?u.23541 α ) _ = fun x y ↦
(· * ·) <$> traverse F x <*> traverse F y := rfl : ∀ {α : Sort ?u.23893} {a : α }, a = a
#align free_magma.traverse_mul' FreeMagma.traverse_mul'
@[ to_additive ( attr := simp )]
theorem traverse_eq ( x ) : FreeMagma.traverse F x = traverse F x := rfl : ∀ {α : Sort ?u.24113} {a : α }, a = a
#align free_magma.traverse_eq FreeMagma.traverse_eq
-- Porting note: dsimp can not prove this
@[ to_additive ( attr := simp , nolint simpNF )]
theorem mul_map_seq ( x y : FreeMagma : Type ?u.24220 → Type ?u.24220 α ) :
( (· * ·) <$> x <*> y : Id ( FreeMagma : Type ?u.24226 → Type ?u.24226 α )) = ( x * y : FreeMagma : Type ?u.24386 → Type ?u.24386 α ) := rfl : ∀ {α : Sort ?u.24422} {a : α }, a = a
#align free_magma.mul_map_seq FreeMagma.mul_map_seq
@[ to_additive ]
instance : IsLawfulTraversable FreeMagma .{u} :=
{ instLawfulMonadFreeMagmaInstMonadFreeMagma with
id_traverse := fun x ↦
FreeMagma.recOnPure x ( fun x ↦ rfl : ∀ {α : Sort ?u.24886} {a : α }, a = a ) fun x y ih1 ih2 ↦ by
rw [ traverse_mul , ih1 , ih2 , mul_map_seq ]
comp_traverse := fun f g x ↦
FreeMagma.recOnPure x
( fun x ↦ by simp only [(. ∘ .), traverse_pure , traverse_pure' , functor_norm] )
( fun x y ih1 ih2 ↦ by
rw [ traverse_mul , ih1 , ih2 , traverse_mul ] ;
simp [ Functor.Comp.map_mk , Functor.map_map , (. ∘ .), Comp.seq_mk , seq_map_assoc ,
map_seq , traverse_mul ] )
naturality := fun η α β f x ↦
FreeMagma.recOnPure x
( fun x ↦ by simp only [ traverse_pure , functor_norm, Function.comp_apply : ∀ {β : Sort ?u.42309} {δ : Sort ?u.42310} {α : Sort ?u.42311} {f : β → δ g : α → β x : α }, (f ∘ g ) x = f (g x ] )
( fun x y ih1 ih2 ↦ by simp only [ traverse_mul , functor_norm, ih1 , ih2 ] )
traverse_eq_map_id := fun f x ↦
FreeMagma.recOnPure x ( fun _ ↦ rfl : ∀ {α : Sort ?u.24958} {a : α }, a = a ) fun x y ih1 ih2 ↦ by
rw [ traverse_mul , ih1 , ih2 , map_mul' , mul_map_seq ] ; rfl }
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 } [ Repr α ] : FreeMagma : Type ?u.43635 → Type ?u.43635 α → Lean.Format
| FreeMagma.of x => repr x
| x * y => "( " ++ x . repr ++ " * " ++ y . repr ++ " )"
#align free_magma.repr FreeMagma.repr
/-- Representation of an element of a free additive magma. -/
protected def FreeAddMagma.repr { α : Type u } [ Repr α ] : FreeAddMagma : Type ?u.44611 → Type ?u.44611 α → Lean.Format
| FreeAddMagma.of x => repr x
| x + y => "( " ++ x . repr ++ " + " ++ y . repr ++ " )"
#align free_add_magma.repr FreeAddMagma.repr
attribute [ to_additive existing ] FreeMagma.repr
@[ to_additive ]
instance { α : Type u } [ Repr α ] : Repr ( FreeMagma : Type ?u.45825 → Type ?u.45825 α ) := ⟨ fun o _ => FreeMagma.repr o ⟩
/-- Length of an element of a free magma. -/
def FreeMagma.length { α : Type u } : FreeMagma : Type ?u.45983 → Type ?u.45983 α → ℕ
| FreeMagma.of _x => 1
| x * y => x . length + y . length
#align free_magma.length FreeMagma.length
/-- Length of an element of a free additive magma. -/
def FreeAddMagma.length { α : Type u } : FreeAddMagma : Type ?u.46419 → Type ?u.46419 α → ℕ
| FreeAddMagma.of _x => 1
| x + y => x . length + y . length
#align free_add_magma.length FreeAddMagma.length
attribute [ to_additive existing ( attr := simp )] FreeMagma.length
/-- Associativity relations for an additive magma. -/
inductive AddMagma.AssocRel : (α : Type u) → [inst : Add α α → α → Prop AddMagma.AssocRel ( α : Type u ) [ Add α ] : α → α → Prop
| intro : ∀ x y z , AddMagma.AssocRel : (α : Type u) → [inst : Add α α → α → Prop AddMagma.AssocRel α ( x + y + z ) ( x + ( y + z ))
| left : ∀ w x y z , AddMagma.AssocRel : (α : Type u) → [inst : Add α α → α → Prop AddMagma.AssocRel α ( w + ( x + y + z )) ( w + ( x + ( y + z )))
#align add_magma.assoc_rel AddMagma.AssocRel : (α : Type u) → [inst : Add α α → α → Prop
/-- Associativity relations for a magma. -/
@[ to_additive AddMagma.AssocRel : (α : Type u) → [inst : Add α α → α → Prop "Associativity relations for an additive magma."]
inductive Magma.AssocRel : (α : Type u) → [inst : Mul α α → α → Prop Magma.AssocRel ( α : Type u ) [ Mul α ] : α → α → Prop
| intro : ∀ x y z , Magma.AssocRel : (α : Type u) → [inst : Mul α α → α → Prop Magma.AssocRel α ( x * y * z ) ( x * ( y * z ))
| left : ∀ w x y z , Magma.AssocRel : (α : Type u) → [inst : Mul α α → α → Prop Magma.AssocRel α ( w * ( x * y * z )) ( w * ( x * ( y * z )))
#align magma.assoc_rel Magma.AssocRel : (α : Type u) → [inst : Mul α α → α → Prop
namespace Magma
/-- Semigroup quotient of a magma. -/
@[ to_additive AddMagma.FreeAddSemigroup : (α : Type u) → [inst : Add α Type u "Additive semigroup quotient of an additive magma."]
def AssocQuotient ( α : Type u ) [ Mul α ] : Type u :=
Quot <| AssocRel : (α : Type ?u.47916) → [inst : Mul α α → α → Prop α
#align magma.assoc_quotient Magma.AssocQuotient : (α : Type u) → [inst : Mul α Type u
namespace AssocQuotient
variable { α : Type u } [ Mul α ]
@[ to_additive ]
theorem quot_mk_assoc ( x y z : α ) : Quot.mk : {α : Sort ?u.47967} → (r : α → α → Prop α → Quot r ( AssocRel : (α : Type ?u.47969) → [inst : Mul α α → α → Prop α ) ( x * y * z ) = Quot.mk : {α : Sort ?u.48062} → (r : α → α → Prop α → Quot r _ : ?m.48063 → ?m.48063 → Prop ( x * ( y * z )) :=
Quot.sound ( AssocRel.intro : ∀ {α : Type ?u.48172} [inst : Mul α x y z : α ), AssocRel α (x * y * z x * (y * z _ _ _ )
#align magma.assoc_quotient.quot_mk_assoc Magma.AssocQuotient.quot_mk_assoc
@[ to_additive ]
theorem quot_mk_assoc_left ( x y z w : α ) :
Quot.mk : {α : Sort ?u.48252} → (r : α → α → Prop α → Quot r ( AssocRel : (α : Type ?u.48254) → [inst : Mul α α → α → Prop α ) ( x * ( y * z * w )) = Quot.mk : {α : Sort ?u.48375} → (r : α → α → Prop α → Quot r _ : ?m.48376 → ?m.48376 → Prop ( x * ( y * ( z * w ))) :=
Quot.sound ( AssocRel.left : ∀ {α : Type ?u.48514} [inst : Mul α w x y z : α ), AssocRel α (w * (x * y * z w * (x * (y * z _ _ _ _ )
#align magma.assoc_quotient.quot_mk_assoc_left Magma.AssocQuotient.quot_mk_assoc_left
@[ to_additive ]
instance : Semigroup : Type ?u.48591 → Type ?u.48591 ( AssocQuotient : (α : Type ?u.48592) → [inst : Mul α Type ?u.48592 α ) where
mul x y := by
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 ) → γ x y ( fun x y ↦ Quot.mk : {α : Sort ?u.48826} → (r : α → α → Prop α → Quot r _ : ?m.48827 → ?m.48827 → Prop ( x * y )) _ _
· rintro a b₁ b₂ (⟨c, d, e⟩ | ⟨c, d, e, f⟩) : ?m.48807 b₁ b₂
⟨c, d, e⟩ | ⟨c, d, e, f⟩ : ?m.48807 b₁ b₂
c ⟨c, d, e⟩ | ⟨c, d, e, f⟩ : ?m.48807 b₁ b₂
d ⟨c, d, e⟩ | ⟨c, d, e, f⟩ : ?m.48807 b₁ b₂
e ⟨c, d, e⟩ | ⟨c, d, e, f⟩ : ?m.48807 b₁ b₂
c ⟨c, d, e⟩ | ⟨c, d, e, f⟩ : ?m.48807 b₁ b₂
d ⟨c, d, e⟩ | ⟨c, d, e, f⟩ : ?m.48807 b₁ b₂
e ⟨c, d, e⟩ | ⟨c, d, e, f⟩ : ?m.48807 b₁ b₂
f ⟨c, d, e⟩ | ⟨c, d, e, f⟩ : ?m.48807 b₁ b₂
(⟨c, d, e⟩ | ⟨c, d, e, f⟩) : ?m.48807 b₁ b₂
refine'_1.intro refine'_1.left <;> refine'_1.intro refine'_1.left simp only
· refine'_1.intro refine'_1.left