-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
rw :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      ((Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V)) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₁ :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₂ :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(U, g ⁻¹ᵁ g ''ᵁ V)) (U.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
      (Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₃ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      CategoryStruct.comp (Y := Γ(Y, f ⁻¹ᵁ g ⁻¹ᵁ g ''ᵁ V))
        (Y.presheaf.map (Quiver.Hom.op ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯))))))
        (Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₄ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := op ((Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)))
          (Quiver.Hom.op ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯)))))
          (Quiver.Hom.op (eqToHom ⋯)))
rw₅ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := (Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)) (eqToHom ⋯ : f ⁻¹ᵁ V ⟶ (f ≫ g) ⁻¹ᵁ g ''ᵁ V)
            ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯))))).op
rw₆ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := (Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)) (eqToHom ⋯ : f ⁻¹ᵁ V ⟶ (f ≫ g) ⁻¹ᵁ g ''ᵁ V)
            ((Opens.map f.base).map (eqToHom ⋯))).op
rw₇ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := (Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)) (eqToHom ⋯ : f ⁻¹ᵁ V ⟶ (f ≫ g) ⁻¹ᵁ g ''ᵁ V)
            (eqToHom ⋯)).op
rw₈ : Scheme.Hom.app f V = Scheme.Hom.app f V ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯))
rw₉ : Scheme.Hom.app f V = Scheme.Hom.app f V ≫ Y.presheaf.map (eqToHom ⋯)
rw₁₀ : Scheme.Hom.app f V = Scheme.Hom.app f V ≫ Y.presheaf.map (𝟙 (op ((Opens.map f.base).obj V)))
rw₁₁ : Scheme.Hom.app f V = Scheme.Hom.app f V ≫ 𝟙 Γ(Y, f ⁻¹ᵁ V)
rw₁₂ rw₁₃ : Scheme.Hom.app f V = Scheme.Hom.app f V
⊢ Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app (f ≫ g) (g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))

Tactic:
rw [Scheme.Hom.comp_app, Category.assoc, Scheme.Hom.appIso_inv_app_assoc, f.naturality_assoc,
    ← Functor.map_comp, ← op_comp, Quiver.Hom.unop_op, eqToHom_map, eqToHom_trans,
    eqToHom_op, eqToHom_refl, CategoryTheory.Functor.map_id, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, Quiver.Hom.unop_op, CategoryTheory.eqToHom_map, AlgebraicGeometry.Scheme.Hom.comp_app, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_assoc, AlgebraicGeometry.Scheme.Hom.naturality_assoc, CategoryTheory.eqToHom_op, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.eqToHom_trans