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
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
e' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), Q f ↔ Q' f
heq : Q = Q'
⊢ HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q

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
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
e' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), Q f ↔ Q' f
heq : Q = Q'
⊢ HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
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
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
U : ↑Y.affineOpens
V : ↑X.affineOpens
e : ↑V ≤ f ⁻¹ᵁ ↑U
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

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
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
U : ↑Y.affineOpens
V : ↑X.affineOpens
e : ↑V ≤ f ⁻¹ᵁ ↑U
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
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
X Y : Scheme
f : X ⟶ Y
H : P f
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (f ⁻¹ᵁ ⊤) ⋯))

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
X Y : Scheme
f : X ⟶ Y
H : P f
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (f ⁻¹ᵁ ⊤) ⋯))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X : Scheme
s : Set ↑X.affineOpens
hs : s.Finite
n : ↑s → ℕ
this✝ : Finite ↑s
val✝ : Fintype ↑s
hU : IsCompact (⨆ i, ↑↑i).carrier
x f : ↑Γ(X, ⨆ i, ↑↑i)
H : (x |_ X.basicOpen f) ⋯ = 0
h₁ : ∀ (i : ↑s), ↑↑i ≤ ⨆ i, ↑↑i
hn :
  ∀ (i : ↑s),
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n i *
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x =
      0
this : ∀ (i : ↑s), (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) (f ^ Finset.univ.sup n * x) = 0
i : ↑s
⊢ (ConcreteCategory.hom (X.sheaf.obj.map (Opens.leSupr (fun i ↦ ↑↑i) i).op)) (f ^ Finset.univ.sup n * x) = 0

Tactic:
]

Goal state after:
X : Scheme
s : Set ↑X.affineOpens
hs : s.Finite
n : ↑s → ℕ
this✝ : Finite ↑s
val✝ : Fintype ↑s
hU : IsCompact (⨆ i, ↑↑i).carrier
x f : ↑Γ(X, ⨆ i, ↑↑i)
H : (x |_ X.basicOpen f) ⋯ = 0
h₁ : ∀ (i : ↑s), ↑↑i ≤ ⨆ i, ↑↑i
hn :
  ∀ (i : ↑s),
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n i *
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x =
      0
this : ∀ (i : ↑s), (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) (f ^ Finset.univ.sup n * x) = 0
i : ↑s
⊢ (ConcreteCategory.hom (X.sheaf.obj.map (Opens.leSupr (fun i ↦ ↑↑i) i).op)) (f ^ Finset.univ.sup n * x) = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case h
X : Scheme
S : ↑X.affineOpens
U₁ U₂ : X.Opens
n₁ n₂ : ℕ
y₁ : ↑Γ(X, U₁)
y₂ : ↑Γ(X, U₂)
f : ↑Γ(X, U₁ ⊔ U₂)
x : ↑Γ(X, X.basicOpen f)
h₁ : ↑S ≤ U₁
h₂ : ↑S ≤ U₂
e₁ :
  (y₁ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ =
    ((f |_ U₁) ⋯ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ ^ n₁ * (x |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯
e₂ :
  (y₂ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ =
    ((f |_ U₂) ⋯ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ ^ n₂ * (x |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯
n m : ℕ
hm : n ≤ m
e :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n *
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n₂ *
        (ConcreteCategory.hom (X.presheaf.map (homOfLE h₁).op)) y₁) =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n *
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n₁ *
        (ConcreteCategory.hom (X.presheaf.map (homOfLE h₂).op)) y₂)
⊢ (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (m - n) *
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n *
        ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n₁ *
          (ConcreteCategory.hom (X.presheaf.map (homOfLE h₂).op)) y₂)) =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (m - n) *
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n *
        ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n₁ *
          (ConcreteCategory.hom (X.presheaf.map (homOfLE h₂).op)) y₂))

Tactic:
]

Goal state after:
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
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsOpenImmersion f
H :
  ∀ (U : ↑Z.affineOpens) (V : ↑Y.affineOpens) (e : ↑V ≤ g ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE g (↑U) (↑V) e))
