awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
U : Scheme
f : U ⟶ X
g : X ⟶ S
inst : IsOpenImmersion f
inst_1 : GeometricallyIrreducible g
inst_2 : Surjective (f ≫ g)
s : ↥S
K : Type u
x_1 : Field K
x : Spec (CommRingCat.of K) ⟶ Spec (S.residueField s)
i : pullback (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s) x ⟶ pullback (Scheme.Hom.fiberToSpecResidueField g s) x :=
  pullback.map (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s) x (Scheme.Hom.fiberToSpecResidueField g s) x
    (pullback.map (f ≫ g) (S.fromSpecResidueField s) g (S.fromSpecResidueField s) f (𝟙 (Spec (S.residueField s))) (𝟙 S)
      ⋯ ⋯)
    (𝟙 (Spec (CommRingCat.of K))) (𝟙 (Spec (S.residueField s))) ⋯ ⋯
rw : Set.Nonempty (α := ↥U) (Set.preimage (β := ↥S) ⇑(f ≫ g) {s})
⊢ Nonempty.{u + 1} ↥(Scheme.Hom.fiber (f ≫ g) s)

Tactic:
rw [((f ≫ g).fiberHomeo s).nonempty_congr, Set.nonempty_coe_sort]

Premises used: Homeomorph.toEquiv, Set.nonempty_coe_sort, AlgebraicGeometry.Scheme.Hom.fiberHomeo, CategoryTheory.CategoryStruct.comp, Equiv.nonempty_congr
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
U : Scheme
f : U ⟶ X
g : X ⟶ S
inst : IsOpenImmersion f
inst_1 : GeometricallyIrreducible g
inst_2 : Surjective (f ≫ g)
s : ↥S
K : Type u
x_1 : Field K
x : Spec (CommRingCat.of K) ⟶ Spec (S.residueField s)
i : pullback (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s) x ⟶ pullback (Scheme.Hom.fiberToSpecResidueField g s) x :=
  pullback.map (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s) x (Scheme.Hom.fiberToSpecResidueField g s) x
    (pullback.map (f ≫ g) (S.fromSpecResidueField s) g (S.fromSpecResidueField s) f (𝟙 (Spec (S.residueField s))) (𝟙 S)
      ⋯ ⋯)
    (𝟙 (Spec (CommRingCat.of K))) (𝟙 (Spec (S.residueField s))) ⋯ ⋯
⊢ Set.Nonempty (α := ↥U) (Set.preimage (β := ↥S) ⇑(f ≫ g) {s})

Tactic:
(Set.singleton_nonempty s).preimage (f ≫ g).surjective

Premises used: Set.singleton_nonempty, CategoryTheory.CategoryStruct.comp, Set.Nonempty.preimage, AlgebraicGeometry.Scheme.Hom.surjective
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
U : Scheme
f : U ⟶ X
g : X ⟶ S
inst : IsOpenImmersion f
inst_1 : GeometricallyIrreducible g
inst_2 : Surjective (f ≫ g)
s : ↥S
K : Type u
x_1 : Field K
x : Spec (CommRingCat.of K) ⟶ Spec (S.residueField s)
i : pullback (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s) x ⟶ pullback (Scheme.Hom.fiberToSpecResidueField g s) x :=
  pullback.map (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s) x (Scheme.Hom.fiberToSpecResidueField g s) x
    (pullback.map (f ≫ g) (S.fromSpecResidueField s) g (S.fromSpecResidueField s) f (𝟙 (Spec (S.residueField s))) (𝟙 S)
      ⋯ ⋯)
    (𝟙 (Spec (CommRingCat.of K))) (𝟙 (Spec (S.residueField s))) ⋯ ⋯
⊢ Set.Nonempty (α := ↥U) (Set.preimage (β := ↥S) ⇑(f ≫ g) {s})

Tactic:
exact (Set.singleton_nonempty s).preimage (f ≫ g).surjective

