awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
H : ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)
K : Type u
inst : Field K
Z : Scheme
fst : Z ⟶ X
snd : Z ⟶ Spec (of K)
y : ↥Y
φ : Y.residueField y ⟶ of K
h : IsPullback fst snd f (Spec.map φ ≫ Y.fromSpecResidueField y)
p : Z ⟶ Scheme.Hom.fiber f y := pullback.lift fst (snd ≫ Spec.map φ) ⋯
h₁ : p ≫ pullback.fst f (Y.fromSpecResidueField y) = fst
⊢ IsPullback (p ≫ pullback.fst f (Y.fromSpecResidueField y)) snd f (Spec.map φ ≫ Y.fromSpecResidueField y)

Tactic:
convert! h
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
H : ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)
K : Type u
inst : Field K
Z : Scheme
fst : Z ⟶ X
snd : Z ⟶ Spec (of K)
y : ↥Y
φ : Y.residueField y ⟶ of K
h : IsPullback fst snd f (Spec.map φ ≫ Y.fromSpecResidueField y)
p : Z ⟶ Scheme.Hom.fiber f y := pullback.lift fst (snd ≫ Spec.map φ) ⋯
⊢ p ≫ pullback.fst f (Y.fromSpecResidueField y) = fst

Tactic:
simp [p]
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
H : ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)
K : Type u
inst : Field K
Z : Scheme
fst : Z ⟶ X
snd : Z ⟶ Spec (of K)
y : ↥Y
φ : Y.residueField y ⟶ of K
h : IsPullback fst snd f (Spec.map φ ≫ Y.fromSpecResidueField y)
p : Z ⟶ Scheme.Hom.fiber f y := pullback.lift fst (snd ≫ Spec.map φ) ⋯
⊢ snd ≫ Spec.map φ = p ≫ Scheme.Hom.fiberToSpecResidueField f y

Tactic:
simp [p, Scheme.Hom.fiberToSpecResidueField]

Premises used: AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
inst : IsIntegral Y
inst_1 : Subsingleton.{u + 1} ↥Y
hf : geometrically P f
⊢ MorphismProperty.universally (fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦ IsIntegral Y → Subsingleton.{u + 1} ↥Y → P X) f

Tactic:
rw [geometrically_eq_universally] at hf

Premises used: AlgebraicGeometry.geometrically_eq_universally
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
inst : IsIntegral Y
inst_1 : Subsingleton.{u + 1} ↥Y
hf : MorphismProperty.universally (fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦ IsIntegral Y → Subsingleton.{u + 1} ↥Y → P X) f
⊢ P X

Tactic:
MorphismProperty.universally_le _ _ hf ‹_› ‹_›

Premises used: CategoryTheory.MorphismProperty.universally_le
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
inst : IsIntegral Y
inst_1 : Subsingleton.{u + 1} ↥Y
hf : MorphismProperty.universally (fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦ IsIntegral Y → Subsingleton.{u + 1} ↥Y → P X) f
⊢ P X

Tactic:
exact MorphismProperty.universally_le _ _ hf ‹_› ‹_›

Premises used: CategoryTheory.MorphismProperty.universally_le
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
X : Scheme
P : ObjectProperty Scheme
R : Type u
inst : CommRing R
f : X ⟶ Spec (of R)
⊢ geometrically P f ↔
    ∀ ⦃K : Type u⦄ [inst_1 : Field K] [inst_2 : Algebra R K] ⦃Y : Scheme.{u}⦄ (fst : Y ⟶ X) (snd : Y ⟶ Spec (of K)),
      IsPullback fst snd f (Spec.map (ofHom (algebraMap R K))) → P Y

Tactic:
⟨fun hs K _ _ Z fst snd h ↦ hs _ _ _ h, fun H K _ y Z fst snd h ↦ ?_⟩

Premises used: Algebra.algebraMap, CommRingCat.ofHom, AlgebraicGeometry.Spec.map, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
X : Scheme
P : ObjectProperty Scheme
R : Type u
inst : CommRing R
f : X ⟶ Spec (of R)
refine :
  ∀
    (H :
      ∀ ⦃K : Type u⦄ [inst_1 : Field K] [inst_2 : Algebra R K] ⦃Y : Scheme.{u}⦄ (fst : Y ⟶ X) (snd : Y ⟶ Spec (of K)),
        IsPullback fst snd f (Spec.map (ofHom (algebraMap R K))) → P Y)
    (K : Type u) (x : Field K) (y : Spec (of K) ⟶ Spec (of R)) (Z : Scheme.{u}) (fst : Z ⟶ X) (snd : Z ⟶ Spec (of K))
    (h : IsPullback fst snd f y), P Z
