awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.LocalClosure (goal)
Goal:
W P Q : MorphismProperty Scheme
X Y : Scheme
inst : W.IsStableUnderBaseChange
inst_1 : Scheme.IsJointlySurjectivePreserving W
inst_2 : W.IsStableUnderComposition
inst_3 : P.IsStableUnderBaseChange
inst_4 : P.IsStableUnderComposition
⊢ (sourceLocalClosure W P).IsStableUnderComposition
have refine : ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z),
  sourceLocalClosure W P f →
    sourceLocalClosure W P g →
      ∀ (𝒰 : Scheme.Cover (Scheme.precoverage W) X) (hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f))
        (𝒱 : Scheme.Cover (Scheme.precoverage W) Y) (hg : ∀ (i : 𝒱.I₀), P (𝒱.f i ≫ g)), sourceLocalClosure W P (f ≫ g)
Tactic: refine ⟨fun {X Y Z} f g ⟨𝒰, hf⟩ ⟨𝒱, hg⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.LocalClosure (goal)
Goal:
W P Q : MorphismProperty Scheme
X_1 Y_1 : Scheme
inst : W.IsStableUnderBaseChange
inst_1 : Scheme.IsJointlySurjectivePreserving W
inst_2 : W.IsStableUnderComposition
inst_3 : P.IsStableUnderBaseChange
inst_4 : P.IsStableUnderComposition
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : sourceLocalClosure W P f
h_1 : sourceLocalClosure W P g
𝒰 : Scheme.Cover (Scheme.precoverage W) X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
𝒱 : Scheme.Cover (Scheme.precoverage W) Y
hg : ∀ (i : 𝒱.I₀), P (𝒱.f i ≫ g)
⊢ sourceLocalClosure W P (f ≫ g)
have refine : ∀ (x : (Precoverage.ZeroHypercover.bind 𝒰 fun (i : 𝒰.I₀) ↦ Precoverage.ZeroHypercover.pullback₁ (𝒰.f i ≫ f) 𝒱).I₀)
  (l : 𝒰.I₀)
  (r :
    PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X l)
      ((fun (i : 𝒰.I₀) ↦
          (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage W)
              ((fun (i : 𝒰.I₀) ↦ Precoverage.ZeroHypercover.pullback₁ (𝒰.f i ≫ f) 𝒱) i) :
            PreZeroHypercover (𝒰.X i)))
        l)),
  P (X :=
    (Precoverage.ZeroHypercover.bind 𝒰 fun (i : 𝒰.I₀) ↦ Precoverage.ZeroHypercover.pullback₁ (𝒰.f i ≫ f) 𝒱).X
      (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
        PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
          ((fun (i : 𝒰.I₀) ↦
              (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage W)
                  ((fun (i : 𝒰.I₀) ↦ Precoverage.ZeroHypercover.pullback₁ (𝒰.f i ≫ f) 𝒱) i) :
                PreZeroHypercover (𝒰.X i)))
            i))
        l r))
    ((Precoverage.ZeroHypercover.bind 𝒰 fun (i : 𝒰.I₀) ↦ Precoverage.ZeroHypercover.pullback₁ (𝒰.f i ≫ f) 𝒱).f
        (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
          PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
            ((fun (i : 𝒰.I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage W)
                    ((fun (i : 𝒰.I₀) ↦ Precoverage.ZeroHypercover.pullback₁ (𝒰.f i ≫ f) 𝒱) i) :
                  PreZeroHypercover (𝒰.X i)))
              i))
          l r) ≫
      f ≫ g)
Tactic: refine ⟨𝒰.bind fun i ↦ (𝒱.pullback₁ (𝒰.f i ≫ f)), fun ⟨l, r⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.LocalIso (goal)
Goal:
⊢ @IsLocalIso = sourceLocalClosure IsOpenImmersion IsOpenImmersion
have h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1), IsLocalIso x_2 ↔ sourceLocalClosure IsOpenImmersion IsOpenImmersion x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.LocalIso (goal)
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ IsLocalIso x_2 ↔ sourceLocalClosure IsOpenImmersion IsOpenImmersion x_2
have h : (∀ (x_3 : ↥x), ∃ (U : x.Opens), x_3 ∈ U ∧ IsOpenImmersion (U.ι ≫ x_2)) ↔
  sourceLocalClosure IsOpenImmersion IsOpenImmersion x_2
