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

Goal state before:
pp: X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.I₀ → X.Opens := fun i ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : 𝒰.I₀ → T.Opens := fun i ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun x ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
g : ↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K))
htU' : t ∈ basicOpen g
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.I₀ := vars g
φ : MvPolynomial 𝒰.I₀ K →+* MvPolynomial 𝒰.I₀ K := (aeval fun i ↦ if i ∈ σ then MvPolynomial.X i else 0).toRingHom
t' : ↥T := (Spec.map (CommRingCat.ofHom φ)) t
ht'g : t' ∈ basicOpen g
h : t' ∉ ⇑fT '' Z
⊢ ∀ (a : ↥X), ∃ i, ∃ (_ : i ∈ σ), a ∈ (U i).carrier

Tactic:
]

Goal state after:
X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.I₀ → X.Opens := fun i ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : 𝒰.I₀ → T.Opens := fun i ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun x ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
g : ↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K))
htU' : t ∈ basicOpen g
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.I₀ := vars g
φ : MvPolynomial 𝒰.I₀ K →+* MvPolynomial 𝒰.I₀ K := (aeval fun i ↦ if i ∈ σ then MvPolynomial.X i else 0).toRingHom
t' : ↥T := (Spec.map (CommRingCat.ofHom φ)) t
ht'g : t' ∈ basicOpen g
h : t' ∉ ⇑fT '' Z
⊢ ∀ (a : ↥X), ∃ i, ∃ (_ : i ∈ σ), a ∈ (U i).carrier
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).IsIntegral) ∧
      (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).FiniteType ↔
    (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.app f ⊤)).IsIntegral) ∧ LocallyOfFiniteType f

Tactic:
]

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).IsIntegral) ∧
      (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).FiniteType ↔
    (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.app f ⊤)).IsIntegral) ∧ LocallyOfFiniteType f
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
inst✝² : CommRing R₀
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
n : ℕ
e : InductionObj R n
⊢ 1 ∈ ↑(coeffSubmodule R₀ e)

Tactic:
]

Goal state after:
R₀ : Type u_1
R : Type u_2
inst✝² : CommRing R₀
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
n : ℕ
e : InductionObj R n
⊢ 1 ∈ ↑(coeffSubmodule R₀ e)
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsClosedImmersion f ↔ IsFinite f ∧ Mono f)
hY : ¬IsAffine Y
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsClosedImmersion (Scheme.Cover.pullbackHom Y.affineCover f i)) ↔
    (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsFinite (Scheme.Cover.pullbackHom Y.affineCover f i)) ∧
      ∀ (i : Y.affineCover.toPreZeroHypercover.1), monomorphisms Scheme (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
]

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsClosedImmersion f ↔ IsFinite f ∧ Mono f)
hY : ¬IsAffine Y
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsClosedImmersion (Scheme.Cover.pullbackHom Y.affineCover f i)) ↔
    (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsFinite (Scheme.Cover.pullbackHom Y.affineCover f i)) ∧
      ∀ (i : Y.affineCover.toPreZeroHypercover.1), monomorphisms Scheme (Scheme.Cover.pullbackHom Y.affineCover f i)
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite) ∧ Epi (Scheme.Hom.appTop f) ↔
    (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite) ∧ Mono f

Tactic:
]

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite) ∧ Epi (Scheme.Hom.appTop f) ↔
    (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite) ∧ Mono f
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Subsingleton ↥X
inst✝¹ : IsReduced X
inst✝ : JacobsonSpace ↥Y
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y} [Subsingleton ↥X] [IsReduced X] [JacobsonSpace ↥Y],
    (∃ S, Y = Spec S) → (IsFinite f ↔ LocallyOfFiniteType f)
hY : ¬∃ S, Y = Spec S
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsFinite (Scheme.Cover.pullbackHom Y.affineCover f i)) ↔
    ∀ (i : Y.affineCover.toPreZeroHypercover.1), LocallyOfFiniteType (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
]

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Subsingleton ↥X
inst✝¹ : IsReduced X
inst✝ : JacobsonSpace ↥Y
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y} [Subsingleton ↥X] [IsReduced X] [JacobsonSpace ↥Y],
    (∃ S, Y = Spec S) → (IsFinite f ↔ LocallyOfFiniteType f)