⊢ geometrically P f ↔
    ∀ ⦃K : Type u⦄ [inst_1 : Field K] [inst_2 : Algebra R K] ⦃Y : Scheme.{u}⦄ (fst : Y ⟶ X) (snd : Y ⟶ Spec (of K)),
      IsPullback fst snd f (Spec.map (ofHom (algebraMap R K))) → P Y

Tactic:
refine ⟨fun hs K _ _ Z fst snd h ↦ hs _ _ _ h, fun H K _ y Z fst snd h ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
X : Scheme
P : ObjectProperty Scheme
R : Type u
inst : CommRing R
f : X ⟶ Spec (of R)
H :
  ∀ ⦃K : Type u⦄ [inst_1 : Field K] [inst_2 : Algebra R K] ⦃Y : Scheme.{u}⦄ (fst : Y ⟶ X) (snd : Y ⟶ Spec (of K)),
    IsPullback fst snd f (Spec.map (ofHom (algebraMap R K))) → P Y
K : Type u
x : Field K
y : Spec (of K) ⟶ Spec (of R)
Z : Scheme
fst : Z ⟶ X
snd : Z ⟶ Spec (of K)
h : IsPullback fst snd f y
obtain : ∀ (φ : of R ⟶ of K) (h : IsPullback fst snd f (Spec.map φ)), P Z
⊢ P Z

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective y

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
X : Scheme
P : ObjectProperty Scheme
R : Type u
inst : CommRing R
f : X ⟶ Spec (of R)
H :
  ∀ ⦃K : Type u⦄ [inst_1 : Field K] [inst_2 : Algebra R K] ⦃Y : Scheme.{u}⦄ (fst : Y ⟶ X) (snd : Y ⟶ Spec (of K)),
    IsPullback fst snd f (Spec.map (ofHom (algebraMap R K))) → P Y
K : Type u
x : Field K
Z : Scheme
fst : Z ⟶ X
snd : Z ⟶ Spec (of K)
φ : of R ⟶ of K
h : IsPullback fst snd f (Spec.map φ)
algInst : Algebra (↑(of R) : Type u) (↑(of K) : Type u) := (Hom.hom φ).toAlgebra
⊢ P Z

Tactic:
exact H fst snd h
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
X : Scheme
P : ObjectProperty Scheme
R : Type u
inst : CommRing R
f : X ⟶ Spec (of R)
inst_1 : P.IsClosedUnderIsomorphisms
⊢ geometrically P f ↔
    ∀ (K : Type u) [inst_2 : Field K] [inst_3 : Algebra R K], P (pullback f (Spec.map (ofHom (algebraMap R K))))

Tactic:
⟨fun hf K _ _ ↦ pullback_of_geometrically hf _ _, fun H ↦ ?_⟩

Premises used: Algebra.algebraMap, CommRingCat.ofHom, AlgebraicGeometry.Spec.map, Iff.intro, AlgebraicGeometry.pullback_of_geometrically
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
X : Scheme
P : ObjectProperty Scheme
R : Type u
inst : CommRing R
f : X ⟶ Spec (of R)
inst_1 : P.IsClosedUnderIsomorphisms
refine :
  ∀ (H : ∀ (K : Type u) [inst_2 : Field K] [inst_3 : Algebra R K], P (pullback f (Spec.map (ofHom (algebraMap R K))))),
    geometrically P f
⊢ geometrically P f ↔
    ∀ (K : Type u) [inst_2 : Field K] [inst_3 : Algebra R K], P (pullback f (Spec.map (ofHom (algebraMap R K))))