Tactic: rw [isLocalIso_iff, sourceLocalClosure.iff_forall_exists]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.LocalIso (goal)
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
h :
  (∀ (x_3 : ↥x), ∃ (U : x.Opens), x_3 ∈ U ∧ IsOpenImmersion (U.ι ≫ x_2)) ↔
    sourceLocalClosure IsOpenImmersion IsOpenImmersion x_2
⊢ IsLocalIso x_2 ↔ sourceLocalClosure IsOpenImmersion IsOpenImmersion x_2
have h₁ : (∀ (x_3 : ↥x), ∃ (U : x.Opens), x_3 ∈ U ∧ IsOpenImmersion (U.ι ≫ x_2)) ↔
  ∀ (x_3 : ↥x), ∃ (U : x.Opens), x_3 ∈ U ∧ IsOpenImmersion (U.ι ≫ x_2)
Tactic: rw [isLocalIso_iff, sourceLocalClosure.iff_forall_exists]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.LocalIso (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtSource @IsLocalIso
have rw : IsZariskiLocalAtSource.{u_1} (sourceLocalClosure IsOpenImmersion IsOpenImmersion)
Tactic: rw [eq_sourceLocalClosure_isOpenImmersion]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.LocalIso (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsMultiplicative @IsLocalIso
have rw : (sourceLocalClosure IsOpenImmersion IsOpenImmersion).IsMultiplicative
Tactic: rw [eq_sourceLocalClosure_isOpenImmersion]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.LocalIso (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsStableUnderBaseChange @IsLocalIso
have rw : (sourceLocalClosure IsOpenImmersion IsOpenImmersion).IsStableUnderBaseChange
Tactic: rw [eq_sourceLocalClosure_isOpenImmersion]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.LocalIso (goal)
Goal:
P : MorphismProperty Scheme
inst : P.ContainsIdentities
inst_1 : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
hf : IsLocalIso f
⊢ P f
have obtain : ∀ (𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X) (h : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)), P f
Tactic: obtain ⟨𝒰, h⟩ := eq_sourceLocalClosure_isOpenImmersion ▸ hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.LocalIso (goal)
Goal:
P : MorphismProperty Scheme
inst : P.ContainsIdentities
inst_1 : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
hf : IsLocalIso f
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X
h : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
⊢ P f
have rw : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
Tactic: rw [IsZariskiLocalAtSource.iff_of_openCover 𝒰 (P := P)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.LocalIso (goal)
Goal:
⊢ @IsLocalIso ≤ ⨅ (P : MorphismProperty Scheme), ⨅ (_ : P.ContainsIdentities), ⨅ (_ : IsZariskiLocalAtSource P), P
have refine_1 : ∀ (i : MorphismProperty Scheme) (i_1 : i.ContainsIdentities) (i_2 : IsZariskiLocalAtSource i), @IsLocalIso ≤ i
Tactic: simp only [le_iInf_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.LocalIso (goal)
Goal:
⊢ ⨅ (P : MorphismProperty Scheme), ⨅ (_ : P.ContainsIdentities), ⨅ (_ : IsZariskiLocalAtSource P), P ≤ @IsLocalIso
have refine_2 : IsZariskiLocalAtSource @IsLocalIso
Tactic: refine iInf_le_of_le @IsLocalIso (iInf_le_of_le inferInstance (iInf_le _ ?_))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
hf :
  Function.Surjective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(CommRingCat.Hom.hom f) : (a : (↑R : Type u_1)) → (↑S : Type u_1))
⊢ IsOpenImmersion (Spec.map f) ↔
    ∃ (e : (↑R : Type u_1)),
      IsIdempotentElem e ∧ Eq (α := Ideal (↑R : Type u_1)) (RingHom.ker (CommRingCat.Hom.hom f)) (Ideal.span {e})
have mp : IsOpenImmersion (Spec.map f) →
  ∃ (e : (↑R : Type u_1)),
    IsIdempotentElem e ∧ Eq (α := Ideal (↑R : Type u_1)) (RingHom.ker (CommRingCat.Hom.hom f)) (Ideal.span {e})
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
hf :
  Function.Surjective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(CommRingCat.Hom.hom f) : (a : (↑R : Type u_1)) → (↑S : Type u_1))
mp :
  IsOpenImmersion (Spec.map f) →
    ∃ (e : (↑R : Type u_1)),
      IsIdempotentElem e ∧ Eq (α := Ideal (↑R : Type u_1)) (RingHom.ker (CommRingCat.Hom.hom f)) (Ideal.span {e})
⊢ IsOpenImmersion (Spec.map f) ↔
    ∃ (e : (↑R : Type u_1)),
      IsIdempotentElem e ∧ Eq (α := Ideal (↑R : Type u_1)) (RingHom.ker (CommRingCat.Hom.hom f)) (Ideal.span {e})
have mpr : (∃ (e : (↑R : Type u_1)),
    IsIdempotentElem e ∧ Eq (α := Ideal (↑R : Type u_1)) (RingHom.ker (CommRingCat.Hom.hom f)) (Ideal.span {e})) →
  IsOpenImmersion (Spec.map f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
hf :
  Function.Surjective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(CommRingCat.Hom.hom f) : (a : (↑R : Type u_1)) → (↑S : Type u_1))
H : IsOpenImmersion (Spec.map f)
⊢ ∃ (e : (↑R : Type u_1)),
    IsIdempotentElem e ∧ Eq (α := Ideal (↑R : Type u_1)) (RingHom.ker (CommRingCat.Hom.hom f)) (Ideal.span {e})
have mp : ∀ (e : (↑R : Type u_1)) (he : IsIdempotentElem e)
  (he' : Set.range (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}),
  ∃ (e : (↑R : Type u_1)),
    IsIdempotentElem e ∧ Eq (α := Ideal (↑R : Type u_1)) (RingHom.ker (CommRingCat.Hom.hom f)) (Ideal.span {e})
Tactic: obtain ⟨e, he, he'⟩ := PrimeSpectrum.isClopen_iff_zeroLocus.mp
      ⟨PrimeSpectrum.isClosed_range_comap_of_surjective _ _ hf,
        (Spec.map f).isOpenEmbedding.isOpen_range⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
hf :
  Function.Surjective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(CommRingCat.Hom.hom f) : (a : (↑R : Type u_1)) → (↑S : Type u_1))
H : IsOpenImmersion (Spec.map f)
e : (↑R : Type u_1)
he : IsIdempotentElem e
he' : Set.range (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}
⊢ ∃ (e : (↑R : Type u_1)),
    IsIdempotentElem e ∧ Eq (α := Ideal (↑R : Type u_1)) (RingHom.ker (CommRingCat.Hom.hom f)) (Ideal.span {e})
have mp : Eq (α := Ideal (↑R : Type u_1)) (RingHom.ker (CommRingCat.Hom.hom f)) (Ideal.span {e})
Tactic: refine ⟨e, he, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion (hypothesis)
Goal:
R S : CommRingCat
f : R ⟶ S
hf :
  Function.Surjective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(CommRingCat.Hom.hom f) : (a : (↑R : Type u_1)) → (↑S : Type u_1))
H : IsOpenImmersion (Spec.map f)
e : (↑R : Type u_1)
he : IsIdempotentElem e
he' : Set.range (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}
φ : R ⟶ CommRingCat.of (HasQuotient.Quotient (↑R : Type u_1) (B := Ideal (↑R : Type u_1)) (Ideal.span {e})) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {e}))
⊢ Eq (α := Ideal (↑R : Type u_1)) (RingHom.ker (CommRingCat.Hom.hom f)) (Ideal.span {e})
have this : IsOpenImmersion (Spec.map φ)
Tactic: have : IsOpenImmersion (Spec.map φ) :=
      have : IsLocalization.Away (1 - e) (↑R ⧸ Ideal.span {e}) :=
        IsLocalization.away_of_isIdempotentElem he.one_sub (by simp) Ideal.Quotient.mk_surjective
      IsOpenImmersion.of_isLocalization (1 - e)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion (hypothesis)
