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
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:
cases hi₁

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

Goal state before:
pp: case refine_2
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
⊢ ∃ x, ¬(Function.update e.val j (e.val j %ₘ e.val i) x).degree = (ofLex e.degree).1 x

Tactic:
use j

Goal state after:
case h
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
⊢ ¬(Function.update e.val j (e.val j %ₘ e.val i) j).degree = (ofLex e.degree).1 j
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
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
⊢ Scheme.Hom.appLE iX US UX hUSX ≫ Scheme.Hom.appLE g UX UY ⋯ =
    Scheme.Hom.appLE f US UT hUST ≫ Scheme.Hom.appLE iY UT UY ⋯

Tactic:
simp only [Scheme.Hom.appLE_comp_appLE, H.w]

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
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsAffineOpen UX
⊢ IsIso (pushoutSection H hUST hUSX hUY)

Tactic:
by
  refine (isIso_pushoutSection_iff ..).mpr (IsPullback.of_map_of_faithful Scheme.Spec ?_).unop
  have : IsAffine _ := hUS
  have : IsAffine _ := hUT
  have : IsAffine _ := hUX
  have hUY' : IsAffineOpen UY :=
    .of_isIso (Scheme.Hom.isPullback_resLE H hUST hUSX hUY).isoPullback.hom
  exact .of_iso (Scheme.Hom.isPullback_resLE H hUST hUSX hUY).flip hUY'.isoSpec hUT.isoSpec
    hUX.isoSpec hUS.isoSpec (by simp) (by simp) (by simp) (by simp)

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S X : Scheme
f g : X ⟶ 𝔸(n; S)
h₁ : f ≫ 𝔸(n; S) ↘ S = g ≫ 𝔸(n; S) ↘ S
h₂ :
  ∀ (i : n),
    (ConcreteCategory.hom (Scheme.Hom.appTop f)) (coord S i) = (ConcreteCategory.hom (Scheme.Hom.appTop g)) (coord S i)
i : n
⊢ (toSpecMvPolyIntEquiv n) (f ≫ toSpecMvPoly n S) i = (toSpecMvPolyIntEquiv n) (g ≫ toSpecMvPoly n S) i

Tactic:
rw [toSpecMvPolyIntEquiv_comp, toSpecMvPolyIntEquiv_comp]

Goal state after:
n : Type u
S X : Scheme
f g : X ⟶ 𝔸(n; S)
h₁ : f ≫ 𝔸(n; S) ↘ S = g ≫ 𝔸(n; S) ↘ S
h₂ :
  ∀ (i : n),
    (ConcreteCategory.hom (Scheme.Hom.appTop f)) (coord S i) = (ConcreteCategory.hom (Scheme.Hom.appTop g)) (coord S i)
i : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop f)) ((toSpecMvPolyIntEquiv n) (toSpecMvPoly n S) i) =
    (ConcreteCategory.hom (Scheme.Hom.appTop g)) ((toSpecMvPolyIntEquiv n) (toSpecMvPoly n S) i)
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
n : ℕ
f : locallyFinsuppWithin U Y
x : X
⊢ (n • f)⁻ x = (n • f⁻) x

Tactic:
simp only [negPart, max_apply, coe_neg, coe_nsmul, Pi.neg_apply, Pi.smul_apply, coe_zero,
    Pi.zero_apply]

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
n : ℕ
f : locallyFinsuppWithin U Y
x : X
⊢ max (-(n • f x)) 0 = n • max (-f x) 0
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
D : locallyFinsupp X ℤ
h : 0 < D
z : X
hz : D z ≠ 0
e : X
he : e ≠ z
⊢ (single z 1) e ≤ D e

Tactic:
simpa [he, single_apply] using! h.le e

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
z : X
hz : z ∈ V
t : Set X
ht : t ∈ 𝓝 z ∧ (t ∩ D.support).Finite
⊢ ∃ t ∈ 𝓝 z, (t ∩ Function.support fun z ↦ if hz : z ∈ V then D z else 0).Finite

Tactic:
use t, ht.1

