mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
q : Ideal ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
hq : q.IsPrime
hfq : (Ideal.Quotient.mk (Ideal.span s)) f ⊗ₜ[R] 1 ∉ q
this : ∀ a ∈ s, (Ideal.Quotient.mk (Ideal.span s)) a ⊗ₜ[R] 1 ∈ q
⊢ comap (algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)) { asIdeal := q, isPrime := hq } ∈ zeroLocus s

Tactic:
simpa [Set.subset_def]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
S : Set (Set (PrimeSpectrum R[X]))
hS : S ⊆ Set.range fun r ↦ ↑(basicOpen r)
hU : IsOpen (⋃₀ S)
t : Set (PrimeSpectrum R[X])
ht : t ∈ S
⊢ IsOpen (comap C '' t)

Tactic:
obtain ⟨r, rfl⟩ := hS ht

Goal state after:
R : Type u_1
inst✝ : CommRing R
S : Set (Set (PrimeSpectrum R[X]))
hS : S ⊆ Set.range fun r ↦ ↑(basicOpen r)
hU : IsOpen (⋃₀ S)
r : R[X]
ht : (fun r ↦ ↑(basicOpen r)) r ∈ S
⊢ IsOpen (comap C '' (fun r ↦ ↑(basicOpen r)) r)
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: X : Scheme
inst✝ : IsLocallyNoetherian X
h : topologicalKrullDim ↥X ≤ 0
U : ↑X.affineOpens
x✝ : IsNoetherianRing ↑Γ(X, ↑U)
⊢ IsArtinianRing ↑Γ(X, ↑U)

Tactic:
isArtinianRing_iff_krullDimLE_zero,

Goal state after:
X : Scheme
inst✝ : IsLocallyNoetherian X
h : topologicalKrullDim ↥X ≤ 0
U : ↑X.affineOpens
x✝ : IsNoetherianRing ↑Γ(X, ↑U)
⊢ Ring.KrullDimLE 0 ↑Γ(X, ↑U)
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun r ↦ ↑(basicOpen r)
hU : IsOpen (⋃₀ S)
t : Set (PrimeSpectrum (MvPolynomial σ R))
ht : t ∈ S
⊢ IsOpen (comap C '' t)

Tactic:
obtain ⟨r, rfl⟩ := hS ht

Goal state after:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun r ↦ ↑(basicOpen r)
hU : IsOpen (⋃₀ S)
r : MvPolynomial σ R
ht : (fun r ↦ ↑(basicOpen r)) r ∈ S
⊢ IsOpen (comap C '' (fun r ↦ ↑(basicOpen r)) r)
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
⊢ CompactSpace ↥X

Tactic:
have ht (i : 𝒰.I₀) : t ∈ Ti i := show ψ (.X i) ≠ 0 by simp [ψ]

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
⊢ CompactSpace ↥X
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mp.symm
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
x y x✝ y✝ : (j : J) × F.obj j
a✝ : Relation.EqvGen F.ColimitTypeRel x✝ y✝
k : J
f : x✝.fst ⟶ k
g : y✝.fst ⟶ k
h : (ConcreteCategory.hom (F.map f)) x✝.snd = (ConcreteCategory.hom (F.map g)) y✝.snd
⊢ ∃ k f g, (ConcreteCategory.hom (F.map f)) y✝.snd = (ConcreteCategory.hom (F.map g)) x✝.snd

Tactic:
exact ⟨k, g, f, h.symm⟩

Goal state after:
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)
⊢ IsEmpty n

Tactic:
have : Nontrivial R := (subsingleton_or_nontrivial R).resolve_left fun H ↦
        not_isEmpty_of_nonempty (Spec R) (inferInstanceAs (IsEmpty (PrimeSpectrum R)))

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
⊢ IsEmpty n
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n✝ : Type u
S : Scheme
n : Type u
R : CommRingCat
h :
  IsAffine (Spec (CommRingCat.of (MvPolynomial n ↑R))) ∧
    (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom C)) ⊤)).IsIntegral
h✝ : Nonempty ↥(Spec R)
this✝¹ : Nontrivial ↑R
i : n
this✝ : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f ↦ f.IsIntegral).RespectsIso
p : Polynomial ↑R
hp : p.Monic
hp' : Polynomial.eval₂ (CommRingCat.Hom.hom (CommRingCat.ofHom C)) (X i) p = 0
this : ↑(uniqueAlgEquiv (↑R) PUnit.{u + 1}).symm p = 0
⊢ False

Tactic:
simp only [AlgEquiv.coe_toAlgHom, EmbeddingLike.map_eq_zero_iff] at this

