[GOAL]
⊢ ∀ {α β : Type ?u.90} (Iα : Mul α) (Iβ : Mul β), Function.Injective MulHom.toFun
[PROOFSTEP]
intros
[GOAL]
α✝ β✝ : Type ?u.90
Iα✝ : Mul α✝
Iβ✝ : Mul β✝
⊢ Function.Injective MulHom.toFun
[PROOFSTEP]
apply @FunLike.coe_injective
[GOAL]
⊢ ∀ {α : Type ?u.90} (I : Mul α), (MulHom.id α).toFun = id
[PROOFSTEP]
aesop_cat
[GOAL]
⊢ ∀ {α β γ : Type ?u.90} (Iα : Mul α) (Iβ : Mul β) (Iγ : Mul γ) (f : α →ₙ* β) (g : β →ₙ* γ),
    (MulHom.comp g f).toFun = g.toFun ∘ f.toFun
[PROOFSTEP]
aesop_cat
[GOAL]
X Y : Type u
inst✝¹ : Mul X
inst✝ : Mul Y
e : X ≃* Y
⊢ toMulHom e ≫ toMulHom (symm e) = 𝟙 (MagmaCat.of X)
[PROOFSTEP]
ext
[GOAL]
case w
X Y : Type u
inst✝¹ : Mul X
inst✝ : Mul Y
e : X ≃* Y
x✝ : (forget MagmaCat).obj (MagmaCat.of X)
⊢ ↑(toMulHom e ≫ toMulHom (symm e)) x✝ = ↑(𝟙 (MagmaCat.of X)) x✝
[PROOFSTEP]
simp_rw [comp_apply, toMulHom_eq_coe, MagmaCat.MulEquiv_coe_eq, symm_apply_apply, id_apply]
[GOAL]
X✝ Y✝ : Type u
X Y : MagmaCat
f : X ⟶ Y
x✝ : IsIso ((forget MagmaCat).map f)
⊢ IsIso f
[PROOFSTEP]
skip
[GOAL]
X✝ Y✝ : Type u
X Y : MagmaCat
f : X ⟶ Y
x✝ : IsIso ((forget MagmaCat).map f)
⊢ IsIso f
[PROOFSTEP]
let i := asIso ((forget MagmaCat).map f)
[GOAL]
X✝ Y✝ : Type u
X Y : MagmaCat
f : X ⟶ Y
x✝ : IsIso ((forget MagmaCat).map f)
i : (forget MagmaCat).obj X ≅ (forget MagmaCat).obj Y := asIso ((forget MagmaCat).map f)
⊢ IsIso f
[PROOFSTEP]
let e : X ≃* Y := { f, i.toEquiv with }
[GOAL]
X✝ Y✝ : Type u
X Y : MagmaCat
f : X ⟶ Y
x✝ : IsIso ((forget MagmaCat).map f)
i : (forget MagmaCat).obj X ≅ (forget MagmaCat).obj Y := asIso ((forget MagmaCat).map f)
e : ↑X ≃* ↑Y :=
  let src := i.toEquiv;
  {
    toEquiv :=
      { toFun := f.toFun, invFun := src.invFun, left_inv := (_ : Function.LeftInverse src.invFun src.toFun),
        right_inv := (_ : Function.RightInverse src.invFun src.toFun) },
    map_mul' := (_ : ∀ (x y : ↑X), MulHom.toFun f (x * y) = MulHom.toFun f x * MulHom.toFun f y) }
⊢ IsIso f
[PROOFSTEP]
exact ⟨(IsIso.of_iso e.toMagmaCatIso).1⟩
[GOAL]
X✝ Y✝ : Type u
X Y : SemigroupCat
f : X ⟶ Y
x✝ : IsIso ((forget SemigroupCat).map f)
⊢ IsIso f
[PROOFSTEP]
skip
[GOAL]
X✝ Y✝ : Type u
X Y : SemigroupCat
f : X ⟶ Y
x✝ : IsIso ((forget SemigroupCat).map f)
⊢ IsIso f
[PROOFSTEP]
let i := asIso ((forget SemigroupCat).map f)
[GOAL]
X✝ Y✝ : Type u
X Y : SemigroupCat
f : X ⟶ Y
x✝ : IsIso ((forget SemigroupCat).map f)
i : (forget SemigroupCat).obj X ≅ (forget SemigroupCat).obj Y := asIso ((forget SemigroupCat).map f)
⊢ IsIso f
[PROOFSTEP]
let e : X ≃* Y := { f, i.toEquiv with }
[GOAL]
X✝ Y✝ : Type u
X Y : SemigroupCat
f : X ⟶ Y
x✝ : IsIso ((forget SemigroupCat).map f)
i : (forget SemigroupCat).obj X ≅ (forget SemigroupCat).obj Y := asIso ((forget SemigroupCat).map f)
e : ↑X ≃* ↑Y :=
  let src := i.toEquiv;
  {
    toEquiv :=
      { toFun := f.toFun, invFun := src.invFun, left_inv := (_ : Function.LeftInverse src.invFun src.toFun),
        right_inv := (_ : Function.RightInverse src.invFun src.toFun) },
    map_mul' := (_ : ∀ (x y : ↑X), MulHom.toFun f (x * y) = MulHom.toFun f x * MulHom.toFun f y) }
⊢ IsIso f
[PROOFSTEP]
exact ⟨(IsIso.of_iso e.toSemigroupCatIso).1⟩
