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
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
intro a
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
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
change ULift.down _ = _
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len X)
⊢ (h.inv (h.hom { down := a })).down = a
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
rw [ULift.up_down]
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len X)
⊢ ((h.hom ≫ h.inv) { down := a }).down = a
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len X)
⊢ (h.inv (h.hom { down := a })).down = a
change ((h.hom ≫ h.inv) _).down = _
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len X)
⊢ (𝟙 X { down := a }).down = a
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len X)
⊢ ((h.hom ≫ h.inv) { down := a }).down = a
simp
no goals
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len X)
⊢ (𝟙 X { down := a }).down = a
rfl
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
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
intro a
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
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
change ULift.down _ = _
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len Y)
⊢ (h.hom (h.inv { down := a })).down = a
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
rw [ULift.up_down]
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len Y)
⊢ ((h.inv ≫ h.hom) { down := a }).down = a
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len Y)
⊢ (h.hom (h.inv { down := a })).down = a
change ((h.inv ≫ h.hom) _).down = _
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len Y)
⊢ (𝟙 Y { down := a }).down = a
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len Y)
⊢ ((h.inv ≫ h.hom) { down := a }).down = a
simp
no goals
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin (len Y)
⊢ (𝟙 Y { down := a }).down = a
rfl