⊢ ∀ (U : ↑Z.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (f ≫ g) ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE (f ≫ g) (↑U) (↑V) e))

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
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsOpenImmersion f
H :
  ∀ (U : ↑Z.affineOpens) (V : ↑Y.affineOpens) (e : ↑V ≤ g ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE g (↑U) (↑V) e))
⊢ ∀ (U : ↑Z.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (f ≫ g) ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE (f ≫ g) (↑U) (↑V) e))
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
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsOpenImmersion f
H :
  ∀ (U : ↑Z.affineOpens) (V : ↑Y.affineOpens) (e : ↑V ≤ g ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE g (↑U) (↑V) e))
U : ↑Z.affineOpens
V : ↑X.affineOpens
e : ↑V ≤ (f ≫ g) ⁻¹ᵁ ↑U
this : IsIso (Scheme.Hom.appLE f (f ''ᵁ ↑V) ↑V ⋯)
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE g (↑U) (f ''ᵁ ↑V) ⋯))

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
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsOpenImmersion f
H :
  ∀ (U : ↑Z.affineOpens) (V : ↑Y.affineOpens) (e : ↑V ≤ g ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE g (↑U) (↑V) e))
U : ↑Z.affineOpens
V : ↑X.affineOpens
e : ↑V ≤ (f ≫ g) ⁻¹ᵁ ↑U
this : IsIso (Scheme.Hom.appLE f (f ''ᵁ ↑V) ↑V ⋯)
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE g (↑U) (f ''ᵁ ↑V) ⋯))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case h
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
this : Finite ↑s
val✝ : Fintype ↑s
i : ↑s
hn : (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) (f ^ Finset.univ.sup n * x) = 0
⊢ (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) (f ^ Finset.univ.sup n * x) = 0

pp: case h
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
this : Finite ↑s
val✝ : Fintype ↑s
i : ↑s
hn : (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) (f ^ (Finset.univ.sup n - n i + n i) * x) = 0
⊢ n i ≤ Finset.univ.sup n

Tactic:
]

Goal state after:
case h
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
this : Finite ↑s
val✝ : Fintype ↑s
i : ↑s
hn : (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) (f ^ Finset.univ.sup n * x) = 0
⊢ (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) (f ^ Finset.univ.sup n * x) = 0

case h
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
this : Finite ↑s
val✝ : Fintype ↑s
i : ↑s
hn : (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) (f ^ (Finset.univ.sup n - n i + n i) * x) = 0
⊢ n i ≤ Finset.univ.sup n
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
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))) ↔
    ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Tactic:
]

Goal state after:
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
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
H : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
⊢ sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f

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
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
H : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
⊢ sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
⊢ ⊥ ≤ ⊥

Tactic:
]

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

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
e : X.basicOpen f ≤ ⊥
⊢ ((1 |_ ⊥) ⋯ |_ X.basicOpen f) e = 0

Tactic:
]

Goal state after:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
e : X.basicOpen f ≤ ⊥
⊢ ((1 |_ ⊥) ⋯ |_ X.basicOpen f) e = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
e : X.basicOpen f ≤ ⊥
⊢ (0 |_ X.basicOpen f) e = 0

Tactic:
]

Goal state after:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
e : X.basicOpen f ≤ ⊥
⊢ (0 |_ X.basicOpen f) e = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
e : X.basicOpen f ≤ ⊥
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case openCover
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
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
H✝ : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
U : ↑X.affineOpens
s : Finset ↑Γ(X, ↑U)
hs : Ideal.span ↑s = ⊤
H : ∀ (f_1 : ↥s), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(X.affineBasicOpen ↑f_1) ⋯))
r : ↑↑s
⊢ ∃ T x x_1,
    ∃ (_ : IsLocalization.Away (↑r) T),
      Q ((algebraMap (↑Γ(X, ↑U)) T).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)))

Tactic:
refine ⟨_, _, _, IsAffineOpen.isLocalization_basicOpen U.2 r, ?_⟩

Goal state after:
case openCover
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
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
H✝ : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
U : ↑X.affineOpens
s : Finset ↑Γ(X, ↑U)
hs : Ideal.span ↑s = ⊤
H : ∀ (f_1 : ↥s), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(X.affineBasicOpen ↑f_1) ⋯))
r : ↑↑s
⊢ Q ((algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen ↑r)).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
h : (1 |_ X.basicOpen f) ⋯ = 0
n : ℕ
hn : f ^ n = 0
⊢ IsNilpotent f

