awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass M'
inst_3 : MulOneClass N'
inst_4 : MulOneClass P
⊢ Eq (α := N ∗ M)
    ((MonoidHom.comp mk (FreeMonoid.map Sum.swap) : (a : FreeMonoid (M ⊕ N)) → N ∗ M) (of (Sum.inr 1)) : N ∗ M)
    (1 : N ∗ M)

Tactic:
simp only [MonoidHom.comp_apply, map_of, Sum.swap_inr, mk_of_inl, map_one]

Premises used: Sum.swap_inr, map_one, Monoid.Coprod.mk_of_inl, FreeMonoid.map_of, MonoidHom.comp_apply
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass M'
inst_3 : MulOneClass N'
inst_4 : MulOneClass P
x y : M
⊢ Eq (α := N ∗ M)
    ((MonoidHom.comp mk (FreeMonoid.map Sum.swap) : (a : FreeMonoid (M ⊕ N)) → N ∗ M) (of (Sum.inl (x * y))) : N ∗ M)
    ((MonoidHom.comp mk (FreeMonoid.map Sum.swap) : (a : FreeMonoid (M ⊕ N)) → N ∗ M)
        (HMul.hMul (α := FreeMonoid (M ⊕ N)) (of (Sum.inl x)) (of (Sum.inl y))) :
      N ∗ M)

Tactic:
simp only [MonoidHom.comp_apply, map_of, Sum.swap_inl, mk_of_inr, map_mul]

Premises used: map_mul, Monoid.Coprod.mk_of_inr, FreeMonoid.map_of, Sum.swap_inl, MonoidHom.comp_apply
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass M'
inst_3 : MulOneClass N'
inst_4 : MulOneClass P
x y : N
⊢ Eq (α := N ∗ M)
    ((MonoidHom.comp mk (FreeMonoid.map Sum.swap) : (a : FreeMonoid (M ⊕ N)) → N ∗ M) (of (Sum.inr (x * y))) : N ∗ M)
    ((MonoidHom.comp mk (FreeMonoid.map Sum.swap) : (a : FreeMonoid (M ⊕ N)) → N ∗ M)
        (HMul.hMul (α := FreeMonoid (M ⊕ N)) (of (Sum.inr x)) (of (Sum.inr y))) :
      N ∗ M)

Tactic:
simp only [MonoidHom.comp_apply, map_of, Sum.swap_inr, mk_of_inl, map_mul]

Premises used: Sum.swap_inr, map_mul, Monoid.Coprod.mk_of_inl, FreeMonoid.map_of, MonoidHom.comp_apply
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Eq (α := N ∗ M →* N ∗ M) (MonoidHom.comp (swap M N) (swap N M)) (MonoidHom.id (N ∗ M))

Tactic:
hom_ext rfl rfl

Premises used: Monoid.Coprod.hom_ext, rfl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
x : M ∗ N
⊢ (swap N M : (a : N ∗ M) → M ∗ N) ((swap M N : (a : M ∗ N) → N ∗ M) x) = x

Tactic:
DFunLike.congr_fun (swap_comp_swap _ _) x

Premises used: DFunLike.congr_fun, Quotient.liftOn', Con.liftOn, Monoid.Coprod.swap_comp_swap
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass M'
inst_3 : MulOneClass N'
f : M →* M'
g : N →* N'
⊢ MonoidHom.comp (swap M' N') (map f g) = (map g f).comp (swap M N)

Tactic:
hom_ext rfl rfl

Premises used: Monoid.Coprod.hom_ext, rfl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass M'
inst_3 : MulOneClass N'
f : M →* M'
g : N →* N'
x : M ∗ N
⊢ Eq (α := N' ∗ M') ((swap M' N' : (a : M' ∗ N') → N' ∗ M') ((map f g : (a : M ∗ N) → M' ∗ N') x) : N' ∗ M')
    ((map g f : (a : N ∗ M) → N' ∗ M') ((swap M N : (a : M ∗ N) → N ∗ M) x) : N' ∗ M')

Tactic:
DFunLike.congr_fun (swap_comp_map f g) x

Premises used: DFunLike.congr_fun, Quotient.liftOn', Con.liftOn, Monoid.Coprod.swap_comp_map
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Eq (α := M →* N ∗ M) (MonoidHom.comp (swap M N) inl) inr

Tactic:
rfl