hY : ¬∃ S, Y = Spec S
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsFinite (Scheme.Cover.pullbackHom Y.affineCover f i)) ↔
    ∀ (i : Y.affineCover.toPreZeroHypercover.1), LocallyOfFiniteType (Scheme.Cover.pullbackHom Y.affineCover f i)
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: case inr
X : Scheme
inst✝² : Subsingleton ↥X
inst✝¹ : IsReduced X
S : CommRingCat
f : X ⟶ Spec S
inst✝ : JacobsonSpace ↥(Spec S)
this :
  ∀ {X : Scheme} [Subsingleton ↥X] [IsReduced X] {f : X ⟶ Spec S},
    (∃ R, X = Spec R) → (IsFinite f ↔ LocallyOfFiniteType f)
hX : ¬∃ R, X = Spec R
⊢ IsFinite (X.isoSpec.inv ≫ f) ↔ LocallyOfFiniteType (X.isoSpec.inv ≫ f)

Tactic:
]

Goal state after:
case inr
X : Scheme
inst✝² : Subsingleton ↥X
inst✝¹ : IsReduced X
S : CommRingCat
f : X ⟶ Spec S
inst✝ : JacobsonSpace ↥(Spec S)
this :
  ∀ {X : Scheme} [Subsingleton ↥X] [IsReduced X] {f : X ⟶ Spec S},
    (∃ R, X = Spec R) → (IsFinite f ↔ LocallyOfFiniteType f)
hX : ¬∃ R, X = Spec R
⊢ IsFinite (X.isoSpec.inv ≫ f) ↔ LocallyOfFiniteType (X.isoSpec.inv ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: case inr
S : CommRingCat
inst✝² : JacobsonSpace ↥(Spec S)
R : CommRingCat
inst✝¹ : Subsingleton ↥(Spec R)
inst✝ : IsReduced (Spec R)
h✝ : Nonempty ↥(Spec R)
this✝ : IrreducibleSpace ↥(Spec R)
this : IsDomain ↑R
φ : S ⟶ R
⊢ (CommRingCat.Hom.hom φ).Finite ↔ (CommRingCat.Hom.hom φ).FiniteType

Tactic:
]

Goal state after:
case inr
S : CommRingCat
inst✝² : JacobsonSpace ↥(Spec S)
R : CommRingCat
inst✝¹ : Subsingleton ↥(Spec R)
inst✝ : IsReduced (Spec R)
h✝ : Nonempty ↥(Spec R)
this✝ : IrreducibleSpace ↥(Spec R)
this : IsDomain ↑R
φ : S ⟶ R
⊢ (CommRingCat.Hom.hom φ).Finite ↔ (CommRingCat.Hom.hom φ).FiniteType
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.I₀ → X.Opens := fun i ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : 𝒰.I₀ → T.Opens := fun i ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun x ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
g : ↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K))
htU' : t ∈ basicOpen g
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.I₀ := vars g
φ : MvPolynomial 𝒰.I₀ K →+* MvPolynomial 𝒰.I₀ K := (aeval fun i ↦ if i ∈ σ then MvPolynomial.X i else 0).toRingHom
t' : ↥T := (Spec.map (CommRingCat.ofHom φ)) t
ht'g : t' ∈ basicOpen g
z : ↥(pullback f q)
hzr : (pullback.snd f q) z = t'
hx : ∀ i ∈ σ, (pullback.fst f q) z ∉ (U i).carrier
i : 𝒰.I₀
hi₁ : t ∈ ⊥
hi₂ : p z ∈ U i
⊢ False

Tactic:
]