Goal:
R S : CommRingCat
f : R ⟶ S
hf :
  Function.Surjective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(CommRingCat.Hom.hom f) : (a : (↑R : Type u_1)) → (↑S : Type u_1))
H : IsOpenImmersion (Spec.map f)
e : (↑R : Type u_1)
he : IsIdempotentElem e
he' : Set.range (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}
φ : R ⟶ CommRingCat.of (HasQuotient.Quotient (↑R : Type u_1) (B := Ideal (↑R : Type u_1)) (Ideal.span {e})) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {e}))
this : IsOpenImmersion (Spec.map φ)
⊢ Eq (α := Ideal (↑R : Type u_1)) (RingHom.ker (CommRingCat.Hom.hom f)) (Ideal.span {e})
have H₁ : Eq (α := Set ↥(Spec R))
  (Set.range (ι :=
    ↥(Spec (CommRingCat.of (HasQuotient.Quotient (↑R : Type u_1) (B := Ideal (↑R : Type u_1)) (Ideal.span {e})))))
    ⇑(Spec.map φ))
  (Set.range (ι := ↥(Spec S)) ⇑(Spec.map f))
Tactic: have H : Set.range (Spec.map φ) = Set.range (Spec.map f) :=
      ((range_comap_of_surjective _ _
        Ideal.Quotient.mk_surjective).trans (by simp)).trans he'.symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion (hypothesis)
