awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : LocallyRingedSpace
h :
  ∀ (x : (↑X.toTopCat : Type u)),
    ∃ (R : CommRingCat.{u}) (f : Spec.toLocallyRingedSpace.obj (op R) ⟶ X),
      Membership.mem (γ := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u))
          (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                  TopCat.carrier) f.base) :
              (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
                (↑(↑X.toPresheafedSpace : TopCat) : Type u)))
          x ∧
        IsOpenImmersion f
x : (↑X.toTopCat : Type u)
R : CommRingCat
f : Spec.toLocallyRingedSpace.obj (op R) ⟶ X
h₁ :
  Membership.mem (γ := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u))
    (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            f.base) :
        (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
          (↑(↑X.toPresheafedSpace : TopCat) : Type u)))
    x
h₂ : IsOpenImmersion f
⊢ ∃ (U : OpenNhds x) (R : CommRingCat.{u}), Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))
have refine : X.restrict (U :=
    Functor.obj (C := Opens (↑X.toTopCat : Type u)) (Opens.toTopCat X.toTopCat)
      (↑(Subtype.mk (p := fun (U : Opens (↑X.toTopCat : Type u)) ↦ x ∈ U)
            {
              carrier :=
                Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        TopCat.carrier) (Hom.toShHom f).hom.base) :
                    (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
                      (↑(↑X.toPresheafedSpace : TopCat) : Type u)),
              is_open' := sorry : Opens (↑X.toTopCat : Type u) }
            h₁) :
        Opens (↑X.toTopCat : Type u)))
    sorry ≅
  Spec.toLocallyRingedSpace.obj (op R)
