awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
⊢ Scheme.Γ.IsRightAdjoint

Tactic:
ΓSpec.adjunction.rightOp.isRightAdjoint

Premises used: AlgebraicGeometry.ΓSpec.adjunction, CategoryTheory.Adjunction.rightOp, CategoryTheory.Adjunction.isRightAdjoint
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
h :
  ∀ ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y),
    geometrically P f ↔
      MorphismProperty.universally (fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦ IsIntegral Y → Subsingleton.{u + 1} ↥Y → P X) f
⊢ geometrically P =
    MorphismProperty.universally fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦ IsIntegral Y → Subsingleton.{u + 1} ↥Y → P X

Tactic:
ext X Y f
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
⊢ geometrically P f ↔
    MorphismProperty.universally (fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦ IsIntegral Y → Subsingleton.{u + 1} ↥Y → P X) f

Tactic:
⟨fun hf Z W snd q fst h _ _ ↦ ?_, fun hf aK y Z W fst snd h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
h :
  ∀ (hf : geometrically P f) (Z W : Scheme.{u}) (snd : Z ⟶ X) (q : W ⟶ Y) (fst : Z ⟶ W) (h : IsPullback fst snd q f),
    IsIntegral W → Subsingleton.{u + 1} ↥W → P Z
h₁ :
  ∀
    (hf :
      MorphismProperty.universally (fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦ IsIntegral Y → Subsingleton.{u + 1} ↥Y → P X)
        f)
    (aK : Type u) (y : Field aK) (Z : Spec (of aK) ⟶ Y) (W : Scheme.{u}) (fst : W ⟶ X) (snd : W ⟶ Spec (of aK))
    (h : IsPullback fst snd f Z), P W
⊢ geometrically P f ↔
    MorphismProperty.universally (fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦ IsIntegral Y → Subsingleton.{u + 1} ↥Y → P X) f

Tactic:
refine ⟨fun hf Z W snd q fst h _ _ ↦ ?_, fun hf aK y Z W fst snd h ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : geometrically P f
Z W : Scheme
snd : Z ⟶ X
q : W ⟶ Y
fst : Z ⟶ W
h : IsPullback fst snd q f
h_1 : IsIntegral W
h_2 : Subsingleton.{u + 1} ↥W
h₁ : P Z
⊢ P Z

Tactic:
let := (isField_of_isIntegral_of_subsingleton W).toField
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : geometrically P f
Z W : Scheme
snd : Z ⟶ X
q : W ⟶ Y
fst : Z ⟶ W
h : IsPullback fst snd q f
h_1 : IsIntegral W
h_2 : Subsingleton.{u + 1} ↥W
this : Field (↑Γ(W, ⊤) : Type u) := ⋯.toField
h₁ : IsPullback snd (fst ≫ W.isoSpec.hom) f (W.isoSpec.inv ≫ q)
⊢ P Z

Tactic:
apply hf (W.isoSpec.inv ≫ q) snd (fst ≫ W.isoSpec.hom)

Premises used: AlgebraicGeometry.Scheme.isoSpec, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : geometrically P f
Z W : Scheme
snd : Z ⟶ X
q : W ⟶ Y
fst : Z ⟶ W
h : IsPullback fst snd q f
h_1 : IsIntegral W
h_2 : Subsingleton.{u + 1} ↥W
this : Field (↑Γ(W, ⊤) : Type u) := ⋯.toField
h₁ : snd ≫ Iso.hom (Iso.refl X) = Iso.hom (Iso.refl Z) ≫ snd
h₂ : fst ≫ W.isoSpec.hom = Iso.hom (Iso.refl Z) ≫ fst ≫ W.isoSpec.hom
h₃ : f ≫ Iso.hom (Iso.refl Y) = Iso.hom (Iso.refl X) ≫ f
h₄ : q ≫ Iso.hom (Iso.refl Y) = W.isoSpec.hom ≫ W.isoSpec.inv ≫ q
⊢ IsPullback snd (fst ≫ W.isoSpec.hom) f (W.isoSpec.inv ≫ q)

Tactic:
apply h.flip.of_iso (.refl _) (.refl _) W.isoSpec (.refl _)