Premises used: Set.singleton_nonempty, CategoryTheory.CategoryStruct.comp, Set.Nonempty.preimage, AlgebraicGeometry.Scheme.Hom.surjective
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
U : Scheme
f : U ⟶ X
g : X ⟶ S
inst : IsOpenImmersion f
inst_1 : GeometricallyIrreducible g
inst_2 : Surjective (f ≫ g)
s : ↥S
K : Type u
x_1 : Field K
x : Spec (CommRingCat.of K) ⟶ Spec (S.residueField s)
i : pullback (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s) x ⟶ pullback (Scheme.Hom.fiberToSpecResidueField g s) x :=
  pullback.map (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s) x (Scheme.Hom.fiberToSpecResidueField g s) x
    (pullback.map (f ≫ g) (S.fromSpecResidueField s) g (S.fromSpecResidueField s) f (𝟙 (Spec (S.residueField s))) (𝟙 S)
      ⋯ ⋯)
    (𝟙 (Spec (CommRingCat.of K))) (𝟙 (Spec (S.residueField s))) ⋯ ⋯
⊢ Nonempty.{u + 1} ↥(Scheme.Hom.fiber (f ≫ g) s)

Tactic:
have : Nonempty ((f ≫ g).fiber s) := by
    rw [((f ≫ g).fiberHomeo s).nonempty_congr, Set.nonempty_coe_sort]
    exact (Set.singleton_nonempty s).preimage (f ≫ g).surjective
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
U : Scheme
f : U ⟶ X
g : X ⟶ S
inst : IsOpenImmersion f
inst_1 : GeometricallyIrreducible g
inst_2 : Surjective (f ≫ g)
s : ↥S
K : Type u
x_1 : Field K
x : Spec (CommRingCat.of K) ⟶ Spec (S.residueField s)
i : pullback (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s) x ⟶ pullback (Scheme.Hom.fiberToSpecResidueField g s) x :=
  pullback.map (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s) x (Scheme.Hom.fiberToSpecResidueField g s) x
    (pullback.map (f ≫ g) (S.fromSpecResidueField s) g (S.fromSpecResidueField s) f (𝟙 (Spec (S.residueField s))) (𝟙 S)
      ⋯ ⋯)
    (𝟙 (Spec (CommRingCat.of K))) (𝟙 (Spec (S.residueField s))) ⋯ ⋯
this : Nonempty.{u + 1} ↥(Scheme.Hom.fiber (f ≫ g) s)
⊢ IrreducibleSpace.{u} ↥(pullback (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s) x)

Tactic:
i.isOpenEmbedding.irreducibleSpace

Premises used: AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Topology.IsOpenEmbedding.irreducibleSpace
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
U : Scheme
f : U ⟶ X
g : X ⟶ S
inst : IsOpenImmersion f
inst_1 : GeometricallyIrreducible g
inst_2 : Surjective (f ≫ g)
s : ↥S
K : Type u
x_1 : Field K
x : Spec (CommRingCat.of K) ⟶ Spec (S.residueField s)
i : pullback (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s) x ⟶ pullback (Scheme.Hom.fiberToSpecResidueField g s) x :=
  pullback.map (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s) x (Scheme.Hom.fiberToSpecResidueField g s) x
    (pullback.map (f ≫ g) (S.fromSpecResidueField s) g (S.fromSpecResidueField s) f (𝟙 (Spec (S.residueField s))) (𝟙 S)
      ⋯ ⋯)
    (𝟙 (Spec (CommRingCat.of K))) (𝟙 (Spec (S.residueField s))) ⋯ ⋯
this : Nonempty.{u + 1} ↥(Scheme.Hom.fiber (f ≫ g) s)
⊢ IrreducibleSpace.{u} ↥(pullback (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s) x)

Tactic:
exact i.isOpenEmbedding.irreducibleSpace

Premises used: AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Topology.IsOpenEmbedding.irreducibleSpace
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1), GeometricallyReduced x_2 ↔ geometrically IsReduced x_2
⊢ @GeometricallyReduced = geometrically IsReduced

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ GeometricallyReduced x_2 ↔ geometrically IsReduced x_2

Tactic:
geometricallyReduced_iff _

