awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
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)
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})
⊢ ∃ (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⟩

Premises used: AlgebraicGeometry.Spec.map, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Topology.IsOpenEmbedding.isOpen_range, And.intro, Iff.mp, PrimeSpectrum.isClopen_iff_zeroLocus, PrimeSpectrum.isClosed_range_comap_of_surjective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
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})

Tactic:
⟨e, he, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
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}
mp : Eq (α := Ideal (↑R : Type u_1)) (RingHom.ker (CommRingCat.Hom.hom f)) (Ideal.span {e})
⊢ ∃ (e : (↑R : Type u_1)),
    IsIdempotentElem e ∧ Eq (α := Ideal (↑R : Type u_1)) (RingHom.ker (CommRingCat.Hom.hom f)) (Ideal.span {e})

Tactic:
refine ⟨e, he, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
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 (F :=
      (↑R : Type u_1) →+* HasQuotient.Quotient (↑R : Type u_1) (B := Ideal (↑R : Type u_1)) (Ideal.span {e}))
      (algebraMap (↑R : Type u_1) (HasQuotient.Quotient (↑R : Type u_1) (B := Ideal (↑R : Type u_1)) (Ideal.span {e}))))
    (Ideal.span {1 - (1 - e)})

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
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}))
⊢ 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)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
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 (α := Set (PrimeSpectrum (↑R : Type u_1)))
    (PrimeSpectrum.zeroLocus
      (↑(RingHom.ker (F :=
            (↑R : Type u_1) →+* HasQuotient.Quotient (↑R : Type u_1) (B := Ideal (↑R : Type u_1)) (Ideal.span {e}))
            (Ideal.Quotient.mk (Ideal.span {e}))) :
        Set (↑R : Type u_1)))
    (PrimeSpectrum.zeroLocus {e})

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
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 (α := 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
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
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
⊢ 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
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
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))
a : Spec.map f = Spec.map (φ ≫ i.inv)
⊢ f = φ ≫ i.inv

Tactic:
apply Spec.map_injective

Premises used: AlgebraicGeometry.Spec.map_injective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
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))
⊢ Spec.map f = Spec.map (φ ≫ i.inv)

Tactic:
simp [i, ← Scheme.Spec_map]

Premises used: AlgebraicGeometry.Scheme.Spec_map
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
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

Tactic:
have : f = φ ≫ i.inv := by apply Spec.map_injective; simp [i, ← Scheme.Spec_map]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
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
mp : Eq (α := Ideal (↑R : Type u_1)) (RingHom.ker (CommRingCat.Hom.hom φ)) (Ideal.span {e})
⊢ Eq (α := Ideal (↑R : Type u_1)) (RingHom.ker (CommRingCat.Hom.hom f)) (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]

Premises used: CommRingCat.Hom.hom, CommRingCat.hom_comp, RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_comap_bot, Iff.mp, CategoryTheory.Iso.inv, Ideal.comap_comap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
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 φ)) (Ideal.span {e})

Tactic:
simp [φ]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
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
⊢ Eq (α := Ideal (↑R : Type u_1))
    (RingHom.ker (F := (↑R : Type u_1) →+* (↑S : Type u_1)) (algebraMap (↑R : Type u_1) (↑S : Type u_1)))
    (Ideal.span {1 - (1 - e)})

Tactic:
simpa using he'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
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
⊢ 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
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
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_1 : Algebra (↑R : Type u_1) (↑S : Type u_1) := (CommRingCat.Hom.hom f).toAlgebra
this : IsLocalization.Away (1 - e) (↑S : Type u_1)
⊢ IsOpenImmersion (Spec.map f)

Tactic:
IsOpenImmersion.of_isLocalization (1 - e)

Premises used: HSub.hSub, AlgebraicGeometry.IsOpenImmersion.of_isLocalization, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
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_1 : Algebra (↑R : Type u_1) (↑S : Type u_1) := (CommRingCat.Hom.hom f).toAlgebra
this : IsLocalization.Away (1 - e) (↑S : Type u_1)
⊢ IsOpenImmersion (Spec.map f)

Tactic:
exact IsOpenImmersion.of_isLocalization (1 - e)

Premises used: HSub.hSub, AlgebraicGeometry.IsOpenImmersion.of_isLocalization, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
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

Tactic:
IsOpenImmersion.iff_isIso_stalkMap.mpr
    ⟨.of_continuous_injective_isOpenMap f.continuous hf ?_, ?_⟩

Premises used: Iff.mpr, AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap, Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap, And.intro, AlgebraicGeometry.Scheme.Hom.continuous
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
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
refine_2 : ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)
⊢ IsOpenImmersion f

Tactic:
refine IsOpenImmersion.iff_isIso_stalkMap.mpr
    ⟨.of_continuous_injective_isOpenMap f.continuous hf ?_, ?_⟩

Premises used: Iff.mpr, AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap, Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap, And.intro, AlgebraicGeometry.Scheme.Hom.continuous
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
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.{u} (X := ↥Y) (Opens.carrier (⨆ (i : 𝒰.I₀), (𝒰.f i ≫ f) ''ᵁ 𝒰.f i ⁻¹ᵁ { carrier := U, is_open' := hU }))

Tactic:
(⨆ i, ((𝒰.f i ≫ f) ''ᵁ (𝒰.f i ⁻¹ᵁ ⟨U, hU⟩))).2

Premises used: AlgebraicGeometry.Scheme.Hom.opensFunctor, CategoryTheory.PreZeroHypercover.f, iSup, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', TopologicalSpace.Opens.mk, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, TopologicalSpace.Opens.is_open', CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
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
h :
  Eq (α := Set ↥Y) (⇑f '' U) (Opens.carrier (⨆ (i : 𝒰.I₀), (𝒰.f i ≫ f) ''ᵁ 𝒰.f i ⁻¹ᵁ { carrier := U, is_open' := hU }))
⊢ IsOpen (X := ↥Y) (⇑f '' U)

Tactic:
convert! (⨆ i, ((𝒰.f i ≫ f) ''ᵁ (𝒰.f i ⁻¹ᵁ ⟨U, hU⟩))).2

Premises used: AlgebraicGeometry.Scheme.Hom.opensFunctor, CategoryTheory.PreZeroHypercover.f, iSup, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', TopologicalSpace.Opens.mk, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, TopologicalSpace.Opens.is_open', CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
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
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
⊢ Eq (α := Set ↥Y) (⇑f '' U) (Opens.carrier (⨆ (i : 𝒰.I₀), (𝒰.f i ≫ f) ''ᵁ 𝒰.f i ⁻¹ᵁ { carrier := U, is_open' := hU }))

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
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
⊢ ∃ (i : 𝒰.I₀) (y : ↥(𝒰.X i)), (𝒰.f i) y = x

Tactic:
have := 𝒰.exists_eq x
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
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
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
⊢ Membership.mem (γ := Set ↥Y)
    (Opens.carrier (⨆ (i : 𝒰.I₀), (𝒰.f i ≫ f) ''ᵁ 𝒰.f i ⁻¹ᵁ { carrier := U, is_open' := hU })) x_1

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
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
⊢ ∃ (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:
grind
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
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
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
⊢ 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

Tactic:
simp