Premises used: AlgebraicGeometry.Scheme.isoSpec, CategoryTheory.Iso.refl, CategoryTheory.IsPullback.of_iso, CategoryTheory.IsPullback.flip
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : geometrically P f
Z W : Scheme
snd : Z ⟶ X
q : W ⟶ Y
fst : Z ⟶ W
h : IsPullback fst snd q f
h_1 : IsIntegral W
h_2 : Subsingleton.{u + 1} ↥W
this : Field (↑Γ(W, ⊤) : Type u) := ⋯.toField
⊢ snd ≫ Iso.hom (Iso.refl X) = Iso.hom (Iso.refl Z) ≫ snd

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : geometrically P f
Z W : Scheme
snd : Z ⟶ X
q : W ⟶ Y
fst : Z ⟶ W
h : IsPullback fst snd q f
h_1 : IsIntegral W
h_2 : Subsingleton.{u + 1} ↥W
this : Field (↑Γ(W, ⊤) : Type u) := ⋯.toField
⊢ fst ≫ W.isoSpec.hom = Iso.hom (Iso.refl Z) ≫ fst ≫ W.isoSpec.hom

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : geometrically P f
Z W : Scheme
snd : Z ⟶ X
q : W ⟶ Y
fst : Z ⟶ W
h : IsPullback fst snd q f
h_1 : IsIntegral W
h_2 : Subsingleton.{u + 1} ↥W
this : Field (↑Γ(W, ⊤) : Type u) := ⋯.toField
⊢ f ≫ Iso.hom (Iso.refl Y) = Iso.hom (Iso.refl X) ≫ f

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : geometrically P f
Z W : Scheme
snd : Z ⟶ X
q : W ⟶ Y
fst : Z ⟶ W
h : IsPullback fst snd q f
h_1 : IsIntegral W
h_2 : Subsingleton.{u + 1} ↥W
this : Field (↑Γ(W, ⊤) : Type u) := ⋯.toField
⊢ q ≫ Iso.hom (Iso.refl Y) = W.isoSpec.hom ≫ W.isoSpec.inv ≫ q

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : MorphismProperty.universally (fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦ IsIntegral Y → Subsingleton.{u + 1} ↥Y → P X) f
aK : Type u
y : Field aK
Z : Spec (of aK) ⟶ Y
W : Scheme
fst : W ⟶ X
snd : W ⟶ Spec (of aK)
h : IsPullback fst snd f Z
⊢ P W

Tactic:
hf _ _ _ h.flip inferInstance inferInstance

Premises used: inferInstance, CategoryTheory.IsPullback.flip
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : MorphismProperty.universally (fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦ IsIntegral Y → Subsingleton.{u + 1} ↥Y → P X) f
aK : Type u
y : Field aK
Z : Spec (of aK) ⟶ Y
W : Scheme
fst : W ⟶ X
snd : W ⟶ Spec (of aK)
h : IsPullback fst snd f Z
⊢ P W

Tactic:
exact hf _ _ _ h.flip inferInstance inferInstance

Premises used: inferInstance, CategoryTheory.IsPullback.flip
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P Q : ObjectProperty Scheme
simp :
  Eq.{u + 2} (α := MorphismProperty Scheme)
    (MorphismProperty.universally fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦
      IsIntegral Y → Subsingleton.{u + 1} ↥Y → (P ⊓ Q) X)
    (MorphismProperty.universally
      ((fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦ IsIntegral Y → Subsingleton.{u + 1} ↥Y → P X) ⊓
        fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦ IsIntegral Y → Subsingleton.{u + 1} ↥Y → Q X))
⊢ geometrically (P ⊓ Q) = geometrically P ⊓ geometrically Q

Tactic:
simp only [geometrically_eq_universally, ← MorphismProperty.universally_inf]

Premises used: CategoryTheory.MorphismProperty.universally_inf, AlgebraicGeometry.geometrically_eq_universally
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P Q : ObjectProperty Scheme
e_P :
  ∀ ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y),
    IsIntegral Y → Subsingleton.{u + 1} ↥Y → (P ⊓ Q) X ↔
      ((fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦ IsIntegral Y → Subsingleton.{u + 1} ↥Y → P X) ⊓
          fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦ IsIntegral Y → Subsingleton.{u + 1} ↥Y → Q X)
        f
⊢ Eq.{u + 2} (α := MorphismProperty Scheme)
    (MorphismProperty.universally fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦
      IsIntegral Y → Subsingleton.{u + 1} ↥Y → (P ⊓ Q) X)
    (MorphismProperty.universally
      ((fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦ IsIntegral Y → Subsingleton.{u + 1} ↥Y → P X) ⊓
        fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦ IsIntegral Y → Subsingleton.{u + 1} ↥Y → Q X))