Premises used: AlgebraicGeometry.geometricallyReduced_iff
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ GeometricallyReduced x_2 ↔ geometrically IsReduced x_2

Tactic:
exact geometricallyReduced_iff _

Premises used: AlgebraicGeometry.geometricallyReduced_iff
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ IsStableUnderBaseChange @GeometricallyReduced

Tactic:
GeometricallyReduced.eq_geometrically ▸ inferInstance

Premises used: Eq.rec, inferInstance, Eq.symm, AlgebraicGeometry.GeometricallyReduced.eq_geometrically
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : GeometricallyReduced g
⊢ GeometricallyReduced (X := pullback f g) (pullback.fst f g)

Tactic:
MorphismProperty.pullback_fst f g inferInstance

Premises used: inferInstance, CategoryTheory.MorphismProperty.pullback_fst
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : GeometricallyReduced f
⊢ GeometricallyReduced (X := pullback f g) (pullback.snd f g)

Tactic:
MorphismProperty.pullback_snd f g inferInstance

Premises used: inferInstance, CategoryTheory.MorphismProperty.pullback_snd
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
V : S.Opens
inst : GeometricallyReduced f
⊢ GeometricallyReduced (f ∣_ V)

Tactic:
MorphismProperty.of_isPullback (isPullback_morphismRestrict ..).flip ‹_›

Premises used: CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.IsPullback.flip, AlgebraicGeometry.isPullback_morphismRestrict
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
s : ↥S
inst : GeometricallyReduced f
⊢ GeometricallyReduced (Scheme.Hom.fiberToSpecResidueField f s)

Tactic:
MorphismProperty.pullback_snd _ _ inferInstance

Premises used: inferInstance, AlgebraicGeometry.Scheme.Hom.fiber, CategoryTheory.MorphismProperty.pullback_snd, AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
s : ↥S
inst : GeometricallyReduced f
⊢ IsReduced.{u_1} (Scheme.Hom.fiber f s)

Tactic:
GeometricallyReduced.geometrically_isReduced _ _ _ (.of_hasPullback _ _)

Premises used: AlgebraicGeometry.GeometricallyReduced.geometrically_isReduced, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
f : X ⟶ Y
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : Finite.{u_1 + 1} (↑(irreducibleComponents ↥Y) : Type u_1)
pt : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → CommRingCat :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.presheaf.stalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
Z : (↑(irreducibleComponents ↥Y) : Type u_1)
rw : Membership.mem (γ := Set (Set ↥Y)) (irreducibleComponents ↥Y) (↑Z : Set ↥Y)
⊢ Membership.mem (γ := Set (Set ↥Y)) (irreducibleComponents ↥Y) (closure {⋯.genericPoint (S := (↑Z : Set ↥Y))})

Tactic:
rw [Z.property.1.closure_genericPoint (isClosed_of_mem_irreducibleComponents _ Z.property)]

Premises used: isClosed_of_mem_irreducibleComponents, And.left, IsIrreducible.closure_genericPoint, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
f : X ⟶ Y
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : Finite.{u_1 + 1} (↑(irreducibleComponents ↥Y) : Type u_1)
pt : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → CommRingCat :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.presheaf.stalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
Z : (↑(irreducibleComponents ↥Y) : Type u_1)
⊢ Membership.mem (γ := Set (Set ↥Y)) (irreducibleComponents ↥Y) (↑Z : Set ↥Y)

Tactic:
Z.property

Premises used: Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
f : X ⟶ Y
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : Finite.{u_1 + 1} (↑(irreducibleComponents ↥Y) : Type u_1)
pt : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → CommRingCat :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.presheaf.stalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
Z : (↑(irreducibleComponents ↥Y) : Type u_1)
⊢ Membership.mem (γ := Set (Set ↥Y)) (irreducibleComponents ↥Y) (↑Z : Set ↥Y)

Tactic:
exact Z.property

Premises used: Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
f : X ⟶ Y
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : Finite.{u_1 + 1} (↑(irreducibleComponents ↥Y) : Type u_1)
pt : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → CommRingCat :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.presheaf.stalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
⊢ ∀ (Z : (↑(irreducibleComponents ↥Y) : Type u_1)), IsField.{u_1} (↑(pt Z) : Type u_1)