Premises used: Sum.swap, Quotient.liftOn', List.map, Con.liftOn, FreeMonoid.of, Con.toQuotient, Monoid.Coprod.inr, rfl, Sum.elim
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
x : M
⊢ Eq (α := N ∗ M) ((swap M N : (a : M ∗ N) → N ∗ M) ((inl : (a : M) → M ∗ N) x) : N ∗ M)
    ((inr : (a : M) → N ∗ M) x : N ∗ M)

Tactic:
rfl

Premises used: Sum.swap, Quotient.liftOn', List.map, Con.liftOn, FreeMonoid.of, Con.toQuotient, rfl, Sum.elim
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Eq (α := N →* N ∗ M) (MonoidHom.comp (swap M N) inr) inl

Tactic:
rfl

Premises used: Sum.swap, Quotient.liftOn', List.map, Con.liftOn, FreeMonoid.of, Monoid.Coprod.inl, Con.toQuotient, rfl, Sum.elim
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
x : N
⊢ Eq (α := N ∗ M) ((swap M N : (a : M ∗ N) → N ∗ M) ((inr : (a : N) → M ∗ N) x) : N ∗ M)
    ((inl : (a : N) → N ∗ M) x : N ∗ M)

Tactic:
rfl

Premises used: Sum.swap, Quotient.liftOn', List.map, Con.liftOn, FreeMonoid.of, Con.toQuotient, rfl, Sum.elim
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Injective (α := M ∗ N) (β := N ∗ M) (⇑(swap M N) : (a : M ∗ N) → N ∗ M)

Tactic:
LeftInverse.injective swap_swap

Premises used: Function.LeftInverse.injective, Monoid.Coprod.swap_swap
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
x y : M ∗ N
⊢ Eq (α := N ∗ M) ((swap M N : (a : M ∗ N) → N ∗ M) x : N ∗ M) ((swap M N : (a : M ∗ N) → N ∗ M) y : N ∗ M) ↔ x = y

Tactic:
swap_injective.eq_iff

Premises used: Monoid.Coprod.swap_injective, Function.Injective.eq_iff
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
x : M ∗ N
⊢ Eq (α := N ∗ M) ((swap M N : (a : M ∗ N) → N ∗ M) x : N ∗ M) (1 : N ∗ M) ↔ x = 1

Tactic:
swap_injective.eq_iff' (map_one _)

Premises used: Monoid.Coprod.swap_injective, Function.Injective.eq_iff', map_one
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Surjective (α := M ∗ N) (β := N ∗ M) (⇑(swap M N) : (a : M ∗ N) → N ∗ M)

Tactic:
LeftInverse.surjective swap_swap

Premises used: Function.LeftInverse.surjective, Monoid.Coprod.swap_swap
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Bijective (α := M ∗ N) (β := N ∗ M) (⇑(swap M N) : (a : M ∗ N) → N ∗ M)

Tactic:
⟨swap_injective, swap_surjective⟩

Premises used: Monoid.Coprod.swap_surjective, Monoid.Coprod.swap_injective, And.intro, Function.Bijective
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Eq (α := Submonoid (M ∗ N)) (MonoidHom.mker (F := M ∗ N →* N ∗ M) (swap M N)) ⊥

Tactic:
Submonoid.ext fun _ ↦ swap_eq_one

Premises used: Submonoid.ext, Monoid.Coprod.swap_eq_one
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Eq (α := Submonoid (N ∗ M)) (MonoidHom.mrange (F := M ∗ N →* N ∗ M) (swap M N)) ⊤

Tactic:
MonoidHom.mrange_eq_top_of_surjective _ swap_surjective

Premises used: Monoid.Coprod.swap_surjective, MonoidHom.mrange_eq_top_of_surjective
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : Monoid P
f : M →* P
g : N →* P
x : FreeMonoid (M ⊕ N)
⊢ Eq.{u_3 + 1} (α := P) ((lift f g : (a : M ∗ N) → P) ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) x : M ∗ N) : P)
    ((((FreeMonoid.lift : (a : M ⊕ N → P) → FreeMonoid (M ⊕ N) →* P) (Sum.elim (⇑f : (a : M) → P) (⇑g : (a : N) → P)) :
            FreeMonoid (M ⊕ N) →* P) :
          (a : FreeMonoid (M ⊕ N)) → P)
        x :
      P)

Tactic:
rfl

