-- Mathlib/AlgebraicGeometry/Restrict.lean
theorem Scheme.homOfLE_app {U V : X.Opens} (e : U ≤ V) (W : Opens V) :
    (X.homOfLE e).app W =
      X.presheaf.map (homOfLE <| X.ι_image_homOfLE_le_ι_image e W).op

Proof state:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
e₁ : Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
e₂ :
  (↑V).presheaf.map (eqToIso this).hom.op ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫ (↑U).presheaf.map ((Opens.map (X.homOfLE e).base).map (eqToIso this).hom.op.unop).op
e₃ :
  Hom.app (X.homOfLE e) W ≫
      X.presheaf.map ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op =
    X.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.map ((Hom.opensFunctor U.ι).map (eqToHom ⋯)).op
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op

Tactic:
rw [← IsIso.eq_comp_inv, ← Functor.map_inv, ← Functor.map_comp] at e₃

Result:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
e₁ : Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
e₂ :
  (↑V).presheaf.map (eqToIso this).hom.op ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫ (↑U).presheaf.map ((Opens.map (X.homOfLE e).base).map (eqToIso this).hom.op.unop).op
e₃ :
  Hom.app (X.homOfLE e) W =
    X.presheaf.map ((homOfLE ⋯).op ≫ ((Hom.opensFunctor U.ι).map (eqToHom ⋯)).op) ≫
      X.presheaf.map (inv ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op)
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op

Proof state:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
e₁ : Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
e₂ :
  (↑V).presheaf.map (eqToIso this).hom.op ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫ (↑U).presheaf.map ((Opens.map (X.homOfLE e).base).map (eqToIso this).hom.op.unop).op
e₃ :
  Hom.app (X.homOfLE e) W ≫ (↑U).presheaf.map ((Opens.map (X.homOfLE e).base).map (eqToIso this).hom.op.unop).op =
    Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op

Tactic:
dsimp at e₃ ⊢

Result:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
e₁ : Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
e₂ :
  (↑V).presheaf.map (eqToIso this).hom.op ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫ (↑U).presheaf.map ((Opens.map (X.homOfLE e).base).map (eqToIso this).hom.op.unop).op
e₃ :
  Hom.app (X.homOfLE e) W ≫
      X.presheaf.map ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op =
    X.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.map ((Hom.opensFunctor U.ι).map (eqToHom ⋯)).op
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op

Proof state:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
e₁ : Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
e₂ :
  (↑V).presheaf.map (eqToIso this).hom.op ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫ (↑U).presheaf.map ((Opens.map (X.homOfLE e).base).map (eqToIso this).hom.op.unop).op
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op

Tactic:
have e₃ := e₂.symm.trans e₁

Result:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
e₁ : Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
e₂ :
  (↑V).presheaf.map (eqToIso this).hom.op ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫ (↑U).presheaf.map ((Opens.map (X.homOfLE e).base).map (eqToIso this).hom.op.unop).op
e₃ :
  Hom.app (X.homOfLE e) W ≫ (↑U).presheaf.map ((Opens.map (X.homOfLE e).base).map (eqToIso this).hom.op.unop).op =
    Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op

Proof state:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
e₁ : Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op

Tactic:
have e₂ := (X.homOfLE e).naturality (eqToIso this).hom.op

Result:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
e₁ : Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
e₂ :
  (↑V).presheaf.map (eqToIso this).hom.op ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫ (↑U).presheaf.map ((Opens.map (X.homOfLE e).base).map (eqToIso this).hom.op.unop).op
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op

Proof state:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
e₁ : Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
e₂ :
  (↑V).presheaf.map (eqToIso this).hom.op ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫ (↑U).presheaf.map ((Opens.map (X.homOfLE e).base).map (eqToIso this).hom.op.unop).op
e₃ :
  Hom.app (X.homOfLE e) W =
    X.presheaf.map ((homOfLE ⋯).op ≫ ((Hom.opensFunctor U.ι).map (eqToHom ⋯)).op) ≫
      X.presheaf.map (inv ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op)
⊢ X.presheaf.map
      (((homOfLE ⋯).op ≫ ((Hom.opensFunctor U.ι).map (eqToHom ⋯)).op) ≫
        inv ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op) =
    X.presheaf.map (homOfLE ⋯).op

Tactic:
congr 1

Result:
no goals

Proof state:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op

Tactic:
have e₁ := Scheme.congr_app (X.homOfLE_ι e) (V.ι ''ᵁ W)

Result:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
e₁ : Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op

Proof state:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
e₁ : Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op

Tactic:
have : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W := W.map_functor_eq (U := V)

Result:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
e₁ : Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op