Tactic:
have hpt (Z : _) : IsField (pt Z) :=
    isField_stalk_of_closure_mem_irreducibleComponents _ _ (by
      rw [Z.property.1.closure_genericPoint (isClosed_of_mem_irreducibleComponents _ Z.property)]
      exact Z.property)
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
f : X ⟶ Y
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : Finite.{u_1 + 1} (↑(irreducibleComponents ↥Y) : Type u_1)
pt : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → CommRingCat :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.presheaf.stalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
hpt : ∀ (Z : (↑(irreducibleComponents ↥Y) : Type u_1)), IsField.{u_1} (↑(pt Z) : Type u_1)
this : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → Field (↑(pt Z) : Type u_1) :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ ⋯.toField
Z : Scheme := ∐ fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec (pt Z)
g : Z ⟶ Y :=
  Sigma.desc fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.fromSpecStalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
⊢ Finite.{u_1 + 1} ↥Z

Tactic:
have : Finite Z := (sigmaMk _).finite_iff.mp inferInstance
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
f : X ⟶ Y
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : Finite.{u_1 + 1} (↑(irreducibleComponents ↥Y) : Type u_1)
pt : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → CommRingCat :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.presheaf.stalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
hpt : ∀ (Z : (↑(irreducibleComponents ↥Y) : Type u_1)), IsField.{u_1} (↑(pt Z) : Type u_1)
this_1 : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → Field (↑(pt Z) : Type u_1) :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ ⋯.toField
Z : Scheme := ∐ fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec (pt Z)
g : Z ⟶ Y :=
  Sigma.desc fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.fromSpecStalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
this : Finite.{u_1 + 1} ↥Z
⊢ QuasiCompact g

Tactic:
have : QuasiCompact g := ⟨fun _ _ _ ↦ (Set.toFinite _).isCompact⟩
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
f : X ⟶ Y
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : Finite.{u_1 + 1} (↑(irreducibleComponents ↥Y) : Type u_1)
pt : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → CommRingCat :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.presheaf.stalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
hpt : ∀ (Z : (↑(irreducibleComponents ↥Y) : Type u_1)), IsField.{u_1} (↑(pt Z) : Type u_1)
this_1 : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → Field (↑(pt Z) : Type u_1) :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ ⋯.toField
Z : Scheme := ∐ fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec (pt Z)
g : Z ⟶ Y :=
  Sigma.desc fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.fromSpecStalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
this_2 : Finite.{u_1 + 1} ↥Z
this : QuasiCompact g
rw : ∀ (x : ↥Y), Membership.mem (γ := Set ↥Y) (closure (Set.range (ι := ↥Z) ⇑g)) x
⊢ IsSchemeTheoreticallyDominant g

Tactic:
rw [isSchemeTheoreticallyDominant_iff_isDominant, isDominant_iff, denseRange_iff_closure_range,
      Set.eq_univ_iff_forall]

Premises used: Set.eq_univ_iff_forall, AlgebraicGeometry.isDominant_iff, denseRange_iff_closure_range, AlgebraicGeometry.isSchemeTheoreticallyDominant_iff_isDominant
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
f : X ⟶ Y
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : Finite.{u_1 + 1} (↑(irreducibleComponents ↥Y) : Type u_1)
pt : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → CommRingCat :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.presheaf.stalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
hpt : ∀ (Z : (↑(irreducibleComponents ↥Y) : Type u_1)), IsField.{u_1} (↑(pt Z) : Type u_1)
this_1 : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → Field (↑(pt Z) : Type u_1) :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ ⋯.toField
Z : Scheme := ∐ fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec (pt Z)
g : Z ⟶ Y :=
  Sigma.desc fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.fromSpecStalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
