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

Goal state before:
pp: case mp.inr
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this✝¹ :
  HasRingHomProperty (affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
this✝ :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
    (RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ Q) →
      ∀ {X Y : Scheme} (f : X ⟶ Y),
        (HasRingHomProperty (affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q)
            fun {R S} [CommRing R] [CommRing S] ↦ Q) →
          IsAffineHom f →
            IsAffine Y →
              (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) →
                affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
hY : ¬IsAffine Y
h : ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
U : ↑Y.affineOpens
this : IsAffine ↑(f ⁻¹ᵁ ↑U)
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U).ι ''ᵁ ⊤)))

Tactic:
apply h

Goal state after:
case mp.inr
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this✝¹ :
  HasRingHomProperty (affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
this✝ :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
    (RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ Q) →
      ∀ {X Y : Scheme} (f : X ⟶ Y),
        (HasRingHomProperty (affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q)
            fun {R S} [CommRing R] [CommRing S] ↦ Q) →
          IsAffineHom f →
            IsAffine Y →
              (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) →
                affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
hY : ¬IsAffine Y
h : ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
U : ↑Y.affineOpens
this : IsAffine ↑(f ⁻¹ᵁ ↑U)
⊢ IsAffineOpen ((↑U).ι ''ᵁ ⊤)
Module: Mathlib.RingTheory.RingHom.Finite

Goal state before:
pp: ⊢ StableUnderComposition @Finite

Tactic:
introv R hf hg
  exact hg.comp hf

Goal state after:
Module: Mathlib.RingTheory.RingHom.FiniteType

Goal state before:
pp: ⊢ StableUnderComposition @FiniteType

Tactic:
introv R hf hg
  exact hg.comp hf

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

Goal state before:
pp: case hprecomp
X Y : Scheme
⊢ ∀ {Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z), IsClosedImmersion f → IsClosedImmersion (e.hom ≫ f)

Tactic:
Z

Goal state after:
case hprecomp
X Y Z : Scheme
⊢ ∀ (e : X ≅ Y) (f : Y ⟶ Z), IsClosedImmersion f → IsClosedImmersion (e.hom ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: case hpostcomp
X Y : Scheme
⊢ ∀ {Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y), IsClosedImmersion f → IsClosedImmersion (f ≫ e.hom)

Tactic:
Z

Goal state after:
case hpostcomp
X Y Z : Scheme
⊢ ∀ (e : Y ≅ Z) (f : X ⟶ Y), IsClosedImmersion f → IsClosedImmersion (f ≫ e.hom)
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
f : X ⟶ Y
h : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))

Tactic:
exact h

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
⊢ IsClosedImmersion (Scheme.Hom.toImage f ≫ Scheme.Hom.imageι f)

Tactic:
rw [Scheme.Hom.toImage_imageι]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
⊢ IsClosedImmersion f
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst✝¹ : IsClosedImmersion i₁
inst✝ : IsClosedImmersion i₂
f : Z₁ ⟶ Z₂
h : f ≫ i₂ = i₁
h' : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
f' : MorphismProperty.Over.mk ⊤ i₁ inst✝¹ ⟶ MorphismProperty.Over.mk ⊤ i₂ inst✝ :=
  MorphismProperty.Over.homMk f h True.intro
⊢ IsIso f'.op

Tactic:
← isIso_iff_of_reflects_iso _ (IsClosedImmersion.overEquivIdealSheafData X).functor

Goal state after:
Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst✝¹ : IsClosedImmersion i₁
inst✝ : IsClosedImmersion i₂
f : Z₁ ⟶ Z₂
h : f ≫ i₂ = i₁
h' : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
f' : MorphismProperty.Over.mk ⊤ i₁ inst✝¹ ⟶ MorphismProperty.Over.mk ⊤ i₂ inst✝ :=
  MorphismProperty.Over.homMk f h True.intro
