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

Goal state before:
pp: case of_basicOpenCover
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑Γ(Y, ⊤)
hS : ⨆ f, Y.basicOpen ↑f = ⊤
hS' : ∀ (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
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑Γ(Y, ⊤)
hS : ⨆ f, Y.basicOpen ↑f = ⊤
hS' : ∀ (r : ↥S), CompactSpace ↥↑(f ⁻¹ᵁ Y.basicOpen ↑r)
⊢ CompactSpace ↥X
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃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) ⋯
U V : ↑X.affineOpens
g : pullback (↑U).ι (↑V).ι ⟶ X := pullback.fst (↑U).ι (↑V).ι ≫ (↑U).ι
e : ↥(pullback (↑U).ι (↑V).ι) ≃ₜ ↑(↑↑U ∩ ↑↑V)
⊢ IsCompact (↑↑U ∩ ↑↑V)

Tactic:
]

Goal state after:
case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃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) ⋯
U V : ↑X.affineOpens
g : pullback (↑U).ι (↑V).ι ⟶ X := pullback.fst (↑U).ι (↑V).ι ≫ (↑U).ι
e : ↥(pullback (↑U).ι (↑V).ι) ≃ₜ ↑(↑↑U ∩ ↑↑V)
⊢ IsCompact (↑↑U ∩ ↑↑V)
Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
H :
  ∀ (R A B : CommRingCat) (f' : Spec A ⟶ Spec R) (g' : Spec B ⟶ Spec R) (iX : Spec A ⟶ X) (iY : Spec B ⟶ Y)
    (iS : Spec R ⟶ S) (e₁ : f' ≫ iS = iX ≫ f) (e₂ : g' ≫ iS = iY ≫ g),
    IsOpenImmersion iX →
      IsOpenImmersion iY → IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(pullback.map f' g' f g iX iY iS e₁ e₂))
𝒰 : S.OpenCover := S.affineOpenCover.openCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover :=
  fun i ↦ ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).affineOpenCover.openCover
𝒲 : (i : (Precoverage.ZeroHypercover.pullback₁ g 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ g 𝒰).X i).OpenCover :=
  fun i ↦ ((Precoverage.ZeroHypercover.pullback₁ g 𝒰).X i).affineOpenCover.openCover
U : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) × (𝒱 i).I₀ × (𝒲 i).I₀ → TopologicalSpace.Opens (↥X × ↥Y) :=
  fun ijk ↦
    {
      carrier :=
        {P |
          P.1 ∈ Scheme.Hom.opensRange ((𝒱 ijk.fst).f ijk.snd.1 ≫ (Precoverage.ZeroHypercover.pullback₁ f 𝒰).f ijk.fst) ∧
            P.2 ∈
              Scheme.Hom.opensRange ((𝒲 ijk.fst).f ijk.snd.2 ≫ (Precoverage.ZeroHypercover.pullback₁ g 𝒰).f ijk.fst)},
      is_open' := ⋯ }
z : ↥(pullback f g)
is : 𝒰.I₀
s : ↥(𝒰.X is)
hsx : (𝒰.f is) s = f ((pullback.fst f g) z)
⊢ (𝒰.f is) s = f ((pullback.fst f g) z)

Tactic:
]

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
H :
  ∀ (R A B : CommRingCat) (f' : Spec A ⟶ Spec R) (g' : Spec B ⟶ Spec R) (iX : Spec A ⟶ X) (iY : Spec B ⟶ Y)
    (iS : Spec R ⟶ S) (e₁ : f' ≫ iS = iX ≫ f) (e₂ : g' ≫ iS = iY ≫ g),
    IsOpenImmersion iX →
      IsOpenImmersion iY → IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(pullback.map f' g' f g iX iY iS e₁ e₂))
𝒰 : S.OpenCover := S.affineOpenCover.openCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover :=
  fun i ↦ ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).affineOpenCover.openCover
𝒲 : (i : (Precoverage.ZeroHypercover.pullback₁ g 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ g 𝒰).X i).OpenCover :=
  fun i ↦ ((Precoverage.ZeroHypercover.pullback₁ g 𝒰).X i).affineOpenCover.openCover
U : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) × (𝒱 i).I₀ × (𝒲 i).I₀ → TopologicalSpace.Opens (↥X × ↥Y) :=
  fun ijk ↦
    {
      carrier :=
        {P |
          P.1 ∈ Scheme.Hom.opensRange ((𝒱 ijk.fst).f ijk.snd.1 ≫ (Precoverage.ZeroHypercover.pullback₁ f 𝒰).f ijk.fst) ∧
            P.2 ∈
              Scheme.Hom.opensRange ((𝒲 ijk.fst).f ijk.snd.2 ≫ (Precoverage.ZeroHypercover.pullback₁ g 𝒰).f ijk.fst)},
      is_open' := ⋯ }
z : ↥(pullback f g)
is : 𝒰.I₀
s : ↥(𝒰.X is)
hsx : (𝒰.f is) s = f ((pullback.fst f g) z)
⊢ (𝒰.f is) s = f ((pullback.fst f g) z)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case of_basicOpenCover
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑Γ(Y, ⊤)
hS : ⨆ f, Y.basicOpen ↑f = ⊤
hS' : ∀ (r : ↥S), CompactSpace ↥↑(f ⁻¹ᵁ Y.basicOpen ↑r)
⊢ IsCompact (⋃ i, ((Opens.map f.base).1 (Y.basicOpen ↑i)).carrier)

Tactic:
]

Goal state after:
case of_basicOpenCover
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑Γ(Y, ⊤)
hS : ⨆ f, Y.basicOpen ↑f = ⊤
hS' : ∀ (r : ↥S), CompactSpace ↥↑(f ⁻¹ᵁ Y.basicOpen ↑r)
⊢ IsCompact (⋃ i, ((Opens.map f.base).1 (Y.basicOpen ↑i)).carrier)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃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) ⋯
U V : ↑X.affineOpens
g : pullback (↑U).ι (↑V).ι ⟶ X := pullback.fst (↑U).ι (↑V).ι ≫ (↑U).ι
e : ↥(pullback (↑U).ι (↑V).ι) ≃ₜ ↑(↑↑U ∩ ↑↑V)
⊢ CompactSpace ↑(↑↑U ∩ ↑↑V)

Tactic:
]

Goal state after:
case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃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) ⋯
U V : ↑X.affineOpens
g : pullback (↑U).ι (↑V).ι ⟶ X := pullback.fst (↑U).ι (↑V).ι ≫ (↑U).ι
e : ↥(pullback (↑U).ι (↑V).ι) ≃ₜ ↑(↑↑U ∩ ↑↑V)
⊢ CompactSpace ↑(↑↑U ∩ ↑↑V)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case mpr
X Y : Scheme
inst✝² : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst✝¹ : IsAffine U₁
inst✝ : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
g : pullback f₁ f₂ ⟶ X := pullback.fst f₁ f₂ ≫ f₁
e : ↥(pullback f₁ f₂) ≃ₜ ↑(Set.range ⇑f₁ ∩ Set.range ⇑f₂)
⊢ CompactSpace ↥(pullback f₁ f₂)

Tactic:
]

Goal state after:
case mpr
X Y : Scheme
inst✝² : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst✝¹ : IsAffine U₁
inst✝ : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
g : pullback f₁ f₂ ⟶ X := pullback.fst f₁ f₂ ≫ f₁
e : ↥(pullback f₁ f₂) ≃ₜ ↑(Set.range ⇑f₁ ∩ Set.range ⇑f₂)
⊢ CompactSpace ↥(pullback f₁ f₂)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X : Scheme
⊢ CompactSpace ↥X ↔ CompactSpace ↥X

Tactic:
]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : CompactSpace ↥Y
⊢ IsCompact (⇑f ⁻¹' Set.univ)

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : CompactSpace ↥Y
⊢ IsCompact (⇑f ⁻¹' Set.univ)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : ↑Y.affineOpens
V₁ V₂ : ↑X.affineOpens
hx₁ : x ∈ ↑V₁
hx₂ : x ∈ ↑V₂
e₂ : ↑V₂ ≤ f ⁻¹ᵁ ↑U₂
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂))
hfx₁ : f x ∈ ↑U₁
r : ↑Γ(Y, ↑U₁)
r' : ↑Γ(Y, ↑U₂)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : f x ∈ Y.basicOpen r
ha : IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
hxa : x ∈ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')
s : ↑Γ(X, ↑V₁)
s' : ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
hBss' : X.basicOpen s = X.basicOpen s'
hBx : x ∈ X.basicOpen s
this✝ :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
this : IsLocalization.Away r' ↑Γ(Y, Y.basicOpen r')
⊢ ∃ r s,
    ∃ (_ : x ∈ X.basicOpen s) (e : X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r),
      P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e))

