J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F✝ F G : J ⥤ C
inst✝ : HasLimit F
α : F ≅ G
s : Cone G
j : J
⊢ ((Cones.postcompose α.inv).obj s).π.app j ≫ α.hom.app j = s.π.app j
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F✝ F G : J ⥤ C
inst✝ : HasLimit F
α : F ≅ G
s : Cone G
j : J
⊢ (fun s => limit.lift F ((Cones.postcompose α.inv).obj s)) s ≫ ((Cones.postcompose α.hom).obj (limit.cone F)).π.app j =
    s.π.app j
rw [Cones.postcompose_obj_π, NatTrans.comp_app, limit.cone_π, ← Category.assoc,
  limit.lift_π]
no goals
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F✝ F G : J ⥤ C
inst✝ : HasLimit F
α : F ≅ G
s : Cone G
j : J
⊢ ((Cones.postcompose α.inv).obj s).π.app j ≫ α.hom.app j = s.π.app j
simp
case w
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F✝ F G : J ⥤ C
inst✝ : HasLimit F
α : F ≅ G
s : Cone G
m : s.pt ⟶ ((Cones.postcompose α.hom).obj (limit.cone F)).pt
w : ∀ (j : J), m ≫ ((Cones.postcompose α.hom).obj (limit.cone F)).π.app j = s.π.app j
⊢ ∀ (j : J), m ≫ limit.π F j = (fun s => limit.lift F ((Cones.postcompose α.inv).obj s)) s ≫ limit.π F j
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F✝ F G : J ⥤ C
inst✝ : HasLimit F
α : F ≅ G
s : Cone G
m : s.pt ⟶ ((Cones.postcompose α.hom).obj (limit.cone F)).pt
w : ∀ (j : J), m ≫ ((Cones.postcompose α.hom).obj (limit.cone F)).π.app j = s.π.app j
⊢ m = (fun s => limit.lift F ((Cones.postcompose α.inv).obj s)) s
apply limit.hom_ext
case w
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F✝ F G : J ⥤ C
inst✝ : HasLimit F
α : F ≅ G
s : Cone G
m : s.pt ⟶ ((Cones.postcompose α.hom).obj (limit.cone F)).pt
w : ∀ (j : J), m ≫ ((Cones.postcompose α.hom).obj (limit.cone F)).π.app j = s.π.app j
j : J
⊢ m ≫ limit.π F j = (fun s => limit.lift F ((Cones.postcompose α.inv).obj s)) s ≫ limit.π F j
case w
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F✝ F G : J ⥤ C
inst✝ : HasLimit F
α : F ≅ G
s : Cone G
m : s.pt ⟶ ((Cones.postcompose α.hom).obj (limit.cone F)).pt
w : ∀ (j : J), m ≫ ((Cones.postcompose α.hom).obj (limit.cone F)).π.app j = s.π.app j
⊢ ∀ (j : J), m ≫ limit.π F j = (fun s => limit.lift F ((Cones.postcompose α.inv).obj s)) s ≫ limit.π F j
intro j
case w
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F✝ F G : J ⥤ C
inst✝ : HasLimit F
α : F ≅ G
s : Cone G
m : s.pt ⟶ ((Cones.postcompose α.hom).obj (limit.cone F)).pt
w : ∀ (j : J), m ≫ ((Cones.postcompose α.hom).obj (limit.cone F)).π.app j = s.π.app j
j : J
⊢ (m ≫ limit.π F j) ≫ (α.app j).hom = s.π.app j
case w
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F✝ F G : J ⥤ C
inst✝ : HasLimit F
α : F ≅ G
s : Cone G
m : s.pt ⟶ ((Cones.postcompose α.hom).obj (limit.cone F)).pt
w : ∀ (j : J), m ≫ ((Cones.postcompose α.hom).obj (limit.cone F)).π.app j = s.π.app j
j : J
⊢ m ≫ limit.π F j = (fun s => limit.lift F ((Cones.postcompose α.inv).obj s)) s ≫ limit.π F j
rw [limit.lift_π, Cones.postcompose_obj_π, NatTrans.comp_app, ← NatIso.app_inv,
  Iso.eq_comp_inv]
no goals
case w
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F✝ F G : J ⥤ C
inst✝ : HasLimit F
α : F ≅ G
s : Cone G
m : s.pt ⟶ ((Cones.postcompose α.hom).obj (limit.cone F)).pt
w : ∀ (j : J), m ≫ ((Cones.postcompose α.hom).obj (limit.cone F)).π.app j = s.π.app j
j : J
⊢ (m ≫ limit.π F j) ≫ (α.app j).hom = s.π.app j
simpa using w j