Tactic: refine ⟨⟨⟨_, h₂.base_open.isOpen_range⟩, h₁⟩, R, ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
⊢ f ''ᵁ ⊤ = opensRange f
have h : (↑(f ''ᵁ ⊤) : Set ↥Y) = (↑(opensRange f) : Set ↥Y)
Tactic: apply Opens.ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsIso f
inst_1 : IsOpenImmersion g
⊢ opensRange (f ≫ g) = opensRange g
have rw : g ''ᵁ opensRange f = opensRange g
Tactic: rw [opensRange_comp, opensRange_of_isIso, image_top_eq_opensRange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsIso f
inst_1 : IsOpenImmersion g
rw : g ''ᵁ opensRange f = opensRange g
⊢ opensRange (f ≫ g) = opensRange g
have rw₁ : g ''ᵁ ⊤ = opensRange g
Tactic: rw [opensRange_comp, opensRange_of_isIso, image_top_eq_opensRange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsIso f
inst_1 : IsOpenImmersion g
rw : g ''ᵁ opensRange f = opensRange g
rw₁ : g ''ᵁ ⊤ = opensRange g
⊢ opensRange (f ≫ g) = opensRange g
have rw₂ : opensRange g = opensRange g
Tactic: rw [opensRange_comp, opensRange_of_isIso, image_top_eq_opensRange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ f ⁻¹ᵁ f ''ᵁ U = U
have h : (↑(f ⁻¹ᵁ f ''ᵁ U) : Set ↥X) = (↑U : Set ↥X)
Tactic: apply Opens.ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
U U' : X.Opens
⊢ f ''ᵁ U ≤ f ''ᵁ U' ↔ U ≤ U'
have refine : ∀ (h : f ''ᵁ U ≤ f ''ᵁ U'), U ≤ U'
Tactic: refine ⟨fun h ↦ ?_, f.image_mono⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
U U' : X.Opens
h : f ''ᵁ U ≤ f ''ᵁ U'
⊢ U ≤ U'
have rw : f ⁻¹ᵁ f ''ᵁ U ≤ f ⁻¹ᵁ f ''ᵁ U'
Tactic: rw [← preimage_image_eq f U, ← preimage_image_eq f U']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : Y.Opens
⊢ f ''ᵁ f ⁻¹ᵁ U = opensRange f ⊓ U
have h : (↑(f ''ᵁ f ⁻¹ᵁ U) : Set ↥Y) = (↑(opensRange f ⊓ U) : Set ↥Y)
Tactic: apply Opens.ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
ι : Sort u_1
s : ι → X.Opens
⊢ f ''ᵁ ⨆ (i : ι), s i = ⨆ (i : ι), f ''ᵁ s i
have h : (↑(f ''ᵁ ⨆ (i : ι), s i) : Set ↥Y) = (↑(⨆ (i : ι), f ''ᵁ s i) : Set ↥Y)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
ι : Sort u_1
κ : ι → Sort u_2
s : (i : ι) → κ i → X.Opens
⊢ f ''ᵁ ⨆ (i : ι), ⨆ (j : κ i), s i j = ⨆ (i : ι), ⨆ (j : κ i), f ''ᵁ s i j
have h : (↑(f ''ᵁ ⨆ (i : ι), ⨆ (j : κ i), s i j) : Set ↥Y) = (↑(⨆ (i : ι), ⨆ (j : κ i), f ''ᵁ s i j) : Set ↥Y)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ IsIso (X := Γ(Y, f ''ᵁ U)) (app f (f ''ᵁ U))
have delta : IsIso (X := Γ(Y, (LocallyRingedSpace.IsOpenImmersion.opensFunctor (toLRSHom f)).obj U))
  (app f ((LocallyRingedSpace.IsOpenImmersion.opensFunctor (toLRSHom f)).obj U))
Tactic: delta opensFunctor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
V : Y.Opens
hV : V ≤ opensRange f
⊢ IsIso (app f V)
have rw : IsIso (X := Γ(Y, f ''ᵁ f ⁻¹ᵁ V)) (app f (f ''ᵁ f ⁻¹ᵁ V))
Tactic: rw [show V = f ''ᵁ f ⁻¹ᵁ V from Opens.ext (Set.image_preimage_eq_of_subset hV).symm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ Eq (α :=
    Y.presheaf.obj (op ((PresheafedSpace.IsOpenImmersion.opensFunctor f.toPshHom).obj U)) ⟶ X.presheaf.obj (op U))
    (f.toPshHom.c.app (op ((PresheafedSpace.IsOpenImmersion.opensFunctor f.toPshHom).obj U)) ≫
      X.presheaf.map (eqToHom ⋯))
    (app f (f ''ᵁ U) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
have rw : Eq (α := Y.presheaf.obj (op ((PresheafedSpace.IsOpenImmersion.opensFunctor f.toPshHom).obj U)) ⟶ X.presheaf.obj (op U))
  (f.toPshHom.c.app (op ((PresheafedSpace.IsOpenImmersion.opensFunctor f.toPshHom).obj U)) ≫ X.presheaf.map (eqToHom sorry))
  (app f (f ''ᵁ U) ≫ X.presheaf.map (eqToHom sorry))
Tactic: rw [eqToHom_op]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ Eq (α :=
    X.presheaf.obj (op U) ⟶
      (Functor.obj (TopCat.Presheaf.pushforward CommRingCat (toLRSHom f).base) X.presheaf).obj
        (op ((PresheafedSpace.IsOpenImmersion.opensFunctor (toLRSHom f).toHom).obj U)))
    (X.presheaf.map (eqToHom ⋯)) (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
have rw : Eq (α :=
  X.presheaf.obj (op U) ⟶
    (Functor.obj (TopCat.Presheaf.pushforward CommRingCat (toLRSHom f).base) X.presheaf).obj
      (op ((PresheafedSpace.IsOpenImmersion.opensFunctor (toLRSHom f).toHom).obj U)))
  (X.presheaf.map (eqToHom sorry)) (X.presheaf.map (eqToHom sorry))
Tactic: rw [eqToHom_op]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ Eq (α := Γ(Y, U) ⟶ Γ(Y, f ''ᵁ V)) (appLE f U V e ≫ Iso.inv (appIso f V)) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
have simp : Eq (α := Γ(Y, U) ⟶ Γ(Y, f ''ᵁ V))
  (Y.presheaf.map
      (Quiver.Hom.op (X := Set.image (α := ↥X) (⇑f) (⇑f ⁻¹' (↑U : Set ↥Y))) (Y := (↑U : Set ↥Y))
        (homOfLE (x := Set.image (α := ↥X) (⇑f) (⇑f ⁻¹' (↑U : Set ↥Y))) (y := (↑U : Set ↥Y)) sorry)) ≫
    Y.presheaf.map (Quiver.Hom.op (homOfLE sorry)))
  (Y.presheaf.map (Quiver.Hom.op (homOfLE sorry)))
Tactic: simp only [appLE, Category.assoc, appIso_inv_naturality, Functor.op_obj, Functor.op_map,
    Quiver.Hom.unop_op, opensFunctor_map_homOfLE, app_appIso_inv_assoc, Opens.carrier_eq_coe]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ Eq (α := Γ(Y, U) ⟶ Γ(Y, f ''ᵁ V))
    (Y.presheaf.map
        (Quiver.Hom.op (X := Set.image (α := ↥X) (⇑f) (⇑f ⁻¹' (↑U : Set ↥Y))) (Y := (↑U : Set ↥Y))
          (homOfLE (x := Set.image (α := ↥X) (⇑f) (⇑f ⁻¹' (↑U : Set ↥Y))) (y := (↑U : Set ↥Y)) ⋯)) ≫
      Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
    (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
have rw : Eq (α := Γ(Y, U) ⟶ Γ(Y, f ''ᵁ V))
  (Y.presheaf.map
    (Quiver.Hom.op (X := Set.image (α := ↥X) (⇑f) (⇑f ⁻¹' (↑U : Set ↥Y))) (Y := (↑U : Set ↥Y))
        (homOfLE (x := Set.image (α := ↥X) (⇑f) (⇑f ⁻¹' (↑U : Set ↥Y))) (y := (↑U : Set ↥Y)) sorry) ≫
      Quiver.Hom.op (homOfLE sorry)))
  (Y.presheaf.map (Quiver.Hom.op (homOfLE sorry)))
Tactic: rw [← Functor.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X Y : Scheme
f : X ⟶ Y
inst_1 : IsOpenImmersion f
U V : X.Opens
e : V ≤ f ⁻¹ᵁ f ''ᵁ U
⊢ V ≤ U
have rwa : ∀ (e : V ≤ U), V ≤ U
Tactic: rwa [preimage_image_eq] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
U V : X.Opens
e : V ≤ f ⁻¹ᵁ f ''ᵁ U
⊢ Iso.inv (appIso f U) ≫ appLE f (f ''ᵁ U) V e = X.presheaf.map (homOfLE ⋯).op
have simp : X.presheaf.map (eqToHom sorry) ≫ X.presheaf.map (homOfLE e).op = X.presheaf.map (homOfLE sorry).op
Tactic: simp only [appLE, appIso_inv_app_assoc, eqToHom_op]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
U V : X.Opens
e : V ≤ f ⁻¹ᵁ f ''ᵁ U
⊢ X.presheaf.map (eqToHom ⋯) ≫ X.presheaf.map (homOfLE e).op = X.presheaf.map (homOfLE ⋯).op
have rw : X.presheaf.map (eqToHom sorry ≫ (homOfLE e).op) = X.presheaf.map (homOfLE sorry).op
Tactic: rw [← Functor.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ CategoryStruct.comp (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (appIso f U))
      (app f (f ''ᵁ U) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) =
    𝟙 Γ(X, U)
have rw : X.presheaf.map (CategoryStruct.comp (Y := op (f ⁻¹ᵁ f ''ᵁ U)) (Quiver.Hom.op (eqToHom sorry)) (Quiver.Hom.op (eqToHom sorry))) =
  X.presheaf.map (𝟙 (op U))
Tactic: rw [Scheme.Hom.appIso_inv_app_assoc, ← Functor.map_comp, ← X.presheaf.map_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X : Scheme
U : X.Opens
⊢ appIso (𝟙 X) U = Functor.mapIso X.presheaf (Iso.op (eqToIso ⋯))
have w : ∀ (x : (↑Γ(X, 𝟙 X ''ᵁ U) : Type u)),
  Eq (α := (↑Γ(X, U) : Type u))
    ((CommRingCat.Hom.hom (Iso.hom (appIso (𝟙 X) U)) : (a : (↑Γ(X, 𝟙 X ''ᵁ U) : Type u)) → (↑Γ(X, U) : Type u)) x :
      (↑Γ(X, U) : Type u))
    ((CommRingCat.Hom.hom (Functor.mapIso X.presheaf (Iso.op (eqToIso sorry))).hom :
          (a : (↑Γ(X, 𝟙 X ''ᵁ U) : Type u)) → (↑Γ(X, U) : Type u))
        x :
      (↑Γ(X, U) : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
U : X.Opens
⊢ Eq (α := Γ(Z, (f ≫ g) ''ᵁ U) ≅ Γ(X, U)) (appIso (f ≫ g) U : Γ(Z, (f ≫ g) ''ᵁ U) ≅ Γ(X, U))
    (Iso.trans (Y := Z.presheaf.obj (op (g ''ᵁ f ''ᵁ U))) (Functor.mapIso Z.presheaf (Iso.op (eqToIso ⋯)))
        (appIso g (f ''ᵁ U) ≪≫ appIso f U) :
      Z.presheaf.obj (op ((f ≫ g) ''ᵁ U)) ≅ Γ(X, U))
have w : Eq (α := Γ(Z, (f ≫ g) ''ᵁ U) ⟶ Γ(X, U)) (Iso.hom (appIso (f ≫ g) U) : Γ(Z, (f ≫ g) ''ᵁ U) ⟶ Γ(X, U))
  (Iso.hom
      (Iso.trans (Y := Z.presheaf.obj (op (g ''ᵁ f ''ᵁ U))) (Functor.mapIso Z.presheaf (Iso.op (eqToIso sorry)))
        (appIso g (f ''ᵁ U) ≪≫ appIso f U)) :
    Γ(Z, (f ≫ g) ''ᵁ U) ⟶ Γ(X, U))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R : CommRingCat
f : (↑R : Type u)
⊢ IsOpenImmersion.{u} (X := Spec (CommRingCat.of (Localization.Away f))) (Y := Spec (CommRingCat.of (↑R : Type u)))
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f))))
have apply : IsOpenEmbedding (X := ↥(Spec (CommRingCat.of (Localization.Away f)))) (Y := ↥(Spec (CommRingCat.of (↑R : Type u))))
  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
        (↑(Spec (CommRingCat.of (Localization.Away f))).toPresheafedSpace : TopCat)) (Y :=
        (↑(Spec (CommRingCat.of (↑R : Type u))).toPresheafedSpace : TopCat))
        (PresheafedSpace.Hom.base
          (InducedCategory.Hom.hom
            (LocallyRingedSpace.Hom.toShHom
              (Hom.toLRSHom (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f))))))))) :
    (a : ↥(Spec (CommRingCat.of (Localization.Away f)))) → ↥(Spec (CommRingCat.of (↑R : Type u))))
Tactic: apply SheafedSpace.IsOpenImmersion.of_stalk_iso (H := ?_)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R : CommRingCat
f : (↑R : Type u)
apply :
  IsOpenEmbedding (X := ↥(Spec (CommRingCat.of (Localization.Away f)))) (Y := ↥(Spec (CommRingCat.of (↑R : Type u))))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (X := (↑(Spec (CommRingCat.of (Localization.Away f))).toPresheafedSpace : TopCat)) (Y :=
          (↑(Spec (CommRingCat.of (↑R : Type u))).toPresheafedSpace : TopCat))
          (PresheafedSpace.Hom.base
            (InducedCategory.Hom.hom
              (LocallyRingedSpace.Hom.toShHom
                (Hom.toLRSHom (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f))))))))) :
      (a : ↥(Spec (CommRingCat.of (Localization.Away f)))) → ↥(Spec (CommRingCat.of (↑R : Type u))))
⊢ IsOpenImmersion.{u} (X := Spec (CommRingCat.of (Localization.Away f))) (Y := Spec (CommRingCat.of (↑R : Type u)))
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f))))
have apply₁ : IsOpenEmbedding (X := ↥(Spec (CommRingCat.of (Localization.Away f)))) (Y := ↥(Spec (CommRingCat.of (↑R : Type u))))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (X := (↑(Spec (CommRingCat.of (Localization.Away f))).toPresheafedSpace : TopCat)) (Y :=
          (↑(Spec (CommRingCat.of (↑R : Type u))).toPresheafedSpace : TopCat))
          (PresheafedSpace.Hom.base
            (InducedCategory.Hom.hom
              (LocallyRingedSpace.Hom.toShHom
                (Hom.toLRSHom (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f))))))))) :
      (a : ↥(Spec (CommRingCat.of (Localization.Away f)))) → ↥(Spec (CommRingCat.of (↑R : Type u)))) →
  ∀ (x : ↥(Spec (CommRingCat.of (Localization.Away f)))),
    IsIso (X :=
      (Spec (CommRingCat.of (↑R : Type u))).presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (X := (↑(Spec (CommRingCat.of (Localization.Away f))).toPresheafedSpace : TopCat)) (Y :=
              (↑(Spec (CommRingCat.of (↑R : Type u))).toPresheafedSpace : TopCat))
              (PresheafedSpace.Hom.base
                (InducedCategory.Hom.hom
                  (LocallyRingedSpace.Hom.toShHom
                    (Hom.toLRSHom (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f)))))))) :
            (a : ↥(Spec (CommRingCat.of (Localization.Away f)))) → ↥(Spec (CommRingCat.of (↑R : Type u))))
          x))
      (PresheafedSpace.Hom.stalkMap
        (InducedCategory.Hom.hom
          (LocallyRingedSpace.Hom.toShHom
            (Hom.toLRSHom (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f)))))))
        x)
