awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Connected (goal)
Goal:
⊢ @GeometricallyConnected = geometrically fun (x : Scheme.{u_1}) ↦ ConnectedSpace.{u_1} ↥x
have h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1),
  GeometricallyConnected x_2 ↔ geometrically (fun (x : Scheme.{u_1}) ↦ ConnectedSpace.{u_1} ↥x) x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Connected (goal)
Goal:
X S : Scheme
f : X ⟶ S
inst : GeometricallyConnected f
x : ↥S
⊢ _root_.IsConnected (α := ↥X) (Set.preimage (β := ↥S) ⇑f {x})
have rw : _root_.IsConnected (α := ↥X) (Set.image (α := ↥(fiber f x)) (⇑(fiberι f x)) Set.univ)
Tactic: rw [← f.range_fiberι, ← Set.image_univ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Connected (goal)
Goal:
X S : Scheme
f : X ⟶ S
inst : GeometricallyConnected f
hf : IsOpenMap (X := ↥X) (Y := ↥S) ⇑f
s : Set ↥S
hs : _root_.IsConnected s
hs' : IsClosed s
⊢ _root_.IsConnected (α := ↥X) (⇑f ⁻¹' s)
have refine : Topology.IsCoinducing (X := ↥X) (Y := ↥S) ⇑f
Tactic: refine Topology.IsCoinducing.isConnected_preimage_of_isClosed f.isConnected_preimage_singleton
    ?_ hs' hs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Connected (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : GeometricallyConnected f
inst_1 : GeometricallyConnected g
inst_2 : UniversallyOpen f
inst_3 : UniversallyOpen g
⊢ GeometricallyConnected (f ≫ g)
have refine : ∀ (K : Type u_1) (x : Field K) (x_1 : Spec (CommRingCat.of K) ⟶ Z), ConnectedSpace.{u_1} ↥(pullback (f ≫ g) x_1)
Tactic: refine ⟨geometrically_iff_of_isClosedUnderIsomorphisms.mpr fun K _ x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Connected (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : GeometricallyConnected f
inst_1 : GeometricallyConnected g
inst_2 : UniversallyOpen f
inst_3 : UniversallyOpen g
K : Type u_1
x_1 : Field K
x : Spec (CommRingCat.of K) ⟶ Z
⊢ ConnectedSpace.{u_1} ↥(pullback (f ≫ g) x)
have rw : ConnectedSpace.{u_1} ↥(pullback (Y := pullback g x) f (pullback.fst g x))
Tactic: rw [← (pullbackRightPullbackFstIso g x f).hom.homeomorph.connectedSpace_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Integral (goal)
Goal:
⊢ @GeometricallyIntegral = geometrically IsIntegral
have h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1), GeometricallyIntegral x_2 ↔ geometrically IsIntegral x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Integral (goal)
Goal:
⊢ @GeometricallyIntegral = @GeometricallyReduced ⊓ @GeometricallyIrreducible
have rw : geometrically IsIntegral = geometrically (IsReduced ⊓ fun (x : Scheme.{u_1}) ↦ IrreducibleSpace.{u_1} ↥x)
Tactic: rw [eq_geometrically, GeometricallyReduced.eq_geometrically,
    GeometricallyIrreducible.eq_geometrically, ← geometrically_inf]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Integral (goal)
Goal:
X S : Scheme
f : X ⟶ S
inst : GeometricallyIntegral f
inst_1 : Flat f
inst_2 : UniversallyOpen f
inst_3 : IsIntegral S
inst_4 : IsLocallyNoetherian S
⊢ IsIntegral X
have rw : IrreducibleSpace.{u_1} ↥X ∧ IsReduced X
Tactic: rw [isIntegral_iff_irreducibleSpace_and_isReduced]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Integral (goal)
Goal:
X S : Scheme
f : X ⟶ S
inst : GeometricallyIntegral f
inst_1 : Subsingleton.{u_1 + 1} ↥S
inst_2 : IsIntegral S
⊢ IsIntegral X
have rw : IrreducibleSpace.{u_1} ↥X ∧ IsReduced X
Tactic: rw [isIntegral_iff_irreducibleSpace_and_isReduced]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Irreducible (goal)
Goal:
⊢ @GeometricallyIrreducible = geometrically fun (x : Scheme.{u_1}) ↦ IrreducibleSpace.{u_1} ↥x
have h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1),
  GeometricallyIrreducible x_2 ↔ geometrically (fun (x : Scheme.{u_1}) ↦ IrreducibleSpace.{u_1} ↥x) x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Irreducible (goal)
Goal:
X S : Scheme
f : X ⟶ S
inst : GeometricallyIrreducible f
hf : IsOpenMap (X := ↥X) (Y := ↥S) ⇑f
s : Set ↥S
hs : IsIrreducible s
⊢ IsIrreducible (X := ↥X) (⇑f ⁻¹' s)
have inr : ∀ (this : ∀ {s : Set ↥S} (hs : IsIrreducible s) (H : ∃ (x : ↥S), s = {x}), IsIrreducible (X := ↥X) (⇑f ⁻¹' s))
  (H : ¬∃ (x : ↥S), s = {x}), IsIrreducible (X := ↥X) (⇑f ⁻¹' s)
Tactic: wlog H : ∃ x, s = {x} generalizing s
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Irreducible (goal)
Goal:
X S : Scheme
f : X ⟶ S
inst : GeometricallyIrreducible f
hf : IsOpenMap (X := ↥X) (Y := ↥S) ⇑f
s : Set ↥S
hs : IsIrreducible s
inr :
  ∀ (this : ∀ {s : Set ↥S} (hs : IsIrreducible s) (H : ∃ (x : ↥S), s = {x}), IsIrreducible (X := ↥X) (⇑f ⁻¹' s))
    (H : ¬∃ (x : ↥S), s = {x}), IsIrreducible (X := ↥X) (⇑f ⁻¹' s)
⊢ IsIrreducible (X := ↥X) (⇑f ⁻¹' s)
have wlog : ∀ {s : Set ↥S} (hs : IsIrreducible s) (H : ∃ (x : ↥S), s = {x}), IsIrreducible (X := ↥X) (⇑f ⁻¹' s)
Tactic: wlog H : ∃ x, s = {x} generalizing s
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Irreducible (goal)
Goal:
X S : Scheme
f : X ⟶ S
inst : GeometricallyIrreducible f
hf : IsOpenMap (X := ↥X) (Y := ↥S) ⇑f
s : Set ↥S
hs : IsIrreducible s
this : ∀ {s : Set ↥S} (hs : IsIrreducible s) (H : ∃ (x : ↥S), s = {x}), IsIrreducible (X := ↥X) (⇑f ⁻¹' s)
H : ¬∃ (x : ↥S), s = {x}
⊢ IsIrreducible (X := ↥X) (⇑f ⁻¹' s)
have inr : (s ∩ Set.range (ι := ↥X) ⇑f).Nonempty
Tactic: refine hs.preimage_of_isPreirreducible_fiber _ hf
      (fun x ↦ (this isIrreducible_singleton ⟨_, rfl⟩).isPreirreducible) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Irreducible (goal)
Goal:
X S : Scheme
f : X ⟶ S
inst : GeometricallyIrreducible f
hf : IsOpenMap (X := ↥X) (Y := ↥S) ⇑f
s : Set ↥S
hs : IsIrreducible s
this : ∀ {s : Set ↥S} (hs : IsIrreducible s) (H : ∃ (x : ↥S), s = {x}), IsIrreducible (X := ↥X) (⇑f ⁻¹' s)
H : ¬∃ (x : ↥S), s = {x}
⊢ (s ∩ Set.range (ι := ↥X) ⇑f).Nonempty
have inr : s.Nonempty
Tactic: rw [Set.range_eq_univ.mpr f.surjective, Set.inter_univ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Irreducible (goal)
Goal:
X S : Scheme
f : X ⟶ S
inst : GeometricallyIrreducible f
hf : IsOpenMap (X := ↥X) (Y := ↥S) ⇑f
s : Set ↥S
hs : IsIrreducible s
H : ∃ (x : ↥S), s = {x}
⊢ IsIrreducible (X := ↥X) (⇑f ⁻¹' s)
have obtain : ∀ (s : ↥S) (hs : IsIrreducible (X := ↥S) {s}), IsIrreducible (X := ↥X) (Set.preimage (β := ↥S) ⇑f {s})
Tactic: obtain ⟨s, rfl⟩ := H
Cleared hypotheses: s, hs, H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Irreducible (goal)
Goal:
X S : Scheme
f : X ⟶ S
inst : GeometricallyIrreducible f
hf : IsOpenMap (X := ↥X) (Y := ↥S) ⇑f
s : ↥S
hs : IsIrreducible (X := ↥S) {s}
⊢ IsIrreducible (X := ↥X) (Set.preimage (β := ↥S) ⇑f {s})
have rw : IsIrreducible (X := ↥X) (Set.image (α := ↥(fiber f s)) (⇑(fiberι f s)) Set.univ)
Tactic: rw [← f.range_fiberι, ← Set.image_univ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Irreducible (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : GeometricallyIrreducible f
inst_1 : GeometricallyIrreducible g
inst_2 : UniversallyOpen f
inst_3 : UniversallyOpen g
⊢ GeometricallyIrreducible (f ≫ g)
have refine : ∀ (K : Type u_1) (x : Field K) (x_1 : Spec (CommRingCat.of K) ⟶ Z), IrreducibleSpace.{u_1} ↥(pullback (f ≫ g) x_1)
Tactic: refine ⟨geometrically_iff_of_isClosedUnderIsomorphisms.mpr fun K _ x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Irreducible (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : GeometricallyIrreducible f
inst_1 : GeometricallyIrreducible g
inst_2 : UniversallyOpen f
inst_3 : UniversallyOpen g
K : Type u_1
x_1 : Field K
x : Spec (CommRingCat.of K) ⟶ Z
⊢ IrreducibleSpace.{u_1} ↥(pullback (f ≫ g) x)
have rw : IrreducibleSpace.{u_1} ↥(pullback (Y := pullback g x) f (pullback.fst g x))
Tactic: rw [← (pullbackRightPullbackFstIso g x f).hom.homeomorph.irreducibleSpace_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Irreducible (goal)
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)
⊢ GeometricallyIrreducible (f ≫ g)
have rw : ∀ (s : ↥S), GeometricallyIrreducible (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s)
Tactic: rw [GeometricallyIrreducible.iff_geometricallyIrreducible_fiber]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Irreducible (goal)
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
⊢ GeometricallyIrreducible (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s)
have refine : ∀ (K : Type u) (x : Field K) (x_1 : Spec (CommRingCat.of K) ⟶ Spec (S.residueField s)),
  IrreducibleSpace.{u} ↥(pullback (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s) x_1)
Tactic: refine ⟨geometrically_iff_of_isClosedUnderIsomorphisms.mpr fun K _ x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Irreducible (goal)
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)
have rw : Set.Nonempty (α := ↥U) (Set.preimage (β := ↥S) ⇑(f ≫ g) {s})
Tactic: rw [((f ≫ g).fiberHomeo s).nonempty_congr, Set.nonempty_coe_sort]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Irreducible (hypothesis)
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))) ⋯ ⋯
⊢ IrreducibleSpace.{u} ↥(pullback (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s) x)
have this : 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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Reduced (goal)
Goal:
⊢ @GeometricallyReduced = geometrically IsReduced
have h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1), GeometricallyReduced x_2 ↔ geometrically IsReduced x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Reduced (goal)
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) (closure {⋯.genericPoint (S := (↑Z : Set ↥Y))})
have rw : Membership.mem (γ := Set (Set ↥Y)) (irreducibleComponents ↥Y) (↑Z : Set ↥Y)
Tactic: rw [Z.property.1.closure_genericPoint (isClosed_of_mem_irreducibleComponents _ Z.property)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Reduced (hypothesis)
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)))
⊢ IsReduced X
have hpt : ∀ (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)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Reduced (hypothesis)
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)))
⊢ IsReduced X
have this₁ : Finite.{u_1 + 1} ↥Z
Tactic: have : Finite Z := (sigmaMk _).finite_iff.mp inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Reduced (hypothesis)
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
⊢ IsReduced X
have this₁ : QuasiCompact g
Tactic: have : QuasiCompact g := ⟨fun _ _ _ ↦ (Set.toFinite _).isCompact⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Reduced (goal)
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
⊢ IsSchemeTheoreticallyDominant g
have rw : ∀ (x : ↥Y), Membership.mem (γ := Set ↥Y) (closure (Set.range (ι := ↥Z) ⇑g)) x
Tactic: rw [isSchemeTheoreticallyDominant_iff_isDominant, isDominant_iff, denseRange_iff_closure_range,
      Set.eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Reduced (goal)
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
have simp : sorry.genericPoint (S := irreducibleComponent y) ⤳ y
Tactic: simp only [g, z, Z, ← Scheme.Hom.comp_apply, Sigma.ι_desc, pt,
        Scheme.fromSpecStalk_closedPoint]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Reduced (hypothesis)
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))
⊢ Membership.mem (γ := Set ↥Y) (closure (Set.range (ι := ↥Z) ⇑g)) y
have hz : 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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Reduced (hypothesis)
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
⊢ IsReduced X
have H : IsSchemeTheoreticallyDominant g
Tactic: have H : IsSchemeTheoreticallyDominant g := by
    rw [isSchemeTheoreticallyDominant_iff_isDominant, isDominant_iff, denseRange_iff_closure_range,
      Set.eq_univ_iff_forall]
    intro y
    let z : Z := Sigma.ι (fun Z ↦ Spec (pt Z)) ⟨_, irreducibleComponent_mem_irreducibleComponents y⟩
      (IsLocalRing.closedPoint _)
    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
    exact hz.mem_closed isClosed_closure (subset_closure ⟨_, rfl⟩)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Reduced (goal)
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
H : IsSchemeTheoreticallyDominant g
⊢ IsReduced X
have suffices : IsReduced.{u_1} (pullback f g)
Tactic: suffices IsReduced (pullback f g) from IsSchemeTheoreticallyDominant.isReduced (pullback.fst f g)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Reduced (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : IsLocallyNoetherian Y
⊢ IsReduced X
have apply : ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀),
  IsReduced.{u_1} ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
Tactic: apply +allowSynthFailures @IsReduced.of_openCover (𝒰 := Y.affineCover.pullback₁ f)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Reduced (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : IsLocallyNoetherian Y
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
⊢ IsReduced.{u_1} ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
have this : IsReduced.{u_1} (Y.affineCover.X i)
Tactic: have : IsReduced (Y.affineCover.X i) := isReduced_of_isOpenImmersion (Y.affineCover.f i)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Reduced (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : GeometricallyReduced f
inst_1 : Flat f
inst_2 : IsReduced Y
inst_3 : IsLocallyNoetherian Y
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
this : IsReduced.{u_1} (Y.affineCover.X i)
⊢ IsReduced.{u_1} ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
have this₁ : Finite.{u_1 + 1} (↑(irreducibleComponents ↥(Y.affineCover.X i)) : Type u_1)
Tactic: have : Finite ↑(irreducibleComponents ↥(Y.affineCover.X i)) := by
    let : IsNoetherian (Y.affineCover.X i) := {}
    exact TopologicalSpace.NoetherianSpace.finite_irreducibleComponents