Goal:
R S : CommRingCat
f : R ⟶ S
hf :
  Function.Surjective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(CommRingCat.Hom.hom f) : (a : (↑R : Type u_1)) → (↑S : Type u_1))
H_1 : IsOpenImmersion (Spec.map f)
e : (↑R : Type u_1)
he : IsIdempotentElem e
he' : Set.range (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}
φ : R ⟶ CommRingCat.of (HasQuotient.Quotient (↑R : Type u_1) (B := Ideal (↑R : Type u_1)) (Ideal.span {e})) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {e}))
this : IsOpenImmersion (Spec.map φ)
H :
  Eq (α := Set ↥(Spec R))
    (Set.range (ι :=
      ↥(Spec (CommRingCat.of (HasQuotient.Quotient (↑R : Type u_1) (B := Ideal (↑R : Type u_1)) (Ideal.span {e})))))
      ⇑(Spec.map φ))
    (Set.range (ι := ↥(Spec S)) ⇑(Spec.map f))
i : S ≅ CommRingCat.of (HasQuotient.Quotient (↑R : Type u_1) (B := Ideal (↑R : Type u_1)) (Ideal.span {e})) :=
  (Scheme.Spec.preimageIso (IsOpenImmersion.isoOfRangeEq (Spec.map φ) (Spec.map f) H)).unop
⊢ Eq (α := Ideal (↑R : Type u_1)) (RingHom.ker (CommRingCat.Hom.hom f)) (Ideal.span {e})
have hi : Function.Injective (α :=
  (↑(CommRingCat.of (HasQuotient.Quotient (↑R : Type u_1) (B := Ideal (↑R : Type u_1)) (Ideal.span {e}))) : Type u_1))
  (β := (↑S : Type u_1))
  (⇑(CommRingCat.Hom.hom i.inv) :
    (a : (↑(CommRingCat.of ((↑R : Type u_1) ⧸ Ideal.span {e})) : Type u_1)) → (↑S : Type u_1))
Tactic: have hi : Function.Injective i.inv.hom := (ConcreteCategory.bijective_of_isIso i.inv).1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
hf :
  Function.Surjective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(CommRingCat.Hom.hom f) : (a : (↑R : Type u_1)) → (↑S : Type u_1))
H_1 : IsOpenImmersion (Spec.map f)
e : (↑R : Type u_1)
he : IsIdempotentElem e
he' : Set.range (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}
φ : R ⟶ CommRingCat.of (HasQuotient.Quotient (↑R : Type u_1) (B := Ideal (↑R : Type u_1)) (Ideal.span {e})) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {e}))
this : IsOpenImmersion (Spec.map φ)
H :
  Eq (α := Set ↥(Spec R))
    (Set.range (ι :=
      ↥(Spec (CommRingCat.of (HasQuotient.Quotient (↑R : Type u_1) (B := Ideal (↑R : Type u_1)) (Ideal.span {e})))))
      ⇑(Spec.map φ))
    (Set.range (ι := ↥(Spec S)) ⇑(Spec.map f))
