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

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

pp: case of_basicOpenCover
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) (s : Finset ↑Γ(Y, ⊤)),
    Ideal.span ↑s = ⊤ → (∀ (r : ↥s), CompactSpace ↥↑(f ⁻¹ᵁ Y.basicOpen ↑r)) → CompactSpace ↥X

Tactic:
·

Goal state after:
case to_basicOpen
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) (r : ↑Γ(Y, ⊤)), CompactSpace ↥X → CompactSpace ↥↑(f ⁻¹ᵁ Y.basicOpen r)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

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

Tactic:
·

Goal state after:
case of_basicOpenCover
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) (s : Finset ↑Γ(Y, ⊤)),
    Ideal.span ↑s = ⊤ → (∀ (r : ↥s), CompactSpace ↥↑(f ⁻¹ᵁ Y.basicOpen ↑r)) → CompactSpace ↥X
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case mpr
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ (∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)) →
    ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
      [IsOpenImmersion f₂],
      (fun X x x_1 x_2 ↦ CompactSpace ↥X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯

Tactic:
·

Goal state after:
case mpr
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ (∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)) →
    ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
      [IsOpenImmersion f₂],
      (fun X x x_1 x_2 ↦ CompactSpace ↥X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
H : SpecializingMap ⇑f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], SpecializingMap ⇑f → (∃ R, Y = Spec R) → IsClosedMap ⇑f
hY : ¬∃ R, Y = Spec R
⊢ IsClosedMap ⇑f

pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
H : SpecializingMap ⇑f
hY : ∃ R, Y = Spec R
⊢ IsClosedMap ⇑f

Tactic:
·

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
H : SpecializingMap ⇑f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], SpecializingMap ⇑f → (∃ R, Y = Spec R) → IsClosedMap ⇑f
hY : ¬∃ R, Y = Spec R
⊢ IsClosedMap ⇑f
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case refine_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover Y :=
  (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind fun x ↦
    ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover
this : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
i : Z.affineCover.I₀
j : (pullback g (Z.affineCover.f i)).affineCover.I₀
⊢ (Precoverage.ZeroHypercover.pullback₁ f
          ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind fun x ↦
            ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover)).X
      ⟨i, j⟩ ⟶
    pullback (f ≫ g) (Z.affineCover.f i)

pp: case refine_2
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover Y :=
  (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind fun x ↦
    ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover
this : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
i : Z.affineCover.I₀
j : (pullback g (Z.affineCover.f i)).affineCover.I₀
⊢ QuasiSeparated ?refine_1

Tactic:
·

Goal state after:
case refine_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover Y :=
  (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind fun x ↦
    ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover
this : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
i : Z.affineCover.I₀
j : (pullback g (Z.affineCover.f i)).affineCover.I₀
⊢ (Precoverage.ZeroHypercover.pullback₁ f
          ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind fun x ↦
            ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover)).X
      ⟨i, j⟩ ⟶
    pullback (f ≫ g) (Z.affineCover.f i)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case inr
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
Z : Set ↥X
hZ : IsClosed Z
H : StableUnderSpecialization (⇑f '' Z)
this :
  ∀ {X : Scheme} (S : CommRingCat) (f : X ⟶ Spec S) [QuasiCompact f] (Z : Set ↥X),
    IsClosed Z → StableUnderSpecialization (⇑f '' Z) → (∃ R, X = Spec R) → IsClosed (⇑f '' Z)
hX : ¬∃ R, X = Spec R
⊢ IsClosed (⇑f '' Z)

pp: X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
Z : Set ↥X
hZ : IsClosed Z
H : StableUnderSpecialization (⇑f '' Z)
hX : ∃ R, X = Spec R
⊢ IsClosed (⇑f '' Z)

Tactic:
·

Goal state after:
case inr
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
Z : Set ↥X
hZ : IsClosed Z
H : StableUnderSpecialization (⇑f '' Z)
this :
  ∀ {X : Scheme} (S : CommRingCat) (f : X ⟶ Spec S) [QuasiCompact f] (Z : Set ↥X),
    IsClosed Z → StableUnderSpecialization (⇑f '' Z) → (∃ R, X = Spec R) → IsClosed (⇑f '' Z)
hX : ¬∃ R, X = Spec R
⊢ IsClosed (⇑f '' Z)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case refine_2
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover Y :=
  (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind fun x ↦
    ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover
this : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
i : Z.affineCover.I₀
j : (pullback g (Z.affineCover.f i)).affineCover.I₀
⊢ QuasiSeparated
    (pullback.map f
        (((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind fun x ↦
              ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover).f
          ⟨i, j⟩)
        f ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).f ⟨i, j⟩.fst) (𝟙 X)
        (((fun i ↦
                ((fun x ↦ ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover)
                    i).toPreZeroHypercover)
              ⟨i, j⟩.fst).f
          ⟨i, j⟩.snd)
        (𝟙 Y) ⋯ ⋯ ≫
      (pullbackRightPullbackFstIso g (Z.affineCover.f i) f).hom)

Tactic:
·

Goal state after:
case refine_2
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover Y :=
  (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind fun x ↦
    ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover
this : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
i : Z.affineCover.I₀
j : (pullback g (Z.affineCover.f i)).affineCover.I₀
⊢ QuasiSeparated
    (pullback.map f
        (((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind fun x ↦
              ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover).f
          ⟨i, j⟩)
        f ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).f ⟨i, j⟩.fst) (𝟙 X)
        (((fun i ↦
                ((fun x ↦ ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover)
                    i).toPreZeroHypercover)
              ⟨i, j⟩.fst).f
          ⟨i, j⟩.snd)
        (𝟙 Y) ⋯ ⋯ ≫
      (pullbackRightPullbackFstIso g (Z.affineCover.f i) f).hom)
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₂) ⋯)) ⋯
⊢ X.basicOpen ((f |_ ↑S) ⋯) ≤ X.basicOpen ((f |_ U₁) ⋯)

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₂) ⋯)) ⋯
⊢ X.basicOpen ((f |_ ↑S) ⋯) ≤ X.basicOpen ((f |_ U₂) ⋯)

Tactic:
·

Goal state after:
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₂) ⋯)) ⋯
⊢ X.basicOpen ((f |_ ↑S) ⋯) ≤ X.basicOpen ((f |_ U₁) ⋯)
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₂) ⋯)) ⋯
⊢ X.basicOpen ((f |_ ↑S) ⋯) ≤ X.basicOpen ((f |_ U₂) ⋯)

Tactic:
·

Goal state after:
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₂) ⋯)) ⋯
⊢ X.basicOpen ((f |_ ↑S) ⋯) ≤ X.basicOpen ((f |_ U₂) ⋯)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case refine_1
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
i : ↑s
⊢ ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x |_
        X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f))
      ⋯ =
    0

pp: case refine_2
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
H' :
  ∀ (i : ↑s),
    ∃ n,
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n *
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x =
        0
⊢ ∃ n, f ^ n * x = 0

Tactic:
·

Goal state after:
case refine_1
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
i : ↑s
⊢ ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x |_
        X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f))
      ⋯ =
    0
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case e'_2
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
i : ↑s
H : (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x = 0
⊢ (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) x) =
    (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ?refine_1.convert_1).op))
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x)

pp: case e'_3
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
i : ↑s
H : (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x = 0
⊢ 0 = (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ?refine_1.convert_1).op)) 0

pp: case refine_1.convert_1
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
i : ↑s
H : (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x = 0
⊢ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ≤ X.basicOpen f

Tactic:
·

Goal state after:
case e'_2
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
i : ↑s
H : (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x = 0
⊢ (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) x) =
    (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ?refine_1.convert_1).op))
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case e'_2
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
i : ↑s
H : (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x = 0
⊢ (ConcreteCategory.hom (X.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op))) x =
    (ConcreteCategory.hom (X.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ?refine_1.convert_1).op))) x

Tactic:
·

Goal state after:
case e'_2
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
i : ↑s
H : (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x = 0
⊢ (ConcreteCategory.hom (X.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op))) x =
    (ConcreteCategory.hom (X.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ?refine_1.convert_1).op))) x
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case e'_3
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
i : ↑s
H : (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x = 0
⊢ 0 = (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ?refine_1.convert_1).op)) 0

