awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫
    CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r) ≫ e₂.toRingEquiv.toCommRingCatIso.hom
| 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)

Tactic:
enter [2, 1]
-- 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 :
  CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫
      CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r) ≫ e₂.toRingEquiv.toCommRingCatIso.hom =
    f ≫ (Scheme.ΓSpecIso S).inv ≫ (Spec S).presheaf.map (Quiver.Hom.op (homOfLE ⋯))
⊢ CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫
      CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r) ≫ e₂.toRingEquiv.toCommRingCatIso.hom =
    f ≫ (Scheme.ΓSpecIso S).inv ≫ (Spec S).presheaf.map (Quiver.Hom.op (homOfLE ⋯))

Tactic:
change _ =
          (f ≫ (Scheme.ΓSpecIso S).inv ≫ (Spec S).presheaf.map (homOfLE le_top).op)

Premises used: AlgebraicGeometry.Spec, Quiver.Hom.op, AlgebraicGeometry.Scheme.ΓSpecIso, CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, le_top, CategoryTheory.homOfLE, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, CategoryTheory.Iso.inv, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- 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 :
  ∀ (x : (↑(CommRingCat.of (↑R : Type u_1)) : Type u_1)),
    Eq (α :=
      (↑((Spec S).presheaf.1 (op (basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)))) :
        Type u_1))
      ((CommRingCat.Hom.hom
              (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫
                CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r) ≫
                  e₂.toRingEquiv.toCommRingCatIso.hom) :
            (a : (↑(CommRingCat.of (↑R : Type u_1)) : Type u_1)) →
              (↑((Spec S).presheaf.1
                    (op (basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)))) :
                Type u_1))
          x :
        (↑((Spec S).presheaf.1 (op (basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)))) :
          Type u_1))
      ((CommRingCat.Hom.hom (f ≫ (Scheme.ΓSpecIso S).inv ≫ (Spec S).presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
            (a : (↑(CommRingCat.of (↑R : Type u_1)) : Type u_1)) →
              (↑((Spec S).presheaf.1
                    (op (basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)))) :
                Type u_1))
          x :
        (↑((Spec S).presheaf.1 (op (basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)))) :
          Type u_1))
⊢ CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫
      CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r) ≫ e₂.toRingEquiv.toCommRingCatIso.hom =
    f ≫ (Scheme.ΓSpecIso S).inv ≫ (Spec S).presheaf.map (Quiver.Hom.op (homOfLE ⋯))

Tactic:
ext
-- 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))))
x : (↑(CommRingCat.of (↑R : Type u_1)) : Type u_1)
⊢ Eq (α :=
    (↑((Spec S).presheaf.1 (op (basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)))) :
      Type u_1))
    ((CommRingCat.Hom.hom
            (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫
              CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r) ≫
                e₂.toRingEquiv.toCommRingCatIso.hom) :
          (a : (↑(CommRingCat.of (↑R : Type u_1)) : Type u_1)) →
            (↑((Spec S).presheaf.1
                  (op (basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)))) :
              Type u_1))
        x :
      (↑((Spec S).presheaf.1 (op (basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)))) :
        Type u_1))
    ((CommRingCat.Hom.hom (f ≫ (Scheme.ΓSpecIso S).inv ≫ (Spec S).presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑(CommRingCat.of (↑R : Type u_1)) : Type u_1)) →
            (↑((Spec S).presheaf.1
                  (op (basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)))) :
              Type u_1))
        x :
      (↑((Spec S).presheaf.1 (op (basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)))) :
        Type u_1))

Tactic:
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]

Premises used: AlgEquiv.toRingEquiv_toRingHom, RingHom.coe_coe, AlgEquiv.commutes, AlgebraicGeometry.IsAffineOpen.algebraMap_Spec_obj, IsLocalization.map_eq, RingEquiv.toCommRingCatIso_hom, CommRingCat.hom_comp, IsLocalization.Away.map, CommRingCat.hom_ofHom, Localization.awayMap, RingHom.comp_apply
-- 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 :
  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₂ :
  CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫
    CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r) ≫ e₂.toRingEquiv.toCommRingCatIso.hom