i : S ≅ CommRingCat.of (HasQuotient.Quotient (↑R : Type u_1) (B := Ideal (↑R : Type u_1)) (Ideal.span {e})) :=
  (Scheme.Spec.preimageIso (IsOpenImmersion.isoOfRangeEq (Spec.map φ) (Spec.map f) H)).unop
hi :
  Function.Injective (α :=
    (↑(CommRingCat.of (HasQuotient.Quotient (↑R : Type u_1) (B := Ideal (↑R : Type u_1)) (Ideal.span {e}))) : Type u_1))
    (β := (↑S : Type u_1))
    (⇑(CommRingCat.Hom.hom i.inv) :
      (a : (↑(CommRingCat.of ((↑R : Type u_1) ⧸ Ideal.span {e})) : Type u_1)) → (↑S : Type u_1))
⊢ f = φ ≫ i.inv
have a : Spec.map f = Spec.map (φ ≫ i.inv)
Tactic: apply Spec.map_injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion (hypothesis)
Goal:
R S : CommRingCat
f : R ⟶ S
hf :
  Function.Surjective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(CommRingCat.Hom.hom f) : (a : (↑R : Type u_1)) → (↑S : Type u_1))
H_1 : IsOpenImmersion (Spec.map f)
e : (↑R : Type u_1)
he : IsIdempotentElem e
he' : Set.range (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}
φ : R ⟶ CommRingCat.of (HasQuotient.Quotient (↑R : Type u_1) (B := Ideal (↑R : Type u_1)) (Ideal.span {e})) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {e}))
this : IsOpenImmersion (Spec.map φ)
H :
  Eq (α := Set ↥(Spec R))
    (Set.range (ι :=
      ↥(Spec (CommRingCat.of (HasQuotient.Quotient (↑R : Type u_1) (B := Ideal (↑R : Type u_1)) (Ideal.span {e})))))
      ⇑(Spec.map φ))
    (Set.range (ι := ↥(Spec S)) ⇑(Spec.map f))
i : S ≅ CommRingCat.of (HasQuotient.Quotient (↑R : Type u_1) (B := Ideal (↑R : Type u_1)) (Ideal.span {e})) :=
  (Scheme.Spec.preimageIso (IsOpenImmersion.isoOfRangeEq (Spec.map φ) (Spec.map f) H)).unop
hi :
  Function.Injective (α :=
    (↑(CommRingCat.of (HasQuotient.Quotient (↑R : Type u_1) (B := Ideal (↑R : Type u_1)) (Ideal.span {e}))) : Type u_1))
    (β := (↑S : Type u_1))
    (⇑(CommRingCat.Hom.hom i.inv) :
      (a : (↑(CommRingCat.of ((↑R : Type u_1) ⧸ Ideal.span {e})) : Type u_1)) → (↑S : Type u_1))
⊢ Eq (α := Ideal (↑R : Type u_1)) (RingHom.ker (CommRingCat.Hom.hom f)) (Ideal.span {e})
have this₁ : f = φ ≫ i.inv
Tactic: have : f = φ ≫ i.inv := by apply Spec.map_injective; simp [i, ← Scheme.Spec_map]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
hf :
  Function.Surjective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(CommRingCat.Hom.hom f) : (a : (↑R : Type u_1)) → (↑S : Type u_1))
H_1 : IsOpenImmersion (Spec.map f)
e : (↑R : Type u_1)
he : IsIdempotentElem e
he' : Set.range (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}
φ : R ⟶ CommRingCat.of (HasQuotient.Quotient (↑R : Type u_1) (B := Ideal (↑R : Type u_1)) (Ideal.span {e})) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {e}))
this_1 : IsOpenImmersion (Spec.map φ)
H :
  Eq (α := Set ↥(Spec R))
    (Set.range (ι :=
      ↥(Spec (CommRingCat.of (HasQuotient.Quotient (↑R : Type u_1) (B := Ideal (↑R : Type u_1)) (Ideal.span {e})))))
      ⇑(Spec.map φ))
    (Set.range (ι := ↥(Spec S)) ⇑(Spec.map f))