pp: case refine_1.convert_1
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
i : ↑s
H : (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x = 0
⊢ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ≤ X.basicOpen f

Tactic:
·

Goal state after:
case e'_3
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
i : ↑s
H : (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x = 0
⊢ 0 = (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ?refine_1.convert_1).op)) 0
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case refine_1.convert_1
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
i : ↑s
H : (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x = 0
⊢ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ≤ X.basicOpen f

Tactic:
·

Goal state after:
case refine_1.convert_1
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
i : ↑s
H : (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x = 0
⊢ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ≤ X.basicOpen f
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case refine_1
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
⊢ IsQuasiSeparated ⊥.carrier →
    ∀ (f : ↑Γ(X, ⊥)) (x : ↑Γ(X, X.basicOpen f)),
      ∃ n y,
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x

pp: case refine_2
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
⊢ ∀ (S : X.Opens),
    IsCompact S.carrier →
      ∀ (U : ↑X.affineOpens),
        (IsQuasiSeparated S.carrier →
            ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
              ∃ n y,
                (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
                  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x) →
          IsQuasiSeparated (S ⊔ ↑U).carrier →
            ∀ (f : ↑Γ(X, S ⊔ ↑U)) (x : ↑Γ(X, X.basicOpen f)),
              ∃ n y,
                (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
                  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x

Tactic:
·

Goal state after:
case refine_1
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
⊢ IsQuasiSeparated ⊥.carrier →
    ∀ (f : ↑Γ(X, ⊥)) (x : ↑Γ(X, X.basicOpen f)),
      ∃ n y,
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case refine_2
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
⊢ ∀ (S : X.Opens),
    IsCompact S.carrier →
      ∀ (U : ↑X.affineOpens),
        (IsQuasiSeparated S.carrier →
            ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
              ∃ n y,
                (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
                  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x) →
          IsQuasiSeparated (S ⊔ ↑U).carrier →
            ∀ (f : ↑Γ(X, S ⊔ ↑U)) (x : ↑Γ(X, X.basicOpen f)),
              ∃ n y,
                (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
                  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x

Tactic:
·

Goal state after:
case refine_2
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
⊢ ∀ (S : X.Opens),
    IsCompact S.carrier →
      ∀ (U : ↑X.affineOpens),
        (IsQuasiSeparated S.carrier →
            ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
              ∃ n y,
                (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
                  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x) →
          IsQuasiSeparated (S ⊔ ↑U).carrier →
            ∀ (f : ↑Γ(X, S ⊔ ↑U)) (x : ↑Γ(X, X.basicOpen f)),
              ∃ n y,
                (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
                  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
Module: Mathlib.RingTheory.LocalProperties.Reduced

Goal state before:
pp: case zero
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
e : x ^ 0 = 0
⊢ x = 0

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
⊢ x = 0

Tactic:
·

Goal state after:
case zero
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
e : x ^ 0 = 0
⊢ x = 0
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 < J.height

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 < J.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 < J.height
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 < J.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 < J.height
Module: Mathlib.RingTheory.Ideal.Height

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

pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : FiniteRingKrullDim R
l : LTSeries (PrimeSpectrum R) := ⋯
m : Ideal R
hm : m.IsMaximal
hle : (RelSeries.last l).asIdeal ≤ m
⊢ ↑(RelSeries.last l).asIdeal.height ≤ ↑m.height

Tactic:
·

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : FiniteRingKrullDim R
l : LTSeries (PrimeSpectrum R) := ⋯
m : Ideal R
hm : m.IsMaximal
hle : (RelSeries.last l).asIdeal ≤ m
⊢ ringKrullDim R ≤ ↑(RelSeries.last l).asIdeal.height
Module: Mathlib.RingTheory.Ideal.Height

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

Tactic:
·

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : FiniteRingKrullDim R
l : LTSeries (PrimeSpectrum R) := ⋯
m : Ideal R
hm : m.IsMaximal
hle : (RelSeries.last l).asIdeal ≤ m
⊢ ↑(RelSeries.last l).asIdeal.height ≤ ↑m.height
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case inl
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : I.IsPrime
inst✝ : FiniteRingKrullDim R
e : ↑I.height = ringKrullDim R
h : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hM'✝ : I ≤ M
hM' : I < M
⊢ I.IsMaximal

pp: case inr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : I.IsPrime
inst✝ : FiniteRingKrullDim R
e : ↑I.height = ringKrullDim R
h : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hM'✝ : I ≤ M
hM' : I = M
⊢ I.IsMaximal

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : I.IsPrime
inst✝ : FiniteRingKrullDim R
e : ↑I.height = ringKrullDim R
h : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hM'✝ : I ≤ M
hM' : I < M
⊢ I.IsMaximal
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case inr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : I.IsPrime
inst✝ : FiniteRingKrullDim R
e : ↑I.height = ringKrullDim R
h : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hM'✝ : I ≤ M
hM' : I = M
⊢ I.IsMaximal

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : I.IsPrime
inst✝ : FiniteRingKrullDim R
e : ↑I.height = ringKrullDim R
h : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hM'✝ : I ≤ M
hM' : I = M
⊢ I.IsMaximal
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case mp
R : Type u_1
inst✝³ : CommRing R
inst✝² : FiniteRingKrullDim R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ ↑I.height = ringKrullDim R → I = IsLocalRing.maximalIdeal R

pp: case mpr
R : Type u_1
inst✝³ : CommRing R
inst✝² : FiniteRingKrullDim R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ I = IsLocalRing.maximalIdeal R → ↑I.height = ringKrullDim R

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝³ : CommRing R
inst✝² : FiniteRingKrullDim R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ ↑I.height = ringKrullDim R → I = IsLocalRing.maximalIdeal R