-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R S : CommRingCat
f : R ⟶ S
r : (↑R : Type u_1)
e₁ : Localization.Away r ≃ₐ[(↑R : Type u_1)] (↑Γ(Spec R, basicOpen r) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (↑Γ(Spec R, basicOpen r) : Type u_1)
e₂ : Localization.Away (M := (↑S : Type u_1))
    ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)) ≃ₐ[(↑S : Type u_1)]
  (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r))
    (Localization.Away (M := (↑S : Type u_1))
      ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)))
    (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1)
this :
  IsOpenImmersion.{u_1} (X := Spec (CommRingCat.of (Localization.Away r))) (Y := Spec (CommRingCat.of (↑R : Type u_1)))
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r))))
a :
  Iso.hom (IsAffineOpen.isoSpec ⋯) ≫
    Spec.map
      (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫
        CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r) ≫ e₂.toRingEquiv.toCommRingCatIso.hom)
a₁ a₂ :
  Spec.map f ∣_ basicOpen r ≫
    ⋯.isoSpec.hom ≫
      Spec.map
        (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫ e₁.toRingEquiv.toCommRingCatIso.hom)
| Eq (α := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme) ⟶ Spec (CommRingCat.of (↑R : Type u_1)))
    (Iso.hom (IsAffineOpen.isoSpec ⋯) ≫
      Spec.map
        (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫
          CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r) ≫ e₂.toRingEquiv.toCommRingCatIso.hom))
    (Spec.map f ∣_ basicOpen r ≫
      ⋯.isoSpec.hom ≫
        Spec.map
          (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫ e₁.toRingEquiv.toCommRingCatIso.hom))

Tactic:
congr
      · enter [2, 1]; tactic =>
        change _ =
          (f ≫ (Scheme.ΓSpecIso S).inv ≫ (Spec S).presheaf.map (homOfLE le_top).op)
        ext
        simp only [Localization.awayMap, IsLocalization.Away.map,
          RingEquiv.toCommRingCatIso_hom, AlgEquiv.toRingEquiv_toRingHom, CommRingCat.hom_comp,
          CommRingCat.hom_ofHom, RingHom.comp_apply, IsLocalization.map_eq, RingHom.coe_coe,
          AlgEquiv.commutes, IsAffineOpen.algebraMap_Spec_obj]
      · enter [2, 2, 1]; tactic =>
        change _ = (Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.map (homOfLE le_top).op
        ext
        simp only [RingEquiv.toCommRingCatIso_hom,
          AlgEquiv.toRingEquiv_toRingHom, CommRingCat.hom_comp, CommRingCat.hom_ofHom,
          RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, AlgEquiv.commutes,
          IsAffineOpen.algebraMap_Spec_obj, homOfLE_leOfHom]

Premises used: AlgebraicGeometry.Spec, AlgEquiv.toRingEquiv_toRingHom, Quiver.Hom.op, RingHom.coe_coe, AlgEquiv.commutes, AlgebraicGeometry.IsAffineOpen.algebraMap_Spec_obj, IsLocalization.map_eq, AlgebraicGeometry.Scheme.ΓSpecIso, RingEquiv.toCommRingCatIso_hom, CommRingCat.hom_comp, CategoryTheory.homOfLE_leOfHom, CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, IsLocalization.Away.map, CommRingCat.hom_ofHom, le_top, CategoryTheory.homOfLE, Localization.awayMap, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.PresheafedSpace.presheaf, RingHom.coe_comp, RingHom.comp_apply, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Function.comp_apply, CategoryTheory.Iso.inv, AlgebraicGeometry.Scheme.toLocallyRingedSpace