Tactic: apply SheafedSpace.IsOpenImmersion.of_stalk_iso (H := ?_)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (hypothesis)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R
inst_3 : IsLocalization.Away f S
⊢ IsOpenImmersion (X := Spec (CommRingCat.of S)) (Y := Spec (CommRingCat.of R))
    (Spec.map (CommRingCat.ofHom (algebraMap R S)))
have e : Eq (α := R →+* S)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
    (↑(↑(AlgEquiv.symm (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f))) :
          Localization.Away f →ₐ[R] S) :
      Localization.Away f →+* S)
    (algebraMap R (Localization.Away f)))
  (algebraMap R S)
Tactic: have e := (IsLocalization.algEquiv (.powers f) S
    (Localization.Away f)).symm.toAlgHom.comp_algebraMap
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R
inst_3 : IsLocalization.Away f S
e :
  Eq (α := R →+* S)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(↑(AlgEquiv.symm (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f))) :
            Localization.Away f →ₐ[R] S) :
        Localization.Away f →+* S)
      (algebraMap R (Localization.Away f)))
    (algebraMap R S)
⊢ IsOpenImmersion (X := Spec (CommRingCat.of S)) (Y := Spec (CommRingCat.of R))
    (Spec.map (CommRingCat.ofHom (algebraMap R S)))
