Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
P : Cᵒᵖ ⥤ D
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
S : Presieve B := (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows
X' : S.category := S.categoryMk π ⋯
P' : S.category := S.categoryMk (c.fst ≫ π) ⋯
fst : P' ⟶ X' := ObjectProperty.homMk (Over.homMk c.fst ⋯)
snd : P' ⟶ X' := ObjectProperty.homMk (Over.homMk c.snd ⋯)
F : S.categoryᵒᵖ ⥤ D := S.diagram.op ⋙ P
G : WalkingParallelPair ⥤ D := parallelPair (P.map c.fst.op) (P.map c.snd.op)
H : WalkingParallelPair ⥤ S.categoryᵒᵖ := parallelPair fst.op snd.op
this : H.Initial
i : H ⋙ F ≅ G :=
  parallelPair.ext (Iso.refl ((H ⋙ F).obj WalkingParallelPair.zero)) (Iso.refl ((H ⋙ F).obj WalkingParallelPair.one)) ⋯
    ⋯
⊢ ∀ (j : WalkingParallelPair),
    ((Cone.postcompose i.symm.hom).obj (Fork.ofι (P.map π.op) ⋯)).π.app j =
      (Iso.refl ((Cone.postcompose i.symm.hom).obj (Fork.ofι (P.map π.op) ⋯)).pt).hom ≫
        (Cone.whisker H (P.mapCone (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.cocone.op)).π.app j

Tactic:
rintro ⟨_ | _⟩

Goal state after:
case zero
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
P : Cᵒᵖ ⥤ D
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
S : Presieve B := (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows
X' : S.category := S.categoryMk π ⋯
P' : S.category := S.categoryMk (c.fst ≫ π) ⋯
fst : P' ⟶ X' := ObjectProperty.homMk (Over.homMk c.fst ⋯)
snd : P' ⟶ X' := ObjectProperty.homMk (Over.homMk c.snd ⋯)
F : S.categoryᵒᵖ ⥤ D := S.diagram.op ⋙ P
G : WalkingParallelPair ⥤ D := parallelPair (P.map c.fst.op) (P.map c.snd.op)
H : WalkingParallelPair ⥤ S.categoryᵒᵖ := parallelPair fst.op snd.op
this : H.Initial
i : H ⋙ F ≅ G :=
  parallelPair.ext (Iso.refl ((H ⋙ F).obj WalkingParallelPair.zero)) (Iso.refl ((H ⋙ F).obj WalkingParallelPair.one)) ⋯
    ⋯
⊢ ((Cone.postcompose i.symm.hom).obj (Fork.ofι (P.map π.op) ⋯)).π.app WalkingParallelPair.zero =
    (Iso.refl ((Cone.postcompose i.symm.hom).obj (Fork.ofι (P.map π.op) ⋯)).pt).hom ≫
      (Cone.whisker H (P.mapCone (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.cocone.op)).π.app
        WalkingParallelPair.zero

case one
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
P : Cᵒᵖ ⥤ D
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
S : Presieve B := (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows
X' : S.category := S.categoryMk π ⋯
P' : S.category := S.categoryMk (c.fst ≫ π) ⋯
fst : P' ⟶ X' := ObjectProperty.homMk (Over.homMk c.fst ⋯)
snd : P' ⟶ X' := ObjectProperty.homMk (Over.homMk c.snd ⋯)
F : S.categoryᵒᵖ ⥤ D := S.diagram.op ⋙ P
G : WalkingParallelPair ⥤ D := parallelPair (P.map c.fst.op) (P.map c.snd.op)
H : WalkingParallelPair ⥤ S.categoryᵒᵖ := parallelPair fst.op snd.op
this : H.Initial
i : H ⋙ F ≅ G :=
  parallelPair.ext (Iso.refl ((H ⋙ F).obj WalkingParallelPair.zero)) (Iso.refl ((H ⋙ F).obj WalkingParallelPair.one)) ⋯
    ⋯
⊢ ((Cone.postcompose i.symm.hom).obj (Fork.ofι (P.map π.op) ⋯)).π.app WalkingParallelPair.one =
    (Iso.refl ((Cone.postcompose i.symm.hom).obj (Fork.ofι (P.map π.op) ⋯)).pt).hom ≫
      (Cone.whisker H (P.mapCone (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.cocone.op)).π.app WalkingParallelPair.one