i : S ≅ CommRingCat.of (HasQuotient.Quotient (↑R : Type u_1) (B := Ideal (↑R : Type u_1)) (Ideal.span {e})) :=
  (Scheme.Spec.preimageIso (IsOpenImmersion.isoOfRangeEq (Spec.map φ) (Spec.map f) H)).unop
hi :
  Function.Injective (α :=
    (↑(CommRingCat.of (HasQuotient.Quotient (↑R : Type u_1) (B := Ideal (↑R : Type u_1)) (Ideal.span {e}))) : Type u_1))
    (β := (↑S : Type u_1))
    (⇑(CommRingCat.Hom.hom i.inv) :
      (a : (↑(CommRingCat.of ((↑R : Type u_1) ⧸ Ideal.span {e})) : Type u_1)) → (↑S : Type u_1))
this : f = φ ≫ i.inv
⊢ Eq (α := Ideal (↑R : Type u_1)) (RingHom.ker (CommRingCat.Hom.hom f)) (Ideal.span {e})
have mp : Eq (α := Ideal (↑R : Type u_1)) (RingHom.ker (CommRingCat.Hom.hom φ)) (Ideal.span {e})
Tactic: rw [this, CommRingCat.hom_comp, RingHom.ker_eq_comap_bot, ← Ideal.comap_comap,
      ← RingHom.ker_eq_comap_bot, (RingHom.injective_iff_ker_eq_bot i.inv.hom).mp hi,
      ← RingHom.ker_eq_comap_bot]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion (hypothesis)
Goal:
R S : CommRingCat
f : R ⟶ S
hf :
  Function.Surjective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(CommRingCat.Hom.hom f) : (a : (↑R : Type u_1)) → (↑S : Type u_1))