⊢ IsIso ((overEquivIdealSheafData X).functor.map f'.op)
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsSeparated g
⊢ (pullback.fst f (𝟙 Y) ≫ pullback.lift (𝟙 X) f ⋯) ≫ (pullback.congrHom ⋯ ⋯).inv = pullback.mapDesc f (𝟙 Y) g

Tactic:
ext : 1

Goal state after:
case h₀
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsSeparated g
⊢ ((pullback.fst f (𝟙 Y) ≫ pullback.lift (𝟙 X) f ⋯) ≫ (pullback.congrHom ⋯ ⋯).inv) ≫ pullback.fst (f ≫ g) (𝟙 Y ≫ g) =
    pullback.mapDesc f (𝟙 Y) g ≫ pullback.fst (f ≫ g) (𝟙 Y ≫ g)

case h₁
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsSeparated g
⊢ ((pullback.fst f (𝟙 Y) ≫ pullback.lift (𝟙 X) f ⋯) ≫ (pullback.congrHom ⋯ ⋯).inv) ≫ pullback.snd (f ≫ g) (𝟙 Y ≫ g) =
    pullback.mapDesc f (𝟙 Y) g ≫ pullback.snd (f ≫ g) (𝟙 Y ≫ g)
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: case inst.refine_1
X✝ Y✝ Z : Scheme
f : X✝ ⟶ Y✝
X Y : Scheme
⊢ ∀ {Z : Scheme} (i : X ⟶ Y),
    MorphismProperty.isomorphisms Scheme i →
      ∀ (f : Y ⟶ Z),
        topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) f →
          topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) (i ≫ f)

Tactic:
Z

Goal state after:
case inst.refine_1
X✝ Y✝ Z✝ : Scheme
f : X✝ ⟶ Y✝
X Y Z : Scheme
⊢ ∀ (i : X ⟶ Y),
    MorphismProperty.isomorphisms Scheme i →
      ∀ (f : Y ⟶ Z),
        topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) f →
          topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) (i ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: case inst.refine_2
X✝ Y✝ Z : Scheme
f : X✝ ⟶ Y✝
X Y : Scheme
⊢ ∀ {Z : Scheme} (i : Y ⟶ Z),
    MorphismProperty.isomorphisms Scheme i →
      ∀ (f : X ⟶ Y),
        topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) f →
          topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) (f ≫ i)

Tactic:
Z