Tactic:
congr with X Y f
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P Q : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
⊢ IsIntegral Y → Subsingleton.{u + 1} ↥Y → (P ⊓ Q) X ↔
    ((fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦ IsIntegral Y → Subsingleton.{u + 1} ↥Y → P X) ⊓
        fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦ IsIntegral Y → Subsingleton.{u + 1} ↥Y → Q X)
      f

Tactic:
⟨fun H ↦ ⟨(H · · |>.1), (H · · |>.2)⟩, fun H a b ↦ ⟨H.1 a b, H.2 a b⟩⟩

Premises used: And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P Q : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
⊢ IsIntegral Y → Subsingleton.{u + 1} ↥Y → (P ⊓ Q) X ↔
    ((fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦ IsIntegral Y → Subsingleton.{u + 1} ↥Y → P X) ⊓
        fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦ IsIntegral Y → Subsingleton.{u + 1} ↥Y → Q X)
      f

Tactic:
exact ⟨fun H ↦ ⟨(H · · |>.1), (H · · |>.2)⟩, fun H a b ↦ ⟨H.1 a b, H.2 a b⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
rw :
  MorphismProperty.IsStableUnderBaseChange.{u, u + 1} (C := Scheme)
    (MorphismProperty.universally fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦ IsIntegral Y → Subsingleton.{u + 1} ↥Y → P X)
⊢ (geometrically P).IsStableUnderBaseChange

Tactic:
rw [geometrically_eq_universally]

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

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
inst : P.IsClosedUnderIsomorphisms
rw :
  IsZariskiLocalAtTarget.{u}
    (MorphismProperty.universally fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦ IsIntegral Y → Subsingleton.{u + 1} ↥Y → P X)
⊢ IsZariskiLocalAtTarget.{u} (geometrically P)

Tactic:
rw [geometrically_eq_universally]

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

Tactic:
universally_isZariskiLocalAtTarget _ fun {X} Y f ι U hU H _ _ ↦ ?_

Premises used: AlgebraicGeometry.universally_isZariskiLocalAtTarget
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
inst : P.IsClosedUnderIsomorphisms
refine :
  ∀ {X : Scheme.{u}} (Y : Scheme.{u}) (f : X ⟶ Y) (ι : Type u) (U : ι → Y.Opens) (hU : TopologicalSpace.IsOpenCover U)
    (H :
      ∀ (i : ι),
        IsIntegral.{u} (↑(U i) : Scheme) → Subsingleton.{u + 1} ↥(↑(U i) : Scheme) → P (↑(f ⁻¹ᵁ U i) : Scheme)),
    IsIntegral Y → Subsingleton.{u + 1} ↥Y → P X
⊢ IsZariskiLocalAtTarget.{u}
    (MorphismProperty.universally fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦ IsIntegral Y → Subsingleton.{u + 1} ↥Y → P X)

Tactic:
refine universally_isZariskiLocalAtTarget _ fun {X} Y f ι U hU H _ _ ↦ ?_

Premises used: AlgebraicGeometry.universally_isZariskiLocalAtTarget
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
inst : P.IsClosedUnderIsomorphisms
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : TopologicalSpace.IsOpenCover U
H : ∀ (i : ι), IsIntegral.{u} (↑(U i) : Scheme) → Subsingleton.{u + 1} ↥(↑(U i) : Scheme) → P (↑(f ⁻¹ᵁ U i) : Scheme)
h : IsIntegral Y
h_1 : Subsingleton.{u + 1} ↥Y
obtain : ∀ (y : ↥Y), P X
⊢ P X

Tactic:
obtain ⟨y⟩ := (inferInstance : Nonempty Y)

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
inst : P.IsClosedUnderIsomorphisms
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : TopologicalSpace.IsOpenCover U
H : ∀ (i : ι), IsIntegral.{u} (↑(U i) : Scheme) → Subsingleton.{u + 1} ↥(↑(U i) : Scheme) → P (↑(f ⁻¹ᵁ U i) : Scheme)
h : IsIntegral Y
h_1 : Subsingleton.{u + 1} ↥Y
y : ↥Y
obtain : ∀ (i : ι) (hy : y ∈ U i), P X
⊢ P X

Tactic:
obtain ⟨i, hy⟩ := hU.exists_mem y

