awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
R : CommRingCat
rw : Spec.map (Scheme.ΓSpecIso R).hom ≫ Spec.map (Scheme.ΓSpecIso R).inv = 𝟙 (Spec R)
⊢ (Spec R).toSpecΓ ≫ Spec.map (Scheme.ΓSpecIso R).inv = 𝟙 (Spec R)
have rw₁ : Spec.map ((Scheme.ΓSpecIso R).inv ≫ (Scheme.ΓSpecIso R).hom) = 𝟙 (Spec R)
Tactic: rw [← SpecMap_ΓSpecIso_hom, ← Spec.map_comp, Iso.inv_hom_id, Spec.map_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
R : CommRingCat
rw : Spec.map (Scheme.ΓSpecIso R).hom ≫ Spec.map (Scheme.ΓSpecIso R).inv = 𝟙 (Spec R)
rw₁ : Spec.map ((Scheme.ΓSpecIso R).inv ≫ (Scheme.ΓSpecIso R).hom) = 𝟙 (Spec R)
⊢ (Spec R).toSpecΓ ≫ Spec.map (Scheme.ΓSpecIso R).inv = 𝟙 (Spec R)
have rw₂ : Spec.map (𝟙 R) = 𝟙 (Spec R)
Tactic: rw [← SpecMap_ΓSpecIso_hom, ← Spec.map_comp, Iso.inv_hom_id, Spec.map_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
R : CommRingCat
rw : Spec.map (Scheme.ΓSpecIso R).hom ≫ Spec.map (Scheme.ΓSpecIso R).inv = 𝟙 (Spec R)
rw₁ : Spec.map ((Scheme.ΓSpecIso R).inv ≫ (Scheme.ΓSpecIso R).hom) = 𝟙 (Spec R)
rw₂ : Spec.map (𝟙 R) = 𝟙 (Spec R)
⊢ (Spec R).toSpecΓ ≫ Spec.map (Scheme.ΓSpecIso R).inv = 𝟙 (Spec R)
have rw₃ : 𝟙 (Spec R) = 𝟙 (Spec R)
Tactic: rw [← SpecMap_ΓSpecIso_hom, ← Spec.map_comp, Iso.inv_hom_id, Spec.map_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : Scheme
r : (↑Γ(X, ⊤) : Type u)
⊢ X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = X.basicOpen r
have rw : X.basicOpen (U := X.toSpecΓ ⁻¹ᵁ ⊤)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Hom.appTop X.toSpecΓ) :
        (a : (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u)) → (↑Γ(X, X.toSpecΓ ⁻¹ᵁ ⊤) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(X, ⊤)) (Iso.inv (ΓSpecIso Γ(X, ⊤))) :
            (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u))
          r :
        (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u))) =
  X.basicOpen r
Tactic: rw [← basicOpen_eq_of_affine, Scheme.preimage_basicOpen, ← Scheme.Hom.appTop]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : Scheme
r : (↑Γ(X, ⊤) : Type u)
⊢ X.basicOpen (U := X.toSpecΓ ⁻¹ᵁ ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop X.toSpecΓ) :
          (a : (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u)) → (↑Γ(X, X.toSpecΓ ⁻¹ᵁ ⊤) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(X, ⊤)) (Iso.inv (ΓSpecIso Γ(X, ⊤))) :
              (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u))
            r :
          (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u))) =
    X.basicOpen r
have e_f : (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
        (Hom.appTop X.toSpecΓ) :
      (a : (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u)) → (↑Γ(X, X.toSpecΓ ⁻¹ᵁ ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X, ⊤)) (Iso.inv (ΓSpecIso Γ(X, ⊤))) :
          (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u))
        r :
      (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u)) =
  r
Tactic: congr
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : Scheme
r : (↑Γ(X, ⊤) : Type u)
⊢ (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Hom.appTop X.toSpecΓ) :
        (a : (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u)) → (↑Γ(X, X.toSpecΓ ⁻¹ᵁ ⊤) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(X, ⊤)) (Iso.inv (ΓSpecIso Γ(X, ⊤))) :
            (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u))
          r :
        (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u)) =
    r
have e_f : (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
        (X := Γ(Spec Γ(X, ⊤), ⊤)) (Iso.hom (ΓSpecIso Γ(X, ⊤))) :
      (a : (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u)) → (↑Γ(X, X.toSpecΓ ⁻¹ᵁ ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X, ⊤)) (Iso.inv (ΓSpecIso Γ(X, ⊤))) :
          (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u))
        r :
      (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u)) =
  r
Tactic: rw [Scheme.toSpecΓ_appTop]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : Scheme
B : CommRingCat
φ : B ⟶ Γ(X, ⊤)
⊢ (Scheme.ΓSpecIso B).inv ≫
      Scheme.Hom.appTop
        ((ΓSpec.adjunction.homEquiv X (op B) : (a : Scheme.Γ.rightOp.obj X ⟶ op B) → X ⟶ Scheme.Spec.obj (op B)) φ.op) =
    φ
