trace of `RespectsIso.ofRestrict_morphismRestrict_iff`

trace.txt

          [] [0.065395s] letI a1 :
                Algebra (Scheme.Γ.obj (Opposite.op Y))
                  (Scheme.Γ.obj (Opposite.op (Y.restrict (Y.basicOpen r).openEmbedding))) :=
                ΓRestrictAlgebra _ ▶
          [] [0.089443s] let U' :=
                ((Opens.map (X.ofRestrict ((Opens.map f.val.base).obj (Y.basicOpen r)).openEmbedding).val.base).obj
                    U).openEmbedding ▶
          [] [3.890884s] letI a2 :
                Algebra (Scheme.Γ.obj (Opposite.op (X.restrict U.openEmbedding)))
                  (Scheme.Γ.obj <|
                    Opposite.op <|
                      (X.restrict ((Opens.map f.val.base).obj (Y.basicOpen r)).openEmbedding).restrict U') :=
                by
                apply RingHom.toAlgebra
                refine X.presheaf.map (@homOfLE _ _ ((IsOpenMap.functor _).obj _) ((IsOpenMap.functor _).obj _) ?_).op
                rw [← SetLike.coe_subset_coe, Functor.op_obj]
                dsimp [Opens.inclusion]
                simp only [Set.image_univ, Set.image_subset_iff, Subtype.range_val]
                rw [ContinuousMap.coe_mk, Subtype.range_val, ContinuousMap.coe_mk, ContinuousMap.coe_mk,
                  Subtype.range_val]
                rfl ▶
          [] [0.025638s] have i1 := AlgebraicGeometry.Γ_restrict_isLocalization Y r ▶
          [] [6.113126s] have i2 :
                IsLocalization.Away ((Scheme.Γ.map (X.ofRestrict U.openEmbedding ≫ f).op) r)
                  (Scheme.Γ.obj <|
                    Opposite.op <|
                      (X.restrict ((Opens.map f.val.base).obj (Y.basicOpen r)).openEmbedding).restrict U') :=
                by
                rw [← U.openEmbedding_obj_top] at hU 
                dsimp [Scheme.Γ_obj_op, Scheme.Γ_map_op, Scheme.restrict]
                apply AlgebraicGeometry.isLocalization_of_eq_basicOpen _ hU
                rw [Opens.openEmbedding_obj_top, Opens.functor_obj_map_obj]
                convert (X.basicOpen_res (Scheme.Γ.map f.op r) (homOfLE le_top).op).symm using 1
                rw [Opens.openEmbedding_obj_top, Opens.openEmbedding_obj_top, inf_comm, Scheme.Γ_map_op]
                  -- Porting note : changed `rw` to `erw`
                erw [← Scheme.preimage_basicOpen] ▶
          [] [0.382143s] have :=
                @RespectsIso.is_localization_away_iff (hP := hP) (R := Scheme.Γ.obj <| Opposite.op Y) (S :=
                  Scheme.Γ.obj (Opposite.op (X.restrict U.openEmbedding))) (R' :=
                  Scheme.Γ.obj (Opposite.op (Y.restrict (Y.basicOpen r).openEmbedding))) (S' :=
                  Scheme.Γ.obj <|
                    Opposite.op <| (X.restrict ((Opens.map f.val.base).obj (Y.basicOpen r)).openEmbedding).restrict U')
                  _ _ _ _ _ _ (Scheme.Γ.map (X.ofRestrict U.openEmbedding ≫ f).op) r ▶
          [] [2.005261s] rw [this, iff_iff_eq] ▶
          [] [0.133919s] congr 1 ▶
          [] [0.926955s] apply IsLocalization.ringHom_ext (R := Scheme.Γ.obj (Opposite.op Y)) (Submonoid.powers r) _ ▶
          [] [6.187248s] rw [IsLocalization.Away.map, IsLocalization.map_comp, RingHom.algebraMap_toAlgebra] ▶
          [] [4.651918s] rw [op_comp, op_comp, Functor.map_comp, Functor.map_comp] ▶
          [] [2.535332s] change _ = comp (X.presheaf.map _) _ ▶
          [] [2.502509s] refine' (@Category.assoc CommRingCat _ _ _ _ _ _ _ _).symm.trans _ ▶
          [] [37.740924s] refine' Eq.trans _ (@Category.assoc CommRingCat _ _ _ _ _ _ _ _) ▶
          [] [0.034441s] dsimp only [Scheme.Γ_map, Quiver.Hom.unop_op] 
          [] [40.784633s] rw [morphismRestrict_c_app, Category.assoc, Category.assoc, Category.assoc] ▶
          [] [139.291024s] erw [f.1.c.naturality_assoc, ← X.presheaf.map_comp, ← X.presheaf.map_comp, ← X.presheaf.map_comp] ▶
          [] [2.122772s] congr 1 ▶
      [Kernel] [0.191193s] typechecking declaration