Tactic:
have := ha.isLocalization_basicOpen s'

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : ↑Y.affineOpens
V₁ V₂ : ↑X.affineOpens
hx₁ : x ∈ ↑V₁
hx₂ : x ∈ ↑V₂
e₂ : ↑V₂ ≤ f ⁻¹ᵁ ↑U₂
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂))
hfx₁ : f x ∈ ↑U₁
r : ↑Γ(Y, ↑U₁)
r' : ↑Γ(Y, ↑U₂)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : f x ∈ Y.basicOpen r
ha : IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
hxa : x ∈ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')
s : ↑Γ(X, ↑V₁)
s' : ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
hBss' : X.basicOpen s = X.basicOpen s'
hBx : x ∈ X.basicOpen s
this✝¹ :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
this✝ : IsLocalization.Away r' ↑Γ(Y, Y.basicOpen r')
this : IsLocalization.Away s' ↑Γ(X, X.basicOpen s')
⊢ ∃ r s,
    ∃ (_ : x ∈ X.basicOpen s) (e : X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r),
      P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hY : QuasiSeparated (terminal.from Y)
inst✝ : QuasiSeparated f
⊢ QuasiSeparated (terminal.from X)

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
hY : QuasiSeparated (terminal.from Y)
inst✝ : QuasiSeparated f
⊢ QuasiSeparated (terminal.from X)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hY : QuasiSeparated (terminal.from Y)
inst✝ : QuasiSeparated f
⊢ QuasiSeparated (f ≫ terminal.from Y)

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
hY : QuasiSeparated (terminal.from Y)
inst✝ : QuasiSeparated f
⊢ QuasiSeparated (f ≫ terminal.from Y)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ QuasiSeparatedSpace ↑↑U

pp: case hs
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ IsOpen ↑U

Tactic:
]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ QuasiSeparatedSpace ↑↑U

case hs
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ IsOpen ↑U
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
I : Type u_1
U : I → X.Opens
hU : IsOpenCover U
hU₁ : ∀ (i : I), IsAffineOpen (U i)
hU₂ : ∀ (i j : I), IsCompact (↑(U i) ∩ ↑(U j))
this : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
⊢ AffineTargetMorphismProperty.diagonal (fun X x x_1 x_2 ↦ CompactSpace ↥X) X.toSpecΓ

Tactic:
]

Goal state after:
X : Scheme
I : Type u_1
U : I → X.Opens
hU : IsOpenCover U
hU₁ : ∀ (i : I), IsAffineOpen (U i)
hU₂ : ∀ (i j : I), IsCompact (↑(U i) ∩ ↑(U j))
this : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
⊢ AffineTargetMorphismProperty.diagonal (fun X x x_1 x_2 ↦ CompactSpace ↥X) X.toSpecΓ
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
I : Type u_1
U : I → X.Opens
hU : IsOpenCover U
hU₁ : ∀ (i : I), IsAffineOpen (U i)
hU₂ : ∀ (i j : I), IsCompact (↑(U i) ∩ ↑(U j))
this✝ : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
this : ∀ (i : (X.openCoverOfIsOpenCover U hU).I₀), IsAffine ((X.openCoverOfIsOpenCover U hU).X i)
i j : (X.openCoverOfIsOpenCover U hU).I₀
⊢ IsCompact (Set.range ⇑((X.openCoverOfIsOpenCover U hU).f i) ∩ Set.range ⇑((X.openCoverOfIsOpenCover U hU).f j))

Tactic:
]