Premises used: TopologicalSpace.IsOpenCover.exists_mem
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
inst : P.IsClosedUnderIsomorphisms
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : TopologicalSpace.IsOpenCover U
H : ∀ (i : ι), IsIntegral.{u} (↑(U i) : Scheme) → Subsingleton.{u + 1} ↥(↑(U i) : Scheme) → P (↑(f ⁻¹ᵁ U i) : Scheme)
h : IsIntegral Y
h_1 : Subsingleton.{u + 1} ↥Y
y : ↥Y
i : ι
hy : y ∈ U i
z : ↥Y
h_2 : Membership.mem (γ := TopologicalSpace.Opens ↥Y) ⊤ z
rwa rwa₁ rwa₂ rwa₃ : y ∈ U i
⊢ z ∈ U i

Tactic:
rwa [Subsingleton.elim z y]

Premises used: Subsingleton.elim
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
inst : P.IsClosedUnderIsomorphisms
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : TopologicalSpace.IsOpenCover U
H : ∀ (i : ι), IsIntegral.{u} (↑(U i) : Scheme) → Subsingleton.{u + 1} ↥(↑(U i) : Scheme) → P (↑(f ⁻¹ᵁ U i) : Scheme)
h : IsIntegral Y
h_1 : Subsingleton.{u + 1} ↥Y
y : ↥Y
i : ι
hy : y ∈ U i
have : ∀ (heq : U i = ⊤), P X
⊢ P X

Tactic:
have heq : U i = ⊤ := eq_top_iff.mpr fun z _ ↦ by rwa [Subsingleton.elim z y]
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
inst : P.IsClosedUnderIsomorphisms
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : TopologicalSpace.IsOpenCover U
H : ∀ (i : ι), IsIntegral.{u} (↑(U i) : Scheme) → Subsingleton.{u + 1} ↥(↑(U i) : Scheme) → P (↑(f ⁻¹ᵁ U i) : Scheme)
h : IsIntegral Y
h_1 : Subsingleton.{u + 1} ↥Y
y : ↥Y
i : ι
hy : y ∈ U i
heq : U i = ⊤
e : (↑(U i) : Scheme) ≅ Y := Y.isoOfEq heq ≪≫ Y.topIso
⊢ f ⁻¹ᵁ U i = ⊤

Tactic:
simp [heq]
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
inst : P.IsClosedUnderIsomorphisms
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : TopologicalSpace.IsOpenCover U
H : ∀ (i : ι), IsIntegral.{u} (↑(U i) : Scheme) → Subsingleton.{u + 1} ↥(↑(U i) : Scheme) → P (↑(f ⁻¹ᵁ U i) : Scheme)
h : IsIntegral Y
h_1 : Subsingleton.{u + 1} ↥Y
y : ↥Y
i : ι
hy : y ∈ U i
heq : U i = ⊤
e : (↑(U i) : Scheme) ≅ Y := Y.isoOfEq heq ≪≫ Y.topIso
e' : (↑(f ⁻¹ᵁ U i) : Scheme) ≅ X := X.isoOfEq ⋯ ≪≫ X.topIso
⊢ P X

Tactic:
P.prop_of_iso e' <| H i (.of_isIso e.inv) (e.hom.homeomorph.subsingleton_congr.mpr ‹_›)

Premises used: Iff.mpr, AlgebraicGeometry.IsIntegral.of_isIso, Homeomorph.toEquiv, Equiv.subsingleton_congr, CategoryTheory.ObjectProperty.prop_of_iso, AlgebraicGeometry.Scheme.Hom.homeomorph, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
inst : P.IsClosedUnderIsomorphisms
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : TopologicalSpace.IsOpenCover U
H : ∀ (i : ι), IsIntegral.{u} (↑(U i) : Scheme) → Subsingleton.{u + 1} ↥(↑(U i) : Scheme) → P (↑(f ⁻¹ᵁ U i) : Scheme)
h : IsIntegral Y
h_1 : Subsingleton.{u + 1} ↥Y
y : ↥Y
i : ι
hy : y ∈ U i
heq : U i = ⊤
e : (↑(U i) : Scheme) ≅ Y := Y.isoOfEq heq ≪≫ Y.topIso
e' : (↑(f ⁻¹ᵁ U i) : Scheme) ≅ X := X.isoOfEq ⋯ ≪≫ X.topIso
⊢ P X

Tactic:
exact P.prop_of_iso e' <| H i (.of_isIso e.inv) (e.hom.homeomorph.subsingleton_congr.mpr ‹_›)