Tactic:
]

Goal state after:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
h : (1 |_ X.basicOpen f) ⋯ = 0
n : ℕ
hn : f ^ n = 0
⊢ IsNilpotent f
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case h
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU'✝ : IsQuasiSeparated ⊥.carrier
f : ↑Γ(X, ⊥)
x : ↑Γ(X, X.basicOpen f)
⊢ X.basicOpen f ≤ ⊥

Tactic:
]

Goal state after:
case h
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU'✝ : IsQuasiSeparated ⊥.carrier
f : ↑Γ(X, ⊥)
x : ↑Γ(X, X.basicOpen f)
⊢ X.basicOpen f ≤ ⊥
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case openCover
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
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
H✝ : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
U : ↑X.affineOpens
s : Finset ↑Γ(X, ↑U)
hs : Ideal.span ↑s = ⊤
H : ∀ (f_1 : ↥s), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(X.affineBasicOpen ↑f_1) ⋯))
r : ↑↑s
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (X.basicOpen ↑r) ⋯))

Tactic:
]

Goal state after:
case openCover
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
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
H✝ : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
U : ↑X.affineOpens
s : Finset ↑Γ(X, ↑U)
hs : Ideal.span ↑s = ⊤
H : ∀ (f_1 : ↥s), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(X.affineBasicOpen ↑f_1) ⋯))
r : ↑↑s
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (X.basicOpen ↑r) ⋯))
Module: Mathlib.RingTheory.LocalProperties.Reduced

Goal state before:
pp: case succ
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : x * (algebraMap R S) ↑m = (algebraMap R S) y
hx' : (algebraMap R S) 0 = (algebraMap R S) (y ^ n.succ)
⊢ x = 0

Tactic:
]

Goal state after:
case succ
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : x * (algebraMap R S) ↑m = (algebraMap R S) y
hx' : (algebraMap R S) 0 = (algebraMap R S) (y ^ n.succ)
⊢ x = 0
Module: Mathlib.RingTheory.LocalProperties.Reduced

Goal state before:
pp: case succ
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : x * (algebraMap R S) ↑m = (algebraMap R S) y
hx' : (algebraMap R S) 0 = (algebraMap R S) (y ^ n.succ)
m' : ↥M
hm' : 0 = (y * ↑m') ^ n.succ
⊢ x = 0

Tactic:
]

Goal state after:
case succ
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : x * (algebraMap R S) ↑m = (algebraMap R S) y
hx' : (algebraMap R S) 0 = (algebraMap R S) (y ^ n.succ)
m' : ↥M
hm' : 0 = (y * ↑m') ^ n.succ
⊢ x = 0
Module: Mathlib.RingTheory.LocalProperties.Reduced

Goal state before:
pp: case succ
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : x * (algebraMap R S) ↑m = (algebraMap R S) y
hx' : (algebraMap R S) 0 = (algebraMap R S) (y ^ n.succ)
m' : ↥M
hm' : y * ↑m' = 0
⊢ ∃ m, ↑m * y = 0

Tactic:
]

Goal state after:
case succ
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : x * (algebraMap R S) ↑m = (algebraMap R S) y
hx' : (algebraMap R S) 0 = (algebraMap R S) (y ^ n.succ)
m' : ↥M
hm' : y * ↑m' = 0
⊢ ∃ m, ↑m * y = 0
Module: Mathlib.RingTheory.LocalProperties.Reduced

Goal state before:
pp: R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : x * (algebraMap R S) ↑m = (algebraMap R S) y
hx' : (algebraMap R S) 0 = (algebraMap R S) (y ^ n.succ)
m' : ↥M
hm' : y * ↑m' = 0
⊢ y * ↑m' = y * ↑m'

Tactic:
]

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

Goal state before:
pp: case hU
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
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
i : 𝒰.I₀
H : Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ((↑(S i)).ι ''ᵁ ⊤) ⋯))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(S i) ⋯))

Tactic:
]