Goal state after:
n✝ : Type u
S : Scheme
n : Type u
R : CommRingCat
h :
  IsAffine (Spec (CommRingCat.of (MvPolynomial n ↑R))) ∧
    (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom C)) ⊤)).IsIntegral
h✝ : Nonempty ↥(Spec R)
this✝¹ : Nontrivial ↑R
i : n
this✝ : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f ↦ f.IsIntegral).RespectsIso
p : Polynomial ↑R
hp : p.Monic
hp' : Polynomial.eval₂ (CommRingCat.Hom.hom (CommRingCat.ofHom C)) (X i) p = 0
this : p = 0
⊢ False
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
W : Set X
inst✝ : Zero Y
f : X → Y
h : LocallyFiniteSupport f
hW : IsCompact W
this : {i | ({↑i} ∩ W).Nonempty}.Finite
lem : ∀ {α : Type u_1} (s t : Set α), Subtype.val '' {i | ({↑i} ∩ t).Nonempty} = t ∩ s
⊢ (W ∩ support f).Finite

Tactic:
← lem f.support W

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
W : Set X
inst✝ : Zero Y
f : X → Y
h : LocallyFiniteSupport f
hW : IsCompact W
this : {i | ({↑i} ∩ W).Nonempty}.Finite
lem : ∀ {α : Type u_1} (s t : Set α), Subtype.val '' {i | ({↑i} ∩ t).Nonempty} = t ∩ s
⊢ (Subtype.val '' {i | ({↑i} ∩ W).Nonempty}).Finite
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case H
X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : X.fromSpecStalk x ≫ f = X.fromSpecStalk x ≫ g
⊢ Spec.map (Scheme.Hom.stalkMap f x) ≫ Y.fromSpecStalk (f x) =
    Spec.map (Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x) ≫ Y.fromSpecStalk (f x)

Tactic:
simpa [Scheme.SpecMap_stalkSpecializes_fromSpecStalk]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: case mpr
X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X ⤏ Y
⊢ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S) → IsOver S f

Tactic:
intro e
    obtain ⟨f, rfl⟩ := PartialMap.toRationalMap_surjective f
    obtain ⟨U, hU, hUl, hUr, e⟩ := PartialMap.toRationalMap_eq_iff.mp e
    exact ⟨⟨f.restrict U hU hUl, by simpa using! e, by simp⟩⟩

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
inst✝ : Flat iX
hUS : IsAffineOpen US
hUX : IsAffineOpen UX
hUT : IsCompact ↑UT
⊢ Mono (pushoutSection H hUST hUSX hUY)

Tactic:
by
  suffices Mono (pushoutSection H.flip hUSX hUST (hUY.trans (inf_comm _ _))) by
    rw [← mono_comp_iff_of_isIso (pushoutSymmetry _ _).hom]; convert! this; cat_disch
  exact mono_pushoutSection_of_isCompact_of_flat_right _ _ _ _ hUS hUX hUT

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: case H
X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X.PartialMap Y
⊢ (Hom.isoImage X.topIso.hom (X.topIso.hom ⁻¹ᵁ 𝟙 X ⁻¹ᵁ f.domain)).inv ≫
      (X.topIso.hom ∣_ 𝟙 X ⁻¹ᵁ f.domain ≫ 𝟙 ↑(𝟙 X ⁻¹ᵁ f.domain)) ≫ f.hom =
    (X.isoOfEq ⋯).hom ≫ f.hom

Tactic:
Hom.id_preimage,

Goal state after:
case H
X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X.PartialMap Y
⊢ (Hom.isoImage X.topIso.hom (X.topIso.hom ⁻¹ᵁ f.domain)).inv ≫ (X.topIso.hom ∣_ f.domain ≫ 𝟙 ↑f.domain) ≫ f.hom =
    (X.isoOfEq ⋯).hom ≫ f.hom
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
xi : (𝒰.functorOfLocallyDirected ⋙ forget).obj i
xj : (𝒰.functorOfLocallyDirected ⋙ forget).obj j
hxij : (𝒰.trans fi) xi = (𝒰.trans fj) xj
⊢ (𝒰.f i) xi = (𝒰.f j) xj

Tactic:
rw [← 𝒰.trans_map fi, ← 𝒰.trans_map fj, Hom.comp_base, Hom.comp_base,
        ConcreteCategory.comp_apply, hxij, ConcreteCategory.comp_apply]

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

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Field K
f : F →+* E
g : E →+* K
hf : f.IsPurelyInseparable
hg : g.IsPurelyInseparable
⊢ (g.comp f).IsPurelyInseparable