this_2 : Finite.{u_1 + 1} ↥Z
this : QuasiCompact g
y : ↥Y
z : ↥Z :=
  (Sigma.ι (C := Scheme) (fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec (pt Z))
      (Subtype.mk (p := fun (x : Set ↥Y) ↦ Membership.mem (γ := Set (Set ↥Y)) (irreducibleComponents ↥Y) x)
        (irreducibleComponent y) ⋯))
    (IsLocalRing.closedPoint
      (↑(pt
            (Subtype.mk (p := fun (x : Set ↥Y) ↦ Membership.mem (γ := Set (Set ↥Y)) (irreducibleComponents ↥Y) x)
              (irreducibleComponent y) ⋯)) :
        Type u_1))
simp : ⋯.genericPoint (S := irreducibleComponent y) ⤳ y
⊢ g z ⤳ y

Tactic:
simp only [g, z, Z, ← Scheme.Hom.comp_apply, Sigma.ι_desc, pt,
        Scheme.fromSpecStalk_closedPoint]

Premises used: AlgebraicGeometry.Scheme.fromSpecStalk_closedPoint, AlgebraicGeometry.Scheme.Hom.comp_apply, CategoryTheory.Limits.Sigma.ι_desc
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
f : X ⟶ Y
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : Finite.{u_1 + 1} (↑(irreducibleComponents ↥Y) : Type u_1)
pt : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → CommRingCat :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.presheaf.stalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
hpt : ∀ (Z : (↑(irreducibleComponents ↥Y) : Type u_1)), IsField.{u_1} (↑(pt Z) : Type u_1)
this_1 : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → Field (↑(pt Z) : Type u_1) :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ ⋯.toField
Z : Scheme := ∐ fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec (pt Z)
g : Z ⟶ Y :=
  Sigma.desc fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.fromSpecStalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
this_2 : Finite.{u_1 + 1} ↥Z
this : QuasiCompact g
y : ↥Y
z : ↥Z :=
  (Sigma.ι (C := Scheme) (fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec (pt Z))
      (Subtype.mk (p := fun (x : Set ↥Y) ↦ Membership.mem (γ := Set (Set ↥Y)) (irreducibleComponents ↥Y) x)
        (irreducibleComponent y) ⋯))
    (IsLocalRing.closedPoint
      (↑(pt
            (Subtype.mk (p := fun (x : Set ↥Y) ↦ Membership.mem (γ := Set (Set ↥Y)) (irreducibleComponents ↥Y) x)
              (irreducibleComponent y) ⋯)) :
        Type u_1))
⊢ ⋯.genericPoint (S := irreducibleComponent y) ⤳ y

Tactic:
(IsIrreducible.isGenericPoint_genericPoint _
        isClosed_irreducibleComponent).specializes mem_irreducibleComponent

Premises used: IsGenericPoint.specializes, IsIrreducible.isGenericPoint_genericPoint, mem_irreducibleComponent, isClosed_irreducibleComponent
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
f : X ⟶ Y
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : Finite.{u_1 + 1} (↑(irreducibleComponents ↥Y) : Type u_1)
pt : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → CommRingCat :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.presheaf.stalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
hpt : ∀ (Z : (↑(irreducibleComponents ↥Y) : Type u_1)), IsField.{u_1} (↑(pt Z) : Type u_1)
this_1 : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → Field (↑(pt Z) : Type u_1) :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ ⋯.toField
Z : Scheme := ∐ fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec (pt Z)
g : Z ⟶ Y :=
  Sigma.desc fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.fromSpecStalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
this_2 : Finite.{u_1 + 1} ↥Z
this : QuasiCompact g
y : ↥Y
z : ↥Z :=
  (Sigma.ι (C := Scheme) (fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec (pt Z))
      (Subtype.mk (p := fun (x : Set ↥Y) ↦ Membership.mem (γ := Set (Set ↥Y)) (irreducibleComponents ↥Y) x)
        (irreducibleComponent y) ⋯))
    (IsLocalRing.closedPoint
      (↑(pt
            (Subtype.mk (p := fun (x : Set ↥Y) ↦ Membership.mem (γ := Set (Set ↥Y)) (irreducibleComponents ↥Y) x)
              (irreducibleComponent y) ⋯)) :
        Type u_1))