Premises used: FreeMonoid.prodAux, Con.liftOn, rfl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : Monoid P
f : M →* P
g : N →* P
x : M
⊢ Eq.{u_3 + 1} (α := P) ((lift f g : (a : M ∗ N) → P) ((inl : (a : M) → M ∗ N) x : M ∗ N) : P) ((f : (a : M) → P) x : P)

Tactic:
rfl

Premises used: FreeMonoid.prodAux, Quotient.liftOn', List.foldl, Con.liftOn, rfl, Sum.elim
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : Monoid P
f : M →* P
g : N →* P
fg : M ∗ N →* P
h₁ : fg.comp inl = f
h₂ : fg.comp inr = g
⊢ fg = lift f g

Tactic:
hom_ext h₁ h₂

Premises used: Monoid.Coprod.hom_ext
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : Monoid P
f : M →* P
g : N →* P
⊢ (lift f g).comp inl = f

Tactic:
rfl

Premises used: FreeMonoid.prodAux, Quotient.liftOn', List.foldl, Con.liftOn, rfl, Sum.elim
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : Monoid P
f : M →* P
g : N →* P
x : N
⊢ Eq.{u_3 + 1} (α := P) ((lift f g : (a : M ∗ N) → P) ((inr : (a : N) → M ∗ N) x : M ∗ N) : P) ((g : (a : N) → P) x : P)

Tactic:
rfl

Premises used: FreeMonoid.prodAux, Quotient.liftOn', List.foldl, Con.liftOn, rfl, Sum.elim
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : Monoid P
f : M →* P
g : N →* P
⊢ (lift f g).comp inr = g

Tactic:
rfl

Premises used: FreeMonoid.prodAux, Quotient.liftOn', List.foldl, Con.liftOn, rfl, Sum.elim
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : Monoid P
f : M →* P
g : N →* P
⊢ (lift f g).comp (swap N M) = lift g f

Tactic:
hom_ext rfl rfl

Premises used: Monoid.Coprod.hom_ext, rfl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : Monoid P
f : M →* P
g : N →* P
x : N ∗ M
⊢ Eq.{u_3 + 1} (α := P) ((lift f g : (a : M ∗ N) → P) ((swap N M : (a : N ∗ M) → M ∗ N) x : M ∗ N) : P)
    ((lift g f : (a : N ∗ M) → P) x : P)

Tactic:
DFunLike.congr_fun (lift_comp_swap f g) x

Premises used: DFunLike.congr_fun, Quotient.liftOn', Monoid.Coprod.lift_comp_swap, Con.liftOn
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : Monoid P
P' : Type u_4
inst_3 : Monoid P'
f : P →* P'
g₁ : M →* P
g₂ : N →* P
rw : f.comp ((lift g₁ g₂).comp inl) = (lift (f.comp g₁) (f.comp g₂)).comp inl
rw₁ : f.comp g₁ = (lift (f.comp g₁) (f.comp g₂)).comp inl
rw₂ rw₃ : f.comp g₁ = f.comp g₁
⊢ (f.comp (lift g₁ g₂)).comp inl = (lift (f.comp g₁) (f.comp g₂)).comp inl

Tactic:
rw [MonoidHom.comp_assoc, lift_comp_inl, lift_comp_inl]

Premises used: MonoidHom.comp_assoc, Monoid.Coprod.lift_comp_inl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : Monoid P
P' : Type u_4
inst_3 : Monoid P'
f : P →* P'
g₁ : M →* P
g₂ : N →* P
rw : f.comp ((lift g₁ g₂).comp inr) = (lift (f.comp g₁) (f.comp g₂)).comp inr
rw₁ : f.comp g₂ = (lift (f.comp g₁) (f.comp g₂)).comp inr
rw₂ rw₃ : f.comp g₂ = f.comp g₂
⊢ (f.comp (lift g₁ g₂)).comp inr = (lift (f.comp g₁) (f.comp g₂)).comp inr

Tactic:
rw [MonoidHom.comp_assoc, lift_comp_inr, lift_comp_inr]

Premises used: MonoidHom.comp_assoc, Monoid.Coprod.lift_comp_inr
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : Monoid P
f : M →* P
g : N →* P
⊢ Eq (α := Submonoid P) (MonoidHom.mrange (lift f g)) (MonoidHom.mrange f ⊔ MonoidHom.mrange g)

Tactic:
simp [mrange_eq]

Premises used: Monoid.Coprod.mrange_eq
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
⊢ Eq (α := M →* M) (MonoidHom.comp (N := M ∗ N) fst inl) (MonoidHom.id M)

