[GOAL]
α : Type u
inst✝ : Group α
x y : SingleObj α
f : x ⟶ y
⊢ inv f = f⁻¹
[PROOFSTEP]
apply IsIso.inv_eq_of_hom_inv_id
[GOAL]
case hom_inv_id
α : Type u
inst✝ : Group α
x y : SingleObj α
f : x ⟶ y
⊢ f ≫ f⁻¹ = 𝟙 x
[PROOFSTEP]
rw [comp_as_mul, inv_mul_self, id_as_one]
[GOAL]
α✝ α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
⊢ Function.LeftInverse
    (fun f =>
      {
        toOneHom :=
          { toFun := fun x => f.map (↑(toEnd α) x), map_one' := (_ : f.map (𝟙 (star α)) = 𝟙 (f.obj (star α))) },
        map_mul' := (_ : ∀ (x y : α), f.map (y ≫ x) = f.map y ≫ f.map x) })
    fun f => Functor.mk { obj := id, map := fun {X Y} => ↑f }
[PROOFSTEP]
aesop_cat
[GOAL]
α✝ α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
⊢ Function.RightInverse
    (fun f =>
      {
        toOneHom :=
          { toFun := fun x => f.map (↑(toEnd α) x), map_one' := (_ : f.map (𝟙 (star α)) = 𝟙 (f.obj (star α))) },
        map_mul' := (_ : ∀ (x y : α), f.map (y ≫ x) = f.map y ≫ f.map x) })
    fun f => Functor.mk { obj := id, map := fun {X Y} => ↑f }
[PROOFSTEP]
aesop_cat
[GOAL]
α : Type u
C : Type ?u.20048
G : Type ?u.20052
inst✝¹ : Category.{?u.20049, ?u.20048} C
inst✝ : Group G
f : C → G
⊢ ∀ (X : C),
    { obj := fun x => (), map := fun {x y} x_1 => f y * (f x)⁻¹ }.map (𝟙 X) =
      𝟙 ({ obj := fun x => (), map := fun {x y} x_1 => f y * (f x)⁻¹ }.obj X)
[PROOFSTEP]
intro
[GOAL]
α : Type u
C : Type ?u.20048
G : Type ?u.20052
inst✝¹ : Category.{?u.20049, ?u.20048} C
inst✝ : Group G
f : C → G
X✝ : C
⊢ { obj := fun x => (), map := fun {x y} x_1 => f y * (f x)⁻¹ }.map (𝟙 X✝) =
    𝟙 ({ obj := fun x => (), map := fun {x y} x_1 => f y * (f x)⁻¹ }.obj X✝)
[PROOFSTEP]
simp only [SingleObj.id_as_one, mul_right_inv]
[GOAL]
α : Type u
C : Type ?u.20048
G : Type ?u.20052
inst✝¹ : Category.{?u.20049, ?u.20048} C
inst✝ : Group G
f : C → G
⊢ ∀ {X Y Z : C} (f_1 : X ⟶ Y) (g : Y ⟶ Z),
    { obj := fun x => (), map := fun {x y} x_1 => f y * (f x)⁻¹ }.map (f_1 ≫ g) =
      { obj := fun x => (), map := fun {x y} x_1 => f y * (f x)⁻¹ }.map f_1 ≫
        { obj := fun x => (), map := fun {x y} x_1 => f y * (f x)⁻¹ }.map g
[PROOFSTEP]
intros
[GOAL]
α : Type u
C : Type ?u.20048
G : Type ?u.20052
inst✝¹ : Category.{?u.20049, ?u.20048} C
inst✝ : Group G
f : C → G
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { obj := fun x => (), map := fun {x y} x_1 => f y * (f x)⁻¹ }.map (f✝ ≫ g✝) =
    { obj := fun x => (), map := fun {x y} x_1 => f y * (f x)⁻¹ }.map f✝ ≫
      { obj := fun x => (), map := fun {x y} x_1 => f y * (f x)⁻¹ }.map g✝
[PROOFSTEP]
dsimp
[GOAL]
α : Type u
C : Type ?u.20048
G : Type ?u.20052
inst✝¹ : Category.{?u.20049, ?u.20048} C
inst✝ : Group G
f : C → G
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ f Z✝ * (f X✝)⁻¹ = (f Y✝ * (f X✝)⁻¹) ≫ (f Z✝ * (f Y✝)⁻¹)
[PROOFSTEP]
rw [SingleObj.comp_as_mul, ← mul_assoc, mul_left_inj, mul_assoc, inv_mul_self, mul_one]
[GOAL]
α : Type u
inst✝ : Monoid α
⊢ α ≃* End (SingleObj.star α)
[PROOFSTEP]
exact SingleObj.toEnd α
[GOAL]
X✝ Y✝ : MonCat
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : toCat.map a₁✝ = toCat.map a₂✝
⊢ a₁✝ = a₂✝
[PROOFSTEP]
simpa [toCat] using h
