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)
refine_1 :
  (Arrow.mk (X := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme)) (Spec.map f ∣_ basicOpen r)).left ≅
    (Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))).left
refine_2 :
  (Arrow.mk (X := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme)) (Spec.map f ∣_ basicOpen r)).right ≅
    (Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))).right
⊢ Arrow.mk (X := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme)) (Spec.map f ∣_ basicOpen r) ≅
    Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))
have refine_3 : Iso.hom ((Spec S).isoOfEq sorry ≪≫ IsAffineOpen.isoSpec sorry ≪≫ Scheme.Spec.mapIso e₂.toRingEquiv.toCommRingCatIso.op) ≫
    (Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))).hom =
  (Arrow.mk (X := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme)) (Spec.map f ∣_ basicOpen r)).hom ≫
    (sorry.isoSpec ≪≫ Scheme.Spec.mapIso e₁.toRingEquiv.toCommRingCatIso.op).hom
Tactic: refine Arrow.isoMk ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (hypothesis)
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)
⊢ Iso.hom ((Spec S).isoOfEq ⋯ ≪≫ IsAffineOpen.isoSpec ⋯ ≪≫ Scheme.Spec.mapIso e₂.toRingEquiv.toCommRingCatIso.op) ≫
      (Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))).hom =
    (Arrow.mk (X := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme)) (Spec.map f ∣_ basicOpen r)).hom ≫
      (⋯.isoSpec ≪≫ Scheme.Spec.mapIso e₁.toRingEquiv.toCommRingCatIso.op).hom
have 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))))
Tactic: have := AlgebraicGeometry.IsOpenImmersion.of_isLocalization
      (S := (Localization.Away r)) r
-- 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))))
⊢ Iso.hom ((Spec S).isoOfEq ⋯ ≪≫ IsAffineOpen.isoSpec ⋯ ≪≫ Scheme.Spec.mapIso e₂.toRingEquiv.toCommRingCatIso.op) ≫
      (Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))).hom =
    (Arrow.mk (X := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme)) (Spec.map f ∣_ basicOpen r)).hom ≫
      (⋯.isoSpec ≪≫ Scheme.Spec.mapIso e₁.toRingEquiv.toCommRingCatIso.op).hom
have refine_3 : Eq (α :=
  (Arrow.mk (X := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme)) (Spec.map f ∣_ basicOpen r)).left ⟶
    Spec (CommRingCat.of (↑R : Type u_1)))
  ((Iso.hom ((Spec S).isoOfEq sorry ≪≫ IsAffineOpen.isoSpec sorry ≪≫ Scheme.Spec.mapIso e₂.toRingEquiv.toCommRingCatIso.op) ≫
      (Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))).hom) ≫
    Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r))))
  (((Arrow.mk (X := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme)) (Spec.map f ∣_ basicOpen r)).hom ≫
      (sorry.isoSpec ≪≫ Scheme.Spec.mapIso e₁.toRingEquiv.toCommRingCatIso.op).hom) ≫
    Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r))))
Tactic: rw [← cancel_mono (Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away r))))]
-- 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 (α :=
    (Arrow.mk (X := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme)) (Spec.map f ∣_ basicOpen r)).left ⟶
      Spec (CommRingCat.of (↑R : Type u_1)))
    ((Iso.hom ((Spec S).isoOfEq ⋯ ≪≫ IsAffineOpen.isoSpec ⋯ ≪≫ Scheme.Spec.mapIso e₂.toRingEquiv.toCommRingCatIso.op) ≫
        (Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))).hom) ≫
      Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r))))
    (((Arrow.mk (X := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme)) (Spec.map f ∣_ basicOpen r)).hom ≫
        (⋯.isoSpec ≪≫ Scheme.Spec.mapIso e₁.toRingEquiv.toCommRingCatIso.op).hom) ≫
      Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r))))
have refine_3 : Eq (α := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme) ⟶ Spec (CommRingCat.of (↑R : Type u_1)))
  (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))
  (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: simp only [Arrow.mk_left, Arrow.mk_right, Scheme.isoOfEq_rfl, Iso.refl_trans,
      Iso.trans_hom, Functor.mapIso_hom, Iso.op_hom, Scheme.Spec_map, Quiver.Hom.unop_op,
      Arrow.mk_hom, Category.assoc, ← Spec.map_comp]
-- 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
-- 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
-- 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))))
| 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)
have a : 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]
-- 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)) ≫
      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 ⋯))
have 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 sorry))) :
          (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: 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))))
| 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)
have 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)
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]
-- 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 :
  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)
| 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)
have a₁ : 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]
-- 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 : CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫ e₁.toRingEquiv.toCommRingCatIso.hom
Tactic: enter [2, 2, 1]