Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝² : Category.{v_2, u_2} 𝒰.I₀
inst✝¹ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
i j : 𝒰.I₀
hij : i ⟶ j
iso1 : (d.cocone i).pt ≅ ((MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)).mapCocone (d.cocone j)).pt :=
  (d.isColimit i).coconePointsIsoOfNatIso
    (isColimitOfPreserves (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)) (d.isColimit j))
    (D.isoWhiskerLeft (MorphismProperty.Over.pullbackComp (Cover.trans 𝒰 hij) (𝒰.f j) (𝒰.f i) ⋯) ≪≫
      (D.associator (MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
          (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))).symm)
heq :
  (MorphismProperty.Over.map ⊤ ⋯).map iso1.hom ≫
      (MorphismProperty.Over.mapPullbackAdj P ⊤ (Cover.trans 𝒰 hij) ⋯ trivial).counit.app (d.cocone j).pt =
    d.transitionMap hij
iso2 : (d.cocone i).pt.left ≅ pullback (d.cocone j).pt.hom (Cover.trans 𝒰 hij) :=
  (MorphismProperty.Over.forget P ⊤ (𝒰.X i) ⋙ CategoryTheory.Over.forget (𝒰.X i)).mapIso iso1
⊢ pullback.fst (d.cocone j).pt.hom (Cover.trans 𝒰 hij) ≫ (Iso.refl ((𝟭 Scheme).obj (d.cocone j).pt.left)).hom =
    iso2.symm.hom ≫ (d.transitionMap hij).left

pp: case refine_2
P : MorphismProperty Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝² : Category.{v_2, u_2} 𝒰.I₀
inst✝¹ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
i j : 𝒰.I₀
hij : i ⟶ j
iso1 : (d.cocone i).pt ≅ ((MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)).mapCocone (d.cocone j)).pt :=
  (d.isColimit i).coconePointsIsoOfNatIso
    (isColimitOfPreserves (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)) (d.isColimit j))
    (D.isoWhiskerLeft (MorphismProperty.Over.pullbackComp (Cover.trans 𝒰 hij) (𝒰.f j) (𝒰.f i) ⋯) ≪≫
      (D.associator (MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
          (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))).symm)
heq :
  (MorphismProperty.Over.map ⊤ ⋯).map iso1.hom ≫
      (MorphismProperty.Over.mapPullbackAdj P ⊤ (Cover.trans 𝒰 hij) ⋯ trivial).counit.app (d.cocone j).pt =
    d.transitionMap hij
iso2 : (d.cocone i).pt.left ≅ pullback (d.cocone j).pt.hom (Cover.trans 𝒰 hij) :=
  (MorphismProperty.Over.forget P ⊤ (𝒰.X i) ⋙ CategoryTheory.Over.forget (𝒰.X i)).mapIso iso1
⊢ pullback.snd (d.cocone j).pt.hom (Cover.trans 𝒰 hij) ≫ (Iso.refl (𝒰.X i)).hom = iso2.symm.hom ≫ (d.cocone i).pt.hom

Tactic:
· simpa [← cancel_epi iso2.hom] using! congr($(heq).left)

Goal state after:
case refine_2
P : MorphismProperty Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝² : Category.{v_2, u_2} 𝒰.I₀
inst✝¹ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
i j : 𝒰.I₀
hij : i ⟶ j
iso1 : (d.cocone i).pt ≅ ((MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)).mapCocone (d.cocone j)).pt :=
  (d.isColimit i).coconePointsIsoOfNatIso
    (isColimitOfPreserves (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)) (d.isColimit j))
    (D.isoWhiskerLeft (MorphismProperty.Over.pullbackComp (Cover.trans 𝒰 hij) (𝒰.f j) (𝒰.f i) ⋯) ≪≫
      (D.associator (MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
          (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))).symm)
heq :
  (MorphismProperty.Over.map ⊤ ⋯).map iso1.hom ≫
      (MorphismProperty.Over.mapPullbackAdj P ⊤ (Cover.trans 𝒰 hij) ⋯ trivial).counit.app (d.cocone j).pt =
    d.transitionMap hij
iso2 : (d.cocone i).pt.left ≅ pullback (d.cocone j).pt.hom (Cover.trans 𝒰 hij) :=
  (MorphismProperty.Over.forget P ⊤ (𝒰.X i) ⋙ CategoryTheory.Over.forget (𝒰.X i)).mapIso iso1
⊢ pullback.snd (d.cocone j).pt.hom (Cover.trans 𝒰 hij) ≫ (Iso.refl (𝒰.X i)).hom = iso2.symm.hom ≫ (d.cocone i).pt.hom