Tactic:
algebraize [f, g, g.comp f]

Goal state after:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Field K
f : F →+* E
g : E →+* K
hf : f.IsPurelyInseparable
hg : g.IsPurelyInseparable
algInst✝² : Algebra F E := f.toAlgebra
algInst✝¹ : Algebra E K := g.toAlgebra
algInst✝ : Algebra F K := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower F E K := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap F K))
algebraizeInst✝¹ : IsPurelyInseparable F E
algebraizeInst✝ : IsPurelyInseparable E K
⊢ (g.comp f).IsPurelyInseparable
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
tfae_3_to_2 :
  (Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable) →
    ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f
tfae_2_to_4 : (∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f) → Surjective (pullback.diagonal f)
hf : Function.Surjective ⇑(pullback.diagonal f)
this : UniversallyInjective f
x : ↥X
algInst✝ : Algebra ↑(Y.residueField (f x)) ↑(X.residueField x) :=
  (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).toAlgebra
σ₁ σ₂ : Field.Emb ↑(Y.residueField (f x)) ↑(X.residueField x)
g₁ : Spec (CommRingCat.of (AlgebraicClosure ↑(X.residueField x))) ⟶ X :=
  (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X).symm ⟨x, CommRingCat.ofHom σ₁.toRingHom⟩
g₂ : Spec (CommRingCat.of (AlgebraicClosure ↑(X.residueField x))) ⟶ X :=
  (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X).symm ⟨x, CommRingCat.ofHom σ₂.toRingHom⟩
⊢ g₁ ≫ f = g₂ ≫ f

Tactic:
by
      simp only [g₁, g₂, Scheme.SpecToEquivOfField_symm_apply, AlgHom.toRingHom_eq_coe,
        Category.assoc, ← f.SpecMap_residueFieldMap_fromSpecResidueField x, ← Spec.map_comp_assoc]
      congr 2
      ext a
      simp only [CommRingCat.hom_comp, RingHom.comp_apply]
      exact (AlgHom.commutes σ₁ a).trans (AlgHom.commutes σ₂ a).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case inr
I : Type u
inst✝⁷ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁶ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝⁵ : IsCofiltered I
inst✝⁴ : ∀ (i : I), IsAffine (D.obj i)
inst✝³ : IsAffine c.pt
i j : I
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝² : IsAffine (Spec R)
S : CommRingCat
inst✝¹ : IsAffine (Spec S)
a : D.obj i ⟶ Spec S
b : D.obj j ⟶ Spec S
hab : c.π.app i ≫ a = c.π.app j ≫ b
φ : R ⟶ S
inst✝ : LocallyOfFiniteType (Spec.map φ)
ha : t.app i = a ≫ Spec.map φ
hb : t.app j = b ≫ Spec.map φ
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), CompactSpace ↥(D.obj i)] [∀ (i : I), IsAffine (D.obj i)]
    [IsAffine c.pt] (t : D ⟶ (Functor.const I).obj (Spec R)) (a : D.obj i ⟶ Spec S) (b : D.obj j ⟶ Spec S),
    c.π.app i ≫ a = c.π.app j ≫ b →
      t.app i = a ≫ Spec.map φ →
        t.app j = b ≫ Spec.map φ → (∃ D', D = D' ⋙ Scheme.Spec) → ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
hD : ¬∃ D', D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
⊢ ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b

Tactic:
have inst (i) : IsIso (e.app i) := by dsimp [e]; infer_instance

Goal state after:
case inr
I : Type u
inst✝⁷ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁶ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝⁵ : IsCofiltered I
inst✝⁴ : ∀ (i : I), IsAffine (D.obj i)
inst✝³ : IsAffine c.pt
i j : I
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝² : IsAffine (Spec R)
S : CommRingCat
inst✝¹ : IsAffine (Spec S)
a : D.obj i ⟶ Spec S
b : D.obj j ⟶ Spec S
hab : c.π.app i ≫ a = c.π.app j ≫ b
φ : R ⟶ S
inst✝ : LocallyOfFiniteType (Spec.map φ)
ha : t.app i = a ≫ Spec.map φ
hb : t.app j = b ≫ Spec.map φ
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), CompactSpace ↥(D.obj i)] [∀ (i : I), IsAffine (D.obj i)]
    [IsAffine c.pt] (t : D ⟶ (Functor.const I).obj (Spec R)) (a : D.obj i ⟶ Spec S) (b : D.obj j ⟶ Spec S),
    c.π.app i ≫ a = c.π.app j ≫ b →
      t.app i = a ≫ Spec.map φ →
        t.app j = b ≫ Spec.map φ → (∃ D', D = D' ⋙ Scheme.Spec) → ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