Premises used: Iff.mpr, AlgebraicGeometry.IsIntegral.of_isIso, Homeomorph.toEquiv, Equiv.subsingleton_congr, CategoryTheory.ObjectProperty.prop_of_iso, AlgebraicGeometry.Scheme.Hom.homeomorph, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : geometrically P f
K : Type u
inst : Field K
y : Spec (of K) ⟶ Y
⊢ P (pullback f y)

Tactic:
hf _ _ _ (.of_hasPullback _ _)

Premises used: CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : geometrically P f
K : Type u
inst : Field K
y : Spec (of K) ⟶ Y
⊢ P (pullback y f)

Tactic:
hf _ _ _ (.flip <| .of_hasPullback _ _)

Premises used: CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
inst : P.IsClosedUnderIsomorphisms
⊢ geometrically P f ↔ ∀ (K : Type u) [inst : Field K] (y : Spec (of K) ⟶ Y), P (pullback f y)

Tactic:
⟨fun h K _ _ ↦ pullback_of_geometrically h _ _, fun H K _ _ Y fst snd h ↦ ?_⟩

Premises used: Iff.intro, AlgebraicGeometry.pullback_of_geometrically
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
inst : P.IsClosedUnderIsomorphisms
refine :
  ∀ (H : ∀ (K : Type u) [inst : Field K] (y : Spec (of K) ⟶ Y), P (pullback f y)) (K : Type u) (x : Field K)
    (x_1 : Spec (of K) ⟶ Y) (Y_1 : Scheme.{u}) (fst : Y_1 ⟶ X) (snd : Y_1 ⟶ Spec (of K)) (h : IsPullback fst snd f x_1),
    P Y_1
⊢ geometrically P f ↔ ∀ (K : Type u) [inst : Field K] (y : Spec (of K) ⟶ Y), P (pullback f y)

Tactic:
refine ⟨fun h K _ _ ↦ pullback_of_geometrically h _ _, fun H K _ _ Y fst snd h ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
X Y_1 : Scheme
f : X ⟶ Y_1
inst : P.IsClosedUnderIsomorphisms
H : ∀ (K : Type u) [inst : Field K] (y : Spec (of K) ⟶ Y_1), P (pullback f y)
K : Type u
x : Field K
x_1 : Spec (of K) ⟶ Y_1
Y : Scheme
fst : Y ⟶ X
snd : Y ⟶ Spec (of K)
h : IsPullback fst snd f x_1
⊢ P Y

Tactic:
P.prop_of_iso h.isoPullback.symm (H _ _)

Premises used: CategoryTheory.ObjectProperty.prop_of_iso, CategoryTheory.IsPullback.isoPullback, CategoryTheory.Iso.symm
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
X Y_1 : Scheme
f : X ⟶ Y_1
inst : P.IsClosedUnderIsomorphisms
H : ∀ (K : Type u) [inst : Field K] (y : Spec (of K) ⟶ Y_1), P (pullback f y)
K : Type u
x : Field K
x_1 : Spec (of K) ⟶ Y_1
Y : Scheme
fst : Y ⟶ X
snd : Y ⟶ Spec (of K)
h : IsPullback fst snd f x_1
⊢ P Y

Tactic:
exact P.prop_of_iso h.isoPullback.symm (H _ _)

Premises used: CategoryTheory.ObjectProperty.prop_of_iso, CategoryTheory.IsPullback.isoPullback, CategoryTheory.Iso.symm
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : geometrically P f
y : ↥Y
⊢ P (Scheme.Hom.fiber f y)

Tactic:
pullback_of_geometrically hf _ _

Premises used: AlgebraicGeometry.Scheme.residueField, AlgebraicGeometry.Scheme.Hom.fiber, AlgebraicGeometry.pullback_of_geometrically
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
⊢ geometrically P f ↔ ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)

Tactic:
⟨fun hf y ↦ (geometrically P).pullback_snd _ _ hf, fun H ↦ ?_⟩

Premises used: AlgebraicGeometry.Scheme.fromSpecResidueField, Iff.intro, CategoryTheory.MorphismProperty.pullback_snd
-- Module: Mathlib.AlgebraicGeometry.Geometrically.Basic
Goal:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
refine : ∀ (H : ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)), geometrically P f
⊢ geometrically P f ↔ ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)

Tactic:
refine ⟨fun hf y ↦ (geometrically P).pullback_snd _ _ hf, fun 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] (y : Spec (of K) ⟶ Y) ⦃Z : Scheme.{u}⦄ (fst : Z ⟶ X) (snd : Z ⟶ Spec (of K)),
    IsPullback fst snd f y → P Z
