mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hP : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this : (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q).IsLocal :=
  HasAffineProperty.isLocal_affineProperty P
X Y S : Scheme
inst✝ : IsAffine S
⊢ ∀ [inst : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) g →
      sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) (pullback.fst f g)

Tactic:
_

Goal state after:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
hP : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this : (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q).IsLocal :=
  HasAffineProperty.isLocal_affineProperty P
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
⊢ ∀ (f : X ⟶ S) (g : Y ⟶ S),
    sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) g →
      sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) (pullback.fst f g)
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: P : (X : Scheme) → ↥X → Prop
h₁ : ∀ (R : CommRingCat) (x : ↥(Spec R)), P (Spec R) x
h₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (x : ↥X), P X x → P Y (f x)
X : Scheme
x : ↥X
⊢ P X x

Tactic:
obtain ⟨y, e⟩ := X.affineCover.covers x

Goal state after:
P : (X : Scheme) → ↥X → Prop
h₁ : ∀ (R : CommRingCat) (x : ↥(Spec R)), P (Spec R) x
h₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (x : ↥X), P X x → P Y (f x)
X : Scheme
x : ↥X
y : ↥(X.affineCover.X (Scheme.Cover.idx X.affineCover x))
e : (X.affineCover.f (Scheme.Cover.idx X.affineCover x)) y = x
⊢ P X x
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q
this : P.Respects IsOpenImmersion
hf : P f
x : ↥X
⊢ ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Tactic:
obtain ⟨U, hU, hfx, _⟩ := Opens.isBasis_iff_nbhd.mp Y.isBasis_affineOpens
      (Opens.mem_top <| f x)

Goal state after:
case refine_1
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q
this : P.Respects IsOpenImmersion
hf : P f
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : f x ∈ U
right✝ : U ≤ ⊤
⊢ ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
x : ↥X
hxU : x ∈ ↑U
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU)) (I.ideal U)

Tactic:
obtain ⟨f, g, hfg, hxf⟩ := exists_basicOpen_le_affine_inter U.2 V.2 x ⟨hxU, h hxU⟩

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
x : ↥X
hxU : x ∈ ↑U
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU)) (I.ideal U)
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↥↑U
x : ↑Γ(X, V)
⊢ (↑(X.basicOpen x)).Nonempty → (↑(U ⊓ X.basicOpen x)).Nonempty

Tactic:
apply nonempty_preirreducible_inter U.isOpen (RingedSpace.basicOpen _ _).isOpen

Goal state after:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↥↑U
x : ↑Γ(X, V)
⊢ (↑U).Nonempty
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case e'
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
R S : Type u
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), Q f ↔ Locally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
_

Goal state after:
case e'
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
R S : Type u
inst✝ : CommRing R
⊢ ∀ [inst : CommRing S] (f : R →+* S), Q f ↔ Locally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case e'
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
R S : Type u
inst✝ : CommRing R
⊢ ∀ [inst : CommRing S] (f : R →+* S), Q f ↔ Locally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
_

Goal state after:
case e'
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (f : R →+* S), Q f ↔ Locally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q' (Localization.localRingHom (Ideal.comap f J) J f ⋯)
hf : P f
x : ↥X
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y},
    P f → ∀ (x : ↥X), IsAffine X ∧ IsAffine Y → Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
h : ¬(IsAffine X ∧ IsAffine Y)
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Tactic:
obtain ⟨U, hU, hfx, _⟩ := Opens.isBasis_iff_nbhd.mp Y.isBasis_affineOpens
      (Opens.mem_top <| f x)

Goal state after:
case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q' (Localization.localRingHom (Ideal.comap f J) J f ⋯)
hf : P f
x : ↥X
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y},
    P f → ∀ (x : ↥X), IsAffine X ∧ IsAffine Y → Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
h : ¬(IsAffine X ∧ IsAffine Y)
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : f x ∈ U
right✝ : U ≤ ⊤
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: case mpr
X : Scheme
x y : ↥X
hy : y ⤳ x
⊢ y ∈ Set.range ⇑(X.fromSpecStalk x)

Tactic:
have := fromSpecStalk_closedPoint (x := y)