have rw : IsOpenImmersion (X := Spec (CommRingCat.of S)) (Y := Spec (CommRingCat.of R))
  (CategoryStruct.comp (Y := Spec (CommRingCat.of (Localization.Away f)))
    (Spec.map
      (CommRingCat.ofHom
        (↑(↑(AlgEquiv.symm (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f))) :
              Localization.Away f →ₐ[R] S) :
          Localization.Away f →+* S)))
    (Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away f)))))
Tactic: rw [← e, CommRingCat.ofHom_comp, Spec.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (hypothesis)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R
inst_3 : IsLocalization.Away f S
e :
  Eq (α := R →+* S)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(↑(AlgEquiv.symm (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f))) :
            Localization.Away f →ₐ[R] S) :
        Localization.Away f →+* S)
      (algebraMap R (Localization.Away f)))
    (algebraMap R S)
⊢ IsOpenImmersion (X := Spec (CommRingCat.of S)) (Y := Spec (CommRingCat.of R))
    (CategoryStruct.comp (Y := Spec (CommRingCat.of (Localization.Away f)))
      (Spec.map
        (CommRingCat.ofHom
          (↑(↑(AlgEquiv.symm (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f))) :
                Localization.Away f →ₐ[R] S) :
            Localization.Away f →+* S)))
      (Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away f)))))