Goal state after:
case inst.refine_2
X✝ Y✝ Z✝ : Scheme
f : X✝ ⟶ Y✝
X Y Z : Scheme
⊢ ∀ (i : Y ⟶ Z),
    MorphismProperty.isomorphisms Scheme i →
      ∀ (f : X ⟶ Y),
        topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) f →
          topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) (f ≫ i)
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: case refine_2
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
H : IsPullback f' g' g f
hg : IsImmersion g
Z : Scheme := pullback f (Scheme.Hom.coborderRange g).ι
e : Y' ⟶ Z := pullback.lift g' (f' ≫ Scheme.Hom.liftCoborder g) ⋯
this : IsPullback e f' (pullback.snd f (Scheme.Hom.coborderRange g).ι) (Scheme.Hom.liftCoborder g)
⊢ IsClosedImmersion e

pp: case refine_1
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
H : IsPullback f' g' g f
hg : IsImmersion g
Z : Scheme := pullback f (Scheme.Hom.coborderRange g).ι
e : Y' ⟶ Z := pullback.lift g' (f' ≫ Scheme.Hom.liftCoborder g) ⋯
⊢ IsPullback (e ≫ pullback.fst f (Scheme.Hom.coborderRange g).ι) f' f
    (Scheme.Hom.liftCoborder g ≫ (Scheme.Hom.coborderRange g).ι)

Tactic:
· exact MorphismProperty.of_isPullback this.flip inferInstance

Goal state after:
case refine_1
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
H : IsPullback f' g' g f
hg : IsImmersion g
Z : Scheme := pullback f (Scheme.Hom.coborderRange g).ι
e : Y' ⟶ Z := pullback.lift g' (f' ≫ Scheme.Hom.liftCoborder g) ⋯
⊢ IsPullback (e ≫ pullback.fst f (Scheme.Hom.coborderRange g).ι) f' f
    (Scheme.Hom.liftCoborder g ≫ (Scheme.Hom.coborderRange g).ι)
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
⊢ prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom = pullback.diagonal (terminal.from X)

Tactic:
ext : 1

Goal state after:
case h₀
X Y Z : Scheme
f : X ⟶ Y
⊢ (prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom) ≫ pullback.fst (terminal.from X) (terminal.from X) =
    pullback.diagonal (terminal.from X) ≫ pullback.fst (terminal.from X) (terminal.from X)

case h₁
X Y Z : Scheme
f : X ⟶ Y
⊢ (prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom) ≫ pullback.snd (terminal.from X) (terminal.from X) =
    pullback.diagonal (terminal.from X) ≫ pullback.snd (terminal.from X) (terminal.from X)
Module: Mathlib.RingTheory.RingHom.FinitePresentation

Goal state before:
pp: ⊢ StableUnderComposition @FinitePresentation

Tactic:
introv R hf hg
  exact hg.comp hf

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ map (RingHom.id R) = id

Tactic:
ext : 1

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
x✝ : BasicConstructibleSetData R
⊢ map (RingHom.id R) x✝ = id x✝
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:
ext : 1

Goal state after:
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
x✝ : BasicConstructibleSetData R
⊢ map (φ.comp ψ) x✝ = (map φ ∘ map ψ) x✝
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u_4
inst✝ : CommRing R
s : Set (PrimeSpectrum R)
hs : StableUnderGeneralization s
hs' : IsConstructible s
⊢ IsOpen s

Tactic:
← isClosed_compl_iff

Goal state after:
R : Type u_4
inst✝ : CommRing R
s : Set (PrimeSpectrum R)
hs : StableUnderGeneralization s
hs' : IsConstructible s
⊢ IsClosed sᶜ
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
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, f a = 0
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective ⇑f'
t : Finset A := Finset.image (fun g ↦ (Ideal.Quotient.mk I) (g' g)) Finset.univ
ht : Ideal.span ↑t = ⊤
this : FinitePresentation R A
g : ↥t
r : S
hr : r ∈ s
hrr : (Ideal.Quotient.mk I) (g' ⟨r, hr⟩) = ↑g
⊢ FinitePresentation R (Localization.Away ↑⟨r, hr⟩)

Tactic:
apply h

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

Goal state before:
pp: X : Scheme
⊢ pullback.diagonal (terminal.from X) = prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom

Tactic:
ext : 1

Goal state after:
case h₀
X : Scheme
⊢ pullback.diagonal (terminal.from X) ≫ pullback.fst (terminal.from X) (terminal.from X) =
    (prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom) ≫ pullback.fst (terminal.from X) (terminal.from X)

case h₁
X : Scheme
⊢ pullback.diagonal (terminal.from X) ≫ pullback.snd (terminal.from X) (terminal.from X) =
    (prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom) ≫ pullback.snd (terminal.from X) (terminal.from X)
Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

Goal state before:
pp: case e'_3
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst✝¹ : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X},
    IsLocallyConstructible s → (∃ R, Y = Spec R) → IsLocallyConstructible (⇑f '' s)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
inst✝ : LocallyOfFinitePresentation (Cover.pullbackHom Y.affineCover f i)
inst : QuasiCompact (Cover.pullbackHom Y.affineCover f i)
e_1✝ : ↑↑(opensRange (Y.affineCover.f i)) = ↥↑(opensRange (Y.affineCover.f i))
⊢ ⇑f '' s ∩ ↑(opensRange (Y.affineCover.f i)) =
    ⇑((TopCat.Hom.hom f.base).comp
          (TopCat.Hom.hom ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i).base)) ''
      ⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s

Tactic:
ContinuousMap.coe_comp,

Goal state after:
case e'_3
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst✝¹ : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X},
    IsLocallyConstructible s → (∃ R, Y = Spec R) → IsLocallyConstructible (⇑f '' s)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
inst✝ : LocallyOfFinitePresentation (Cover.pullbackHom Y.affineCover f i)
inst : QuasiCompact (Cover.pullbackHom Y.affineCover f i)
e_1✝ : ↑↑(opensRange (Y.affineCover.f i)) = ↥↑(opensRange (Y.affineCover.f i))
⊢ ⇑f '' s ∩ ↑(opensRange (Y.affineCover.f i)) =
    ⇑(TopCat.Hom.hom f.base) ∘ ⇑(TopCat.Hom.hom ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i).base) ''
      ⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s
Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

Goal state before:
pp: X : Scheme
s : Set ↥X
hs : IsLocallyConstructible s
R : CommRingCat
f : X ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst✝¹ : QuasiCompact f
this :
  ∀ {X : Scheme} {s : Set ↥X},
    IsLocallyConstructible s →
      ∀ (R : CommRingCat) (f : X ⟶ Spec R) [hf : LocallyOfFinitePresentation f] [QuasiCompact f],
        (∃ S, X = Spec S) → IsLocallyConstructible (⇑f '' s)
hX : ¬∃ S, X = Spec S
inst✝ : CompactSpace ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
i : 𝒰.I₀
inst : QuasiCompact (𝒰.f i ≫ f)
⊢ ⇑(TopCat.Hom.hom f.base) '' (s ∩ ↑(opensRange (𝒰.f i))) =
    ⇑((TopCat.Hom.hom f.base).comp (TopCat.Hom.hom (𝒰.f i).base)) '' ⇑(𝒰.f i) ⁻¹' s

Tactic:
ContinuousMap.coe_comp,

Goal state after:
X : Scheme
s : Set ↥X
hs : IsLocallyConstructible s
R : CommRingCat
f : X ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst✝¹ : QuasiCompact f
this :
  ∀ {X : Scheme} {s : Set ↥X},
    IsLocallyConstructible s →
      ∀ (R : CommRingCat) (f : X ⟶ Spec R) [hf : LocallyOfFinitePresentation f] [QuasiCompact f],
        (∃ S, X = Spec S) → IsLocallyConstructible (⇑f '' s)
hX : ¬∃ S, X = Spec S
inst✝ : CompactSpace ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
i : 𝒰.I₀
inst : QuasiCompact (𝒰.f i ≫ f)
⊢ ⇑(TopCat.Hom.hom f.base) '' (s ∩ ↑(opensRange (𝒰.f i))) =
    ⇑(TopCat.Hom.hom f.base) ∘ ⇑(TopCat.Hom.hom (𝒰.f i).base) '' ⇑(𝒰.f i) ⁻¹' s
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case Kf
X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ ↑↑U ∩ (↑↑U ∩ ↑↑V) ⊆ Set.range ⇑(IsAffineOpen.fromSpec ⋯)

Tactic:
IsAffineOpen.range_fromSpec

Goal state after:
case Kf
X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ ↑↑U ∩ (↑↑U ∩ ↑↑V) ⊆ ↑↑U
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ ↑↑U ∩ ↑↑V ⊆ Set.range ⇑(IsAffineOpen.fromSpec ⋯)

Tactic:
IsAffineOpen.range_fromSpec

Goal state after:
X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ ↑↑U ∩ ↑↑V ⊆ ↑↑U
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
y : ↥Y
⊢ IsPullback
    (pullback.map snd (Y.fromSpecResidueField y) f (Z.fromSpecResidueField (g y)) fst
      (Spec.map (Scheme.Hom.residueFieldMap g y)) g ⋯ ⋯)
    (Scheme.Hom.fiberToSpecResidueField snd y) (Scheme.Hom.fiberToSpecResidueField f (g y))
    (Spec.map (Scheme.Hom.residueFieldMap g y))

Tactic:
by
  refine .of_right (h₁₂ := pullback.fst _ _) ?_ ?_
      (IsPullback.of_hasPullback f (Z.fromSpecResidueField (g y)))
  · simpa using! (IsPullback.of_hasPullback _ _).paste_horiz h
  · simp [Scheme.Hom.fiberToSpecResidueField]

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

Goal state before:
pp: P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
H : ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)
K : Type u
inst✝ : Field K
y : Spec (of K) ⟶ Y
⊢ ∀ ⦃Z : Scheme⦄ (fst : Z ⟶ X) (snd : Z ⟶ Spec (of K)), IsPullback fst snd f y → P Z

Tactic:
Z

Goal state after:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
H : ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)
K : Type u
inst✝ : Field K
y : Spec (of K) ⟶ Y
Z : Scheme
⊢ ∀ (fst : Z ⟶ X) (snd : Z ⟶ Spec (of K)), IsPullback fst snd f y → P Z
Module: Mathlib.AlgebraicGeometry.Noetherian

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

