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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN : ∀ (s : ↥S), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s ↦ algebraMap R (Localization.Away s)
suitableN : R → Set ℕ := fun s ↦ {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}
minN : R → ℕ := fun s ↦ sInf (suitableN s)
hSuit : ∀ (s : ↥S), minN ↑s ∈ suitableN ↑s
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → I n = I m

Tactic:
let N := Finset.sup S minN

Goal state after:
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN : ∀ (s : ↥S), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s ↦ algebraMap R (Localization.Away s)
suitableN : R → Set ℕ := fun s ↦ {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}
minN : R → ℕ := fun s ↦ sInf (suitableN s)
hSuit : ∀ (s : ↥S), minN ↑s ∈ suitableN ↑s
N : ℕ := S.sup minN
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → I n = I m
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 (Cover.pullbackHom Y.affineCover f i ≫ Y.affineCover.f i).base) ''
      ⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s

Tactic:
Cover.pullbackHom_map,

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 ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i ≫ f).base) ''
      ⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
⊢ x ∈ comap C '' ↑(basicOpen f) ↔ ∃ i, f.coeff i ∉ x.asIdeal

Tactic:
trans f.map (algebraMap R x.asIdeal.ResidueField) ≠ 0

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
⊢ x ∈ comap C '' ↑(basicOpen f) ↔ map (algebraMap R x.asIdeal.ResidueField) f ≠ 0

R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
⊢ map (algebraMap R x.asIdeal.ResidueField) f ≠ 0 ↔ ∃ i, f.coeff i ∉ x.asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
⊢ x ∈ comap C '' ↑(basicOpen f) ↔ ∃ i, coeff i f ∉ x.asIdeal

Tactic:
trans f.map (algebraMap R x.asIdeal.ResidueField) ≠ 0

Goal state after:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
⊢ x ∈ comap C '' ↑(basicOpen f) ↔ (map (algebraMap R x.asIdeal.ResidueField)) f ≠ 0

R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
⊢ (map (algebraMap R x.asIdeal.ResidueField)) f ≠ 0 ↔ ∃ i, coeff i f ∉ x.asIdeal
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsLocallyNoetherian Y
hY : ∃ R, Y = Spec R
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] [IsLocallyNoetherian Y],
    (∃ R, Y = Spec R) → (∃ S, X = Spec S) → id (IsLocallyNoetherian X)
hX : ¬∃ S, X = Spec S
⊢ id (IsLocallyNoetherian X)

pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsLocallyNoetherian Y
hY : ∃ R, Y = Spec R
hX : ∃ S, X = Spec S
⊢ id (IsLocallyNoetherian X)

Tactic:
· exact (isLocallyNoetherian_iff_openCover X.affineCover).mpr
      fun i ↦ this (X.affineCover.f i ≫ f) hY ⟨_, rfl⟩

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsLocallyNoetherian Y
hY : ∃ R, Y = Spec R
hX : ∃ S, X = Spec S
⊢ id (IsLocallyNoetherian X)
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsStableUnderComposition @UniversallyOpen

Tactic:
rw [eq]
  infer_instance

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

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

Tactic:
constructor
  intro X' Y' i₁ i₂ f' H
  have := UniversallyClosed.universally_isClosedMap _ _ _
    ((IsPullback.of_hasPullback i₁ f).paste_horiz H)
  exact IsClosedMap.of_comp_surjective (MorphismProperty.pullback_fst (P := @Surjective) _ _ ‹_›).1
    (Scheme.Hom.continuous _) this

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

Goal state before:
pp: R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] x ↦ x.IsIntegral) (Localization.awayMap f ↑r)
r : S
this✝² : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this✝¹ : Algebra (Localization.Away t) (Localization.Away (f t)) := (Localization.awayMap f t).toAlgebra
this✝ : IsScalarTower R (Localization.Away t) (Localization.Away (f t))
this : _root_.IsIntegral (Localization.Away t) ((algebraMap S (Localization.Away (f t))) r)
n m : ℕ
hp : Monic 1
e : ↑⟨(algebraMap R S) t ^ m, ⋯⟩ * eval₂ (algebraMap R S) ((algebraMap R S) ↑⟨(fun x ↦ t ^ x) n, ⋯⟩ * r) 1 = 0
hp' : ¬1 ≤ natDegree 1
⊢ ↑⟨t, ht⟩ ^ m • r ∈ Subalgebra.toSubmodule (integralClosure R S)