have simp : (Scheme.ΓSpecIso B).inv ≫ Scheme.Hom.app (Spec.map φ.op.unop) ⊤ ≫ Scheme.Hom.app (ΓSpec.adjunction.unit.app X) ⊤ = φ
Tactic: simp only [Adjunction.homEquiv_apply, Scheme.Spec_map, Opens.map_top, Scheme.Hom.comp_app]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : Scheme
B : CommRingCat
φ : B ⟶ Γ(X, ⊤)
⊢ Scheme.Hom.appTop
      ((ΓSpec.adjunction.homEquiv X (op B) : (a : Scheme.Γ.rightOp.obj X ⟶ op B) → X ⟶ Scheme.Spec.obj (op B)) φ.op) =
    (Scheme.ΓSpecIso B).hom ≫ φ
have rw : (Scheme.ΓSpecIso B).inv ≫
    Scheme.Hom.appTop
      ((ΓSpec.adjunction.homEquiv X (op B) : (a : Scheme.Γ.rightOp.obj X ⟶ op B) → X ⟶ Scheme.Spec.obj (op B)) φ.op) =
  φ
Tactic: rw [← Iso.inv_comp_eq, ΓSpecIso_inv_ΓSpec_adjunction_homEquiv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : Scheme
B : CommRingCat
φ : B ⟶ Γ(X, ⊤)
rw :
  (Scheme.ΓSpecIso B).inv ≫
      Scheme.Hom.appTop
        ((ΓSpec.adjunction.homEquiv X (op B) : (a : Scheme.Γ.rightOp.obj X ⟶ op B) → X ⟶ Scheme.Spec.obj (op B)) φ.op) =
    φ
⊢ Scheme.Hom.appTop
      ((ΓSpec.adjunction.homEquiv X (op B) : (a : Scheme.Γ.rightOp.obj X ⟶ op B) → X ⟶ Scheme.Spec.obj (op B)) φ.op) =
    (Scheme.ΓSpecIso B).hom ≫ φ
have rw₁ : φ = φ
Tactic: rw [← Iso.inv_comp_eq, ΓSpecIso_inv_ΓSpec_adjunction_homEquiv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
R S : CommRingCat
φ ψ : R ⟶ S
⊢ map φ = map ψ ↔ φ = ψ
have rw : Scheme.Spec.map φ.op = Scheme.Spec.map ψ.op ↔ map φ = map ψ
Tactic: rw [iff_comm, ← Quiver.Hom.op_inj.eq_iff, ← Scheme.Spec.map_injective.eq_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
R S : CommRingCat
f : Spec S ⟶ Spec R
⊢ ∃ (a : R ⟶ S), map a = f
have h : map (preimage f) = f
Tactic: use Spec.preimage f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
Goal:
P : ObjectProperty Scheme
⊢ geometrically P =
    MorphismProperty.universally fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦ IsIntegral Y → Subsingleton.{u + 1} ↥Y → P X
have 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
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
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
have 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
Tactic: refine ⟨fun hf Z W snd q fst h _ _ ↦ ?_, fun hf aK y Z W fst snd h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
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
⊢ geometrically P f ↔
    MorphismProperty.universally (fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦ IsIntegral Y → Subsingleton.{u + 1} ↥Y → P X) f
have 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
Tactic: refine ⟨fun hf Z W snd q fst h _ _ ↦ ?_, fun hf aK y Z W fst snd h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
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
⊢ P Z
have h₁ : IsPullback snd (fst ≫ W.isoSpec.hom) f (W.isoSpec.inv ≫ q)
Tactic: apply hf (W.isoSpec.inv ≫ q) snd (fst ≫ W.isoSpec.hom)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
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
⊢ IsPullback snd (fst ≫ W.isoSpec.hom) f (W.isoSpec.inv ≫ q)
have h₁ : snd ≫ Iso.hom (Iso.refl X) = Iso.hom (Iso.refl Z) ≫ snd
Tactic: apply h.flip.of_iso (.refl _) (.refl _) W.isoSpec (.refl _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
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
⊢ IsPullback snd (fst ≫ W.isoSpec.hom) f (W.isoSpec.inv ≫ q)
have h₂ : fst ≫ W.isoSpec.hom = Iso.hom (Iso.refl Z) ≫ fst ≫ W.isoSpec.hom
Tactic: apply h.flip.of_iso (.refl _) (.refl _) W.isoSpec (.refl _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
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
⊢ IsPullback snd (fst ≫ W.isoSpec.hom) f (W.isoSpec.inv ≫ q)
have h₃ : f ≫ Iso.hom (Iso.refl Y) = Iso.hom (Iso.refl X) ≫ f
Tactic: apply h.flip.of_iso (.refl _) (.refl _) W.isoSpec (.refl _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
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
⊢ IsPullback snd (fst ≫ W.isoSpec.hom) f (W.isoSpec.inv ≫ q)
have h₄ : q ≫ Iso.hom (Iso.refl Y) = W.isoSpec.hom ≫ W.isoSpec.inv ≫ q
Tactic: apply h.flip.of_iso (.refl _) (.refl _) W.isoSpec (.refl _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
Goal:
P Q : ObjectProperty Scheme
⊢ geometrically (P ⊓ Q) = geometrically P ⊓ geometrically Q
have 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))
Tactic: simp only [geometrically_eq_universally, ← MorphismProperty.universally_inf]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
Goal:
P Q : ObjectProperty Scheme
⊢ 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))
have 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
Tactic: congr with X Y f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
Goal:
P : ObjectProperty Scheme
⊢ (geometrically P).IsStableUnderBaseChange
have 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)
Tactic: rw [geometrically_eq_universally]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
Goal:
P : ObjectProperty Scheme
inst : P.IsClosedUnderIsomorphisms
⊢ IsZariskiLocalAtTarget.{u} (geometrically P)
have rw : IsZariskiLocalAtTarget.{u}
  (MorphismProperty.universally fun (X Y : Scheme.{u}) (x : X ⟶ Y) ↦ IsIntegral Y → Subsingleton.{u + 1} ↥Y → P X)
Tactic: rw [geometrically_eq_universally]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
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)
have 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
Tactic: refine universally_isZariskiLocalAtTarget _ fun {X} Y f ι U hU H _ _ ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
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
⊢ P X
have obtain : ∀ (y : ↥Y), P X
Tactic: obtain ⟨y⟩ := (inferInstance : Nonempty Y)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
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
⊢ P X
have obtain : ∀ (i : ι) (hy : y ∈ U i), P X
Tactic: obtain ⟨i, hy⟩ := hU.exists_mem y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
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
⊢ P X
have have : ∀ (heq : U i = ⊤), P X
Tactic: have heq : U i = ⊤ := eq_top_iff.mpr fun z _ ↦ by rwa [Subsingleton.elim z y]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
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)
have 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
Tactic: refine ⟨fun h K _ _ ↦ pullback_of_geometrically h _ _, fun H K _ _ Y fst snd h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
Goal:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
⊢ geometrically P f ↔ ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)
have refine : ∀ (H : ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)), geometrically P f
Tactic: refine ⟨fun hf y ↦ (geometrically P).pullback_snd _ _ hf, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
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
⊢ P Z
have 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
Tactic: obtain ⟨⟨y, φ⟩, rfl⟩ := (Scheme.SpecToEquivOfField _ _).symm.surjective y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
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 φ) ⋯
⊢ P Z
have apply : IsPullback p snd (Scheme.Hom.fiberToSpecResidueField f y) (Spec.map φ)
Tactic: apply H y (Spec.map φ) p snd
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
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 φ)
have refine_1 : IsPullback (p ≫ pullback.fst f (Y.fromSpecResidueField y)) snd f (Spec.map φ ≫ Y.fromSpecResidueField y)
Tactic: refine .flip (.of_bot (.flip ?_) ?_ (IsPullback.of_hasPullback f (Y.fromSpecResidueField y)).flip)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
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)
⊢ IsPullback p snd (Scheme.Hom.fiberToSpecResidueField f y) (Spec.map φ)
have refine_2 : snd ≫ Spec.map φ = p ≫ Scheme.Hom.fiberToSpecResidueField f y
Tactic: refine .flip (.of_bot (.flip ?_) ?_ (IsPullback.of_hasPullback f (Y.fromSpecResidueField y)).flip)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
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 ≫ pullback.fst f (Y.fromSpecResidueField y)) snd f (Spec.map φ ≫ Y.fromSpecResidueField y)
have h₁ : p ≫ pullback.fst f (Y.fromSpecResidueField y) = fst
Tactic: convert! h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (hypothesis)
Goal:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
inst : IsIntegral Y
inst_1 : Subsingleton.{u + 1} ↥Y
hf : geometrically P f
⊢ P X
have hf₁ : 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
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
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
have 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
Tactic: refine ⟨fun hs K _ _ Z fst snd h ↦ hs _ _ _ h, fun H K _ y Z fst snd h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
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
⊢ P Z
have obtain : ∀ (φ : of R ⟶ of K) (h : IsPullback fst snd f (Spec.map φ)), P Z
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
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))))
have 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
Tactic: refine ⟨fun hf K _ _ ↦ pullback_of_geometrically hf _ _, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
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))))
⊢ geometrically P f
have rw : ∀ (K : Type u) [inst_2 : Field K] (y : Spec (of K) ⟶ Spec (of R)), P (pullback f y)
Tactic: rw [geometrically_iff_of_isClosedUnderIsomorphisms]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Geometrically.Basic (goal)
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)
⊢ P (pullback f y)
have obtain : ∀ (φ : of R ⟶ of K), P (pullback f (Spec.map φ))
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective y
Cleared hypotheses: y