have H : IsIso (X := CommRingCat.of (Localization.Away f)) (Y := CommRingCat.of S)
  (CommRingCat.ofHom
    (AlgHom.toRingHom
      (↑(AlgEquiv.symm (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f))) :
        Localization.Away f →ₐ[R] S)))
Tactic: have H : IsIso (CommRingCat.ofHom (IsLocalization.algEquiv
    (Submonoid.powers f) S (Localization.Away f)).symm.toAlgHom.toRingHom) := by
    exact inferInstanceAs (IsIso <| (IsLocalization.algEquiv
      (Submonoid.powers f) S (Localization.Away f)).toRingEquiv.toCommRingCatIso.inv)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R
inst_3 : IsLocalization.Away f S
e :
  Eq (α := R →+* S)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(↑(AlgEquiv.symm (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f))) :
            Localization.Away f →ₐ[R] S) :
        Localization.Away f →+* S)
      (algebraMap R (Localization.Away f)))
    (algebraMap R S)
H :
  IsIso (X := CommRingCat.of (Localization.Away f)) (Y := CommRingCat.of S)
    (CommRingCat.ofHom
      (AlgHom.toRingHom
        (↑(AlgEquiv.symm (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f))) :
          Localization.Away f →ₐ[R] S)))
⊢ IsOpenImmersion (X := Spec (CommRingCat.of S)) (Y := Spec (CommRingCat.of R))
    (CategoryStruct.comp (Y := Spec (CommRingCat.of (Localization.Away f)))
      (Spec.map
        (CommRingCat.ofHom
          (↑(↑(AlgEquiv.symm (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f))) :
                Localization.Away f →ₐ[R] S) :
            Localization.Away f →+* S)))
      (Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away f)))))