Tactic:
simp [Algebra.smul_def, show algebraMap R S t ^ m = 0 by simpa using e]

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

Goal state before:
pp: 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
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
ι : Type u_1
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
this : ∀ (i : ι), VX i ≤ iX ⁻¹ᵁ US
algInst✝¹ : Algebra ↑Γ(S, US) ↑Γ(X, UX) := (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).toAlgebra
algInst✝ : Algebra ↑Γ(S, US) ↑Γ(T, UT) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).toAlgebra
algebraizeInst✝ : Module.Flat ↑Γ(S, US) ↑Γ(T, UT)
⊢ Mono (pushoutSection H hUST hUSX hUY)

Tactic:
let (i : _) := (iX.appLE US (VX i) (by aesop)).hom.toAlgebra

Goal state after:
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
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
ι : Type u_1
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
this✝ : ∀ (i : ι), VX i ≤ iX ⁻¹ᵁ US
algInst✝¹ : Algebra ↑Γ(S, US) ↑Γ(X, UX) := (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).toAlgebra
algInst✝ : Algebra ↑Γ(S, US) ↑Γ(T, UT) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).toAlgebra
algebraizeInst✝ : Module.Flat ↑Γ(S, US) ↑Γ(T, UT)
this : (i : ι) → Algebra ↑Γ(S, US) ↑Γ(X, VX i) :=
  fun i ↦ (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US (VX i) ⋯)).toAlgebra
⊢ Mono (pushoutSection H hUST hUSX hUY)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected

Goal state before:
pp: I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cone F
cG : Cone G
f : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
g : s.pt ⟶ cF.pt
hg : ∀ (j : I), g ≫ cF.π.app j = s.π.app j
⊢ ∀ (j : I),
    (g ≫ f.hom) ≫ cG.π.app j =
      (⋯.lift (s.π.app (Classical.arbitrary I)) (hcG.lift ((Cone.postcompose α).obj s)) ⋯ ≫ f.hom) ≫ cG.π.app j

Tactic:
simp [reassoc_of% hg]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
h : Function.Injective (F.descColimitType c)
⊢ ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
    c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'

Tactic:
j

Goal state after:
case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
h : Function.Injective (F.descColimitType c)
j : J
⊢ ∀ (j' : J) (x : F.obj j) (x' : F.obj j'),
    c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
h :
  ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
    c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
⊢ ∀ (j : J) (x x' : F.obj j),
    c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x'

Tactic:
j

Goal state after:
case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
h :
  ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
    c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
j : J
⊢ ∀ (x x' : F.obj j),
    c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x'
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
h :
  ∀ (j : J) (x x' : F.obj j),
    c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x'
⊢ ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
    c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'

Tactic:
j

Goal state after:
case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
h :
  ∀ (j : J) (x x' : F.obj j),
    c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x'
j : J
⊢ ∀ (j' : J) (x : F.obj j) (x' : F.obj j'),
    c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case a
n : Type u
S : Scheme
inst✝ : IsEmpty n
⊢ IsAffine (Spec ℤ[n]) ∧ isomorphisms CommRingCat (Scheme.Hom.appTop (Spec.map (CommRingCat.ofHom C)))

Tactic:
← arrow_mk_iso_iff (isomorphisms _) (arrowIsoΓSpecOfIsAffine _)

Goal state after:
case a
n : Type u
S : Scheme
inst✝ : IsEmpty n
⊢ IsAffine (Spec ℤ[n]) ∧ isomorphisms CommRingCat (CommRingCat.ofHom C)
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ IsFractionRing ↑R ↑(Spec R).functionField

Tactic:
convert! StructureSheaf.IsLocalization.to_stalk R (genericPoint (Spec R))

Goal state after:
X : Scheme
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ IsFractionRing ↑R ↑(Spec R).functionField ↔
    IsLocalization.AtPrime (↑((Spec.structureSheaf ↑R).presheaf.stalk (genericPoint ↥(Spec R))))
      (genericPoint ↥(Spec R)).asIdeal
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
⊢ Nonempty ↥c.pt

Tactic:
cases isEmpty_or_nonempty I

Goal state after:
case inl
I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
h✝ : IsEmpty I
⊢ Nonempty ↥c.pt

case inr
I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
h✝ : Nonempty I
⊢ Nonempty ↥c.pt
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
h✝ : Nonempty I
i : I
this✝⁴ : IsCofiltered I
𝒰 : (D.obj i).OpenCover := (D.obj i).affineCover.finiteSubcover
this✝³ : ∀ (i' : 𝒰.I₀), IsAffine (𝒰.X i')
j : 𝒰.I₀
H : ∀ {i' : I} (f : i' ⟶ i), Nonempty ↥((Precoverage.ZeroHypercover.pullback₁ (D.map f) 𝒰).X j)
F : Over i ⥤ Scheme := Over.post D ⋙ Over.pullback (𝒰.f j) ⋙ Over.forget (𝒰.X j)
this✝² : ∀ (i' : Over i), IsAffine (F.obj i')
this✝¹ : ∀ (i' : Over i), Nonempty ↥(F.obj i')
e : F ⟶ (F ⋙ Γ.rightOp) ⋙ Scheme.Spec := F.whiskerLeft ΓSpec.adjunction.unit
this✝ : ∀ (i_1 : Over i), IsIso (e.app i_1)
this : IsIso e
c' : LimitCone F :=
  { cone := (Cone.postcompose (asIso e).inv).obj (Scheme.Spec.mapCone (limit.cone (F ⋙ Γ.rightOp))),
    isLimit :=
      (IsLimit.postcomposeInvEquiv (asIso e) (Scheme.Spec.mapCone (limit.cone (F ⋙ Γ.rightOp)))).symm
        (isLimitOfPreserves Scheme.Spec (limit.isLimit (F ⋙ Γ.rightOp))) }
⊢ Nonempty ↥c'.cone.pt

Tactic:
apply +allowSynthFailures PrimeSpectrum.instNonemptyOfNontrivial

Goal state after:
I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
h✝ : Nonempty I
i : I
this✝⁴ : IsCofiltered I
𝒰 : (D.obj i).OpenCover := ⋯
this✝³ : ∀ (i' : 𝒰.I₀), IsAffine (𝒰.X i')
j : 𝒰.I₀
H : ∀ {i' : I} (f : i' ⟶ i), Nonempty ↥((Precoverage.ZeroHypercover.pullback₁ (D.map f) 𝒰).X j)
F : Over i ⥤ Scheme := ⋯
this✝² : ∀ (i' : Over i), IsAffine (F.obj i')
this✝¹ : ∀ (i' : Over i), Nonempty ↥(F.obj i')
e : F ⟶ (F ⋙ Γ.rightOp) ⋙ Scheme.Spec := ⋯
this✝ : ∀ (i_1 : Over i), IsIso (e.app i_1)
this : IsIso e
c' : LimitCone F := ⋯
⊢ Nontrivial ↑(Opposite.unop (limit.cone (F ⋙ Γ.rightOp)).pt)
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.190} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : 𝒰.I₀
x : ↥(pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)))
iso : pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)) ≅ pullback f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) :=
  pullbackRightPullbackFstIso f (𝒰.f j) (pullback.fst f (𝒰.f i)) ≪≫
    pullback.congrHom ⋯ ⋯ ≪≫ pullbackAssoc f (𝒰.f i) (𝒰.f i) (𝒰.f j)