⊢ ⋯.genericPoint (S := irreducibleComponent y) ⤳ y

Tactic:
exact (IsIrreducible.isGenericPoint_genericPoint _
        isClosed_irreducibleComponent).specializes mem_irreducibleComponent

Premises used: IsGenericPoint.specializes, IsIrreducible.isGenericPoint_genericPoint, mem_irreducibleComponent, isClosed_irreducibleComponent
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
f : X ⟶ Y
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : Finite.{u_1 + 1} (↑(irreducibleComponents ↥Y) : Type u_1)
pt : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → CommRingCat :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.presheaf.stalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
hpt : ∀ (Z : (↑(irreducibleComponents ↥Y) : Type u_1)), IsField.{u_1} (↑(pt Z) : Type u_1)
this_1 : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → Field (↑(pt Z) : Type u_1) :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ ⋯.toField
Z : Scheme := ∐ fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec (pt Z)
g : Z ⟶ Y :=
  Sigma.desc fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.fromSpecStalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
this_2 : Finite.{u_1 + 1} ↥Z
this : QuasiCompact g
y : ↥Y
z : ↥Z :=
  (Sigma.ι (C := Scheme) (fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec (pt Z))
      (Subtype.mk (p := fun (x : Set ↥Y) ↦ Membership.mem (γ := Set (Set ↥Y)) (irreducibleComponents ↥Y) x)
        (irreducibleComponent y) ⋯))
    (IsLocalRing.closedPoint
      (↑(pt
            (Subtype.mk (p := fun (x : Set ↥Y) ↦ Membership.mem (γ := Set (Set ↥Y)) (irreducibleComponents ↥Y) x)
              (irreducibleComponent y) ⋯)) :
        Type u_1))
⊢ g z ⤳ y

Tactic:
have hz : g z ⤳ y := by
      simp only [g, z, Z, ← Scheme.Hom.comp_apply, Sigma.ι_desc, pt,
        Scheme.fromSpecStalk_closedPoint]
      exact (IsIrreducible.isGenericPoint_genericPoint _
        isClosed_irreducibleComponent).specializes mem_irreducibleComponent
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced
Goal:
X Y : Scheme
f : X ⟶ Y
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : Finite.{u_1 + 1} (↑(irreducibleComponents ↥Y) : Type u_1)
pt : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → CommRingCat :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.presheaf.stalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
hpt : ∀ (Z : (↑(irreducibleComponents ↥Y) : Type u_1)), IsField.{u_1} (↑(pt Z) : Type u_1)
this_1 : (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) → Field (↑(pt Z) : Type u_1) :=
  fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ ⋯.toField
Z : Scheme := ∐ fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec (pt Z)
g : Z ⟶ Y :=
  Sigma.desc fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Y.fromSpecStalk (⋯.genericPoint (S := (↑Z : Set ↥Y)))
this_2 : Finite.{u_1 + 1} ↥Z
this : QuasiCompact g
y : ↥Y
z : ↥Z :=
  (Sigma.ι (C := Scheme) (fun (Z : (↑(irreducibleComponents ↥Y) : Type u_1)) ↦ Spec (pt Z))
      (Subtype.mk (p := fun (x : Set ↥Y) ↦ Membership.mem (γ := Set (Set ↥Y)) (irreducibleComponents ↥Y) x)
        (irreducibleComponent y) ⋯))
    (IsLocalRing.closedPoint
      (↑(pt
            (Subtype.mk (p := fun (x : Set ↥Y) ↦ Membership.mem (γ := Set (Set ↥Y)) (irreducibleComponents ↥Y) x)
              (irreducibleComponent y) ⋯)) :
        Type u_1))
hz : g z ⤳ y
⊢ Membership.mem (γ := Set ↥Y) (closure (Set.range (ι := ↥Z) ⇑g)) y

Tactic:
hz.mem_closed isClosed_closure (subset_closure ⟨_, rfl⟩)

Premises used: subset_closure, Exists.intro, isClosed_closure, rfl, Specializes.mem_closed