[GOAL]
X Y : MonCat
⊢ FunLike (↑X →* ↑Y) ↑X fun x => ↑Y
[PROOFSTEP]
infer_instance
  -- porting note: added
[GOAL]
G : Type u_1
inst✝ : Group G
⊢ Group ↑(of G)
[PROOFSTEP]
assumption
[GOAL]
⊢ ConcreteCategory CommMonCat
[PROOFSTEP]
dsimp only [CommMonCat]
[GOAL]
⊢ ConcreteCategory (Bundled CommMonoid)
[PROOFSTEP]
infer_instance
[GOAL]
X Y : CommMonCat
⊢ FunLike (↑X →* ↑Y) ↑X fun x => ↑Y
[PROOFSTEP]
infer_instance
  -- porting note: added
[GOAL]
R S : MonCat
i : R ⟶ S
r : ↑R
h : r = 1
⊢ ↑i r = 1
[PROOFSTEP]
simp [h]
[GOAL]
R S : CommMonCat
i : R ⟶ S
r : ↑R
h : r = 1
⊢ ↑i r = 1
[PROOFSTEP]
simp [h]
  -- We verify that when constructing a morphism in `CommMonCat`,
  -- when we construct the `toFun` field, the types are presented as `↑R`.
[GOAL]
R : CommMonCat
x : ↑R
⊢ ↑R
[PROOFSTEP]
match_target (R : Type u)
[GOAL]
R : CommMonCat
x : ↑R
⊢ ↑R
[PROOFSTEP]
guard_hyp x : (R : Type u)
[GOAL]
R : CommMonCat
x : ↑R
⊢ ↑R
[PROOFSTEP]
exact x * x
[GOAL]
R : CommMonCat
⊢ (fun x => x * x) 1 = 1
[PROOFSTEP]
simp
[GOAL]
R : CommMonCat
x y : ↑R
⊢ OneHom.toFun { toFun := fun x => x * x, map_one' := (_ : 1 * 1 = 1) } (x * y) =
    OneHom.toFun { toFun := fun x => x * x, map_one' := (_ : 1 * 1 = 1) } x *
      OneHom.toFun { toFun := fun x => x * x, map_one' := (_ : 1 * 1 = 1) } y
[PROOFSTEP]
dsimp
[GOAL]
R : CommMonCat
x y : ↑R
⊢ x * y * (x * y) = x * x * (y * y)
[PROOFSTEP]
rw [mul_assoc x y (x * y), ← mul_assoc y x y, mul_comm y x, mul_assoc, mul_assoc]
[GOAL]
X✝ Y✝ : Type u
X Y : MonCat
f : X ⟶ Y
x✝ : IsIso ((forget MonCat).map f)
⊢ IsIso f
[PROOFSTEP]
let i := asIso ((forget MonCat).map f)
[GOAL]
X✝ Y✝ : Type u
X Y : MonCat
f : X ⟶ Y
x✝ : IsIso ((forget MonCat).map f)
i : (forget MonCat).obj X ≅ (forget MonCat).obj Y := asIso ((forget MonCat).map f)
⊢ IsIso f
[PROOFSTEP]
let e : X ≃* Y := MulEquiv.mk i.toEquiv (by aesop)
[GOAL]
X✝ Y✝ : Type u
X Y : MonCat
f : X ⟶ Y
x✝ : IsIso ((forget MonCat).map f)
i : (forget MonCat).obj X ≅ (forget MonCat).obj Y := asIso ((forget MonCat).map f)
⊢ ∀ (x y : ↑X), Equiv.toFun i.toEquiv (x * y) = Equiv.toFun i.toEquiv x * Equiv.toFun i.toEquiv y
[PROOFSTEP]
aesop
[GOAL]
X✝ Y✝ : Type u
X Y : MonCat
f : X ⟶ Y
x✝ : IsIso ((forget MonCat).map f)
i : (forget MonCat).obj X ≅ (forget MonCat).obj Y := asIso ((forget MonCat).map f)
e : ↑X ≃* ↑Y := { toEquiv := i.toEquiv, map_mul' := (_ : ∀ (x_1 y : ↑X), ↑f (x_1 * y) = ↑f x_1 * ↑f y) }
⊢ IsIso f
[PROOFSTEP]
exact IsIso.of_iso e.toMonCatIso
[GOAL]
X✝ Y✝ : Type u
X Y : CommMonCat
f : X ⟶ Y
x✝ : IsIso ((forget CommMonCat).map f)
⊢ IsIso f
[PROOFSTEP]
let i := asIso ((forget CommMonCat).map f)
[GOAL]
X✝ Y✝ : Type u
X Y : CommMonCat
f : X ⟶ Y
x✝ : IsIso ((forget CommMonCat).map f)
i : (forget CommMonCat).obj X ≅ (forget CommMonCat).obj Y := asIso ((forget CommMonCat).map f)
⊢ IsIso f
[PROOFSTEP]
let e : X ≃* Y := MulEquiv.mk i.toEquiv (MonoidHom.map_mul (show MonoidHom X Y from f))
[GOAL]
X✝ Y✝ : Type u
X Y : CommMonCat
f : X ⟶ Y
x✝ : IsIso ((forget CommMonCat).map f)
i : (forget CommMonCat).obj X ≅ (forget CommMonCat).obj Y := asIso ((forget CommMonCat).map f)
e : ↑X ≃* ↑Y :=
  { toEquiv := i.toEquiv,
    map_mul' :=
      (_ :
        ∀ (a b : ↑X),
          ↑(let_fun this := f;
                this)
              (a * b) =
            ↑(let_fun this := f;
                  this)
                a *
              ↑(let_fun this := f;
                  this)
                b) }
⊢ IsIso f
[PROOFSTEP]
exact IsIso.of_iso e.toCommMonCatIso
