awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Integral
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : GeometricallyIntegral g
⊢ GeometricallyIntegral (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.Integral
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : GeometricallyIntegral f
⊢ GeometricallyIntegral (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.Integral
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
V : S.Opens
inst : GeometricallyIntegral f
⊢ GeometricallyIntegral (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.Integral
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
s : ↥S
inst : GeometricallyIntegral f
⊢ GeometricallyIntegral (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.Integral
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
s : ↥S
inst : GeometricallyIntegral f
⊢ IsIntegral.{u_1} (Scheme.Hom.fiber f s)

Tactic:
GeometricallyIntegral.geometrically_isIntegral _ _ _ (.of_hasPullback _ _)

Premises used: CategoryTheory.IsPullback.of_hasPullback, AlgebraicGeometry.GeometricallyIntegral.geometrically_isIntegral
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Integral
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : GeometricallyIntegral 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.Integral
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
rw : IrreducibleSpace.{u_1} ↥X ∧ IsReduced X
⊢ IsIntegral X

Tactic:
rw [isIntegral_iff_irreducibleSpace_and_isReduced]

Premises used: AlgebraicGeometry.isIntegral_iff_irreducibleSpace_and_isReduced
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Integral
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
⊢ IrreducibleSpace.{u_1} ↥X ∧ IsReduced X

Tactic:
⟨GeometricallyIrreducible.irreducibleSpace f f.isOpenMap,
    GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherian f⟩

Premises used: AlgebraicGeometry.GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherian, AlgebraicGeometry.Scheme.Hom.isOpenMap, And.intro, AlgebraicGeometry.GeometricallyIrreducible.irreducibleSpace
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Integral
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
⊢ IrreducibleSpace.{u_1} ↥X ∧ IsReduced X

Tactic:
exact ⟨GeometricallyIrreducible.irreducibleSpace f f.isOpenMap,
    GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherian f⟩
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Integral
Goal:
X S : Scheme
f : X ⟶ S
inst : GeometricallyIntegral f
inst_1 : Subsingleton.{u_1 + 1} ↥S
inst_2 : IsIntegral S
rw : IrreducibleSpace.{u_1} ↥X ∧ IsReduced X
⊢ IsIntegral X

Tactic:
rw [isIntegral_iff_irreducibleSpace_and_isReduced]

Premises used: AlgebraicGeometry.isIntegral_iff_irreducibleSpace_and_isReduced
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Integral
Goal:
X S : Scheme
f : X ⟶ S
inst : GeometricallyIntegral f
inst_1 : Subsingleton.{u_1 + 1} ↥S
inst_2 : IsIntegral S
⊢ IrreducibleSpace.{u_1} ↥X ∧ IsReduced X

Tactic:
⟨GeometricallyIrreducible.irreducibleSpace_of_subsingleton f,
    GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherian f⟩

Premises used: AlgebraicGeometry.GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherian, AlgebraicGeometry.GeometricallyIrreducible.irreducibleSpace_of_subsingleton, And.intro
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Integral
Goal:
X S : Scheme
f : X ⟶ S
inst : GeometricallyIntegral f
inst_1 : Subsingleton.{u_1 + 1} ↥S
inst_2 : IsIntegral S
⊢ IrreducibleSpace.{u_1} ↥X ∧ IsReduced X

Tactic:
refine ⟨GeometricallyIrreducible.irreducibleSpace_of_subsingleton f,
    GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherian f⟩
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Integral
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : GeometricallyIntegral f
inst_1 : Flat f
inst_2 : UniversallyOpen f
inst_3 : IsIntegral Y
inst_4 : IsLocallyNoetherian Y
⊢ IsIntegral.{u_1} (pullback f g)

Tactic:
GeometricallyIntegral.isIntegral_of_isLocallyNoetherian (pullback.snd _ _)

Premises used: CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.GeometricallyIntegral.isIntegral_of_isLocallyNoetherian
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Integral
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : GeometricallyIntegral g
inst_1 : Flat g
inst_2 : UniversallyOpen g
inst_3 : IsIntegral X
inst_4 : IsLocallyNoetherian X
⊢ IsIntegral.{u_1} (pullback f g)

Tactic:
GeometricallyIntegral.isIntegral_of_isLocallyNoetherian (pullback.fst _ _)

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

Tactic:
simp only [GeometricallyIntegral.eq_geometrically,
    ← geometrically_iff_forall_fiberToSpecResidueField]

Premises used: AlgebraicGeometry.geometrically_iff_forall_fiberToSpecResidueField, AlgebraicGeometry.GeometricallyIntegral.eq_geometrically
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible
Goal:
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
⊢ @GeometricallyIrreducible = geometrically fun (x : Scheme.{u_1}) ↦ IrreducibleSpace.{u_1} ↥x

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

Tactic:
geometricallyIrreducible_iff _

Premises used: AlgebraicGeometry.geometricallyIrreducible_iff
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ GeometricallyIrreducible x_2 ↔ geometrically (fun (x : Scheme.{u_1}) ↦ IrreducibleSpace.{u_1} ↥x) x_2

Tactic:
exact geometricallyIrreducible_iff _

Premises used: AlgebraicGeometry.geometricallyIrreducible_iff
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ IsStableUnderBaseChange @GeometricallyIrreducible

Tactic:
GeometricallyIrreducible.eq_geometrically ▸ inferInstance

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

Tactic:
GeometricallyIrreducible.geometrically_irreducibleSpace _ _ _ (.of_hasPullback _ _)

Premises used: AlgebraicGeometry.GeometricallyIrreducible.geometrically_irreducibleSpace, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : GeometricallyIrreducible 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.Irreducible
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)
wlog : ∀ {s : Set ↥S} (hs : IsIrreducible s) (H : ∃ (x : ↥S), s = {x}), IsIrreducible (X := ↥X) (⇑f ⁻¹' s)
⊢ IsIrreducible (X := ↥X) (⇑f ⁻¹' s)

Tactic:
wlog H : ∃ x, s = {x} generalizing s
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible
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}
inr : (s ∩ Set.range (ι := ↥X) ⇑f).Nonempty
⊢ IsIrreducible (X := ↥X) (⇑f ⁻¹' s)

Tactic:
refine hs.preimage_of_isPreirreducible_fiber _ hf
      (fun x ↦ (this isIrreducible_singleton ⟨_, rfl⟩).isPreirreducible) ?_

Premises used: isIrreducible_singleton, IsIrreducible.isPreirreducible, IsIrreducible.preimage_of_isPreirreducible_fiber, Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible
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}
inr : s.Nonempty
⊢ (s ∩ Set.range (ι := ↥X) ⇑f).Nonempty

Tactic:
rw [Set.range_eq_univ.mpr f.surjective, Set.inter_univ]

Premises used: Iff.mpr, Set.range_eq_univ, Set.inter_univ, AlgebraicGeometry.Scheme.Hom.surjective
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible
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.Nonempty

Tactic:
hs.nonempty

Premises used: IsIrreducible.nonempty
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible
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.Nonempty

Tactic:
exact hs.nonempty

Premises used: IsIrreducible.nonempty
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible
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}
obtain : ∀ (s : ↥S) (hs : IsIrreducible (X := ↥S) {s}), IsIrreducible (X := ↥X) (Set.preimage (β := ↥S) ⇑f {s})
⊢ IsIrreducible (X := ↥X) (⇑f ⁻¹' s)

Tactic:
obtain ⟨s, rfl⟩ := H

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible
Goal:
X S : Scheme
f : X ⟶ S
inst : GeometricallyIrreducible f
hf : IsOpenMap (X := ↥X) (Y := ↥S) ⇑f
s : ↥S
hs : IsIrreducible (X := ↥S) {s}
rw : IsIrreducible (X := ↥X) (Set.image (α := ↥(fiber f s)) (⇑(fiberι f s)) Set.univ)
⊢ IsIrreducible (X := ↥X) (Set.preimage (β := ↥S) ⇑f {s})

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

Premises used: Set.image_univ, AlgebraicGeometry.Scheme.Hom.range_fiberι
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible
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.image (α := ↥(fiber f s)) (⇑(fiberι f s)) Set.univ)

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

Premises used: Continuous.continuousOn, IrreducibleSpace.isIrreducible_univ, IsIrreducible.image, AlgebraicGeometry.Scheme.Hom.fiberι, AlgebraicGeometry.Scheme.Hom.continuous
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible
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.image (α := ↥(fiber f s)) (⇑(fiberι f s)) Set.univ)

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

Premises used: Continuous.continuousOn, IrreducibleSpace.isIrreducible_univ, IsIrreducible.image, AlgebraicGeometry.Scheme.Hom.fiberι, AlgebraicGeometry.Scheme.Hom.continuous
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible
Goal:
X S : Scheme
f : X ⟶ S
inst : GeometricallyIrreducible f
inst_1 : IrreducibleSpace.{u_1} ↥S
hf : IsOpenMap (X := ↥X) (Y := ↥S) ⇑f
⊢ IrreducibleSpace.{u_1} ↥X

Tactic:
simpa [irreducibleSpace_def] using
    f.isIrreducible_preimage hf (IrreducibleSpace.isIrreducible_univ _)

Premises used: IrreducibleSpace.isIrreducible_univ, AlgebraicGeometry.Scheme.Hom.isIrreducible_preimage, irreducibleSpace_def
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible
Goal:
X S : Scheme
f : X ⟶ S
inst : GeometricallyIrreducible f
inst_1 : Subsingleton.{u_1 + 1} ↥S
inst_2 : Nonempty.{u_1 + 1} ↥S
⊢ IrreducibleSpace.{u_1} ↥X

Tactic:
have : IrreducibleSpace S := ⟨‹_›⟩
  GeometricallyIrreducible.irreducibleSpace (f := f) fun _ _ ↦ isOpen_discrete _

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

Tactic:
GeometricallyIrreducible.irreducibleSpace (pullback.snd _ _) (pullback.snd f g).isOpenMap

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

Tactic:
GeometricallyIrreducible.irreducibleSpace (pullback.fst _ _) (pullback.fst f g).isOpenMap

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

Tactic:
simp only [GeometricallyIrreducible.eq_geometrically,
    ← geometrically_iff_forall_fiberToSpecResidueField]

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

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

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

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

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

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

Tactic:
infer_instance
-- 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)
rw : ∀ (s : ↥S), GeometricallyIrreducible (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s)
⊢ GeometricallyIrreducible (f ≫ g)

Tactic:
rw [GeometricallyIrreducible.iff_geometricallyIrreducible_fiber]

Premises used: AlgebraicGeometry.GeometricallyIrreducible.iff_geometricallyIrreducible_fiber
-- 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
⊢ GeometricallyIrreducible (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s)

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

Premises used: Iff.mpr, AlgebraicGeometry.GeometricallyIrreducible.mk, AlgebraicGeometry.geometrically_iff_of_isClosedUnderIsomorphisms
-- 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
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)
⊢ GeometricallyIrreducible (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s)

Tactic:
refine ⟨geometrically_iff_of_isClosedUnderIsomorphisms.mpr fun K _ x ↦ ?_⟩
-- 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)
⊢ (f ≫ g) ≫ 𝟙 S = f ≫ g

Tactic:
simp
-- 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)
⊢ S.fromSpecResidueField s ≫ 𝟙 S = 𝟙 (Spec (S.residueField s)) ≫ S.fromSpecResidueField s

Tactic:
simp
-- 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)
⊢ Scheme.Hom.fiberToSpecResidueField (f ≫ g) s ≫ 𝟙 (Spec (S.residueField s)) =
    pullback.map (f ≫ g) (S.fromSpecResidueField s) g (S.fromSpecResidueField s) f (𝟙 (Spec (S.residueField s))) (𝟙 S) ⋯
        ⋯ ≫
      Scheme.Hom.fiberToSpecResidueField g s

Tactic:
simp [Scheme.Hom.fiberToSpecResidueField]

Premises used: AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField
-- 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)
⊢ x ≫ 𝟙 (Spec (S.residueField s)) = 𝟙 (Spec (CommRingCat.of K)) ≫ x

Tactic:
simp