Goal state after:
X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.I₀ → X.Opens := fun i ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : 𝒰.I₀ → T.Opens := fun i ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun x ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
g : ↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K))
htU' : t ∈ basicOpen g
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.I₀ := vars g
φ : MvPolynomial 𝒰.I₀ K →+* MvPolynomial 𝒰.I₀ K := (aeval fun i ↦ if i ∈ σ then MvPolynomial.X i else 0).toRingHom
t' : ↥T := (Spec.map (CommRingCat.ofHom φ)) t
ht'g : t' ∈ basicOpen g
z : ↥(pullback f q)
hzr : (pullback.snd f q) z = t'
hx : ∀ i ∈ σ, (pullback.fst f q) z ∉ (U i).carrier
i : 𝒰.I₀
hi₁ : t ∈ ⊥
hi₂ : p z ∈ U i
⊢ False
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : UniversallyClosed f
⊢ Continuous ⇑f ∧ IsClosedMap ⇑f ∧ ∀ (y : ↥Y), IsCompact (⇑f ⁻¹' {y})

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : UniversallyClosed f
⊢ Continuous ⇑f ∧ IsClosedMap ⇑f ∧ ∀ (y : ↥Y), IsCompact (⇑f ⁻¹' {y})
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : UniversallyClosed f
y : ↥Y
this : CompactSpace ↥(pullback f (Y.fromSpecResidueField y))
⊢ IsCompact (Set.range ⇑(pullback.fst f (Y.fromSpecResidueField y)))

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : UniversallyClosed f
y : ↥Y
this : CompactSpace ↥(pullback f (Y.fromSpecResidueField y))
⊢ IsCompact (Set.range ⇑(pullback.fst f (Y.fromSpecResidueField y)))
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: ⊢ @UniversallyClosed = (topologically @SpecializingMap).universally ⊓ universally @QuasiCompact

Tactic:
← universally_inf

Goal state after:
⊢ @UniversallyClosed = (topologically @SpecializingMap ⊓ @QuasiCompact).universally
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: ⊢ @UniversallyClosed = (topologically @SpecializingMap ⊓ @QuasiCompact).universally

Tactic:
]

Goal state after:
⊢ @UniversallyClosed = (topologically @SpecializingMap ⊓ @QuasiCompact).universally
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: case a
⊢ universally @UniversallyClosed ≤ (topologically @SpecializingMap ⊓ @QuasiCompact).universally

Tactic:
]

Goal state after:
case a
⊢ universally @UniversallyClosed ≤ (topologically @SpecializingMap ⊓ @QuasiCompact).universally
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: case a
⊢ (topologically @SpecializingMap ⊓ @QuasiCompact).universally ≤ (topologically @IsClosedMap).universally

Tactic:
]

Goal state after:
case a
⊢ (topologically @SpecializingMap ⊓ @QuasiCompact).universally ≤ (topologically @IsClosedMap).universally
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsDominant f
⊢ Set.range ⇑f = Set.range ⇑f

Tactic:
]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsDominant f
⊢ Surjective f

Tactic:
by
  rw [surjective_iff, ← Set.range_eq_univ, ← f.denseRange.closure_range,
    f.isClosedMap.isClosed_range.closure_eq]

Goal state after:
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : X.IsQuasiAffine
⊢ IsSeparated (X.toSpecΓ ≫ terminal.from (Spec Γ(X, ⊤)))

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : X.IsQuasiAffine
⊢ IsSeparated (X.toSpecΓ ≫ terminal.from (Spec Γ(X, ⊤)))
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : X.IsQuasiAffine
⊢ IsIso ⊥.subschemeι

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : X.IsQuasiAffine
⊢ IsIso ⊥.subschemeι
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : X.IsQuasiAffine
this : IsIso (Hom.imageι X.toSpecΓ)
⊢ IsOpenImmersion (Hom.toImage X.toSpecΓ ≫ Hom.imageι X.toSpecΓ)

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : X.IsQuasiAffine
this : IsIso (Hom.imageι X.toSpecΓ)
⊢ IsOpenImmersion (Hom.toImage X.toSpecΓ ≫ Hom.imageι X.toSpecΓ)
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : Y.IsQuasiAffine
inst✝¹ : IsImmersion f
inst✝ : CompactSpace ↥X
⊢ IsImmersion (f ≫ Y.toSpecΓ)

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : Y.IsQuasiAffine
inst✝¹ : IsImmersion f
inst✝ : CompactSpace ↥X
⊢ IsImmersion (f ≫ Y.toSpecΓ)
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X : Scheme
inst✝ : X.IsQuasiAffine
U : TopologicalSpace.Opens ↥X
x : ↥X
hxU : x ∈ U
r : ↑Γ(X, ⊤)
hxr :
  (ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base) x ∈
    ↑(PrimeSpectrum.basicOpen r)
hrU :
  ↑(PrimeSpectrum.basicOpen r) ⊆
    ⇑(ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base) '' ↑U
⊢ IsAffineOpen (X.toSpecΓ ''ᵁ X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r)