Goal state after:
case mpr
X : Scheme
x y : ↥X
hy : y ⤳ x
this : (X.fromSpecStalk y) (closedPoint ↑(X.presheaf.stalk y)) = y
⊢ y ∈ Set.range ⇑(X.fromSpecStalk x)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
⊢ ker f = ⊥

Tactic:
ext U
  simp [map_eq_zero_iff _ (ConcreteCategory.bijective_of_isIso (f.app U)).1]

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case h₀
X : Scheme
I : X.IdealSheafData
i : ↑X.affineOpens
⊢ I.glueDataT i i ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) =
    𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2) ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)

Tactic:
← cancel_mono (glueDataObjι _ _)

Goal state after:
case h₀
X : Scheme
I : X.IdealSheafData
i : ↑X.affineOpens
⊢ (I.glueDataT i i ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫ I.glueDataObjι i =
    (𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2) ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫ I.glueDataObjι i
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case h₀
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ (pullback.lift (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 ⋯)
          (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 ⋯) ⋯ ≫
        pullback.snd (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE ⋯))
          (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯))) ≫
      pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯) =
    (pullback.fst (pullback.fst (I.glueDataObjι (i, j).1) (X.homOfLE ⋯))
          (pullback.fst (I.glueDataObjι (i, k).1) (X.homOfLE ⋯)) ≫
        I.glueDataT i j) ≫
      pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)

Tactic:
← cancel_mono (glueDataObjι _ _)

Goal state after:
case h₀
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ ((pullback.lift (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 ⋯)
            (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 ⋯) ⋯ ≫
          pullback.snd (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE ⋯))
            (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯))) ≫
        pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)) ≫
      I.glueDataObjι (j, i).1 =
    ((pullback.fst (pullback.fst (I.glueDataObjι (i, j).1) (X.homOfLE ⋯))
            (pullback.fst (I.glueDataObjι (i, k).1) (X.homOfLE ⋯)) ≫
          I.glueDataT i j) ≫
        pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)) ≫
      I.glueDataObjι (j, i).1
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this : QuasiSeparatedSpace ↥X
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
⊢ IsCompact ↑⊤

Tactic:
← iSup_basicOpen_of_span_eq_top _ _ e

Goal state after:
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this : QuasiSeparatedSpace ↥X
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
⊢ IsCompact ↑(⨆ i ∈ ↑s', X.basicOpen i)
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case to_basicOpen
X✝ Y✝ Z : Scheme
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
⊢ ∀ [IsAffine Y] (f : X ⟶ Y) (r : ↑Γ(Y, ⊤)), IsAffine X → IsAffine ↑(f ⁻¹ᵁ Y.basicOpen r)

Tactic:
_

Goal state after:
case to_basicOpen
X✝ Y✝ Z : Scheme
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
inst✝ : IsAffine Y
⊢ ∀ (f : X ⟶ Y) (r : ↑Γ(Y, ⊤)), IsAffine X → IsAffine ↑(f ⁻¹ᵁ Y.basicOpen r)
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case of_basicOpenCover
X✝ Y✝ Z : Scheme
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
⊢ ∀ [IsAffine Y] (f : X ⟶ Y) (s : Finset ↑Γ(Y, ⊤)),
    Ideal.span ↑s = ⊤ → (∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r)) → IsAffine X

Tactic:
_

Goal state after:
case of_basicOpenCover
X✝ Y✝ Z : Scheme
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
inst✝ : IsAffine Y
⊢ ∀ (f : X ⟶ Y) (s : Finset ↑Γ(Y, ⊤)), Ideal.span ↑s = ⊤ → (∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r)) → IsAffine X
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case e_a
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
this✝ : IsIso (X.homOfLE ⋯)
H : inv (X.homOfLE ⋯) = X.homOfLE ⋯
this :
  inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
      I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueData.ι V =
    I.glueData.ι U
⊢ I.glueDataObjMap h =
    (inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫ I.glueDataT U V) ≫
      pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯)

Tactic:
← cancel_mono (glueDataObjι _ _)