| 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)

Tactic:
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]

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.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, IsLocalization.Away.map, CommRingCat.hom_ofHom, le_top, CategoryTheory.homOfLE, Localization.awayMap, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.PresheafedSpace.presheaf, RingHom.comp_apply, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, CategoryTheory.Iso.inv, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- 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))))
| 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)

Tactic:
· 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]

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.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, IsLocalization.Away.map, CommRingCat.hom_ofHom, le_top, CategoryTheory.homOfLE, Localization.awayMap, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.PresheafedSpace.presheaf, RingHom.comp_apply, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, CategoryTheory.Iso.inv, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- 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 : CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away 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:
enter [2, 2, 1]
-- 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 :
  CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫ e₁.toRingEquiv.toCommRingCatIso.hom =
    (Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.map (Quiver.Hom.op (homOfLE ⋯))
⊢ CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫ e₁.toRingEquiv.toCommRingCatIso.hom =
    (Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.map (Quiver.Hom.op (homOfLE ⋯))

Tactic:
change _ = (Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.map (homOfLE le_top).op

Premises used: AlgebraicGeometry.Spec, Quiver.Hom.op, AlgebraicGeometry.Scheme.ΓSpecIso, CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, le_top, CategoryTheory.homOfLE, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, CategoryTheory.Iso.inv, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- 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 :
  ∀ (x : (↑(CommRingCat.of (↑R : Type u_1)) : Type u_1)),
    Eq (α := (↑((Spec R).presheaf.1 (op (basicOpen r))) : Type u_1))
      ((CommRingCat.Hom.hom
              (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫
                e₁.toRingEquiv.toCommRingCatIso.hom) :
            (a : (↑(CommRingCat.of (↑R : Type u_1)) : Type u_1)) →
              (↑((Spec R).presheaf.1 (op (basicOpen r))) : Type u_1))
          x :
        (↑((Spec R).presheaf.1 (op (basicOpen r))) : Type u_1))
      ((CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
            (a : (↑(CommRingCat.of (↑R : Type u_1)) : Type u_1)) →
              (↑((Spec R).presheaf.1 (op (basicOpen r))) : Type u_1))
          x :
        (↑((Spec R).presheaf.1 (op (basicOpen r))) : Type u_1))
⊢ CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫ e₁.toRingEquiv.toCommRingCatIso.hom =
    (Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.map (Quiver.Hom.op (homOfLE ⋯))

Tactic:
ext
-- 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))))
x : (↑(CommRingCat.of (↑R : Type u_1)) : Type u_1)
⊢ Eq (α := (↑((Spec R).presheaf.1 (op (basicOpen r))) : Type u_1))
    ((CommRingCat.Hom.hom
            (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫
              e₁.toRingEquiv.toCommRingCatIso.hom) :
          (a : (↑(CommRingCat.of (↑R : Type u_1)) : Type u_1)) → (↑((Spec R).presheaf.1 (op (basicOpen r))) : Type u_1))
        x :
      (↑((Spec R).presheaf.1 (op (basicOpen r))) : Type u_1))
    ((CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑(CommRingCat.of (↑R : Type u_1)) : Type u_1)) → (↑((Spec R).presheaf.1 (op (basicOpen r))) : Type u_1))
        x :
      (↑((Spec R).presheaf.1 (op (basicOpen r))) : Type u_1))

Tactic:
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: AlgEquiv.toRingEquiv_toRingHom, RingHom.coe_coe, AlgEquiv.commutes, AlgebraicGeometry.IsAffineOpen.algebraMap_Spec_obj, RingEquiv.toCommRingCatIso_hom, CommRingCat.hom_comp, CategoryTheory.homOfLE_leOfHom, CommRingCat.hom_ofHom, RingHom.coe_comp, Function.comp_apply