Tactic:
]

Goal state after:
X : Scheme
inst✝ : X.IsQuasiAffine
U : TopologicalSpace.Opens ↥X
x : ↥X
hxU : x ∈ U
r : ↑Γ(X, ⊤)
hxr :
  (ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base) x ∈
    ↑(PrimeSpectrum.basicOpen r)
hrU :
  ↑(PrimeSpectrum.basicOpen r) ⊆
    ⇑(ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base) '' ↑U
⊢ IsAffineOpen (X.toSpecΓ ''ᵁ X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r)
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ (∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Flat) ↔
    ∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Flat

Tactic:
]

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
inst✝¹ : Subsingleton ↥Y
inst✝ : IsIntegral Y
i : X.affineCover.I₀
⊢ (CommRingCat.Hom.hom (Spec.preimage (X.affineCover.f i ≫ f ≫ Y.isoSpec.hom))).Flat

Tactic:
]

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
inst✝¹ : Subsingleton ↥Y
inst✝ : IsIntegral Y
i : X.affineCover.I₀
⊢ (CommRingCat.Hom.hom (Spec.preimage (X.affineCover.f i ≫ f ≫ Y.isoSpec.hom))).Flat
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
⊢ Topology.IsCoinducing ⇑f ∧ Function.Surjective ⇑f

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
⊢ Topology.IsCoinducing ⇑f ∧ Function.Surjective ⇑f
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case pos
n : ℕ
P : (R : Type u) → [inst : CommRing R] → InductionObj R n → Prop
hP₁ : ∀ (R : Type u) [inst : CommRing R], P R { val := 0 }
hP₂ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic → (∀ (j : Fin n), j ≠ i → e.val j = 0) → P R e
hP₃ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree → i ≠ j → P R { val := Function.update e.val j (e.val j %ₘ e.val i) } → P R e
hP₄ :
  ∀ (R : Type u) [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        P (Away c)
            { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val } →
          P (R ⧸ Ideal.span {c}) { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } → P R e
v : DegreeType n
H_IH : ∀ y < v, ∀ {R : Type u} [inst : CommRing R] (e : InductionObj R n), y = e.degree → P R e
R : Type u
inst✝ : CommRing R
e : InductionObj R n
hv : v = e.degree
h✝ : Nontrivial R
he0 : ∃ x, ¬e.val x = 0
i : Fin n
hi : (e.val i).Monic
j : Fin n
hj : j ≠ i
hj' : e.val j ≠ 0
i_min : (e.val i).degree ≤ (e.val j).degree
k : Fin n
hjk : k = j
⊢ (e.val j %ₘ e.val i).degree ≤ (ofLex e.degree).1 j

Tactic:
]