Tactic:
refine ⟨fun hf K _ _ ↦ pullback_of_geometrically hf _ _, fun H ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
X : Scheme
P : ObjectProperty Scheme
R : Type u
inst : CommRing R
f : X ⟶ Spec (of R)
inst_1 : P.IsClosedUnderIsomorphisms
H : ∀ (K : Type u) [inst_2 : Field K] [inst_3 : Algebra R K], P (pullback f (Spec.map (ofHom (algebraMap R K))))
rw : ∀ (K : Type u) [inst_2 : Field K] (y : Spec (of K) ⟶ Spec (of R)), P (pullback f y)
⊢ geometrically P f

Tactic:
rw [geometrically_iff_of_isClosedUnderIsomorphisms]

Premises used: AlgebraicGeometry.geometrically_iff_of_isClosedUnderIsomorphisms
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
X : Scheme
P : ObjectProperty Scheme
R : Type u
inst : CommRing R
f : X ⟶ Spec (of R)
inst_1 : P.IsClosedUnderIsomorphisms
H : ∀ (K : Type u) [inst_2 : Field K] [inst_3 : Algebra R K], P (pullback f (Spec.map (ofHom (algebraMap R K))))
K : Type u
_ : ∀ [inst_2 : Field K] (y : Spec (of K) ⟶ Spec (of R)), P (pullback f y)
⊢ ∀ [inst_2 : Field K] (y : Spec (of K) ⟶ Spec (of R)), P (pullback f y)

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
X : Scheme
P : ObjectProperty Scheme
R : Type u
inst : CommRing R
f : X ⟶ Spec (of R)
inst_1 : P.IsClosedUnderIsomorphisms
H : ∀ (K : Type u) [inst_3 : Field K] [inst_4 : Algebra R K], P (pullback f (Spec.map (ofHom (algebraMap R K))))
K : Type u
inst_2 : Field K
y : Spec (of K) ⟶ Spec (of R)
obtain : ∀ (φ : of R ⟶ of K), P (pullback f (Spec.map φ))
⊢ P (pullback f y)

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective y

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
X : Scheme
P : ObjectProperty Scheme
R : Type u
inst : CommRing R
f : X ⟶ Spec (of R)
inst_1 : P.IsClosedUnderIsomorphisms
H : ∀ (K : Type u) [inst_3 : Field K] [inst_4 : Algebra R K], P (pullback f (Spec.map (ofHom (algebraMap R K))))
K : Type u
inst_2 : Field K
φ : of R ⟶ of K
algInst : Algebra (↑(of R) : Type u) (↑(of K) : Type u) := (Hom.hom φ).toAlgebra
⊢ P (pullback f (Spec.map φ))

Tactic:
H K
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
X : Scheme
P : ObjectProperty Scheme
R : Type u
inst : CommRing R
f : X ⟶ Spec (of R)
inst_1 : P.IsClosedUnderIsomorphisms
H : ∀ (K : Type u) [inst_3 : Field K] [inst_4 : Algebra R K], P (pullback f (Spec.map (ofHom (algebraMap R K))))
K : Type u
inst_2 : Field K
φ : of R ⟶ of K
algInst : Algebra (↑(of R) : Type u) (↑(of K) : Type u) := (Hom.hom φ).toAlgebra
⊢ P (pullback f (Spec.map φ))

Tactic:
exact H K
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Connected
Goal:
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
⊢ @GeometricallyConnected = geometrically fun (x : Scheme.{u_1}) ↦ ConnectedSpace.{u_1} ↥x

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Connected
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ GeometricallyConnected x_2 ↔ geometrically (fun (x : Scheme.{u_1}) ↦ ConnectedSpace.{u_1} ↥x) x_2

Tactic:
geometricallyConnected_iff _

Premises used: AlgebraicGeometry.geometricallyConnected_iff
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Connected
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ GeometricallyConnected x_2 ↔ geometrically (fun (x : Scheme.{u_1}) ↦ ConnectedSpace.{u_1} ↥x) x_2

Tactic:
exact geometricallyConnected_iff _

Premises used: AlgebraicGeometry.geometricallyConnected_iff
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Connected
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ IsStableUnderBaseChange @GeometricallyConnected

Tactic:
GeometricallyConnected.eq_geometrically ▸ inferInstance

