awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
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))))
⊢ 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 ⋯))
have 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 sorry))) :
          (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: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
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))))
| Spec.map f ∣_ basicOpen r ≫
    ⋯.isoSpec.hom ≫
      Spec.map
        (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫ e₁.toRingEquiv.toCommRingCatIso.hom)
have a : sorry.isoSpec.hom ≫
  Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫ e₁.toRingEquiv.toCommRingCatIso.hom)
Tactic: 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
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 :
  ⋯.isoSpec.hom ≫
    Spec.map
      (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)
have a₁ : Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫ e₁.toRingEquiv.toCommRingCatIso.hom)
Tactic: 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
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 :
  ⋯.isoSpec.hom ≫
    Spec.map
      (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫ e₁.toRingEquiv.toCommRingCatIso.hom)
a₁ :
  Spec.map (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)
have a₂ : CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫ e₁.toRingEquiv.toCommRingCatIso.hom
Tactic: 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
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))))
| Spec.map f ∣_ basicOpen r ≫
    ⋯.isoSpec.hom ≫
      Spec.map
        (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫ e₁.toRingEquiv.toCommRingCatIso.hom)
have a : sorry.isoSpec.hom ≫
  Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫ e₁.toRingEquiv.toCommRingCatIso.hom)
Tactic: · 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
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 :
  ⋯.isoSpec.hom ≫
    Spec.map
      (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)
have a₁ : Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫ e₁.toRingEquiv.toCommRingCatIso.hom)
Tactic: · 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
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 :
  ⋯.isoSpec.hom ≫
    Spec.map
      (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫ e₁.toRingEquiv.toCommRingCatIso.hom)
a₁ :
  Spec.map (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)
have a₂ : CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫ e₁.toRingEquiv.toCommRingCatIso.hom
Tactic: · 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
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))))
| 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))
have a : Iso.hom (IsAffineOpen.isoSpec sorry) ≫
  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: 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
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)
| 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))
have a₁ : Spec.map f ∣_ basicOpen r ≫
  sorry.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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
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))))
⊢ 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))
have refine_3 : Iso.hom (IsAffineOpen.isoSpec sorry) ≫
    Spec.map (f ≫ (Scheme.ΓSpecIso S).inv ≫ (Spec S).presheaf.map (Quiver.Hom.op (homOfLE sorry))) =
  Spec.map f ∣_ basicOpen r ≫
    sorry.isoSpec.hom ≫ Spec.map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.map (Quiver.Hom.op (homOfLE sorry)))
Tactic: conv =>
      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]