-- Mathlib/AlgebraicGeometry/Restrict.lean
theorem morphismRestrict_app {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) (V : U.toScheme.Opens) :
    (f ∣_ U).app V = f.app (U.ι ''ᵁ V) ≫
        X.presheaf.map (eqToHom (image_morphismRestrict_preimage f U V)).op

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
this :
  Y.presheaf.map (homOfLE ⋯).op ≫ Hom.appLE (f ∣_ U) (U.ι ⁻¹ᵁ U.ι ''ᵁ V) ((f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V) ⋯ =
    (Hom.appLE f (U.ι ''ᵁ V) (f ⁻¹ᵁ U.ι ''ᵁ V) ⋯ ≫ X.presheaf.map (homOfLE ⋯).op) ≫
      X.presheaf.map ((Hom.opensFunctor (f ⁻¹ᵁ U).ι).map (eqToHom ⋯)).op
e : U.ι ⁻¹ᵁ U.ι ''ᵁ V = V
e' : (f ∣_ U) ⁻¹ᵁ V = (f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V
⊢ Hom.app (f ∣_ U) V = Hom.app f (U.ι ''ᵁ V) ≫ X.presheaf.map (eqToHom ⋯).op

Tactic:
simp only [Opens.toScheme_presheaf_obj, Hom.app_eq_appLE, eqToHom_op, Hom.appLE_map]

Result:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
this :
  Y.presheaf.map (homOfLE ⋯).op ≫ Hom.appLE (f ∣_ U) (U.ι ⁻¹ᵁ U.ι ''ᵁ V) ((f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V) ⋯ =
    (Hom.appLE f (U.ι ''ᵁ V) (f ⁻¹ᵁ U.ι ''ᵁ V) ⋯ ≫ X.presheaf.map (homOfLE ⋯).op) ≫
      X.presheaf.map ((Hom.opensFunctor (f ⁻¹ᵁ U).ι).map (eqToHom ⋯)).op
e : U.ι ⁻¹ᵁ U.ι ''ᵁ V = V
e' : (f ∣_ U) ⁻¹ᵁ V = (f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V
⊢ Hom.appLE (f ∣_ U) V ((f ∣_ U) ⁻¹ᵁ V) ⋯ = Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V) ⋯

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
this :
  Y.presheaf.map (homOfLE ⋯).op ≫ Hom.appLE (f ∣_ U) (U.ι ⁻¹ᵁ U.ι ''ᵁ V) ((f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V) ⋯ =
    (Hom.appLE f (U.ι ''ᵁ V) (f ⁻¹ᵁ U.ι ''ᵁ V) ⋯ ≫ X.presheaf.map (homOfLE ⋯).op) ≫
      X.presheaf.map ((Hom.opensFunctor (f ⁻¹ᵁ U).ι).map (eqToHom ⋯)).op
e : U.ι ⁻¹ᵁ U.ι ''ᵁ V = V
⊢ (f ∣_ U) ⁻¹ᵁ V = (f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V

Tactic:
rw [e]

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
this :
  Hom.app (f ∣_ U ≫ U.ι) (U.ι ''ᵁ V) = Hom.app ((f ⁻¹ᵁ U).ι ≫ f) (U.ι ''ᵁ V) ≫ (↑(f ⁻¹ᵁ U)).presheaf.map (eqToHom ⋯).op
⊢ Hom.app (f ∣_ U) V = Hom.app f (U.ι ''ᵁ V) ≫ X.presheaf.map (eqToHom ⋯).op

Tactic:
simp only [Scheme.preimage_comp, Opens.toScheme_presheaf_obj, Hom.app_eq_appLE, comp_appLE,
  Opens.ι_appLE, eqToHom_op, Opens.toScheme_presheaf_map, eqToHom_unop] at this

Result:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
this :
  Y.presheaf.map (homOfLE ⋯).op ≫ Hom.appLE (f ∣_ U) (U.ι ⁻¹ᵁ U.ι ''ᵁ V) ((f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V) ⋯ =
    (Hom.appLE f (U.ι ''ᵁ V) (f ⁻¹ᵁ U.ι ''ᵁ V) ⋯ ≫ X.presheaf.map (homOfLE ⋯).op) ≫
      X.presheaf.map ((Hom.opensFunctor (f ⁻¹ᵁ U).ι).map (eqToHom ⋯)).op
⊢ Hom.app (f ∣_ U) V = Hom.app f (U.ι ''ᵁ V) ≫ X.presheaf.map (eqToHom ⋯).op

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
⊢ Hom.app (f ∣_ U) V = Hom.app f (U.ι ''ᵁ V) ≫ X.presheaf.map (eqToHom ⋯).op

Tactic:
have := Scheme.congr_app (morphismRestrict_ι f U) (U.ι ''ᵁ V)

Result:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
this :
  Hom.app (f ∣_ U ≫ U.ι) (U.ι ''ᵁ V) = Hom.app ((f ⁻¹ᵁ U).ι ≫ f) (U.ι ''ᵁ V) ≫ (↑(f ⁻¹ᵁ U)).presheaf.map (eqToHom ⋯).op
⊢ Hom.app (f ∣_ U) V = Hom.app f (U.ι ''ᵁ V) ≫ X.presheaf.map (eqToHom ⋯).op

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
this :
  Y.presheaf.map (homOfLE ⋯).op ≫ Hom.appLE (f ∣_ U) (U.ι ⁻¹ᵁ U.ι ''ᵁ V) ((f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V) ⋯ =
    (Hom.appLE f (U.ι ''ᵁ V) (f ⁻¹ᵁ U.ι ''ᵁ V) ⋯ ≫ X.presheaf.map (homOfLE ⋯).op) ≫
      X.presheaf.map ((Hom.opensFunctor (f ⁻¹ᵁ U).ι).map (eqToHom ⋯)).op
e : U.ι ⁻¹ᵁ U.ι ''ᵁ V = V
e' : (f ∣_ U) ⁻¹ᵁ V = (f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V
⊢ ((↑U).presheaf.map (eqToHom e).op ≫ Hom.appLE (f ∣_ U) (U.ι ⁻¹ᵁ U.ι ''ᵁ V) ((f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V) ⋯) ≫
      (↑(f ⁻¹ᵁ U)).presheaf.map (eqToHom e').op =
    Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V) ⋯

Tactic:
simp only [Opens.toScheme_presheaf_obj, eqToHom_eq_homOfLE, Opens.toScheme_presheaf_map,
  Quiver.Hom.unop_op, Hom.opensFunctor_map_homOfLE]

Result:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
this :
  Y.presheaf.map (homOfLE ⋯).op ≫ Hom.appLE (f ∣_ U) (U.ι ⁻¹ᵁ U.ι ''ᵁ V) ((f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V) ⋯ =
    (Hom.appLE f (U.ι ''ᵁ V) (f ⁻¹ᵁ U.ι ''ᵁ V) ⋯ ≫ X.presheaf.map (homOfLE ⋯).op) ≫
      X.presheaf.map ((Hom.opensFunctor (f ⁻¹ᵁ U).ι).map (eqToHom ⋯)).op
e : U.ι ⁻¹ᵁ U.ι ''ᵁ V = V
e' : (f ∣_ U) ⁻¹ᵁ V = (f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V
⊢ (Y.presheaf.map (homOfLE ⋯).op ≫ Hom.appLE (f ∣_ U) (U.ι ⁻¹ᵁ U.ι ''ᵁ V) ((f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V) ⋯) ≫
      X.presheaf.map (homOfLE ⋯).op =
    Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V) ⋯

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
this :
  Y.presheaf.map (homOfLE ⋯).op ≫ Hom.appLE (f ∣_ U) (U.ι ⁻¹ᵁ U.ι ''ᵁ V) ((f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V) ⋯ =
    (Hom.appLE f (U.ι ''ᵁ V) (f ⁻¹ᵁ U.ι ''ᵁ V) ⋯ ≫ X.presheaf.map (homOfLE ⋯).op) ≫
      X.presheaf.map ((Hom.opensFunctor (f ⁻¹ᵁ U).ι).map (eqToHom ⋯)).op
e : U.ι ⁻¹ᵁ U.ι ''ᵁ V = V
⊢ Hom.app (f ∣_ U) V = Hom.app f (U.ι ''ᵁ V) ≫ X.presheaf.map (eqToHom ⋯).op

Tactic:
have e' : (f ∣_ U) ⁻¹ᵁ V = (f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V := by rw [e]

Result:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
this :
  Y.presheaf.map (homOfLE ⋯).op ≫ Hom.appLE (f ∣_ U) (U.ι ⁻¹ᵁ U.ι ''ᵁ V) ((f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V) ⋯ =
    (Hom.appLE f (U.ι ''ᵁ V) (f ⁻¹ᵁ U.ι ''ᵁ V) ⋯ ≫ X.presheaf.map (homOfLE ⋯).op) ≫
      X.presheaf.map ((Hom.opensFunctor (f ⁻¹ᵁ U).ι).map (eqToHom ⋯)).op
e : U.ι ⁻¹ᵁ U.ι ''ᵁ V = V
e' : (f ∣_ U) ⁻¹ᵁ V = (f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V
⊢ Hom.app (f ∣_ U) V = Hom.app f (U.ι ''ᵁ V) ≫ X.presheaf.map (eqToHom ⋯).op

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
this :
  Y.presheaf.map (homOfLE ⋯).op ≫ Hom.appLE (f ∣_ U) (U.ι ⁻¹ᵁ U.ι ''ᵁ V) ((f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V) ⋯ =
    (Hom.appLE f (U.ι ''ᵁ V) (f ⁻¹ᵁ U.ι ''ᵁ V) ⋯ ≫ X.presheaf.map (homOfLE ⋯).op) ≫
      X.presheaf.map ((Hom.opensFunctor (f ⁻¹ᵁ U).ι).map (eqToHom ⋯)).op
e : U.ι ⁻¹ᵁ U.ι ''ᵁ V = V
e' : (f ∣_ U) ⁻¹ᵁ V = (f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V
⊢ (Y.presheaf.map (homOfLE ⋯).op ≫ Hom.appLE (f ∣_ U) (U.ι ⁻¹ᵁ U.ι ''ᵁ V) ((f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V) ⋯) ≫
      X.presheaf.map (homOfLE ⋯).op =
    Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V) ⋯

Tactic:
rw [this, Hom.appLE_map, Hom.appLE_map, Hom.appLE_map]

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
this :
  Y.presheaf.map (homOfLE ⋯).op ≫ Hom.appLE (f ∣_ U) (U.ι ⁻¹ᵁ U.ι ''ᵁ V) ((f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V) ⋯ =
    (Hom.appLE f (U.ι ''ᵁ V) (f ⁻¹ᵁ U.ι ''ᵁ V) ⋯ ≫ X.presheaf.map (homOfLE ⋯).op) ≫
      X.presheaf.map ((Hom.opensFunctor (f ⁻¹ᵁ U).ι).map (eqToHom ⋯)).op
e : U.ι ⁻¹ᵁ U.ι ''ᵁ V = V
e' : (f ∣_ U) ⁻¹ᵁ V = (f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V
⊢ Hom.appLE (f ∣_ U) V ((f ∣_ U) ⁻¹ᵁ V) ⋯ = Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V) ⋯

Tactic:
rw [← (f ∣_ U).appLE_map' _ e', ← (f ∣_ U).map_appLE' _ e]

Result:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
this :
  Y.presheaf.map (homOfLE ⋯).op ≫ Hom.appLE (f ∣_ U) (U.ι ⁻¹ᵁ U.ι ''ᵁ V) ((f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V) ⋯ =
    (Hom.appLE f (U.ι ''ᵁ V) (f ⁻¹ᵁ U.ι ''ᵁ V) ⋯ ≫ X.presheaf.map (homOfLE ⋯).op) ≫
      X.presheaf.map ((Hom.opensFunctor (f ⁻¹ᵁ U).ι).map (eqToHom ⋯)).op
e : U.ι ⁻¹ᵁ U.ι ''ᵁ V = V
e' : (f ∣_ U) ⁻¹ᵁ V = (f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V
⊢ ((↑U).presheaf.map (eqToHom e).op ≫ Hom.appLE (f ∣_ U) (U.ι ⁻¹ᵁ U.ι ''ᵁ V) ((f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V) ⋯) ≫
      (↑(f ⁻¹ᵁ U)).presheaf.map (eqToHom e').op =
    Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V) ⋯