Goal state after:
X : Scheme
I : Type u_1
U : I → X.Opens
hU : IsOpenCover U
hU₁ : ∀ (i : I), IsAffineOpen (U i)
hU₂ : ∀ (i j : I), IsCompact (↑(U i) ∩ ↑(U j))
this✝ : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
this : ∀ (i : (X.openCoverOfIsOpenCover U hU).I₀), IsAffine ((X.openCoverOfIsOpenCover U hU).X i)
i j : (X.openCoverOfIsOpenCover U hU).I₀
⊢ IsCompact (Set.range ⇑((X.openCoverOfIsOpenCover U hU).f i) ∩ Set.range ⇑((X.openCoverOfIsOpenCover U hU).f j))
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : ↑Y.affineOpens
V₁ V₂ : ↑X.affineOpens
hx₁ : x ∈ ↑V₁
hx₂ : x ∈ ↑V₂
e₂ : ↑V₂ ≤ f ⁻¹ᵁ ↑U₂
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂))
hfx₁ : f x ∈ ↑U₁
r : ↑Γ(Y, ↑U₁)
r' : ↑Γ(Y, ↑U₂)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : f x ∈ Y.basicOpen r
ha : IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
hxa : x ∈ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')
s : ↑Γ(X, ↑V₁)
s' : ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
hBss' : X.basicOpen s = X.basicOpen s'
hBx : x ∈ X.basicOpen s
this✝¹ :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
this✝ : IsLocalization.Away r' ↑Γ(Y, Y.basicOpen r')
this : IsLocalization.Away s' ↑Γ(X, X.basicOpen s')
⊢ X.basicOpen s' ≤ f ⁻¹ᵁ Y.basicOpen r'

Tactic:
]

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : ↑Y.affineOpens
V₁ V₂ : ↑X.affineOpens
hx₁ : x ∈ ↑V₁
hx₂ : x ∈ ↑V₂
e₂ : ↑V₂ ≤ f ⁻¹ᵁ ↑U₂
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂))
hfx₁ : f x ∈ ↑U₁
r : ↑Γ(Y, ↑U₁)
r' : ↑Γ(Y, ↑U₂)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : f x ∈ Y.basicOpen r
ha : IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
hxa : x ∈ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')
s : ↑Γ(X, ↑V₁)
s' : ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
hBss' : X.basicOpen s = X.basicOpen s'
hBx : x ∈ X.basicOpen s
this✝¹ :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
this✝ : IsLocalization.Away r' ↑Γ(Y, Y.basicOpen r')
this : IsLocalization.Away s' ↑Γ(X, X.basicOpen s')
⊢ X.basicOpen s' ≤ f ⁻¹ᵁ Y.basicOpen r'
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
⊢ autoParam (QuasiCompact (pullback.diagonal (terminal.from X))) QuasiSeparated.quasiCompact_diagonal._autoParam ↔
    QuasiCompact (prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom)

Tactic:
]

Goal state after:
X : Scheme
⊢ autoParam (QuasiCompact (pullback.diagonal (terminal.from X))) QuasiSeparated.quasiCompact_diagonal._autoParam ↔
    QuasiCompact (prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X : Scheme
U : X.Opens
x✝ : ∃ R f, Set.range ⇑f = ↑U
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range ⇑f = ↑U
⊢ Set.range ⇑(IsOpenImmersion.lift U.ι f ⋯) = Set.univ

Tactic:
]

Goal state after:
X : Scheme
U : X.Opens
x✝ : ∃ R f, Set.range ⇑f = ↑U
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range ⇑f = ↑U
⊢ Set.range ⇑(IsOpenImmersion.lift U.ι f ⋯) = Set.univ
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparatedSpace ↥X
⊢ QuasiSeparatedSpace ↥X

Tactic:
]

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparatedSpace ↥X
⊢ QuasiSeparatedSpace ↥X
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X : Scheme
U : X.Opens
x✝ : ∃ R f, Set.range ⇑f = ↑U
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range ⇑f = ↑U
⊢ Set.range ⇑f = ↑U

Tactic:
]

Goal state after:
X : Scheme
U : X.Opens
x✝ : ∃ R f, Set.range ⇑f = ↑U
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range ⇑f = ↑U
⊢ Set.range ⇑f = ↑U
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
⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1), topologically (@IsClosedMap) (Scheme.Cover.pullbackHom Y.affineCover f i)

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
⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1), topologically (@IsClosedMap) (Scheme.Cover.pullbackHom Y.affineCover f i)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
⊢ QuasiSeparated f

Tactic:
by
  let 𝒰 := (Z.affineCover.pullback₁ g).bind fun x => Scheme.affineCover _
  have (i : _) : IsAffine (𝒰.X i) := by dsimp [𝒰]; infer_instance
  apply HasAffineProperty.of_openCover
    ((Z.affineCover.pullback₁ g).bind fun x => Scheme.affineCover _)
  rintro ⟨i, j⟩; dsimp at i j
  refine @quasiSeparatedSpace_of_quasiSeparated _ _ ?_
    (HasAffineProperty.of_isPullback (.of_hasPullback _ (Z.affineCover.f i)) ‹_›) ?_
  · exact pullback.map _ _ _ _ (𝟙 _) _ _ (by simp) (Category.comp_id _) ≫
      (pullbackRightPullbackFstIso g (Z.affineCover.f i) f).hom
  · exact inferInstance

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
⊢ MorphismProperty.diagonal @QuasiCompact ≤ MorphismProperty.diagonal @QuasiCompact