⊢ ∀ [inst : Field K] (y : Spec (of K) ⟶ Y) ⦃Z : Scheme.{u}⦄ (fst : Z ⟶ X) (snd : Z ⟶ Spec (of K)),
    IsPullback fst snd f y → P Z

Tactic:
_
-- 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
y : Spec (of K) ⟶ Y
Z : Scheme
fst : Z ⟶ X
snd : Z ⟶ Spec (of K)
h : IsPullback fst snd f y
obtain :
  ∀ (y : ↥Y) (φ : Y.residueField y ⟶ of K)
    (h :
      IsPullback fst snd f
        ((Equiv.symm (Scheme.SpecToEquivOfField K Y) : (a : (x : ↥Y) × (Y.residueField x ⟶ of K)) → Spec (of K) ⟶ Y)
          (Sigma.mk (β := fun (x : ↥Y) ↦ Y.residueField x ⟶ of K) y φ))),
    P Z
⊢ P Z

Tactic:
obtain ⟨⟨y, φ⟩, rfl⟩ := (Scheme.SpecToEquivOfField _ _).symm.surjective y

Premises used: AlgebraicGeometry.Scheme.SpecToEquivOfField, Equiv.surjective, Equiv.symm, rfl
-- 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
    ((Equiv.symm (Scheme.SpecToEquivOfField K Y) : (a : (x : ↥Y) × (Y.residueField x ⟶ of K)) → Spec (of K) ⟶ Y)
      (Sigma.mk (β := fun (x : ↥Y) ↦ Y.residueField x ⟶ of K) y φ))
⊢ fst ≫ f = (snd ≫ Spec.map φ) ≫ Y.fromSpecResidueField y

Tactic:
simp [h.w, Scheme.SpecToEquivOfField]

Premises used: AlgebraicGeometry.Scheme.SpecToEquivOfField, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w
-- 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
    ((Equiv.symm (Scheme.SpecToEquivOfField K Y) : (a : (x : ↥Y) × (Y.residueField x ⟶ of K)) → Spec (of K) ⟶ Y)
      (Sigma.mk (β := fun (x : ↥Y) ↦ Y.residueField x ⟶ of K) y φ))
let : P Z
⊢ P Z

Tactic:
let p : Z ⟶ f.fiber y :=
    pullback.lift fst (snd ≫ Spec.map φ) (by simp [h.w, Scheme.SpecToEquivOfField])
-- 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
    ((Equiv.symm (Scheme.SpecToEquivOfField K Y) : (a : (x : ↥Y) × (Y.residueField x ⟶ of K)) → Spec (of K) ⟶ Y)
      (Sigma.mk (β := fun (x : ↥Y) ↦ Y.residueField x ⟶ of K) y φ))
p : Z ⟶ Scheme.Hom.fiber f y := pullback.lift fst (snd ≫ Spec.map φ) ⋯
apply : IsPullback p snd (Scheme.Hom.fiberToSpecResidueField f y) (Spec.map φ)
⊢ P Z

Tactic:
apply H y (Spec.map φ) p snd

Premises used: AlgebraicGeometry.Spec.map
-- 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 φ) ⋯
⊢ IsPullback p snd (Scheme.Hom.fiberToSpecResidueField f y) (Spec.map φ)

Tactic:
.flip (.of_bot (.flip ?_) ?_ (IsPullback.of_hasPullback f (Y.fromSpecResidueField y)).flip)

Premises used: CategoryTheory.IsPullback.of_bot, AlgebraicGeometry.Scheme.fromSpecResidueField, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_hasPullback
-- 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 φ) ⋯
refine_1 : IsPullback (p ≫ pullback.fst f (Y.fromSpecResidueField y)) snd f (Spec.map φ ≫ Y.fromSpecResidueField y)
refine_2 : snd ≫ Spec.map φ = p ≫ Scheme.Hom.fiberToSpecResidueField f y
⊢ IsPullback p snd (Scheme.Hom.fiberToSpecResidueField f y) (Spec.map φ)

Tactic:
refine .flip (.of_bot (.flip ?_) ?_ (IsPullback.of_hasPullback f (Y.fromSpecResidueField y)).flip)
-- 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 φ) ⋯
⊢ IsPullback fst snd f (Spec.map φ ≫ Y.fromSpecResidueField y)

Tactic:
h