Goal state after:
case pos
n : ℕ
P : (R : Type u) → [inst : CommRing R] → InductionObj R n → Prop
hP₁ : ∀ (R : Type u) [inst : CommRing R], P R { val := 0 }
hP₂ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic → (∀ (j : Fin n), j ≠ i → e.val j = 0) → P R e
hP₃ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree → i ≠ j → P R { val := Function.update e.val j (e.val j %ₘ e.val i) } → P R e
hP₄ :
  ∀ (R : Type u) [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        P (Away c)
            { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val } →
          P (R ⧸ Ideal.span {c}) { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } → P R e
v : DegreeType n
H_IH : ∀ y < v, ∀ {R : Type u} [inst : CommRing R] (e : InductionObj R n), y = e.degree → P R e
R : Type u
inst✝ : CommRing R
e : InductionObj R n
hv : v = e.degree
h✝ : Nontrivial R
he0 : ∃ x, ¬e.val x = 0
i : Fin n
hi : (e.val i).Monic
j : Fin n
hj : j ≠ i
hj' : e.val j ≠ 0
i_min : (e.val i).degree ≤ (e.val j).degree
k : Fin n
hjk : k = j
⊢ (e.val j %ₘ e.val i).degree ≤ (ofLex e.degree).1 j
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: case e'_1
X : Scheme
inst✝ : CompactSpace ↥X
H : ∀ (x : ↥X), ∃ r, IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this✝ : QuasiSeparatedSpace ↥X
x : ↥X
r : ↑Γ(X, ⊤)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
this : IsOpenImmersion ((X.basicOpen r).ι ≫ X.toSpecΓ)
⊢ X.basicOpen r = X.basicOpen r

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: case e'_3.e'_6
X : Scheme
inst✝ : CompactSpace ↥X
H : ∀ (x : ↥X), ∃ r, IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this✝ : QuasiSeparatedSpace ↥X
x : ↥X
r : ↑Γ(X, ⊤)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
this : IsOpenImmersion ((X.basicOpen r).ι ≫ X.toSpecΓ)
e_1✝ : ↑(X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r) = ↑(X.basicOpen r)
⊢ X.basicOpen r = X.basicOpen r

Tactic:
]

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

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥Y
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y),
    IsOpen (⇑f ⁻¹' s) → (∃ R, Y = Spec R) → IsOpen s
hY : ¬∃ R, Y = Spec R
𝒰 : Y.OpenCover := Y.affineCover
⊢ ∀ (i : 𝒰.I₀), IsOpen (s ∩ ↑(Scheme.Hom.opensRange (𝒰.f i)))

Tactic:
]

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥Y
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y),
    IsOpen (⇑f ⁻¹' s) → (∃ R, Y = Spec R) → IsOpen s
hY : ¬∃ R, Y = Spec R
𝒰 : Y.OpenCover := Y.affineCover
⊢ ∀ (i : 𝒰.I₀), IsOpen (s ∩ ↑(Scheme.Hom.opensRange (𝒰.f i)))
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X : Scheme
inst✝ : CompactSpace ↥X
H : ∀ (x : ↥X), ∃ r, IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this : QuasiSeparatedSpace ↥X
x : ↥X
r : ↑Γ(X, ⊤)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
⊢ IsOpenImmersion ((X.basicOpen r).toSpecΓ ≫ Spec.map (X.presheaf.map (homOfLE ⋯).op))

Tactic:
]

Goal state after:
X : Scheme
inst✝ : CompactSpace ↥X
H : ∀ (x : ↥X), ∃ r, IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this : QuasiSeparatedSpace ↥X
x : ↥X
r : ↑Γ(X, ⊤)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
⊢ IsOpenImmersion ((X.basicOpen r).toSpecΓ ≫ Spec.map (X.presheaf.map (homOfLE ⋯).op))
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥Y
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y),
    IsOpen (⇑f ⁻¹' s) → (∃ R, Y = Spec R) → IsOpen s
hY : ¬∃ R, Y = Spec R
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
⊢ IsOpen (⇑(𝒰.f i) '' ⇑(𝒰.f i) ⁻¹' s)

Tactic:
]

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥Y
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y),
    IsOpen (⇑f ⁻¹' s) → (∃ R, Y = Spec R) → IsOpen s
hY : ¬∃ R, Y = Spec R
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
⊢ IsOpen (⇑(𝒰.f i) '' ⇑(𝒰.f i) ⁻¹' s)
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
this : CompactSpace ↥X
x : ↥X
r : ↑Γ(Y, ⊤)
hr : IsAffineOpen (Y.basicOpen r)
hxr : f x ∈ ↑(Y.basicOpen r)
⊢ IsAffineOpen (f ⁻¹ᵁ Y.basicOpen r) ∧ x ∈ f ⁻¹ᵁ Y.basicOpen r

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
this : CompactSpace ↥X
x : ↥X
r : ↑Γ(Y, ⊤)
hr : IsAffineOpen (Y.basicOpen r)
hxr : f x ∈ ↑(Y.basicOpen r)
⊢ IsAffineOpen (f ⁻¹ᵁ Y.basicOpen r) ∧ x ∈ f ⁻¹ᵁ Y.basicOpen r
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥Y
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y),
    IsOpen (⇑f ⁻¹' s) → (∃ R, Y = Spec R) → IsOpen s
hY : ¬∃ R, Y = Spec R
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
⊢ IsOpen (⇑(pullback.snd (𝒰.f i) f) ⁻¹' ⇑f ⁻¹' s)

Tactic:
]

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥Y
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y),
    IsOpen (⇑f ⁻¹' s) → (∃ R, Y = Spec R) → IsOpen s
hY : ¬∃ R, Y = Spec R
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
⊢ IsOpen (⇑(pullback.snd (𝒰.f i) f) ⁻¹' ⇑f ⁻¹' s)