have simp : IsOpenImmersion (X := Spec (CommRingCat.of S)) (Y := Spec (CommRingCat.of R))
  (CategoryStruct.comp (Y := Spec (CommRingCat.of (Localization.Away f)))
    (Spec.map
      (CommRingCat.ofHom
        (↑(AlgEquiv.symm (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f))) :
          Localization.Away f →+* S)))
    (Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away f)))))
Tactic: simp only [AlgHom.toRingHom_eq_coe, AlgEquiv.toAlgHom_toRingHom] at H ⊢
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
⊢ ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X),
    IsOpenImmersion f ∧
      Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec R)) ⇑f) x ∧ Set.range (ι := ↥(Spec R)) ⇑f ⊆ (↑U : Set ↥X)
have obtain : ∀ (V : TopologicalSpace.Opens (↑X.toTopCat : Type u)) (hxV : x ∈ V) (R : CommRingCat.{u})
  (e :
    X.restrict (U :=
        Functor.obj (Opens.toTopCat X.toTopCat)
          (↑(Subtype.mk (p := fun (U : TopologicalSpace.Opens (↑X.toTopCat : Type u)) ↦ x ∈ U) V hxV) :
            TopologicalSpace.Opens (↑X.toTopCat : Type u)))
        sorry ≅
      Spec.toLocallyRingedSpace.obj (op R)),
  ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X),
    IsOpenImmersion f ∧
      Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec R)) ⇑f) x ∧ Set.range (ι := ↥(Spec R)) ⇑f ⊆ (↑U : Set ↥X)
Tactic: obtain ⟨⟨V, hxV⟩, R, ⟨e⟩⟩ := X.2 x