Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: case refine_2
X✝ Y Z T : Scheme
M N K : X✝.Modules
φ : M ⟶ N
U✝ V✝ : X✝.Opens
X : Scheme
U V : X.Opens
f : V ⟶ U
this✝⁴ :
  (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥↑V) (Opens.grothendieckTopology ↑U.carrier)
this✝³ :
  Functor.IsDenseSubsite (Opens.grothendieckTopology ↥U) ((Opens.grothendieckTopology ↥X).over U)
    (Opens.overEquivalence U).inverse
this✝² : (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥V) (Opens.grothendieckTopology ↥↑U)
this✝¹ :
  ((Opens.overEquivalence V).symm.functor ⋙ Over.map f).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
this✝ :
  (Opens.overEquivalence U).symm.functor.IsContinuous (Opens.grothendieckTopology ↥↑U)
    ((Opens.grothendieckTopology ↥X).over U)
this :
  (Hom.opensFunctor (X.homOfLE ⋯) ⋙ (Opens.overEquivalence U).symm.functor).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
W : (TopologicalSpace.Opens ↥V)ᵒᵖ
x : ↑(((Opens.sheafRestrict V).obj X.ringCatSheaf).obj.obj W)
⊢ (RingCat.Hom.hom
        (((((Opens.overPullbackSheafEquivOver V).app X.ringCatSheaf).inv ≫
                  ((Opens.overEquivalence V).symm.functor.sheafPushforwardContinuous RingCat
                        (Opens.grothendieckTopology ↥V) ((Opens.grothendieckTopology ↥X).over V)).map
                    (Sheaf.pushforwardOverMapIso X.ringCatSheaf f).inv) ≫
                (Functor.sheafPushforwardContinuousNatTrans
                      (NatIso.ofComponents (fun W ↦ Over.isoMk (eqToIso ⋯) ⋯) ⋯).hom RingCat
                      (Opens.grothendieckTopology ↥V) ((Opens.grothendieckTopology ↥X).over U)).app
                  (Sheaf.over X.ringCatSheaf U)).hom.app
          W))
      x =
    (RingCat.Hom.hom
        (({
                  hom :=
                    Functor.whiskerRight
                      { app := fun U_1 ↦ (Hom.appIso (X.homOfLE ⋯) (Opposite.unop U_1)).inv, naturality := ⋯ }
                      (forget₂ CommRingCat RingCat) } ≫
                ((Hom.opensFunctor (X.homOfLE ⋯)).sheafPushforwardContinuous RingCat (Opens.grothendieckTopology ↥↑V)
                      (Opens.grothendieckTopology ↥U)).map
                  ((Opens.overPullbackSheafEquivOver U).app X.ringCatSheaf).inv).hom.app
          W))
      x

Tactic:
suffices X.presheaf.map _ x = ((X.homOfLE <| leOfHom f).appIso _).inv x by simpa

Goal state after:
case refine_2
X✝ Y Z T : Scheme
M N K : X✝.Modules
φ : M ⟶ N
U✝ V✝ : X✝.Opens
X : Scheme
U V : X.Opens
f : V ⟶ U
this✝⁴ :
  (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥↑V) (Opens.grothendieckTopology ↑U.carrier)
this✝³ :
  Functor.IsDenseSubsite (Opens.grothendieckTopology ↥U) ((Opens.grothendieckTopology ↥X).over U)
    (Opens.overEquivalence U).inverse
this✝² : (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥V) (Opens.grothendieckTopology ↥↑U)
this✝¹ :
  ((Opens.overEquivalence V).symm.functor ⋙ Over.map f).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
this✝ :
  (Opens.overEquivalence U).symm.functor.IsContinuous (Opens.grothendieckTopology ↥↑U)
    ((Opens.grothendieckTopology ↥X).over U)
this :
  (Hom.opensFunctor (X.homOfLE ⋯) ⋙ (Opens.overEquivalence U).symm.functor).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
W : (TopologicalSpace.Opens ↥V)ᵒᵖ
x : ↑(((Opens.sheafRestrict V).obj X.ringCatSheaf).obj.obj W)
⊢ (ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯))) x =
    (ConcreteCategory.hom (Hom.appIso (X.homOfLE ⋯) (Opposite.unop W)).inv) x