Goal state after:
case e_a
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
this✝ : IsIso (X.homOfLE ⋯)
H : inv (X.homOfLE ⋯) = X.homOfLE ⋯
this :
  inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
      I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueData.ι V =
    I.glueData.ι U
⊢ I.glueDataObjMap h ≫ I.glueDataObjι V =
    ((inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫ I.glueDataT U V) ≫
        pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯)) ≫
      I.glueDataObjι V
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQb : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this : (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty.RespectsIso
X Y S : Scheme
⊢ ∀ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) g →
      affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) (Limits.pullback.fst f g)

Tactic:
_

Goal state after:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQb : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this : (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty.RespectsIso
X Y S : Scheme
inst✝ : IsAffine S
⊢ ∀ [inst : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) g →
      affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) (Limits.pullback.fst f g)
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQb : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this : (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty.RespectsIso
X Y S : Scheme
inst✝ : IsAffine S
⊢ ∀ [inst : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) g →
      affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) (Limits.pullback.fst f g)

Tactic:
_

Goal state after:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQb : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this : (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty.RespectsIso
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
⊢ ∀ (f : X ⟶ S) (g : Y ⟶ S),
    affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) g →
      affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) (Limits.pullback.fst f g)
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: Q✝ Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
hf : affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
⊢ IsAffineHom f

Tactic:
HasAffineProperty.iff_of_isAffine (P := @IsAffineHom)

Goal state after:
Q✝ Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
hf : affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
⊢ IsAffine X
Module: Mathlib.RingTheory.RingHom.FiniteType

Goal state before:
pp: ⊢ RespectsIso @FiniteType

Tactic:
refine finiteType_stableUnderComposition.respectsIso (fun {R S} _ _ e ↦ ?_)

Goal state after:
R S : Type u_5
x✝¹ : CommRing R
x✝ : CommRing S
e : R ≃+* S
⊢ e.toRingHom.FiniteType
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: case refine_1
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
Q' : ObjectProperty CommRingCat := fun S ↦ ∃ R ∈ Set.range fun U ↦ Γ(X, U), ∃ f, (CommRingCat.Hom.hom f).FiniteType
this : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q'
⊢ ∀ S ∈ Set.range (unop ∘ F.obj), ∃ s, Ideal.span s = ⊤ ∧ ∀ f ∈ s, Q'.isoClosure (CommRingCat.of (Localization.Away f))

Tactic:
rintro _ ⟨S, rfl⟩

Goal state after:
case refine_1
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
Q' : ObjectProperty CommRingCat := fun S ↦ ∃ R ∈ Set.range fun U ↦ Γ(X, U), ∃ f, (CommRingCat.Hom.hom f).FiniteType
this : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q'
S : P.CostructuredArrow ⊤ Scheme.Spec X
⊢ ∃ s, Ideal.span s = ⊤ ∧ ∀ f ∈ s, Q'.isoClosure (CommRingCat.of (Localization.Away f))
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
⊢ IsClosedImmersion (Scheme.Hom.toImage f ≫ Scheme.Hom.imageι f)

Tactic:
Scheme.Hom.toImage_imageι

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
⊢ IsClosedImmersion f
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ ⊤.comap f = ⊤