Premises used: Eq.rec, inferInstance, Eq.symm, AlgebraicGeometry.GeometricallyConnected.eq_geometrically
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Connected
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : GeometricallyConnected g
⊢ GeometricallyConnected (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.Connected
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : GeometricallyConnected f
⊢ GeometricallyConnected (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.Connected
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
V : S.Opens
inst : GeometricallyConnected f
⊢ GeometricallyConnected (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.Connected
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
s : ↥S
inst : GeometricallyConnected f
⊢ GeometricallyConnected (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.Connected
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
s : ↥S
inst : GeometricallyConnected f
⊢ ConnectedSpace.{u_1} ↥(Scheme.Hom.fiber f s)

Tactic:
GeometricallyConnected.geometrically_connectedSpace _ _ _ (.of_hasPullback _ _)

Premises used: AlgebraicGeometry.GeometricallyConnected.geometrically_connectedSpace, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Connected
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : GeometricallyConnected f
⊢ Surjective f

Tactic:
⟨fun x ↦ ⟨_, (f.range_fiberι x).le ⟨Nonempty.some inferInstance, rfl⟩⟩⟩

Premises used: AlgebraicGeometry.Scheme.Hom.range_fiberι, CategoryTheory.ConcreteCategory.hom, inferInstance, Nonempty.some, Eq.le, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.Hom.fiberι, AlgebraicGeometry.Surjective.mk, Exists.intro, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe, rfl
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Connected
Goal:
X S : Scheme
f : X ⟶ S
inst : GeometricallyConnected f
x : ↥S
rw : _root_.IsConnected (α := ↥X) (Set.image (α := ↥(fiber f x)) (⇑(fiberι f x)) Set.univ)
⊢ _root_.IsConnected (α := ↥X) (Set.preimage (β := ↥S) ⇑f {x})

Tactic:
rw [← f.range_fiberι, ← Set.image_univ]

Premises used: Set.image_univ, AlgebraicGeometry.Scheme.Hom.range_fiberι
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Connected
Goal:
X S : Scheme
f : X ⟶ S
inst : GeometricallyConnected f
x : ↥S
⊢ _root_.IsConnected (α := ↥X) (Set.image (α := ↥(fiber f x)) (⇑(fiberι f x)) Set.univ)

Tactic:
isConnected_univ.image _ (f.fiberι _).continuous.continuousOn

Premises used: Continuous.continuousOn, IsConnected.image, isConnected_univ, AlgebraicGeometry.Scheme.Hom.fiberι, AlgebraicGeometry.Scheme.Hom.continuous
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Connected
Goal:
X S : Scheme
f : X ⟶ S
inst : GeometricallyConnected f
x : ↥S
⊢ _root_.IsConnected (α := ↥X) (Set.image (α := ↥(fiber f x)) (⇑(fiberι f x)) Set.univ)

Tactic:
exact isConnected_univ.image _ (f.fiberι _).continuous.continuousOn

Premises used: Continuous.continuousOn, IsConnected.image, isConnected_univ, AlgebraicGeometry.Scheme.Hom.fiberι, AlgebraicGeometry.Scheme.Hom.continuous
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Connected
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)

Tactic:
Topology.IsCoinducing.isConnected_preimage_of_isClosed f.isConnected_preimage_singleton
    ?_ hs' hs

Premises used: Topology.IsCoinducing.isConnected_preimage_of_isClosed, AlgebraicGeometry.Scheme.Hom.isConnected_preimage_singleton
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Connected
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
refine : Topology.IsCoinducing (X := ↥X) (Y := ↥S) ⇑f
⊢ _root_.IsConnected (α := ↥X) (⇑f ⁻¹' s)

Tactic:
refine Topology.IsCoinducing.isConnected_preimage_of_isClosed f.isConnected_preimage_singleton
    ?_ hs' hs

Premises used: Topology.IsCoinducing.isConnected_preimage_of_isClosed, AlgebraicGeometry.Scheme.Hom.isConnected_preimage_singleton
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Connected
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
⊢ Topology.IsCoinducing (X := ↥X) (Y := ↥S) ⇑f

Tactic:
(hf.isQuotientMap f.continuous f.surjective).isCoinducing

Premises used: IsOpenMap.isQuotientMap, Topology.IsQuotientMap.isCoinducing, AlgebraicGeometry.Scheme.Hom.continuous, AlgebraicGeometry.Scheme.Hom.surjective
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Connected
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
⊢ Topology.IsCoinducing (X := ↥X) (Y := ↥S) ⇑f

Tactic:
exact (hf.isQuotientMap f.continuous f.surjective).isCoinducing

Premises used: IsOpenMap.isQuotientMap, Topology.IsQuotientMap.isCoinducing, AlgebraicGeometry.Scheme.Hom.continuous, AlgebraicGeometry.Scheme.Hom.surjective
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Connected
Goal:
X S : Scheme
f : X ⟶ S
inst : GeometricallyConnected f
inst_1 : ConnectedSpace.{u_1} ↥S
hf : IsOpenMap (X := ↥X) (Y := ↥S) ⇑f
⊢ ConnectedSpace.{u_1} ↥X

Tactic:
simpa [connectedSpace_iff_univ] using f.isConnected_preimage hf isConnected_univ

Premises used: isConnected_univ, AlgebraicGeometry.Scheme.Hom.isConnected_preimage, connectedSpace_iff_univ
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Connected
Goal:
X S : Scheme
f : X ⟶ S
inst : GeometricallyConnected f
inst_1 : Subsingleton.{u_1 + 1} ↥S
inst_2 : Nonempty.{u_1 + 1} ↥S
⊢ ConnectedSpace.{u_1} ↥X

Tactic:
have : ConnectedSpace S := ⟨‹_›⟩
  GeometricallyConnected.connectedSpace (f := f) fun _ _ ↦ isOpen_discrete _

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.GeometricallyConnected.connectedSpace, ConnectedSpace.mk, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', isOpen_discrete, AlgebraicGeometry.PresheafedSpace.Hom.base, Set.image, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Connected
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : GeometricallyConnected f
inst_1 : UniversallyOpen f
inst_2 : ConnectedSpace.{u_1} ↥Y
⊢ ConnectedSpace.{u_1} ↥(pullback f g)

Tactic:
GeometricallyConnected.connectedSpace (pullback.snd _ _) (pullback.snd f g).isOpenMap

Premises used: CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.GeometricallyConnected.connectedSpace, AlgebraicGeometry.Scheme.Hom.isOpenMap
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Connected
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : GeometricallyConnected g
inst_1 : UniversallyOpen g
inst_2 : ConnectedSpace.{u_1} ↥X
⊢ ConnectedSpace.{u_1} ↥(pullback f g)

Tactic:
GeometricallyConnected.connectedSpace (pullback.fst _ _) (pullback.fst f g).isOpenMap

Premises used: AlgebraicGeometry.GeometricallyConnected.connectedSpace, AlgebraicGeometry.Scheme.Hom.isOpenMap, CategoryTheory.Limits.pullback.fst
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Connected
Goal:
X S : Scheme
f : X ⟶ S
⊢ GeometricallyConnected f ↔ ∀ (s : ↥S), GeometricallyConnected (Scheme.Hom.fiberToSpecResidueField f s)

Tactic:
simp only [eq_geometrically, ← geometrically_iff_forall_fiberToSpecResidueField]

Premises used: AlgebraicGeometry.geometrically_iff_forall_fiberToSpecResidueField, AlgebraicGeometry.GeometricallyConnected.eq_geometrically
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Connected
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)

Tactic:
⟨geometrically_iff_of_isClosedUnderIsomorphisms.mpr fun K _ x ↦ ?_⟩

Premises used: Iff.mpr, AlgebraicGeometry.GeometricallyConnected.mk, AlgebraicGeometry.geometrically_iff_of_isClosedUnderIsomorphisms
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Connected
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
refine :
  ∀ (K : Type u_1) (x : Field K) (x_1 : Spec (CommRingCat.of K) ⟶ Z), ConnectedSpace.{u_1} ↥(pullback (f ≫ g) x_1)
⊢ GeometricallyConnected (f ≫ g)

Tactic:
refine ⟨geometrically_iff_of_isClosedUnderIsomorphisms.mpr fun K _ x ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Connected
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
rw : ConnectedSpace.{u_1} ↥(pullback (Y := pullback g x) f (pullback.fst g x))
⊢ ConnectedSpace.{u_1} ↥(pullback (f ≫ g) x)

Tactic:
rw [← (pullbackRightPullbackFstIso g x f).hom.homeomorph.connectedSpace_iff]

Premises used: Homeomorph.connectedSpace_iff, CategoryTheory.Limits.pullbackRightPullbackFstIso, AlgebraicGeometry.Scheme.Hom.homeomorph, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Connected
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 (Y := pullback g x) f (pullback.fst g x))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Integral
Goal:
h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1), GeometricallyIntegral x_2 ↔ geometrically IsIntegral x_2
⊢ @GeometricallyIntegral = geometrically IsIntegral

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Integral
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ GeometricallyIntegral x_2 ↔ geometrically IsIntegral x_2

Tactic:
geometricallyIntegral_iff _

Premises used: AlgebraicGeometry.geometricallyIntegral_iff
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Integral
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ GeometricallyIntegral x_2 ↔ geometrically IsIntegral x_2

Tactic:
exact geometricallyIntegral_iff _

Premises used: AlgebraicGeometry.geometricallyIntegral_iff
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Integral
Goal:
rw : geometrically IsIntegral = geometrically (IsReduced ⊓ fun (x : Scheme.{u_1}) ↦ IrreducibleSpace.{u_1} ↥x)
⊢ @GeometricallyIntegral = @GeometricallyReduced ⊓ @GeometricallyIrreducible

Tactic:
rw [eq_geometrically, GeometricallyReduced.eq_geometrically,
    GeometricallyIrreducible.eq_geometrically, ← geometrically_inf]

Premises used: AlgebraicGeometry.GeometricallyIrreducible.eq_geometrically, AlgebraicGeometry.geometrically_inf, AlgebraicGeometry.GeometricallyIntegral.eq_geometrically, AlgebraicGeometry.GeometricallyReduced.eq_geometrically
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Integral
Goal:
⊢ Eq.{u_1 + 2} (α := {X Y : Scheme.{u_1}} → (f : X ⟶ Y) → Prop)
    (fun ⦃X Y : Scheme.{u_1}⦄ (x : X ⟶ Y) ↦ geometrically (fun (X : Scheme.{u_1}) ↦ IsIntegral X) x)
    fun ⦃X Y : Scheme.{u_1}⦄ (x : X ⟶ Y) ↦
    geometrically
      (fun (a : Scheme.{u_1}) ↦
        ((fun (X : Scheme.{u_1}) ↦ IsReduced X) ⊓ fun (x : Scheme.{u_1}) ↦ IrreducibleSpace.{u_1} ↥x) a)
      x

Tactic:
simp [isIntegral_iff_irreducibleSpace_and_isReduced, and_comm]

Premises used: and_comm, AlgebraicGeometry.isIntegral_iff_irreducibleSpace_and_isReduced
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Integral
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : GeometricallyIntegral f
⊢ GeometricallyReduced f

Tactic:
(GeometricallyIntegral.eq_geometricallyReduced_inf_geometricallyIrreducible.le _ _ _ ‹_›).1

Premises used: Eq.le, And.left, AlgebraicGeometry.GeometricallyIntegral.eq_geometricallyReduced_inf_geometricallyIrreducible
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Integral
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : GeometricallyIntegral f
⊢ GeometricallyIrreducible f

Tactic:
(GeometricallyIntegral.eq_geometricallyReduced_inf_geometricallyIrreducible.le _ _ _ ‹_›).2

Premises used: Eq.le, And.right, AlgebraicGeometry.GeometricallyIntegral.eq_geometricallyReduced_inf_geometricallyIrreducible
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Integral
Goal:
X S : Scheme
f : X ⟶ S
inst : GeometricallyReduced f
inst_1 : GeometricallyIrreducible f
⊢ GeometricallyIntegral f

Tactic:
GeometricallyIntegral.eq_geometricallyReduced_inf_geometricallyIrreducible.ge _ _ _ ⟨‹_›, ‹_›⟩

Premises used: Eq.ge, And.intro, AlgebraicGeometry.GeometricallyIntegral.eq_geometricallyReduced_inf_geometricallyIrreducible
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Integral
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ IsStableUnderBaseChange @GeometricallyIntegral

Tactic:
GeometricallyIntegral.eq_geometrically ▸ inferInstance

Premises used: Eq.rec, inferInstance, Eq.symm, AlgebraicGeometry.GeometricallyIntegral.eq_geometrically