Tactic:
rfl

Premises used: FreeMonoid.prodAux, Quotient.liftOn', List.foldl, Con.liftOn, rfl, Sum.elim
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
x : M
⊢ (fst : (a : M ∗ N) → M) ((inl : (a : M) → M ∗ N) x : M ∗ N) = x

Tactic:
rfl

Premises used: FreeMonoid.prodAux, Quotient.liftOn', List.foldl, Con.liftOn, rfl, Sum.elim
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
⊢ Eq (α := N →* M) (MonoidHom.comp fst inr) 1

Tactic:
rfl

Premises used: FreeMonoid.prodAux, Quotient.liftOn', List.foldl, Con.liftOn, rfl, Sum.elim
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
x : N
⊢ Eq.{u_1 + 1} (α := M) ((fst : (a : M ∗ N) → M) ((inr : (a : N) → M ∗ N) x : M ∗ N) : M) (1 : M)

Tactic:
rfl

Premises used: FreeMonoid.prodAux, Quotient.liftOn', List.foldl, Con.liftOn, rfl, Sum.elim
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
⊢ Eq (α := M →* N) (MonoidHom.comp snd inl) 1

Tactic:
rfl

Premises used: FreeMonoid.prodAux, Quotient.liftOn', List.foldl, Con.liftOn, rfl, Sum.elim
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
x : M
⊢ Eq.{u_2 + 1} (α := N) ((snd : (a : M ∗ N) → N) ((inl : (a : M) → M ∗ N) x : M ∗ N) : N) (1 : N)

Tactic:
rfl

Premises used: FreeMonoid.prodAux, Quotient.liftOn', List.foldl, Con.liftOn, rfl, Sum.elim
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
⊢ Eq (α := N →* N) (MonoidHom.comp (N := M ∗ N) snd inr) (MonoidHom.id N)

Tactic:
rfl

Premises used: FreeMonoid.prodAux, Quotient.liftOn', List.foldl, Con.liftOn, rfl, Sum.elim
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
x : N
⊢ (snd : (a : M ∗ N) → N) ((inr : (a : N) → M ∗ N) x : M ∗ N) = x

Tactic:
rfl

Premises used: FreeMonoid.prodAux, Quotient.liftOn', List.foldl, Con.liftOn, rfl, Sum.elim
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
⊢ Eq (α := M →* M × N) (MonoidHom.comp toProd inl) (MonoidHom.inl M N)

Tactic:
rfl

Premises used: FreeMonoid.prodAux, Quotient.liftOn', MonoidHom.inl, List.foldl, Con.liftOn, rfl, Sum.elim
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
⊢ Eq (α := N →* M × N) (MonoidHom.comp toProd inr) (MonoidHom.inr M N)

Tactic:
rfl

Premises used: FreeMonoid.prodAux, MonoidHom.inr, Quotient.liftOn', List.foldl, Con.liftOn, rfl, Sum.elim
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
x : M
⊢ Eq (α := M × N) ((toProd : (a : M ∗ N) → M × N) ((inl : (a : M) → M ∗ N) x) : M × N) ((x, 1) : M × N)

Tactic:
rfl

Premises used: FreeMonoid.prodAux, Quotient.liftOn', List.foldl, Con.liftOn, rfl, Sum.elim
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
x : N
⊢ Eq (α := M × N) ((toProd : (a : M ∗ N) → M × N) ((inr : (a : N) → M ∗ N) x) : M × N) ((1, x) : M × N)

Tactic:
rfl

Premises used: FreeMonoid.prodAux, Quotient.liftOn', List.foldl, Con.liftOn, rfl, Sum.elim
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
h₁ : Eq (α := M →* M × N) (MonoidHom.comp (MonoidHom.prod fst snd) inl) (MonoidHom.comp toProd inl)
h₂ : Eq (α := N →* M × N) (MonoidHom.comp (MonoidHom.prod fst snd) inr) (MonoidHom.comp toProd inr)
⊢ Eq (α := M ∗ N →* M × N) (MonoidHom.prod fst snd) toProd