hD : ¬∃ D', D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst : ∀ (i : I), IsIso (e.app i)
⊢ ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: case refine_1
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
⊢ ∃ V, IsCompact V.carrier ∧ (fun p ↦ f p.fst p.snd) '' V.carrier = U

Tactic:
refine ⟨⟨s.sigma fun i ↦ if h : i ∈ s then V i h else ∅, isOpen_sigma_iff.mpr ?_⟩, ?_, ?_⟩
    · intro i
      by_cases h : i ∈ s
      · simpa [h] using (V _ _).2
      · simp [h]
    · dsimp only
      exact Set.isCompact_sigma hs fun i ↦ (by simp_all)
    · aesop

Goal state after:
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
s : Set 𝒰.I₀
hs : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun x ↦ ↥(𝒰.X x)) i)
hcV : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
hU : ⋃ i, ⋃ (h : i ∈ s), (fun x ↦ ⇑(𝒰.f x)) i '' ↑(V i h) = ↑U
t : (i : 𝒰.I₀) → i ∈ s → Set (f i).I₀
ht : ∀ (i : 𝒰.I₀) (hi : i ∈ s), (t i hi).Finite
W : (i : 𝒰.I₀) → (hi : i ∈ s) → (i_1 : (f i).I₀) → i_1 ∈ t i hi → TopologicalSpace.Opens ((fun x ↦ ↥((f i).X x)) i_1)
hcW : ∀ (i : 𝒰.I₀) (hi : i ∈ s) (i_1 : (f i).I₀) (h : i_1 ∈ t i hi), IsCompact (W i hi i_1 h).carrier
hV : ∀ (i : 𝒰.I₀) (hi : i ∈ s), ⋃ i_1, ⋃ (h : i_1 ∈ t i hi), (fun x ↦ ⇑((f i).f x)) i_1 '' ↑(W i hi i_1 h) = ↑(V i hi)
this✝ : Finite ↑s
this : ∀ (i : 𝒰.I₀) (hi : i ∈ s), Finite ↑(t i hi)
⊢ IsCompactOpenCovered (fun x ↦ ⇑((𝒰.bind f).f x)) ↑U

Tactic:
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 ..) ?_

Goal state after:
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
s : Set 𝒰.I₀
hs : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun x ↦ ↥(𝒰.X x)) i)
hcV : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
hU : ⋃ i, ⋃ (h : i ∈ s), (fun x ↦ ⇑(𝒰.f x)) i '' ↑(V i h) = ↑U
t : (i : 𝒰.I₀) → i ∈ s → Set (f i).I₀
ht : ∀ (i : 𝒰.I₀) (hi : i ∈ s), (t i hi).Finite
W : (i : 𝒰.I₀) → (hi : i ∈ s) → (i_1 : (f i).I₀) → i_1 ∈ t i hi → TopologicalSpace.Opens ((fun x ↦ ↥((f i).X x)) i_1)
hcW : ∀ (i : 𝒰.I₀) (hi : i ∈ s) (i_1 : (f i).I₀) (h : i_1 ∈ t i hi), IsCompact (W i hi i_1 h).carrier
hV : ∀ (i : 𝒰.I₀) (hi : i ∈ s), ⋃ i_1, ⋃ (h : i_1 ∈ t i hi), (fun x ↦ ⇑((f i).f x)) i_1 '' ↑(W i hi i_1 h) = ↑(V i hi)
this✝ : Finite ↑s
this : ∀ (i : 𝒰.I₀) (hi : i ∈ s), Finite ↑(t i hi)
⊢ ⋃ k, ⇑((𝒰.bind f).f ⟨↑k.fst, ↑k.snd⟩) '' ↑(W ↑k.fst ⋯ ⟨↑k.fst, ↑k.snd⟩.snd ⋯) = ↑U
Module: Mathlib.Topology.Category.TopCat.EffectiveEpi

Goal state before:
pp: B X : TopCat
π : X ⟶ B
hπ : IsQuotientMap ⇑(ConcreteCategory.hom π)
W✝ : TopCat
e : X ⟶ W✝
h : ∀ {Z : TopCat} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W✝
hm : π ≫ g = e
this : g = ofHom (hπ.liftEquiv ⟨Hom.hom e, ⋯⟩)
⊢ g = ofHom (hπ.lift (Hom.hom e) ⋯)

Tactic:
by assumption

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst✝ : EffectiveEpiFamily X f
W✝ : C
e : (a : α) → Y a ⟶ W✝
w : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
⊢ (g a ≫ f a) ≫ EffectiveEpiFamily.desc X f (fun a ↦ i a ≫ e a) ⋯ = e a