this :
  ∀ (k : 𝒰.I₀) (hki : k ⟶ i) (hkj : k ⟶ j),
    pullback.lift (pullback.map f (𝒰.f k) f (𝒰.f i) (𝟙 Y) (𝒰.trans hki) (𝟙 X) ⋯ ⋯)
        (pullback.map f (𝒰.f k) f (𝒰.f j) (𝟙 Y) (𝒰.trans hkj) (𝟙 X) ⋯ ⋯) ⋯ =
      pullback.map f (𝒰.f k) f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) (𝟙 Y)
          (pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯) (𝟙 X) ⋯ ⋯ ≫
        iso.inv
k : 𝒰.I₀
hki : k ⟶ i
hkj : k ⟶ j
yk : ↥(𝒰.X k)
hyk :
  (pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯) yk = (iso.hom ≫ pullback.snd f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)) x
⊢ x ∈
    Set.range
      ⇑(pullback.lift (pullback.map f (𝒰.f k) f (𝒰.f i) (𝟙 Y) (𝒰.trans hki) (𝟙 X) ⋯ ⋯)
          (pullback.map f (𝒰.f k) f (𝒰.f j) (𝟙 Y) (𝒰.trans hkj) (𝟙 X) ⋯ ⋯) ⋯)

Tactic:
rw [this, Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp, Pullback.range_map]

Goal state after:
P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.190} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : 𝒰.I₀
x : ↥(pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)))
iso : pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)) ≅ pullback f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) :=
  pullbackRightPullbackFstIso f (𝒰.f j) (pullback.fst f (𝒰.f i)) ≪≫
    pullback.congrHom ⋯ ⋯ ≪≫ pullbackAssoc f (𝒰.f i) (𝒰.f i) (𝒰.f j)
this :
  ∀ (k : 𝒰.I₀) (hki : k ⟶ i) (hkj : k ⟶ j),
    pullback.lift (pullback.map f (𝒰.f k) f (𝒰.f i) (𝟙 Y) (𝒰.trans hki) (𝟙 X) ⋯ ⋯)
        (pullback.map f (𝒰.f k) f (𝒰.f j) (𝟙 Y) (𝒰.trans hkj) (𝟙 X) ⋯ ⋯) ⋯ =
      pullback.map f (𝒰.f k) f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) (𝟙 Y)
          (pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯) (𝟙 X) ⋯ ⋯ ≫
        iso.inv
k : 𝒰.I₀
hki : k ⟶ i
hkj : k ⟶ j
yk : ↥(𝒰.X k)
hyk :
  (pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯) yk = (iso.hom ≫ pullback.snd f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)) x