Tactic:
ext1
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
⊢ Eq (α := M →* M × N) (MonoidHom.comp (MonoidHom.prod fst snd) inl) (MonoidHom.comp toProd inl)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
⊢ Eq (α := N →* M × N) (MonoidHom.comp (MonoidHom.prod fst snd) inr) (MonoidHom.comp toProd inr)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
x : M ∗ N
rw :
  Eq (α := M × N) (((fst : (a : M ∗ N) → M) x, (snd : (a : M ∗ N) → N) x) : M × N)
    ((MonoidHom.prod fst snd : (a : M ∗ N) → M × N) x : M × N)
rw₁ rw₂ :
  Eq (α := M × N) (((fst : (a : M ∗ N) → M) x, (snd : (a : M ∗ N) → N) x) : M × N)
    (((fst : (a : M ∗ N) → M) x, (snd : (a : M ∗ N) → N) x) : M × N)
⊢ Eq (α := M × N) (((fst : (a : M ∗ N) → M) x, (snd : (a : M ∗ N) → N) x) : M × N)
    ((toProd : (a : M ∗ N) → M × N) x : M × N)

Tactic:
rw [← fst_prod_snd, MonoidHom.prod_apply]

Premises used: MonoidHom.prod_apply, Monoid.Coprod.fst_prod_snd
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
rw : Eq (α := M ∗ N →* M) (MonoidHom.comp (MonoidHom.fst M N) (MonoidHom.prod fst snd)) fst
rw₁ rw₂ : Eq (α := M ∗ N →* M) fst fst
⊢ Eq (α := M ∗ N →* M) (MonoidHom.comp (MonoidHom.fst M N) toProd) fst

Tactic:
rw [← fst_prod_snd, MonoidHom.fst_comp_prod]

Premises used: MonoidHom.fst_comp_prod, Monoid.Coprod.fst_prod_snd
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
x : M ∗ N
rw :
  Eq.{u_1 + 1} (α := M) (((toProd : (a : M ∗ N) → M × N) x).1 : M)
    ((MonoidHom.comp (MonoidHom.fst M N) toProd : (a : M ∗ N) → M) x : M)
⊢ Eq.{u_1 + 1} (α := M) (((toProd : (a : M ∗ N) → M × N) x).1 : M) ((fst : (a : M ∗ N) → M) x : M)

Tactic:
rw [← fst_comp_toProd]

Premises used: Monoid.Coprod.fst_comp_toProd
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
x : M ∗ N
⊢ Eq.{u_1 + 1} (α := M) (((toProd : (a : M ∗ N) → M × N) x).1 : M)
    ((MonoidHom.comp (MonoidHom.fst M N) toProd : (a : M ∗ N) → M) x : M)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
rw : Eq (α := M ∗ N →* N) (MonoidHom.comp (MonoidHom.snd M N) (MonoidHom.prod fst snd)) snd
rw₁ rw₂ : Eq (α := M ∗ N →* N) snd snd
⊢ Eq (α := M ∗ N →* N) (MonoidHom.comp (MonoidHom.snd M N) toProd) snd

Tactic:
rw [← fst_prod_snd, MonoidHom.snd_comp_prod]

Premises used: MonoidHom.snd_comp_prod, Monoid.Coprod.fst_prod_snd
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
x : M ∗ N
rw :
  Eq.{u_2 + 1} (α := N) (((toProd : (a : M ∗ N) → M × N) x).2 : N)
    ((MonoidHom.comp (MonoidHom.snd M N) toProd : (a : M ∗ N) → N) x : N)
⊢ Eq.{u_2 + 1} (α := N) (((toProd : (a : M ∗ N) → M × N) x).2 : N) ((snd : (a : M ∗ N) → N) x : N)

Tactic:
rw [← snd_comp_toProd]

Premises used: Monoid.Coprod.snd_comp_toProd
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
x : M ∗ N
⊢ Eq.{u_2 + 1} (α := N) (((toProd : (a : M ∗ N) → M × N) x).2 : N)
    ((MonoidHom.comp (MonoidHom.snd M N) toProd : (a : M ∗ N) → N) x : N)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
⊢ Eq (α := M ∗ N →* N) (MonoidHom.comp fst (swap M N)) snd

Tactic:
lift_comp_swap _ _

Premises used: Monoid.Coprod.snd, Monoid.Coprod.fst, Monoid.Coprod.lift_comp_swap
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
x : M ∗ N
⊢ Eq.{u_2 + 1} (α := N) ((fst : (a : N ∗ M) → N) ((swap M N : (a : M ∗ N) → N ∗ M) x : N ∗ M) : N)
    ((snd : (a : M ∗ N) → N) x : N)

Tactic:
lift_swap _ _ _