e : (↑R : Type u_1)
he : IsIdempotentElem e
he' : Eq (α := Ideal (↑R : Type u_1)) (RingHom.ker (CommRingCat.Hom.hom f)) (Ideal.span {e})
this : Algebra (↑R : Type u_1) (↑S : Type u_1) := (CommRingCat.Hom.hom f).toAlgebra
⊢ IsOpenImmersion (Spec.map f)
have this₁ : IsLocalization.Away (1 - e) (↑S : Type u_1)
Tactic: have : IsLocalization.Away (1 - e) S :=
      IsLocalization.away_of_isIdempotentElem he.one_sub (by simpa using he') hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} X
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
⊢ IsOpenImmersion f
have refine_1 : IsOpenMap (X := ↥X) (Y := ↥Y) ⇑f
Tactic: refine IsOpenImmersion.iff_isIso_stalkMap.mpr
    ⟨.of_continuous_injective_isOpenMap f.continuous hf ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} X
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
refine_1 : IsOpenMap (X := ↥X) (Y := ↥Y) ⇑f
⊢ IsOpenImmersion f
have refine_2 : ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)
Tactic: refine IsOpenImmersion.iff_isIso_stalkMap.mpr
    ⟨.of_continuous_injective_isOpenMap f.continuous hf ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} X
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
U : Set ↥X
hU : IsOpen U
⊢ IsOpen (X := ↥Y) (⇑f '' U)
have h : Eq (α := Set ↥Y) (⇑f '' U) (Opens.carrier (⨆ (i : 𝒰.I₀), (𝒰.f i ≫ f) ''ᵁ 𝒰.f i ⁻¹ᵁ { carrier := U, is_open' := hU }))
Tactic: convert! (⨆ i, ((𝒰.f i ≫ f) ''ᵁ (𝒰.f i ⁻¹ᵁ ⟨U, hU⟩))).2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} X
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
U : Set ↥X
hU : IsOpen U
⊢ Eq (α := Set ↥Y) (⇑f '' U) (Opens.carrier (⨆ (i : 𝒰.I₀), (𝒰.f i ≫ f) ''ᵁ 𝒰.f i ⁻¹ᵁ { carrier := U, is_open' := hU }))
have h : ∀ (x : ↥Y),
  Membership.mem (γ := Set ↥Y) (⇑f '' U) x ↔
    Membership.mem (γ := Set ↥Y)
      (Opens.carrier (⨆ (i : 𝒰.I₀), (𝒰.f i ≫ f) ''ᵁ 𝒰.f i ⁻¹ᵁ { carrier := U, is_open' := hU })) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} X
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
U : Set ↥X
hU : IsOpen U
x_1 : ↥Y
h : Membership.mem (γ := Set ↥Y) (⇑f '' U) x_1
x : ↥X
left : x ∈ U
right : f x = x_1
⊢ Membership.mem (γ := Set ↥Y)
    (Opens.carrier (⨆ (i : 𝒰.I₀), (𝒰.f i ≫ f) ''ᵁ 𝒰.f i ⁻¹ᵁ { carrier := U, is_open' := hU })) x_1
have this : ∃ (i : 𝒰.I₀) (y : ↥(𝒰.X i)), (𝒰.f i) y = x
Tactic: have := 𝒰.exists_eq x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} X
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
U : Set ↥X
hU : IsOpen U
x_1 : ↥Y
h : Membership.mem (γ := Set ↥Y) (⇑f '' U) x_1
x : ↥X
left : x ∈ U
right : f x = x_1
this : ∃ (i : 𝒰.I₀) (y : ↥(𝒰.X i)), (𝒰.f i) y = x
⊢ Membership.mem (γ := Set ↥Y)
    (Opens.carrier (⨆ (i : 𝒰.I₀), (𝒰.f i ≫ f) ''ᵁ 𝒰.f i ⁻¹ᵁ { carrier := U, is_open' := hU })) x_1
have simp : ∃ (i : 𝒰.I₀) (x : ↥(𝒰.X i)),
  Membership.mem (α := ↥X) U ((𝒰.f i) x : ↥X) ∧
    (TopCat.Hom.hom f.base : (a : ↥X) → ↥Y) ((TopCat.Hom.hom (𝒰.f i).base : (a : ↥(𝒰.X i)) → ↥X) x : ↥X) = x_1
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} X
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
U : Set ↥X
hU : IsOpen U
x : ↥Y
⊢ Membership.mem (γ := Set ↥Y)
      (Opens.carrier (⨆ (i : 𝒰.I₀), (𝒰.f i ≫ f) ''ᵁ 𝒰.f i ⁻¹ᵁ { carrier := U, is_open' := hU })) x →
    Membership.mem (γ := Set ↥Y) (⇑f '' U) x
have simp : ∀ (x_1 : 𝒰.I₀) (x_2 : ↥(𝒰.X x_1)),
  Membership.mem (α := ↥X) U ((𝒰.f x_1) x_2 : ↥X) →
    (TopCat.Hom.hom f.base : (a : ↥X) → ↥Y) ((TopCat.Hom.hom (𝒰.f x_1).base : (a : ↥(𝒰.X x_1)) → ↥X) x_2 : ↥X) = x →
      ∃ x_3 ∈ U, f x_3 = x
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} X
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
x : ↥X
⊢ IsIso (Scheme.Hom.stalkMap f x)
have refine_2 : ∀ (i : 𝒰.I₀) (x : ↥(𝒰.X i)), IsIso (X := Y.presheaf.stalk (f ((𝒰.f i) x : ↥X))) (Scheme.Hom.stalkMap f ((𝒰.f i) x))
Tactic: obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} X
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
i : 𝒰.I₀
x : ↥(𝒰.X i)
⊢ IsIso (X := Y.presheaf.stalk (f ((𝒰.f i) x : ↥X))) (Scheme.Hom.stalkMap f ((𝒰.f i) x))
have refine_2 : IsIso (Scheme.Hom.stalkMap (𝒰.f i ≫ f) x ≫ inv (Scheme.Hom.stalkMap (𝒰.f i) x))
Tactic: rw [← (IsIso.comp_inv_eq _).mpr (Scheme.Hom.stalkMap_comp (𝒰.f i) f x)]