⊢ x ∈
    ⇑iso.inv ''
      (⇑(pullback.fst f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)) ⁻¹' Set.range ⇑(𝟙 Y) ∩
        ⇑(pullback.snd f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)) ⁻¹'
          Set.range ⇑(pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯))
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰 : X.OpenCover
inst✝ : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis (Set.range fun i ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
⊢ ∃ k hki hkj y,
    (pullback.lift (IsOpenImmersion.lift (𝒰.f i) (𝒰.f k) ⋯) (IsOpenImmersion.lift (𝒰.f j) (𝒰.f k) ⋯) ⋯) y = x

Tactic:
have : (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x ∈
      (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i).opensRange := ⟨x, rfl⟩

Goal state after:
P : MorphismProperty Scheme
X : Scheme
𝒰 : X.OpenCover
inst✝ : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis (Set.range fun i ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this : (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x ∈ Hom.opensRange (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
⊢ ∃ k hki hkj y,
    (pullback.lift (IsOpenImmersion.lift (𝒰.f i) (𝒰.f k) ⋯) (IsOpenImmersion.lift (𝒰.f j) (𝒰.f k) ⋯) ⋯) y = x
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: S : Scheme
𝒰 : S.OpenCover
inst✝² : Category.{u_2, u_1} 𝒰.I₀
inst✝¹ : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝ : Quiver.IsThin 𝒰.I₀
i : 𝒰.I₀
⊢ ∀ {j : 𝒰.I₀} (hij : i ⟶ j), Function.Injective ⇑(d.functor.map hij)

Tactic:
j

Goal state after:
S : Scheme
𝒰 : S.OpenCover
inst✝² : Category.{u_2, u_1} 𝒰.I₀
inst✝¹ : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝ : Quiver.IsThin 𝒰.I₀
i j : 𝒰.I₀
⊢ ∀ (hij : i ⟶ j), Function.Injective ⇑(d.functor.map hij)
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case neg
R✝ : Type u_2
inst✝² : CommRing R✝
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
R₀✝ : Type u_1
R₀ : CommRing R₀✝
inst✝ : Algebra R₀✝ R
f : R[X]
M : Type u_2 := R[X] ⧸ Ideal.span {g.val i}
this✝ : Module.Free R M
this : Module.Finite R M
x : PrimeSpectrum R
j : Fin n
hij : ¬i = j
⊢ zeroLocus {g.val i} ⊆ Set.univ

Tactic:
exact Set.subset_univ _

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

Goal state before:
pp: case hP₃
R✝ : Type u_2
inst✝¹ : CommRing R✝
n : ℕ
R : Type u_2
inst✝ : CommRing R
c : InductionObj R n
i : Fin n
⊢ ∀ (j : Fin n),
    (c.val i).Monic →
      (c.val i).degree ≤ (c.val j).degree →
        i ≠ j →
          (∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
              Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }) →
            ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R], Statement R₀ R n c

Tactic:
j

Goal state after:
case hP₃
R✝ : Type u_2
inst✝¹ : CommRing R✝
n : ℕ
R : Type u_2
inst✝ : CommRing R
c : InductionObj R n
i j : Fin n
⊢ (c.val i).Monic →
    (c.val i).degree ≤ (c.val j).degree →
      i ≠ j →
        (∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
            Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }) →
          ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R], Statement R₀ R n c
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case refine_1.refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.129} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.129} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a : J
i : (𝒱 a).I₀
⊢ ∀ {j : (𝒱 a).I₀} (hij : i ⟶ j),
    Cover.trans (𝒱 a) hij ≫ ((d.cocone j).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor j =
      ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i

Tactic:
j

Goal state after:
case refine_1.refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.129} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.129} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a : J
i j : (𝒱 a).I₀
⊢ ∀ (hij : i ⟶ j),
    Cover.trans (𝒱 a) hij ≫ ((d.cocone j).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor j =
      ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i
Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact

Goal state before:
pp: S : Scheme
𝒰✝¹ 𝒰✝ : PreZeroHypercover S
K : Precoverage Scheme
X : Scheme
𝒰 : PreZeroHypercover X
inst✝¹ : QuasiCompactCover 𝒰
f : (x : 𝒰.I₀) → PreZeroHypercover (𝒰.X x)
inst✝ : ∀ (x : 𝒰.I₀), QuasiCompactCover (f x)
U : X.Opens
hU : IsAffineOpen U
⊢ IsCompactOpenCovered (fun x ↦ ⇑((𝒰.bind f).f x)) ↑U

Tactic:
obtain ⟨s, hs, V, hcV, hU⟩ := hU.isCompactOpenCovered 𝒰
    have (i) (hi) : IsCompactOpenCovered ((f i).f ·) (V i hi) :=
      isCompactOpenCovered_of_isCompact (f i) (hcV i hi)
    choose t ht W hcW hV using this
    have : Finite s := hs
    have (i) (hi) : Finite (t i hi) := ht i hi
    refine .of_finite (κ := Σ (i : s), t i.1 i.2) (fun p ↦ ⟨p.1, p.2⟩) (fun p ↦ W _ p.1.2 _ p.2.2)
      (fun p ↦ hcW ..) ?_
    simpa [← hV, Set.iUnion_sigma, Set.iUnion_subtype, Set.image_iUnion, Set.image_image] using! hU

Goal state after: