-- Mathlib/CategoryTheory/FintypeCat.lean
theorem is_skeletal : Skeletal Skeleton.{u} := fun X Y ⟨h⟩ =>
  ext _ _ <|
    Fin.equiv_iff_eq.mp <|
      Nonempty.intro <|
        { toFun := fun x => (h.hom ⟨x⟩).down
          invFun := fun x => (h.inv ⟨x⟩).down
          left_inv

Proof state:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin X.len
⊢ (h.inv { down := (fun x => (h.hom { down := x }).down) a }).down = a

Tactic:
rw [ULift.up_down]

Result:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin X.len
⊢ (h.inv (h.hom { down := a })).down = a

Proof state:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin X.len
⊢ (fun x => (h.inv { down := x }).down) ((fun x => (h.hom { down := x }).down) a) = a

Tactic:
change ULift.down _ = _

Result:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin X.len
⊢ (h.inv { down := (fun x => (h.hom { down := x }).down) a }).down = a

Proof state:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin X.len
⊢ (𝟙 X { down := a }).down = a

Tactic:
rfl

Result:
no goals

Proof state:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
⊢ Function.LeftInverse (fun x => (h.inv { down := x }).down) fun x => (h.hom { down := x }).down

Tactic:
intro a

Result:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin X.len
⊢ (fun x => (h.inv { down := x }).down) ((fun x => (h.hom { down := x }).down) a) = a

Proof state:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin Y.len
⊢ ((h.inv ≫ h.hom) { down := a }).down = a

Tactic:
simp

Result:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin Y.len
⊢ (𝟙 Y { down := a }).down = a

Proof state:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin X.len
⊢ ((h.hom ≫ h.inv) { down := a }).down = a

Tactic:
simp

Result:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin X.len
⊢ (𝟙 X { down := a }).down = a

Proof state:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin Y.len
⊢ (h.hom (h.inv { down := a })).down = a

Tactic:
change ((h.inv ≫ h.hom) _).down = _

Result:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin Y.len
⊢ ((h.inv ≫ h.hom) { down := a }).down = a

Proof state:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin Y.len
⊢ (fun x => (h.hom { down := x }).down) ((fun x => (h.inv { down := x }).down) a) = a

Tactic:
change ULift.down _ = _

Result:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin Y.len
⊢ (h.hom { down := (fun x => (h.inv { down := x }).down) a }).down = a

Proof state:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin X.len
⊢ (h.inv (h.hom { down := a })).down = a

Tactic:
change ((h.hom ≫ h.inv) _).down = _

Result:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin X.len
⊢ ((h.hom ≫ h.inv) { down := a }).down = a

Proof state:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
⊢ Function.RightInverse (fun x => (h.inv { down := x }).down) fun x => (h.hom { down := x }).down

Tactic:
intro a

Result:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin Y.len
⊢ (fun x => (h.hom { down := x }).down) ((fun x => (h.inv { down := x }).down) a) = a

Proof state:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin Y.len
⊢ (𝟙 Y { down := a }).down = a

Tactic:
rfl

Result:
no goals

Proof state:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin Y.len
⊢ (h.hom { down := (fun x => (h.inv { down := x }).down) a }).down = a

Tactic:
rw [ULift.up_down]

Result:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin Y.len
⊢ (h.hom (h.inv { down := a })).down = a