Tactic:
simp only [Category.assoc, EffectiveEpiFamily.fac]
    rw [← Category.id_comp (e a), ← Category.assoc, ← Category.assoc]
    apply w
    simp only [Category.comp_id, Category.id_comp, ← Category.assoc]
    aesop

Goal state after:
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: X Y S : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
f : X ⟶ S
hf : fst π π ≫ f = snd π π ≫ f
b : ↑Y.toPresheafedSpace ⟶ ↑S.toPresheafedSpace
hfac : π.base ≫ b = f.base
⊢ ∃ 𝒰, ∀ (i : 𝒰.I₀), ∃ u, fst π (𝒰.f i) ≫ f = snd π (𝒰.f i) ≫ u

Tactic:
let 𝒰 := Y.openCoverOfIsOpenCover _ <| Y.isBasis_affineOpens.isOpenCover_mem_and_le
    (S.isBasis_affineOpens.isOpenCover.comap b.hom)

Goal state after:
X Y S : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
f : X ⟶ S
hf : fst π π ≫ f = snd π π ≫ f
b : ↑Y.toPresheafedSpace ⟶ ↑S.toPresheafedSpace
hfac : π.base ≫ b = f.base
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover (fun V ↦ (↑V).1) ⋯
⊢ ∃ 𝒰, ∀ (i : 𝒰.I₀), ∃ u, fst π (𝒰.f i) ≫ f = snd π (𝒰.f i) ≫ u
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: case refine_1
X Y : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
this✝ : Epi π
Z : Scheme
f : X ⟶ Z
hf : pullback.fst π π ≫ f = pullback.snd π π ≫ f
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), pullback.fst π (𝒰.f i) ≫ f = pullback.snd π (𝒰.f i) ≫ u i
i j : 𝒰.I₀
this : Epi (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
⊢ pullback.fst (𝒰.f i) (𝒰.f j) ≫ u i = pullback.snd (𝒰.f i) (𝒰.f j) ≫ u j

Tactic:
rw [← cancel_epi (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)),
      ← cancel_epi (pullback.congrHom rfl pullback.condition.symm).hom]

Goal state after:
case refine_1
X Y : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
this✝ : Epi π
Z : Scheme
f : X ⟶ Z
hf : pullback.fst π π ≫ f = pullback.snd π π ≫ f
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), pullback.fst π (𝒰.f i) ≫ f = pullback.snd π (𝒰.f i) ≫ u i
i j : 𝒰.I₀
this : Epi (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
⊢ (pullback.congrHom ⋯ ⋯).hom ≫
      pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) ≫ pullback.fst (𝒰.f i) (𝒰.f j) ≫ u i =
    (pullback.congrHom ⋯ ⋯).hom ≫
      pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) ≫ pullback.snd (𝒰.f i) (𝒰.f j) ≫ u j
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case h₀
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.499} 𝒰.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.499} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
m : d.gluedCocone.pt ⟶ s.pt
hm : ∀ (j : J), d.gluedCocone.ι.app j ≫ m = s.ι.app j
i : 𝒱.I₀
a : J
⊢ (Comma.Hom.hom ((d.cocone i).ι.app a)).left ≫ colimit.ι d.relativeGluingData.functor i ≫ m.left =
    pullback.fst (D.obj a).hom (𝒰.f i) ≫ (s.ι.app a).left

Tactic:
rw [← congr($(hm a).left)]

Goal state after:
case h₀
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.499} 𝒰.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.499} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
m : d.gluedCocone.pt ⟶ s.pt
hm : ∀ (j : J), d.gluedCocone.ι.app j ≫ m = s.ι.app j
i : 𝒱.I₀
a : J
⊢ (Comma.Hom.hom ((d.cocone i).ι.app a)).left ≫ colimit.ι d.relativeGluingData.functor i ≫ m.left =
    pullback.fst (D.obj a).hom (𝒰.f i) ≫ (d.gluedCocone.ι.app a ≫ m).left
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: k₀ k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) (n + 1) ^ numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) (n + 1) *
      degBound k₀ (fun t ↦ Nat.casesOn t k D) (n + 1) =
    (k₀ * k) ^ (k₀ * k) * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) (n + 1)

Tactic:
degBound_casesOn_succ,

Goal state after:
k₀ k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) (n + 1) ^ numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) (n + 1) *
      ((k₀ * k) ^ (k₀ * k) * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n) =
    (k₀ * k) ^ (k₀ * k) * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) (n + 1)