Premises used: Monoid.Coprod.lift_swap
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
⊢ Eq (α := M ∗ N →* M) (MonoidHom.comp snd (swap M N)) fst

Tactic:
lift_comp_swap _ _

Premises used: Monoid.Coprod.snd, Monoid.Coprod.fst, Monoid.Coprod.lift_comp_swap
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
x : M ∗ N
⊢ Eq.{u_1 + 1} (α := M) ((snd : (a : N ∗ M) → M) ((swap M N : (a : M ∗ N) → N ∗ M) x : N ∗ M) : M)
    ((fst : (a : M ∗ N) → M) x : M)

Tactic:
lift_swap _ _ _

Premises used: Monoid.Coprod.lift_swap
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
⊢ Eq (α := M ∗ N →* N ∗ M) (lift inr inl) (swap M N)

Tactic:
hom_ext rfl rfl

Premises used: Monoid.Coprod.hom_ext, rfl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
⊢ Eq (α := M ∗ N →* M ∗ N) (lift inl inr) (MonoidHom.id (M ∗ N))

Tactic:
hom_ext rfl rfl

Premises used: Monoid.Coprod.hom_ext, rfl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
⊢ Injective (α := M) (β := M ∗ N) (⇑inl : (a : M) → M ∗ N)

Tactic:
LeftInverse.injective fst_apply_inl

Premises used: Function.LeftInverse.injective, Monoid.Coprod.fst_apply_inl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
⊢ Injective (α := N) (β := M ∗ N) (⇑inr : (a : N) → M ∗ N)

Tactic:
LeftInverse.injective snd_apply_inr

Premises used: Function.LeftInverse.injective, Monoid.Coprod.snd_apply_inr
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
⊢ Surjective (α := M ∗ N) (β := M) (⇑fst : (a : M ∗ N) → M)

Tactic:
LeftInverse.surjective fst_apply_inl

Premises used: Monoid.Coprod.fst_apply_inl, Function.LeftInverse.surjective
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
⊢ Surjective (α := M ∗ N) (β := N) (⇑snd : (a : M ∗ N) → N)

Tactic:
LeftInverse.surjective snd_apply_inr

Premises used: Function.LeftInverse.surjective, Monoid.Coprod.snd_apply_inr
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
x : M × N
rw :
  HMul.hMul (α := M × N) (β := M × N) ((toProd : (a : M ∗ N) → M × N) ((inl : (a : M) → M ∗ N) x.1) : M × N)
      ((toProd : (a : M ∗ N) → M × N) ((inr : (a : N) → M ∗ N) x.2) : M × N) =
    x
rw₁ :
  HMul.hMul (α := M × N) (β := M × N) (x.1, 1) ((toProd : (a : M ∗ N) → M × N) ((inr : (a : N) → M ∗ N) x.2) : M × N) =
    x
rw₂ : (x.1, 1) * (1, x.2) = x
rw₃ rw₄ : x = x
⊢ (toProd : (a : M ∗ N) → M × N)
      (HMul.hMul (α := M ∗ N) (β := M ∗ N) ((inl : (a : M) → M ∗ N) x.1 : M ∗ N)
        ((inr : (a : N) → M ∗ N) x.2 : M ∗ N)) =
    x

Tactic:
rw [map_mul, toProd_apply_inl, toProd_apply_inr, Prod.fst_mul_snd]

Premises used: Prod.fst_mul_snd, Monoid.Coprod.toProd_apply_inr, map_mul, Monoid.Coprod.toProd_apply_inl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
x : FreeMonoid (G ⊕ H)
rw :
  HMul.hMul (α := G ∗ H) (β := G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
          ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
            (List.reverse
              (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) x)))) :
        G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) x : G ∗ H) =
    1
⊢ (coprodCon G H : (a : FreeMonoid (G ⊕ H)) → FreeMonoid (G ⊕ H) → Prop)
    (HMul.hMul (α := FreeMonoid (G ⊕ H))
      ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
          (List.reverse (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) x))) :
        FreeMonoid (G ⊕ H))
      x)
    1

Tactic:
rw [← mk_eq_mk, map_mul, map_one]

Premises used: map_mul, map_one, Monoid.Coprod.mk_eq_mk
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
⊢ HMul.hMul (α := G ∗ H) (β := G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
          ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
            (List.reverse
              (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) 1)))) :
        G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) 1 : G ∗ H) =
    1

Tactic:
simp