Tactic:
by
  rw [comap, Hom.ker_eq_top_iff_isEmpty]
  exact Function.isEmpty (pullback.snd f _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
U : (↑(coborderRange f)).Opens
| TopologicalSpace.Opens.map f.base

Tactic:
rw [← f.liftCoborder_ι]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
U : (↑(coborderRange f)).Opens
| TopologicalSpace.Opens.map (liftCoborder f ≫ (coborderRange f).ι).base
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
H : IsPullback f' g' g f
hg : IsImmersion g
Z : Scheme := pullback f (Scheme.Hom.coborderRange g).ι
e : Y' ⟶ Z := pullback.lift g' (f' ≫ Scheme.Hom.liftCoborder g) ⋯
⊢ IsImmersion g'

Tactic:
have : IsClosedImmersion e := by
      have := (IsPullback.paste_horiz_iff (.of_hasPullback f g.coborderRange.ι)
        (show e ≫ Limits.pullback.snd _ _ = _ from Limits.pullback.lift_snd _ _ _)).mp ?_
      · exact MorphismProperty.of_isPullback this.flip inferInstance
      · simpa [e] using H.flip

Goal state after:
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
H : IsPullback f' g' g f
hg : IsImmersion g
Z : Scheme := pullback f (Scheme.Hom.coborderRange g).ι
e : Y' ⟶ Z := pullback.lift g' (f' ≫ Scheme.Hom.liftCoborder g) ⋯
this : IsClosedImmersion e
⊢ IsImmersion g'
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y Z : Scheme
f✝ f : X ⟶ Y
inst✝ : IsImmersion f
⊢ LocallyOfFiniteType f

Tactic:
rw [← f.liftCoborder_ι]

Goal state after:
X Y Z : Scheme
f✝ f : X ⟶ Y
inst✝ : IsImmersion f
⊢ LocallyOfFiniteType (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsImmersion f
inst✝ : QuasiCompact f
⊢ (Hom.ker (Hom.imageι f)).comap (Hom.coborderRange f).ι = Hom.ker (Hom.liftCoborder f)

Tactic:
Hom.imageι,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsImmersion f
inst✝ : QuasiCompact f
⊢ (Hom.ker (Hom.ker f).subschemeι).comap (Hom.coborderRange f).ι = Hom.ker (Hom.liftCoborder f)
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X✝ Y✝ Z : Scheme
this :
  AffineTargetMorphismProperty.IsLocal fun X x f [IsAffine x] ↦
    IsAffine X ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
X Y S : Scheme
⊢ ∀ [IsAffine S] [IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    IsAffine Y ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g)) →
      IsAffine (Limits.pullback f g) ∧
        Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop (Limits.pullback.fst f g)))

Tactic:
_

Goal state after:
X✝ Y✝ Z : Scheme
this :
  AffineTargetMorphismProperty.IsLocal fun X x f [IsAffine x] ↦
    IsAffine X ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
X Y S : Scheme
inst✝ : IsAffine S
⊢ ∀ [IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    IsAffine Y ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g)) →
      IsAffine (Limits.pullback f g) ∧
        Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop (Limits.pullback.fst f g)))
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X✝ Y✝ Z : Scheme
this :
  AffineTargetMorphismProperty.IsLocal fun X x f [IsAffine x] ↦
    IsAffine X ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
X Y S : Scheme
inst✝ : IsAffine S
⊢ ∀ [IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    IsAffine Y ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g)) →
      IsAffine (Limits.pullback f g) ∧
        Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop (Limits.pullback.fst f g)))

Tactic:
_

Goal state after:
X✝ Y✝ Z : Scheme
this :
  AffineTargetMorphismProperty.IsLocal fun X x f [IsAffine x] ↦
    IsAffine X ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
⊢ ∀ (f : X ⟶ S) (g : Y ⟶ S),
    IsAffine Y ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g)) →
      IsAffine (Limits.pullback f g) ∧
        Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop (Limits.pullback.fst f g)))
Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley

Goal state before:
pp: case refine_1
R✝ : Type u_1
S : Type u_2
inst✝¹ : CommRing R✝
inst✝ : CommRing S
f : R✝ →+* S
hf : f.FinitePresentation
s : Set (PrimeSpectrum S)
hs : IsConstructible s
R : Type u_1
⊢ ∀ [inst : CommRing R] (S : Type u_2) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f →
      (RingHom.ker f).FG → ∀ (s : Set (PrimeSpectrum S)), IsConstructible s → IsConstructible (comap f '' s)

Tactic:
_

Goal state after:
case refine_1
R✝ : Type u_1
S : Type u_2
inst✝² : CommRing R✝
inst✝¹ : CommRing S
f : R✝ →+* S
hf : f.FinitePresentation
s : Set (PrimeSpectrum S)
hs : IsConstructible s
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (S : Type u_2) [inst : CommRing S] (f : R →+* S),
    Surjective ⇑f →
      (RingHom.ker f).FG → ∀ (s : Set (PrimeSpectrum S)), IsConstructible s → IsConstructible (comap f '' s)