Goal state after:
case hU
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
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
i : 𝒰.I₀
H : Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ((↑(S i)).ι ''ᵁ ⊤) ⋯))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(S i) ⋯))
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ I = ⊤ ∨ I.height ≠ ⊤ ↔ I = ⊤ ∨ I.height ≠ ⊤

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : I.FiniteHeight
inst✝ : I.IsPrime
⊢ I.height ≠ ⊤

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : I.FiniteHeight
inst✝ : I.IsPrime
⊢ I.height ≠ ⊤
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : I.FiniteHeight
inst✝ : I.IsPrime
⊢ I.height < ⊤

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : I.FiniteHeight
inst✝ : I.IsPrime
⊢ I.height < ⊤
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
p : Ideal R
inst✝¹ : p.IsPrime
inst✝ : p.FiniteHeight
n : ℕ
hn : ↑n = Order.height { asIdeal := p, isPrime := inst✝¹ }
⊢ ∃ l, RelSeries.last l = { asIdeal := p, isPrime := ⋯ } ∧ ↑l.length = Order.height { asIdeal := p, isPrime := inst✝¹ }

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
p : Ideal R
inst✝¹ : p.IsPrime
inst✝ : p.FiniteHeight
n : ℕ
hn : ↑n = Order.height { asIdeal := p, isPrime := inst✝¹ }
⊢ ∃ l, RelSeries.last l = { asIdeal := p, isPrime := ⋯ } ∧ ↑l.length = Order.height { asIdeal := p, isPrime := inst✝¹ }
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
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
⊢ (∀ (i : (Scheme.coverOfIsIso (𝟙 X)).I₀),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appTop ((Scheme.coverOfIsIso (𝟙 X)).f i ≫ f)))) ↔
    Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))

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
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
⊢ (∀ (i : (Scheme.coverOfIsIso (𝟙 X)).I₀),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appTop ((Scheme.coverOfIsIso (𝟙 X)).f i ≫ f)))) ↔
    Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
h : I < J
inst✝ : I.FiniteHeight
hJ : J = ⊤
⊢ I.height < ⊤

Tactic:
]

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
h : I < J
inst✝ : I.FiniteHeight
hJ : J = ⊤
⊢ I.height < ⊤
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
R S : CommRingCat
φ : R ⟶ S
H : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ Q (CommRingCat.Hom.hom φ) ↔ Q (CommRingCat.Hom.hom φ)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
h : I < J
inst✝ : I.FiniteHeight
hJ : ¬J = ⊤
⊢ I.height + 1 ≤ ⨅ J_1 ∈ J.minimalPrimes, J_1.height

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
h : I < J
inst✝ : I.FiniteHeight
hJ : ¬J = ⊤
⊢ I.height + 1 ≤ ⨅ J_1 ∈ J.minimalPrimes, J_1.height
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ ↑(Order.height { asIdeal := I, isPrime := inst✝ }) ≤ ringKrullDim R

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ ↑(Order.height { asIdeal := I, isPrime := inst✝ }) ≤ ringKrullDim R
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≠ ⊤
P : Ideal R
hP : P ∈ I.minimalPrimes
⊢ ↑(⨅ J ∈ I.minimalPrimes, J.height) ≤ ringKrullDim R

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≠ ⊤
P : Ideal R
hP : P ∈ I.minimalPrimes
⊢ ↑(⨅ J ∈ I.minimalPrimes, J.height) ≤ ringKrullDim R
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : FiniteRingKrullDim R
l : LTSeries (PrimeSpectrum R) := LTSeries.longestOf (PrimeSpectrum R)
m : Ideal R
hm : m.IsMaximal
hle : (RelSeries.last l).asIdeal ≤ m
⊢ ringKrullDim R ≤ ↑(RelSeries.last l).asIdeal.primeHeight

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : FiniteRingKrullDim R
l : LTSeries (PrimeSpectrum R) := LTSeries.longestOf (PrimeSpectrum R)
m : Ideal R
hm : m.IsMaximal
hle : (RelSeries.last l).asIdeal ≤ m
⊢ ringKrullDim R ≤ ↑(RelSeries.last l).asIdeal.primeHeight