Goal state after:
case right
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
z : X
hz : z ∈ V
t : Set X
ht : t ∈ 𝓝 z ∧ (t ∩ D.support).Finite
⊢ (t ∩ Function.support fun z ↦ if hz : z ∈ V then D z else 0).Finite
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
i : ↑R
hi : i ∈ ↑s
⊢ ↑(f ↑⟨i, hi⟩ ⋯) • i = 0

Tactic:
smul_eq_mul

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
hi : i ∈ ↑s
⊢ ↑(f ↑⟨i, hi⟩ ⋯) * i = 0
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_2
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
y : ↥Y
e : sX x = sY y
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : sX x ∈ ↑U
hyU : sY y ∈ U
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ ↑V
iVU : ↑V ⊆ (sY ⁻¹ᵁ U).carrier
this :
  Scheme.Hom.appLE sY U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU
W : X.Opens
hxW : x ∈ W
φ' : Γ(Y, V) ⟶ Γ(X, W)
i : W ≤ sX ⁻¹ᵁ U
hW : IsAffineOpen W
h₁ : Y.presheaf.germ V y hyV ≫ φ = φ' ≫ X.presheaf.germ W x hxW
h₂ : Scheme.Hom.app sX U ≫ X.presheaf.map i.hom.op = Scheme.Hom.appLE sY U V iVU ≫ φ'
⊢ hW.fromSpec ≫ sX = hW.isoSpec.inv ≫ W.ι ≫ sX

Tactic:
IsAffineOpen.isoSpec_inv_ι_assoc

Goal state after:
case refine_2
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
y : ↥Y
e : sX x = sY y
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : sX x ∈ ↑U
hyU : sY y ∈ U
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ ↑V
iVU : ↑V ⊆ (sY ⁻¹ᵁ U).carrier
this :
  Scheme.Hom.appLE sY U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU
W : X.Opens
hxW : x ∈ W
φ' : Γ(Y, V) ⟶ Γ(X, W)
i : W ≤ sX ⁻¹ᵁ U
hW : IsAffineOpen W
h₁ : Y.presheaf.germ V y hyV ≫ φ = φ' ≫ X.presheaf.germ W x hxW
h₂ : Scheme.Hom.app sX U ≫ X.presheaf.map i.hom.op = Scheme.Hom.appLE sY U V iVU ≫ φ'
⊢ hW.fromSpec ≫ sX = hW.fromSpec ≫ sX
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: case H
X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
g : Y.PartialMap Z
⊢ ((f.restrict U hU hU').comp g).hom =
    (X.isoOfEq ⋯).hom ≫ ((f.comp g).restrict (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain ⊓ U) ⋯ ⋯).hom

Tactic:
· simp [morphismRestrict_comp, isoImage_ι_inv_morphismRestrict_homOfLE_assoc, isoOfEq_hom]

Goal state after:
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: case refine_1.refine_2
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
U : Set S
x✝ : IsCompactOpenCovered f U
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hU : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
⊢ IsCompact { carrier := s.sigma fun i ↦ if h : i ∈ s then ↑(V i h) else ∅, is_open' := ⋯ }.carrier

pp: case refine_1.refine_3
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
U : Set S
x✝ : IsCompactOpenCovered f U
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hU : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
⊢ (fun p ↦ f p.fst p.snd) '' { carrier := s.sigma fun i ↦ if h : i ∈ s then ↑(V i h) else ∅, is_open' := ⋯ }.carrier = U

Tactic:
· dsimp only
      exact Set.isCompact_sigma hs fun i ↦ (by simp_all)

Goal state after:
case refine_1.refine_3
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
U : Set S
x✝ : IsCompactOpenCovered f U
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hU : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
⊢ (fun p ↦ f p.fst p.snd) '' { carrier := s.sigma fun i ↦ if h : i ∈ s then ↑(V i h) else ∅, is_open' := ⋯ }.carrier = U
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
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {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✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : ¬c.val i = 1
⊢ (coeffSubmodule R₀ c ^ (c.val j).degree.succ) ^ c'.degBound ^ c'.degBound ≤
    coeffSubmodule R₀ c ^ c.degBound ^ c.degBound

Tactic:
← pow_mul

Goal state after:
case neg
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {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✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : ¬c.val i = 1
⊢ coeffSubmodule R₀ c ^ ((c.val j).degree.succ * c'.degBound ^ c'.degBound) ≤
    coeffSubmodule R₀ c ^ c.degBound ^ c.degBound
Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact

Goal state before:
pp: case refine_2
S : Scheme
𝒰✝ 𝒰 : PreZeroHypercover S
K : Precoverage Scheme
inst✝ : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
U : S.Opens
hU : IsAffineOpen U
hsub : ⇑f '' ↑U' ⊆ ↑U
s : Set 𝒰.I₀
hf : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun x ↦ ↥(𝒰.X x)) i)
hc : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
heq : ⋃ i, ⋃ (h : i ∈ s), (fun x ↦ ⇑(𝒰.f x)) i '' ↑(V i h) = ↑U
x : ↥T
hx : x ∈ ↑U'
⊢ x ∈
    ⋃ i,
      ⋃ (h : i ∈ s),
        (fun x ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) i ''
          ↑((fun i hi ↦ pullback.fst f (𝒰.f i) ⁻¹ᵁ U' ⊓ pullback.snd f (𝒰.f i) ⁻¹ᵁ V i hi) i h)

Tactic:
have : f x ∈ (U : Set S) := hsub ⟨x, hx, rfl⟩

Goal state after:
case refine_2
S : Scheme
𝒰✝ 𝒰 : PreZeroHypercover S
K : Precoverage Scheme
inst✝ : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
U : S.Opens
hU : IsAffineOpen U
hsub : ⇑f '' ↑U' ⊆ ↑U
s : Set 𝒰.I₀
hf : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun x ↦ ↥(𝒰.X x)) i)
hc : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
heq : ⋃ i, ⋃ (h : i ∈ s), (fun x ↦ ⇑(𝒰.f x)) i '' ↑(V i h) = ↑U
x : ↥T
hx : x ∈ ↑U'
this : f x ∈ ↑U
⊢ x ∈
    ⋃ i,
      ⋃ (h : i ∈ s),
        (fun x ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) i ''
          ↑((fun i hi ↦ pullback.fst f (𝒰.f i) ⁻¹ᵁ U' ⊓ pullback.snd f (𝒰.f i) ⁻¹ᵁ V i hi) i h)
Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
⊢ ∃ 𝒱 f, Finite 𝒱.I₀ ∧ ∀ (j : 𝒱.cover.I₀), IsOpenImmersion (f.h₀ j)

Tactic:
obtain ⟨n, f, V, hV, h⟩ := QuasiCompactCover.exists_isAffineOpen_of_isCompact 𝒰.1
    (show IsCompact (⊤ : TopologicalSpace.Opens S).carrier from isCompact_univ)

Goal state after:
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
h : ⋃ i, ⇑(𝒰.f (f i)) '' ↑(V i) = ↑⊤
⊢ ∃ 𝒱 f, Finite 𝒱.I₀ ∧ ∀ (j : 𝒱.cover.I₀), IsOpenImmersion (f.h₀ j)
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case inl
I : Type u
inst✝⁴ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝³ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
a b : D.obj i ⟶ X
ha : t.app i = a ≫ f
hb : t.app i = b ≫ f
hab : c.π.app i ≫ a = c.π.app i ≫ b
this : ∀ (i : I), IsAffineHom (c.π.app i)
A : ExistsHomHomCompEqCompAux D t f :=
  { c := c, hc := hc, i := i, a := a, ha := ha, b := b, hb := hb, hab := hab, 𝒰S := S.affineCover, h𝒰S := ⋯,
    𝒰X := fun i ↦ ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i).affineCover, h𝒰X := ⋯ }
𝒰 : (pullback.diagonalObj f).OpenCover := Pullback.diagonalCover f A.𝒰S A.𝒰X
W : (pullback.diagonalObj f).Opens := Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
k : A.𝒰D.I₀ → I
hki' : (j : A.𝒰D.I₀) → k j ⟶ A.i'
heq :
  ∀ (j : A.𝒰D.I₀),
    (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.a =
      (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.b
𝒰Df : (D.obj A.i').OpenCover := A.𝒰D.finiteSubcover
h : IsEmpty ↥(D.obj A.i')
⊢ ∃ k hik, D.map hik ≫ a = D.map hik ≫ b

Tactic:
exact ⟨A.i', A.hii', isInitialOfIsEmpty.hom_ext _ _⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: 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_2} 𝒰.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_2} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
a : J
i : 𝒰.I₀
pf✝¹³ : ⊤.IsMultiplicative
pf✝¹² : ⊤.IsMultiplicative
pf✝¹¹ : HasPullback (D.obj a).hom (𝒰.f i)
pf✝¹⁰ : (precoverage IsOpenImmersion).IsStableUnderBaseChange
pf✝⁹ : ∀ (i : 𝒰.I₀), HasPullback (D.obj a).hom (𝒰.f i)
pf✝⁸ : ∀ (i : 𝒰.I₀), HasPullback (D.obj a).hom (𝒰.f i)
pf✝⁷ : ∀ (i : (Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰).I₀), P.HasPullbacksAlong (𝒰.f i)
pf✝⁶ : ∀ (i : (Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰).I₀), P.IsStableUnderBaseChangeAlong (𝒰.f i)
pf✝⁵ : ⊤.IsStableUnderBaseChange
pf✝⁴ : HasColimit d.relativeGluingData.functor
pf✝³ : ∀ {j : (Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰).I₀}, P.HasPullbacksAlong (𝒰.f j)
pf✝² : ∀ {j : (Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰).I₀}, P.IsStableUnderBaseChangeAlong (𝒰.f j)
h1 :
  ∀ {i j : (Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰).I₀} (hij : i ⟶ j),
    Cover.trans (Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰) hij ≫
        ((d.cocone j).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor j =
      ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i
h2 :
  ∀ (i : (Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰).I₀),
    (((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i) ≫
        Over.hom (((Functor.const J).obj d.glued).obj a).toComma =
      (Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰).f i ≫ Over.hom (D.obj a).toComma
pf✝¹ : P.HasPullbacksAlong (𝒰.f i)
pf✝ : P.IsStableUnderBaseChangeAlong (𝒰.f i)
𝒱 : (D.obj a).left.OpenCover := Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
⊢ pullback.fst (D.obj a).hom (𝒰.f i) ≫
      (OpenCover.glueMorphismsOverOfLocallyDirected (Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰)
          (fun i ↦ ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i) h1 h2).left =
    ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i

Tactic:
apply 𝒱.map_glueMorphismsOverOfLocallyDirected_left _ h1 h2

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
inst✝² : IsRegularEpiCategory D
F : C ⥤ D
inst✝¹ : F.PreservesEpimorphisms
inst✝ : HasPullbacks D
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : EffectiveEpi x✝¹
⊢ IsRegularEpi (F.map x✝¹)

Tactic:
apply IsRegularEpiCategory.regularEpiOfEpi

Goal state after:
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: X Y : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
⊢ IsRegularEpi π

Tactic:
have : Epi π := Flat.epi_of_flat_of_surjective _

Goal state after:
X Y : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
this : Epi π
⊢ IsRegularEpi π
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 : R
i : Fin n
e : InductionObj R n
he : c = (e.val i).leadingCoeff
⊢ c ≠ 0 →
    (∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ (Away c)],
        Statement R₀ (Away c) n
          { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val }) →
      (∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ (R ⧸ Ideal.span {c})],
          Statement R₀ (R ⧸ Ideal.span {c}) n { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val }) →
        ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R], Statement R₀ R n e

Tactic:
hc

Goal state after:
case hP₄
R✝ : Type u_2
inst✝¹ : CommRing R✝
n : ℕ
R : Type u_2
inst✝ : CommRing R
c : R
i : Fin n
e : InductionObj R n
he : c = (e.val i).leadingCoeff
hc : c ≠ 0
⊢ (∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ (Away c)],
      Statement R₀ (Away c) n
        { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val }) →
    (∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ (R ⧸ Ideal.span {c})],
        Statement R₀ (R ⧸ Ideal.span {c}) n { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val }) →
      ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R], Statement R₀ R n e