Tactic:
have : NoetherianSpace (S i) := by
        apply noetherianSpace_of_isAffineOpen (S i).1 (S i).2

Goal state after:
case mpr.convert_3.convert_3
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
h : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
i : ι
this : NoetherianSpace ↥↑↑(S i)
⊢ CompactSpace ↑(S i).1.carrier
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
x : ↥X
hx : ∀ i ∈ σ, x ∉ (U i).carrier
⊢ t' ∈ ⇑fT '' Z

Tactic:
obtain ⟨z, rfl, hzr⟩ := exists_preimage_pullback x t' (Subsingleton.elim (f x) (q t'))

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
⊢ t' ∈ ⇑fT '' Z
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

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

Tactic:
← universally_eq_iff (P := @UniversallyClosed).mpr inferInstance

Goal state after:
case a
⊢ universally @UniversallyClosed ≤ (topologically @SpecializingMap ⊓ @QuasiCompact).universally
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.IsQuotientMap ⇑f

Tactic:
Topology.isQuotientMap_iff

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

Goal state before:
pp: n : Type u
S X : Scheme
inst✝ : X.Over S
v : n → ↑Γ(X, ⊤)
⊢ (fun f i ↦ (ConcreteCategory.hom (Scheme.Hom.appTop ↑f)) (coord S i)) ((fun v ↦ ⟨homOfVector (X ↘ S) v, ⋯⟩) v) = v

Tactic:
by ext i; simp [-TopologicalSpace.Opens.map_top, homOfVector_appTop_coord]

Goal state after: