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

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↥Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace ↥Y], (∃ S, Y = Spec S) → JacobsonSpace ↥X
hY : ¬∃ S, Y = Spec S
⊢ ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀),
    JacobsonSpace ↥(Scheme.Hom.opensRange ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i))

Tactic:
intro i

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↥Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace ↥Y], (∃ S, Y = Spec S) → JacobsonSpace ↥X
hY : ¬∃ S, Y = Spec S
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
⊢ JacobsonSpace ↥(Scheme.Hom.opensRange ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i))
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↥(Spec R)
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [LocallyOfFiniteType f] [JacobsonSpace ↥(Spec R)],
    (∃ S, X = Spec S) → JacobsonSpace ↥X
hX : ¬∃ S, X = Spec S
inst : JacobsonSpace ↥(Spec R)
⊢ ∀ (i : X.affineCover.I₀), JacobsonSpace ↥(Scheme.Hom.opensRange (X.affineCover.f i))

Tactic:
intro i

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↥(Spec R)
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [LocallyOfFiniteType f] [JacobsonSpace ↥(Spec R)],
    (∃ S, X = Spec S) → JacobsonSpace ↥X
hX : ¬∃ S, X = Spec S
inst : JacobsonSpace ↥(Spec R)
i : X.affineCover.I₀
⊢ JacobsonSpace ↥(Scheme.Hom.opensRange (X.affineCover.f i))
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfinj : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
⊢ (Scheme.Hom.ker f).ideal ⟨⊤, ⋯⟩ = ⊥.ideal ⟨⊤, ⋯⟩

Tactic:
by simpa [f.ker_apply ⟨⊤, isAffineOpen_top Y⟩, ← RingHom.injective_iff_ker_eq_bot]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
hf : Function.Injective ⇑f
⊢ diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤

Tactic:
by
  rw [← top_le_iff]
  rintro x -
  simp only [diagonalCoverDiagonalRange, openCoverOfBase_I₀, openCoverOfBase_X,
    openCoverOfLeftRight_I₀, Opens.iSup_mk, Opens.carrier_eq_coe, Hom.coe_opensRange, Opens.mem_mk,
    Set.mem_iUnion, Set.mem_range, Sigma.exists]
  have H : pullback.fst f f x = pullback.snd f f x :=
    hf (by rw [← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply, pullback.condition])
  let i := 𝒰.idx (f (pullback.fst f f x))
  obtain ⟨y : 𝒰.X i, hy : 𝒰.f i y = f _⟩ :=
    𝒰.covers (f (pullback.fst f f x))
  obtain ⟨z, hz₁, hz₂⟩ := exists_preimage_pullback _ _ hy.symm
  let j := (𝒱 i).idx z
  obtain ⟨w : (𝒱 i).X j, hy : (𝒱 i).f j w = z⟩ := (𝒱 i).covers z
  refine ⟨i, j, ?_⟩
  simp_rw [diagonalCover_map]
  change x ∈ Set.range _
  simp only [diagonalCover, openCoverOfBase_I₀,
    Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover, PreZeroHypercover.pullback₁_X,
    Precoverage.ZeroHypercover.bind_toPreZeroHypercover, openCoverOfBase_X,
    PreZeroHypercover.bind_X, openCoverOfLeftRight_I₀, openCoverOfLeftRight_X]
  rw [range_map]
  simp [← H, ← hz₁, ← hy]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
φ : S →+* T
ψ : R →+* S
⊢ map (φ.comp ψ) = map φ ∘ map ψ

Tactic:
by
  ext : 1; simp [map_comp]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : ∀ (i : 𝒰.I₀) (j : (𝒱 i).I₀), IsAffine ((𝒱 i).X j)
U : (i : 𝒰.I₀) × (𝒱 i).I₀ → (↑(diagonalCoverDiagonalRange f 𝒰 𝒱)).Opens :=
  fun i ↦ (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ⁻¹ᵁ Hom.opensRange ((diagonalCover f 𝒰 𝒱).f ⟨i.fst, (i.snd, i.snd)⟩)
hU :
  ∀ (i : (i : 𝒰.I₀) × (𝒱 i).I₀),
    (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ''ᵁ U i = Hom.opensRange ((diagonalCover f 𝒰 𝒱).f ⟨i.fst, (i.snd, i.snd)⟩)
hf : iSup U = ⊤
⊢ ∀ (i : (i : 𝒰.I₀) × (𝒱 i).I₀), IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱 ∣_ U i)

Tactic:
intro i

Goal state after:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : ∀ (i : 𝒰.I₀) (j : (𝒱 i).I₀), IsAffine ((𝒱 i).X j)
U : (i : 𝒰.I₀) × (𝒱 i).I₀ → (↑(diagonalCoverDiagonalRange f 𝒰 𝒱)).Opens :=
  fun i ↦ (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ⁻¹ᵁ Hom.opensRange ((diagonalCover f 𝒰 𝒱).f ⟨i.fst, (i.snd, i.snd)⟩)
hU :
  ∀ (i : (i : 𝒰.I₀) × (𝒱 i).I₀),
    (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ''ᵁ U i = Hom.opensRange ((diagonalCover f 𝒰 𝒱).f ⟨i.fst, (i.snd, i.snd)⟩)
hf : iSup U = ⊤
i : (i : 𝒰.I₀) × (𝒱 i).I₀
⊢ IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱 ∣_ U i)
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : IsClosedImmersion f
hf : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
⊢ (Scheme.Hom.ker f).ideal ⟨⊤, ⋯⟩ = ⊥.ideal ⟨⊤, ⋯⟩

Tactic:
by simpa [f.ker_apply ⟨⊤, isAffineOpen_top Y⟩, ← RingHom.injective_iff_ker_eq_bot]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R S✝
ι : Type u_3
inst✝³ : Finite ι
S : ι → Type u_4
inst✝² : (i : ι) → CommRing (S i)
inst✝¹ : (i : ι) → Algebra R (S i)
inst✝ : ∀ (i : ι), FinitePresentation R (S i)
⊢ FinitePresentation R ((a : ι) → S a)

Tactic:
let (i : ι) : Algebra (Π a, S a) (S i) := (Pi.evalAlgHom R S i).toAlgebra

Goal state after:
R : Type u_1
S✝ : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R S✝
ι : Type u_3
inst✝³ : Finite ι
S : ι → Type u_4
inst✝² : (i : ι) → CommRing (S i)
inst✝¹ : (i : ι) → Algebra R (S i)
inst✝ : ∀ (i : ι), FinitePresentation R (S i)
this : (i : ι) → Algebra ((a : ι) → S a) (S i) := fun i ↦ (Pi.evalAlgHom R S i).toAlgebra
⊢ FinitePresentation R ((a : ι) → S a)
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: case inr
X Y : Scheme
inst✝ : Subsingleton ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this : ∀ {X Y : Scheme} [Subsingleton ↥Y] (f : X ⟶ Y) (g : Y ⟶ X), g ≫ f = 𝟙 Y → (∃ R, X = Spec R) → IsClosedImmersion g
hX : ¬∃ R, X = Spec R
⊢ ∀ (i : X.affineCover.toPreZeroHypercover.1), IsClosedImmersion (Scheme.Cover.pullbackHom X.affineCover g i)

Tactic:
intro i

Goal state after:
case inr
X Y : Scheme
inst✝ : Subsingleton ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this : ∀ {X Y : Scheme} [Subsingleton ↥Y] (f : X ⟶ Y) (g : Y ⟶ X), g ≫ f = 𝟙 Y → (∃ R, X = Spec R) → IsClosedImmersion g
hX : ¬∃ R, X = Spec R
i : X.affineCover.toPreZeroHypercover.1
⊢ IsClosedImmersion (Scheme.Cover.pullbackHom X.affineCover g i)
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case mpr.hS'
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
hCNoeth : ∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)
fS : 𝒰.I₀ → ↑X.affineOpens := ⋯
⊢ ∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(X, ↑(fS i))

Tactic:
intro i

Goal state after:
case mpr.hS'
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
hCNoeth : ∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)
fS : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
i : 𝒰.I₀
⊢ IsNoetherianRing ↑Γ(X, ↑(fS i))
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: case refine_2
X : Scheme
𝒰 : X.OpenCover
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian (𝒰.X i)
⊢ DiscreteTopology ↥X

Tactic:
refine discreteTopology_iff_isOpen_singleton.mpr fun x ↦ ?_
    obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x
    simpa using (𝒰.f i).isOpenEmbedding.isOpenMap _ (isOpen_discrete {x})

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case mpr.convert_3
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
h : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
⊢ ∀ (i : ι), IsCompact (S i).1.carrier

Tactic:
intro i

Goal state after:
case mpr.convert_3
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
h : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
i : ι
⊢ IsCompact (S i).1.carrier
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
inst✝ : IsNoetherian X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
⊢ ∀ (i : 𝒰.I₀), NoetherianSpace ↑(Set.range ⇑(𝒰.f i))

Tactic:
intro i

Goal state after:
X : Scheme
inst✝ : IsNoetherian X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
i : 𝒰.I₀
⊢ NoetherianSpace ↑(Set.range ⇑(𝒰.f i))
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
⊢ IsNoetherian (Spec (CommRingCat.of R))

Tactic:
by
  suffices IsNoetherianRing (CommRingCat.of R) by infer_instance
  assumption

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced

Goal state before:
pp: x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ GeometricallyReduced x✝ ↔ geometrically IsReduced x✝

Tactic:
exact geometricallyReduced_iff _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝³ : GeometricallyReduced f
inst✝² : Flat f
inst✝¹ : IsReduced Y
inst✝ : IsLocallyNoetherian Y
⊢ ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀),
    IsReduced ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)

Tactic:
intro i

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝³ : GeometricallyReduced f
inst✝² : Flat f
inst✝¹ : IsReduced Y
inst✝ : IsLocallyNoetherian Y
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
⊢ IsReduced ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
hf : GeneralizingMap ⇑f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f],
    GeneralizingMap ⇑f →
      (∃ R, Y = Spec R) → topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hY : ¬∃ R, Y = Spec R
⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap)
      (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
intro i

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
hf : GeneralizingMap ⇑f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f],
    GeneralizingMap ⇑f →
      (∃ R, Y = Spec R) → topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap)
    (Scheme.Cover.pullbackHom Y.affineCover f i)
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: case inr
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFinitePresentation f
hf : GeneralizingMap ⇑f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f],
    GeneralizingMap ⇑f →
      (∃ S, X = Spec S) → topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hX : ¬∃ S, X = Spec S
⊢ ∀ (i : X.affineCover.I₀),
    topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) (X.affineCover.f i ≫ f)

Tactic:
intro i

Goal state after:
case inr
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFinitePresentation f
hf : GeneralizingMap ⇑f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f],
    GeneralizingMap ⇑f →
      (∃ S, X = Spec S) → topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hX : ¬∃ S, X = Spec S
i : X.affineCover.I₀
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) (X.affineCover.f i ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: X Y Z S : Scheme
⊢ HasAffineProperty (@IsIntegralHom) (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ RingHom.IsIntegral)

Tactic:
rw [HasAffineProperty.affineAnd_iff _ RingHom.isIntegral_respectsIso
    RingHom.isIntegral_isStableUnderBaseChange.localizationPreserves.away
    RingHom.isIntegral_ofLocalizationSpan]

Goal state after:
X Y Z S : Scheme
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y),
    IsIntegralHom f ↔
      IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → (CommRingCat.Hom.hom (Scheme.Hom.app f U)).IsIntegral
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₀), t ∈ (Opens.comap { toFun := comap φ, continuous_toFun := ⋯ }) (Ti i) → p z ∉ U i

Tactic:
intro i

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₀
⊢ t ∈ (Opens.comap { toFun := comap φ, continuous_toFun := ⋯ }) (Ti i) → p z ∉ U i
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:
intro i

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.AffineSpace

Goal state before:
pp: n : Type u
S X : Scheme
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
intro i

Goal state after:
n : Type u
S X : Scheme
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : n
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case hX
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ ∀ (i : n),
    (CommRingCat.Hom.hom
          (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)) ≫
            Scheme.Hom.app
              (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
                (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))
              ⊤))
        (X i) =
      (CommRingCat.Hom.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) (X i)

Tactic:
intro i

Goal state after:
case hX
n : Type u
S : Scheme
inst✝ : IsAffine S
i : n
⊢ (CommRingCat.Hom.hom
        (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)) ≫
          Scheme.Hom.app
            (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
              (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))
            ⊤))
      (X i) =
    (CommRingCat.Hom.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) (X i)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case inr
n : Type u
S : Scheme
this : ∀ {n : Type u} (S : Scheme), (∃ R, S = Spec R) → topologically (@IsOpenMap) (𝔸(n; S) ↘ S)
hS : ¬∃ R, S = Spec R
⊢ ∀ (i : S.affineCover.toPreZeroHypercover.1),
    topologically (@IsOpenMap) (Scheme.Cover.pullbackHom S.affineCover (𝔸(n; S) ↘ S) i)

Tactic:
intro i

Goal state after:
case inr
n : Type u
S : Scheme
this : ∀ {n : Type u} (S : Scheme), (∃ R, S = Spec R) → topologically (@IsOpenMap) (𝔸(n; S) ↘ S)
hS : ¬∃ R, S = Spec R
i : S.affineCover.toPreZeroHypercover.1
⊢ topologically (@IsOpenMap) (Scheme.Cover.pullbackHom S.affineCover (𝔸(n; S) ↘ S) i)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case inr
n : Type u
S : Scheme
h : IsReduced S
this : ∀ {n : Type u} (S : Scheme) [h : IsReduced S], (∃ R, S = Spec R) → IsReduced 𝔸(n; S)
hS : ¬∃ R, S = Spec R
⊢ ∀ (i : (Precoverage.ZeroHypercover.pullback₁ (𝔸(n; S) ↘ S) S.affineCover).I₀),
    IsReduced ((Precoverage.ZeroHypercover.pullback₁ (𝔸(n; S) ↘ S) S.affineCover).X i)

Tactic:
intro i

Goal state after:
case inr
n : Type u
S : Scheme
h : IsReduced S
this : ∀ {n : Type u} (S : Scheme) [h : IsReduced S], (∃ R, S = Spec R) → IsReduced 𝔸(n; S)
hS : ¬∃ R, S = Spec R
i : (Precoverage.ZeroHypercover.pullback₁ (𝔸(n; S) ↘ S) S.affineCover).I₀
⊢ IsReduced ((Precoverage.ZeroHypercover.pullback₁ (𝔸(n; S) ↘ S) S.affineCover).X i)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n✝ : Type u
S : Scheme
n : Type u
R : CommRingCat
h : IsIntegralHom (𝔸(n; Spec R) ↘ Spec R)
h✝ : Nonempty ↥(Spec R)
this : Nontrivial ↑R
⊢ ∀ (a : n), False

Tactic:
intro i

Goal state after:
n✝ : Type u
S : Scheme
n : Type u
R : CommRingCat
h : IsIntegralHom (𝔸(n; Spec R) ↘ Spec R)
h✝ : Nonempty ↥(Spec R)
this : Nontrivial ↑R
i : n
⊢ False
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case mpr
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : Zero Y
inst✝ : T1Space X
D : locallyFinsuppWithin U Y
x : X
hx : x ∉ {x | D x = 0} ∧ x ∈ U
⊢ x ∈ D.support

Tactic:
mem_ofPred_eq

Goal state after:
case mpr
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : Zero Y
inst✝ : T1Space X
D : locallyFinsuppWithin U Y
x : X
hx : ¬D x = 0 ∧ x ∈ U
⊢ x ∈ D.support
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: case refine_1
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
hUST : UT ≤ f ⁻¹ᵁ US
UY : Y.Opens
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
hUSX : iSup VX ≤ iX ⁻¹ᵁ US
hUY : UY = g ⁻¹ᵁ iSup VX ⊓ iY ⁻¹ᵁ UT
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
⊢ ∀ (i : CategoryTheory.Pairwise ι), D.obj i ≤ iSup VX

Tactic:
rintro (i | ⟨i, j⟩)

Goal state after:
case refine_1.single
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
hUST : UT ≤ f ⁻¹ᵁ US
UY : Y.Opens
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
hUSX : iSup VX ≤ iX ⁻¹ᵁ US
hUY : UY = g ⁻¹ᵁ iSup VX ⊓ iY ⁻¹ᵁ UT
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
i : ι
⊢ D.obj (Pairwise.single i) ≤ iSup VX

case refine_1.pair
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
hUST : UT ≤ f ⁻¹ᵁ US
UY : Y.Opens
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
hUSX : iSup VX ≤ iX ⁻¹ᵁ US
hUY : UY = g ⁻¹ᵁ iSup VX ⊓ iY ⁻¹ᵁ UT
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
i j : ι
⊢ D.obj (Pairwise.pair i j) ≤ iSup VX
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
inst✝ : IsLocallyNoetherian X
this : ∀ (R : CommRingCat), IsNoetherianRing ↑R → (Spec R).IsGermInjective
⊢ X.IsGermInjective

Tactic:
refine @Scheme.IsGermInjective.of_openCover _ (X.affineOpenCover.openCover) (fun i ↦ this _ ?_)
    exact isLocallyNoetherian_Spec.mp
      (isLocallyNoetherian_of_isOpenImmersion (X.affineOpenCover.f i))

Goal state after:
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y S : Scheme
f✝ : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R✝ A : CommRingCat
inst✝ : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing ↑R
I : Ideal ↑R
hI : I.IsPrime
J : Ideal ↑R := RingHom.ker (algebraMap (↑R) (Localization.AtPrime I))
hJ : ∀ (x : ↑R), x ∈ J ↔ ∃ y, ↑y * x = 0
f : (x : ↑R) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : ↑R) (a : x ∈ J), ↑(f x a) * x = 0
s : Finset ↑R
hs : Ideal.span ↑s = J
hs' : ↑s ⊆ ↑J
x y : ↑R
e : y * x = 0
hy : y ∉ I
⊢ ↑s ⊆ ↑(↑R ∙ ↑(∏ x ∈ s.attach, f ↑x ⋯)).annihilator

Tactic:
intro i

Goal state after:
X Y S : Scheme
f✝ : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R✝ A : CommRingCat
inst✝ : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing ↑R
I : Ideal ↑R
hI : I.IsPrime
J : Ideal ↑R := RingHom.ker (algebraMap (↑R) (Localization.AtPrime I))
hJ : ∀ (x : ↑R), x ∈ J ↔ ∃ y, ↑y * x = 0
f : (x : ↑R) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : ↑R) (a : x ∈ J), ↑(f x a) * x = 0
s : Finset ↑R
hs : Ideal.span ↑s = J
hs' : ↑s ⊆ ↑J
x y : ↑R
e : y * x = 0
hy : y ∉ I
i : ↑R
⊢ i ∈ ↑s → i ∈ ↑(↑R ∙ ↑(∏ x ∈ s.attach, f ↑x ⋯)).annihilator