Tactic:
]

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

Goal state before:
pp: X : TopCat
F : TopCat.Presheaf CommRingCat X
U₁ U₂ U₃ U₄ U₅ U₆ U₇ : Opens ↑X
n₁ n₂ : ℕ
y₁ : ↑(F.obj (op U₁))
y₂ : ↑(F.obj (op U₂))
f : ↑(F.obj (op (U₁ ⊔ U₂)))
x : ↑(F.obj (op U₃))
h₄₁ : U₄ ≤ U₁
h₄₂ : U₄ ≤ U₂
h₅₁ : U₅ ≤ U₁
h₅₃ : U₅ ≤ U₃
h₆₂ : U₆ ≤ U₂
h₆₃ : U₆ ≤ U₃
h₇₄ : U₇ ≤ U₄
h₇₅ : U₇ ≤ U₅
h₇₆ : U₇ ≤ U₆
e₁ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x
e₂ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₂ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ *
      ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₂ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ *
      ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₂ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x)

Tactic:
]

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

Goal state before:
pp: X : Scheme
P : X.Opens → Prop
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : ↑X.affineOpens), P S → P (S ⊔ ↑U)
s✝ : Set ↑X.affineOpens
hs✝ : s✝.Finite
hS : IsCompact ↑(⨆ i ∈ s✝, ↑i)
x : ↑X.affineOpens
s : Set ↑X.affineOpens
x✝ : x ∉ s
hs : s.Finite
h₄ : P (⨆ i ∈ s, ↑i)
⊢ P ((⨆ x ∈ s, ↑x) ⊔ ↑x)

Tactic:
]

Goal state after:
X : Scheme
P : X.Opens → Prop
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : ↑X.affineOpens), P S → P (S ⊔ ↑U)
s✝ : Set ↑X.affineOpens
hs✝ : s✝.Finite
hS : IsCompact ↑(⨆ i ∈ s✝, ↑i)
x : ↑X.affineOpens
s : Set ↑X.affineOpens
x✝ : x ∉ s
hs : s.Finite
h₄ : P (⨆ i ∈ s, ↑i)
⊢ P ((⨆ x ∈ s, ↑x) ⊔ ↑x)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) 0
⊢ ∃ n, f ^ n * x = 0

Tactic:
]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) 0
⊢ ∃ n, f ^ n * x = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: 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
i : ↑s
⊢ ↑↑i ≤ ⨆ i, ↑↑i

Tactic:
]

Goal state after:
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
i : ↑s
⊢ ↑↑i ≤ ⨆ i, ↑↑i
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 : ℕ
e :
  ↑⟨(fun x ↦ (f |_ ↑S) ⋯ ^ x) n, ⋯⟩ * (((f |_ U₁) ⋯ ^ n₂ * y₁) |_ ↑S) h₁ =
    ↑⟨(fun x ↦ (f |_ ↑S) ⋯ ^ x) n, ⋯⟩ * (((f |_ U₂) ⋯ ^ n₁ * y₂) |_ ↑S) h₂
m : ℕ
hm : n ≤ m
⊢ (((f |_ U₁) ⋯ ^ (m - n + n + n₂) * y₁) |_ ↑S) h₁ = (((f |_ U₂) ⋯ ^ (m - n + n + n₁) * y₂) |_ ↑S) h₂

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₂) ⋯)) ⋯
n : ℕ
e :
  ↑⟨(fun x ↦ (f |_ ↑S) ⋯ ^ x) n, ⋯⟩ * (((f |_ U₁) ⋯ ^ n₂ * y₁) |_ ↑S) h₁ =
    ↑⟨(fun x ↦ (f |_ ↑S) ⋯ ^ x) n, ⋯⟩ * (((f |_ U₂) ⋯ ^ n₁ * y₂) |_ ↑S) h₂
m : ℕ
hm : n ≤ m
⊢ (((f |_ U₁) ⋯ ^ (m - n + n + n₂) * y₁) |_ ↑S) h₁ = (((f |_ U₂) ⋯ ^ (m - n + n + n₁) * y₂) |_ ↑S) h₂
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 = 0

Tactic:
]

Goal state after: