[GOAL]
X Y : FintypeCat
f g : X ⟶ Y
h : ∀ (x : ↑X), f x = g x
⊢ f = g
[PROOFSTEP]
funext
[GOAL]
case h
X Y : FintypeCat
f g : X ⟶ Y
h : ∀ (x : ↑X), f x = g x
x✝ : ↑X
⊢ f x✝ = g x✝
[PROOFSTEP]
apply h
[GOAL]
A B : FintypeCat
⊢ Function.LeftInverse
    (fun i =>
      { toFun := i.hom, invFun := i.inv, left_inv := (_ : ∀ (a : ↑A), i.inv (i.hom a) = a),
        right_inv := (_ : ∀ (a : ↑B), i.hom (i.inv a) = a) })
    fun e => Iso.mk ↑e ↑e.symm
[PROOFSTEP]
aesop_cat
[GOAL]
A B : FintypeCat
⊢ Function.RightInverse
    (fun i =>
      { toFun := i.hom, invFun := i.inv, left_inv := (_ : ∀ (a : ↑A), i.inv (i.hom a) = a),
        right_inv := (_ : ∀ (a : ↑B), i.hom (i.inv a) = a) })
    fun e => Iso.mk ↑e ↑e.symm
[PROOFSTEP]
aesop_cat
[GOAL]
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
[PROOFSTEP]
intro a
[GOAL]
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len X)
⊢ (fun x => (h.inv { down := x }).down) ((fun x => (h.hom { down := x }).down) a) = a
[PROOFSTEP]
change ULift.down _ = _
[GOAL]
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len X)
⊢ (h.inv { down := (fun x => (h.hom { down := x }).down) a }).down = a
[PROOFSTEP]
rw [ULift.up_down]
[GOAL]
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len X)
⊢ (h.inv (h.hom { down := a })).down = a
[PROOFSTEP]
change ((h.hom ≫ h.inv) _).down = _
[GOAL]
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len X)
⊢ ((h.hom ≫ h.inv) { down := a }).down = a
[PROOFSTEP]
simp
[GOAL]
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len X)
⊢ (𝟙 X { down := a }).down = a
[PROOFSTEP]
rfl
[GOAL]
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
[PROOFSTEP]
intro a
[GOAL]
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len Y)
⊢ (fun x => (h.hom { down := x }).down) ((fun x => (h.inv { down := x }).down) a) = a
[PROOFSTEP]
change ULift.down _ = _
[GOAL]
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len Y)
⊢ (h.hom { down := (fun x => (h.inv { down := x }).down) a }).down = a
[PROOFSTEP]
rw [ULift.up_down]
[GOAL]
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len Y)
⊢ (h.hom (h.inv { down := a })).down = a
[PROOFSTEP]
change ((h.inv ≫ h.hom) _).down = _
[GOAL]
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len Y)
⊢ ((h.inv ≫ h.hom) { down := a }).down = a
[PROOFSTEP]
simp
[GOAL]
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len Y)
⊢ (𝟙 Y { down := a }).down = a
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ Fintype.card ↑(incl.obj (mk n)) = n
[PROOFSTEP]
convert Finset.card_fin n
[GOAL]
case h.e'_2
n : ℕ
⊢ Fintype.card ↑(incl.obj (mk n)) = Finset.card Finset.univ
[PROOFSTEP]
apply Fintype.ofEquiv_card
[GOAL]
⊢ IsEquivalence Skeleton.incl
[PROOFSTEP]
infer_instance
