[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : C
f : End X
h : IsIso f
⊢ f * inv f = 1
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : C
f : End X
h : IsIso f
⊢ inv f * f = 1
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : C
f g : (End X)ˣ
⊢ Equiv.toFun
      { toFun := fun f => Iso.mk (↑f) f.inv,
        invFun := fun f =>
          { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X), inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) },
        left_inv :=
          (_ :
            ∀ (x : (End X)ˣ),
              (fun f =>
                    { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                      inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                  ((fun f => Iso.mk (↑f) f.inv) x) =
                x),
        right_inv :=
          (_ :
            ∀ (x : Aut X),
              (fun f => Iso.mk (↑f) f.inv)
                  ((fun f =>
                      { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                        inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                    x) =
                x) }
      (f * g) =
    Equiv.toFun
        { toFun := fun f => Iso.mk (↑f) f.inv,
          invFun := fun f =>
            { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X), inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) },
          left_inv :=
            (_ :
              ∀ (x : (End X)ˣ),
                (fun f =>
                      { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                        inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                    ((fun f => Iso.mk (↑f) f.inv) x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : Aut X),
                (fun f => Iso.mk (↑f) f.inv)
                    ((fun f =>
                        { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                          inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                      x) =
                  x) }
        f *
      Equiv.toFun
        { toFun := fun f => Iso.mk (↑f) f.inv,
          invFun := fun f =>
            { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X), inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) },
          left_inv :=
            (_ :
              ∀ (x : (End X)ˣ),
                (fun f =>
                      { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                        inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                    ((fun f => Iso.mk (↑f) f.inv) x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : Aut X),
                (fun f => Iso.mk (↑f) f.inv)
                    ((fun f =>
                        { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                          inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                      x) =
                  x) }
        g
[PROOFSTEP]
cases f
[GOAL]
case mk
C : Type u
inst✝ : Category.{v, u} C
X : C
g : (End X)ˣ
val✝ inv✝ : End X
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
⊢ Equiv.toFun
      { toFun := fun f => Iso.mk (↑f) f.inv,
        invFun := fun f =>
          { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X), inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) },
        left_inv :=
          (_ :
            ∀ (x : (End X)ˣ),
              (fun f =>
                    { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                      inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                  ((fun f => Iso.mk (↑f) f.inv) x) =
                x),
        right_inv :=
          (_ :
            ∀ (x : Aut X),
              (fun f => Iso.mk (↑f) f.inv)
                  ((fun f =>
                      { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                        inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                    x) =
                x) }
      ({ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } * g) =
    Equiv.toFun
        { toFun := fun f => Iso.mk (↑f) f.inv,
          invFun := fun f =>
            { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X), inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) },
          left_inv :=
            (_ :
              ∀ (x : (End X)ˣ),
                (fun f =>
                      { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                        inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                    ((fun f => Iso.mk (↑f) f.inv) x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : Aut X),
                (fun f => Iso.mk (↑f) f.inv)
                    ((fun f =>
                        { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                          inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                      x) =
                  x) }
        { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } *
      Equiv.toFun
        { toFun := fun f => Iso.mk (↑f) f.inv,
          invFun := fun f =>
            { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X), inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) },
          left_inv :=
            (_ :
              ∀ (x : (End X)ˣ),
                (fun f =>
                      { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                        inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                    ((fun f => Iso.mk (↑f) f.inv) x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : Aut X),
                (fun f => Iso.mk (↑f) f.inv)
                    ((fun f =>
                        { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                          inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                      x) =
                  x) }
        g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
X : C
val✝¹ inv✝¹ : End X
val_inv✝¹ : val✝¹ * inv✝¹ = 1
inv_val✝¹ : inv✝¹ * val✝¹ = 1
val✝ inv✝ : End X
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
⊢ Equiv.toFun
      { toFun := fun f => Iso.mk (↑f) f.inv,
        invFun := fun f =>
          { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X), inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) },
        left_inv :=
          (_ :
            ∀ (x : (End X)ˣ),
              (fun f =>
                    { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                      inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                  ((fun f => Iso.mk (↑f) f.inv) x) =
                x),
        right_inv :=
          (_ :
            ∀ (x : Aut X),
              (fun f => Iso.mk (↑f) f.inv)
                  ((fun f =>
                      { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                        inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                    x) =
                x) }
      ({ val := val✝¹, inv := inv✝¹, val_inv := val_inv✝¹, inv_val := inv_val✝¹ } *
        { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }) =
    Equiv.toFun
        { toFun := fun f => Iso.mk (↑f) f.inv,
          invFun := fun f =>
            { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X), inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) },
          left_inv :=
            (_ :
              ∀ (x : (End X)ˣ),
                (fun f =>
                      { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                        inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                    ((fun f => Iso.mk (↑f) f.inv) x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : Aut X),
                (fun f => Iso.mk (↑f) f.inv)
                    ((fun f =>
                        { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                          inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                      x) =
                  x) }
        { val := val✝¹, inv := inv✝¹, val_inv := val_inv✝¹, inv_val := inv_val✝¹ } *
      Equiv.toFun
        { toFun := fun f => Iso.mk (↑f) f.inv,
          invFun := fun f =>
            { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X), inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) },
          left_inv :=
            (_ :
              ∀ (x : (End X)ˣ),
                (fun f =>
                      { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                        inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                    ((fun f => Iso.mk (↑f) f.inv) x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : Aut X),
                (fun f => Iso.mk (↑f) f.inv)
                    ((fun f =>
                        { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                          inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                      x) =
                  x) }
        { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X Y : C
h : X ≅ Y
x✝ : Aut X
⊢ (fun y => Iso.mk (h.hom ≫ y.hom ≫ h.inv) (h.hom ≫ y.inv ≫ h.inv))
      ((fun x => Iso.mk (h.inv ≫ x.hom ≫ h.hom) (h.inv ≫ x.inv ≫ h.hom)) x✝) =
    x✝
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X Y : C
h : X ≅ Y
x✝ : Aut Y
⊢ (fun x => Iso.mk (h.inv ≫ x.hom ≫ h.hom) (h.inv ≫ x.inv ≫ h.hom))
      ((fun y => Iso.mk (h.hom ≫ y.hom ≫ h.inv) (h.hom ≫ y.inv ≫ h.inv)) x✝) =
    x✝
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X Y : C
h : X ≅ Y
⊢ ∀ (x y : Aut X),
    Equiv.toFun
        { toFun := fun x => Iso.mk (h.inv ≫ x.hom ≫ h.hom) (h.inv ≫ x.inv ≫ h.hom),
          invFun := fun y => Iso.mk (h.hom ≫ y.hom ≫ h.inv) (h.hom ≫ y.inv ≫ h.inv),
          left_inv :=
            (_ :
              ∀ (x : Aut X),
                (fun y => Iso.mk (h.hom ≫ y.hom ≫ h.inv) (h.hom ≫ y.inv ≫ h.inv))
                    ((fun x => Iso.mk (h.inv ≫ x.hom ≫ h.hom) (h.inv ≫ x.inv ≫ h.hom)) x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : Aut Y),
                (fun x => Iso.mk (h.inv ≫ x.hom ≫ h.hom) (h.inv ≫ x.inv ≫ h.hom))
                    ((fun y => Iso.mk (h.hom ≫ y.hom ≫ h.inv) (h.hom ≫ y.inv ≫ h.inv)) x) =
                  x) }
        (x * y) =
      Equiv.toFun
          { toFun := fun x => Iso.mk (h.inv ≫ x.hom ≫ h.hom) (h.inv ≫ x.inv ≫ h.hom),
            invFun := fun y => Iso.mk (h.hom ≫ y.hom ≫ h.inv) (h.hom ≫ y.inv ≫ h.inv),
            left_inv :=
              (_ :
                ∀ (x : Aut X),
                  (fun y => Iso.mk (h.hom ≫ y.hom ≫ h.inv) (h.hom ≫ y.inv ≫ h.inv))
                      ((fun x => Iso.mk (h.inv ≫ x.hom ≫ h.hom) (h.inv ≫ x.inv ≫ h.hom)) x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : Aut Y),
                  (fun x => Iso.mk (h.inv ≫ x.hom ≫ h.hom) (h.inv ≫ x.inv ≫ h.hom))
                      ((fun y => Iso.mk (h.hom ≫ y.hom ≫ h.inv) (h.hom ≫ y.inv ≫ h.inv)) x) =
                    x) }
          x *
        Equiv.toFun
          { toFun := fun x => Iso.mk (h.inv ≫ x.hom ≫ h.hom) (h.inv ≫ x.inv ≫ h.hom),
            invFun := fun y => Iso.mk (h.hom ≫ y.hom ≫ h.inv) (h.hom ≫ y.inv ≫ h.inv),
            left_inv :=
              (_ :
                ∀ (x : Aut X),
                  (fun y => Iso.mk (h.hom ≫ y.hom ≫ h.inv) (h.hom ≫ y.inv ≫ h.inv))
                      ((fun x => Iso.mk (h.inv ≫ x.hom ≫ h.hom) (h.inv ≫ x.inv ≫ h.hom)) x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : Aut Y),
                  (fun x => Iso.mk (h.inv ≫ x.hom ≫ h.hom) (h.inv ≫ x.inv ≫ h.hom))
                      ((fun y => Iso.mk (h.hom ≫ y.hom ≫ h.inv) (h.hom ≫ y.inv ≫ h.inv)) x) =
                    x) }
          y
[PROOFSTEP]
simp [Aut_mul_def]
