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

Goal state before:
pp: case mk
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t₂ : Triplet f g
x✝ : ↥X
y✝ : ↥Y
s✝ : ↥S
hx✝ : f x✝ = s✝
hy✝ : g y✝ = s✝
ex : { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.x = t₂.x
ey : { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.y = t₂.y
⊢ { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ } = t₂

Tactic:
cases t₂

Goal state after:
case mk.mk
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝¹ : ↥X
y✝¹ : ↥Y
s✝¹ : ↥S
hx✝¹ : f x✝¹ = s✝¹
hy✝¹ : g y✝¹ = s✝¹
x✝ : ↥X
y✝ : ↥Y
s✝ : ↥S
hx✝ : f x✝ = s✝
hy✝ : g y✝ = s✝
ex : { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ }.x = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.x
ey : { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ }.y = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.y
⊢ { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ } = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom =
    (Spec T.tensor).fromSpecResidueField p

Tactic:
by
  apply T.isPullback_SpecMap_tensor.hom_ext
  · rw [← cancel_mono <| X.fromSpecResidueField T.x]
    simp_rw [Category.assoc, ← T.specTensorTo_fst, tensorCongr_SpecTensorTo_assoc]
    rw [← Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc, ofPointTensor_SpecTensorTo_assoc]
  · rw [← cancel_mono <| Y.fromSpecResidueField T.y]
    simp_rw [Category.assoc, ← T.specTensorTo_snd, tensorCongr_SpecTensorTo_assoc]
    rw [← Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc, ofPointTensor_SpecTensorTo_assoc]

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

Goal state before:
pp: R S : Type u_5
x✝¹ : CommRing R
x✝ : CommRing S
e : R ≃+* S
⊢ e.toRingHom.FiniteType

Tactic:
algebraize [e.toRingHom]

Goal state after:
R S : Type u_5
x✝¹ : CommRing R
x✝ : CommRing S
e : R ≃+* S
algInst✝ : Algebra R S := e.toRingHom.toAlgebra
⊢ e.toRingHom.FiniteType
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

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

Tactic:
by
  have := @of_comp_isClosedImmersion _ _ _ f.toImage f.imageι inferInstance
    (by rw [Scheme.Hom.toImage_imageι]; infer_instance)
  have : IsHomeomorph f.toImage :=
    isHomeomorph_iff_isEmbedding_surjective.mpr ⟨f.toImage.isEmbedding, by
      rw [← Set.range_eq_univ, ← f.toImage.isClosedEmbedding.isClosed_range.closure_eq]
      exact f.toImage.denseRange.closure_eq⟩
  refine isomorphisms_eq_stalkwise.ge _ ⟨?_, ?_⟩
  · exact inferInstanceAs (IsIso (TopCat.isoOfHomeo this.homeomorph).hom)
  · intro x
    refine ⟨?_, f.toImage.stalkMap_surjective x⟩
    change Function.Injective (CommRingCat.Hom.hom (((TopCat.Presheaf.stalkFunctor CommRingCat
      (f.toImage x)).map f.toImage.c) ≫ X.presheaf.stalkPushforward _ _ x))
    simp only [TopCat.Presheaf.stalkFunctor_obj, CommRingCat.hom_comp, RingHom.coe_comp]
    refine .comp ?_ (f.stalkFunctor_toImage_injective _)
    have := TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_isInducing CommRingCat
      (f := f.toImage.base) f.toImage.isEmbedding.isInducing X.presheaf x
    exact ((ConcreteCategory.isIso_iff_bijective _).mp this).1

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : X.IsSeparated
⊢ IsSeparated f

Tactic:
apply +allowSynthFailures @IsSeparated.of_comp (g := terminal.from Y)

Goal state after:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : X.IsSeparated
⊢ IsSeparated (f ≫ terminal.from Y)
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case inr.mp
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
⊢ Polynomial.map (algebraMap R I.ResidueField) (LinearMap.charpoly ((Algebra.lmul R A) f)) =
      X ^ ((LinearMap.mul R A) f).charpoly.natDegree →
    ∀ i < ((LinearMap.mul R A) f).charpoly.natDegree, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I

pp: case inr.mpr
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
⊢ (∀ i < ((LinearMap.mul R A) f).charpoly.natDegree, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I) →
    Polynomial.map (algebraMap R I.ResidueField) (LinearMap.charpoly ((Algebra.lmul R A) f)) =
      X ^ ((LinearMap.mul R A) f).charpoly.natDegree

Tactic:
· intro e i hi
    replace e := congr(($e).coeff i)
    simpa only [Algebra.coe_lmul_eq_mul, coeff_map, coeff_X_pow, hi.ne, ↓reduceIte,
      ← RingHom.mem_ker, Ideal.ker_algebraMap_residueField] using e

Goal state after:
case inr.mpr
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
⊢ (∀ i < ((LinearMap.mul R A) f).charpoly.natDegree, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I) →
    Polynomial.map (algebraMap R I.ResidueField) (LinearMap.charpoly ((Algebra.lmul R A) f)) =
      X ^ ((LinearMap.mul R A) f).charpoly.natDegree
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: 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'
eq✝ : c.ι j x = c.ι j' x'
k : J
g : IsFiltered.max j j' ⟶ k
eq :
  (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom (F.map (leftToMax j j'))) x) =
    (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom (F.map (rightToMax j j'))) x')
⊢ (ConcreteCategory.hom (F.map (leftToMax j j' ≫ g))) x = (ConcreteCategory.hom (F.map (rightToMax j j' ≫ g))) x'

Tactic:
by simp [eq]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case mp.inr.inr
n : Type u
S : Scheme
h : IsIntegralHom (𝔸(n; S) ↘ S)
h✝ : Nonempty ↥S
this : ∀ {n : Type u} (S : Scheme), IsIntegralHom (𝔸(n; S) ↘ S) → Nonempty ↥S → (∃ R, S = Spec R) → IsEmpty n
hS : ¬∃ R, S = Spec R
⊢ IsEmpty n

Tactic:
obtain ⟨x⟩ := ‹Nonempty S›
      obtain ⟨y, hy⟩ := S.affineCover.covers x
      exact this (S.affineCover.X _) (MorphismProperty.IsStableUnderBaseChange.of_isPullback
        (isPullback_map (S.affineCover.f _)) h) ⟨y⟩ ⟨_, rfl⟩

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

Goal state before:
pp: X : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosed {x}
⊢ pointOfClosedPoint f x hx ≫ f = 𝟙 (Spec (CommRingCat.of K))

Tactic:
simp [pointOfClosedPoint, ← SpecMap_residueFieldIsoBase_inv, ← Spec.map_comp]

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

Goal state before:
pp: case hxy
R₀ : Type u_1
inst✝² : CommRing R₀
n : ℕ
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := ⋯
q₂ : R →ₐ[R₀] R ⧸ Ideal.span {c} := ⋯
q₂_surjective : Surjective ⇑q₂
e₁ : InductionObj (Localization.Away c) n := ⋯
e₂ : InductionObj (R ⧸ Ideal.span {c}) n := ⋯
degBound_e₁_le : e₁.degBound ≤ e.degBound
⊢ (e₂.val i).degree < (e.val i).degree

Tactic:
exact degree_map_lt (by simp [q₂, ← hi]) (by simpa [hi] using hc)

Goal state after:
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : f x = g x
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : f x ∈ ↑V
hxV' : g x ∈ V
U : X.Opens
hxU : x ∈ U
left✝ : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hxU))
this✝ : IsAffine ↑V
this :
  ∀ (U₀ : X.Opens) (V₀ : Y.Opens) (eU : U = U₀) (eV : V = V₀), Scheme.Hom.appLE f V₀ U₀ ⋯ = Scheme.Hom.appLE g V₀ U₀ ⋯
⊢ Scheme.Hom.resLE f V U ⋯ = Scheme.Hom.resLE g V U ⋯

Tactic:
by
    rw [← cancel_mono V.toScheme.isoSpec.hom]
    simp only [Scheme.isoSpec, asIso_hom, Scheme.toSpecΓ_naturality,
      Scheme.Hom.app_eq_appLE, Scheme.Hom.resLE_appLE]
    congr 2
    apply this <;> simp

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

Goal state before:
pp: X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↥X
hx : x ∈ U
⊢ (Spec.map (inv (Hom.stalkMap U.ι ⟨x, hx⟩)) ≫ (↑U).fromSpecStalk ⟨x, hx⟩) ≫ X.homOfLE hU' ≫ f.hom =
    (Spec.map (inv (Hom.stalkMap f.domain.ι ⟨x, ⋯⟩)) ≫ (↑f.domain).fromSpecStalk ⟨x, ⋯⟩) ≫ f.hom

Tactic:
have e : ⟨x, hU' hx⟩ = X.homOfLE hU' ⟨x, hx⟩ := by
    rw [Scheme.homOfLE_base]
    rfl

Goal state after:
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↥X
hx : x ∈ U
e : ⟨x, ⋯⟩ = (X.homOfLE hU') ⟨x, hx⟩
⊢ (Spec.map (inv (Hom.stalkMap U.ι ⟨x, hx⟩)) ≫ (↑U).fromSpecStalk ⟨x, hx⟩) ≫ X.homOfLE hU' ≫ f.hom =
    (Spec.map (inv (Hom.stalkMap f.domain.ι ⟨x, ⋯⟩)) ≫ (↑f.domain).fromSpecStalk ⟨x, ⋯⟩) ≫ f.hom
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
f : X.PartialMap Y
g : X ⟶ Y
inst✝¹ : IsOver S f
inst✝ : Hom.IsOver g S
⊢ (f.restrict (f.domain ⊓ (Hom.toPartialMap g).domain) ⋯ ⋯).hom =
      ((Hom.toPartialMap g).restrict (f.domain ⊓ (Hom.toPartialMap g).domain) ⋯ ⋯).hom ↔
    f.hom = f.domain.ι ≫ g

Tactic:
← cancel_epi (X.isoOfEq (inf_top_eq f.domain)).hom

Goal state after:
X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
f : X.PartialMap Y
g : X ⟶ Y
inst✝¹ : IsOver S f
inst✝ : Hom.IsOver g S
⊢ (f.restrict (f.domain ⊓ (Hom.toPartialMap g).domain) ⋯ ⋯).hom =
      ((Hom.toPartialMap g).restrict (f.domain ⊓ (Hom.toPartialMap g).domain) ⋯ ⋯).hom ↔
    (X.isoOfEq ⋯).hom ≫ f.hom = (X.isoOfEq ⋯).hom ≫ f.domain.ι ≫ g
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
⊢ Limits.pullback.fst (f.openCoverDomain.f x) (f.openCoverDomain.f y) ≫ (X.isoOfEq ⋯).inv ≫ (Exists.choose ⋯).hom =
    Limits.pullback.snd (f.openCoverDomain.f x) (f.openCoverDomain.f y) ≫ (X.isoOfEq ⋯).inv ≫ (Exists.choose ⋯).hom

Tactic:
let g (x : f.openCoverDomain.I₀) := x.2.choose

Goal state after:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : f.openCoverDomain.I₀ → X.PartialMap Y := fun x ↦ Exists.choose ⋯
⊢ Limits.pullback.fst (f.openCoverDomain.f x) (f.openCoverDomain.f y) ≫ (X.isoOfEq ⋯).inv ≫ (Exists.choose ⋯).hom =
    Limits.pullback.snd (f.openCoverDomain.f x) (f.openCoverDomain.f y) ≫ (X.isoOfEq ⋯).inv ≫ (Exists.choose ⋯).hom
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: case refine_2
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 : 𝒰.I₀
h : (fun i ↦ Hom.opensRange (𝒰.f i)) k ≤ Hom.opensRange (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
y : ↥(𝒰.X k)
hy : (𝒰.f k) y = (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x
⊢ Hom.opensRange (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) ≤ Hom.opensRange (𝒰.f j)

Tactic:
simp_rw [pullback.condition, Scheme.Hom.opensRange_comp]

Goal state after:
case refine_2
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 : 𝒰.I₀
h : (fun i ↦ Hom.opensRange (𝒰.f i)) k ≤ Hom.opensRange (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
y : ↥(𝒰.X k)
hy : (𝒰.f k) y = (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x
⊢ 𝒰.f j ''ᵁ Hom.opensRange (pullback.snd (𝒰.f i) (𝒰.f j)) ≤ Hom.opensRange (𝒰.f j)
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 j : 𝒰.I₀} (hij : i ⟶ j), Function.Injective ⇑(d.functor.map hij)

Tactic:
intro i j hij

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.AlgebraicGeometry.Cover.Over

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover (precoverage P) X
f : W ⟶ X
inst✝³ : W.Over S
inst✝² : X.Over S
inst✝¹ : Cover.Over S 𝒰
inst✝ : Hom.IsOver f S
j : (Cover.pullbackCoverOver S 𝒰 f).I₀
⊢ (Cover.pullbackCoverOver S 𝒰 f).f j ≫ W ↘ S = (Cover.pullbackCoverOver S 𝒰 f).X j ↘ S

Tactic:
by exact Over.w (pullback.fst (f.asOver S) ((𝒰.f j).asOver S))

Goal state after:
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} ⊆ zeroLocus {0}

Tactic:
zeroLocus_singleton_zero

Goal state after:
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
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝³ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
⊢ ∃ i' hii',
    ⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X))ᶜ = ∅

Tactic:
let W := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
  by_contra! h
  let Z (i' : I) (hii' : i' ⟶ A.i) :=
    (D.map hii' ≫ pullback.lift A.a A.b (A.ha.symm.trans A.hb)) ⁻¹' Wᶜ
  have hZ (i') (hii' : i' ⟶ A.i) : IsClosed (Z i' hii') :=
    (W.isOpen.isClosed_compl).preimage <| Scheme.Hom.continuous _
  obtain ⟨s, hs⟩ := exists_mem_of_isClosed_of_nonempty' D A.c A.hc Z hZ h
    (fun _ _ ↦ (hZ _ _).isCompact) (fun i i' hii' hij ↦ by simp [Z, Set.MapsTo])
  refine hs A.i (𝟙 A.i) (Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange _ _ _ ?_)
  use (A.c.π.app A.i ≫ A.a) s
  have H : A.c.π.app A.i ≫ A.a ≫ pullback.diagonal f =
      A.c.π.app A.i ≫ pullback.lift A.a A.b (A.ha.symm.trans A.hb) := by ext <;> simp [hab]
  simp [← Scheme.Hom.comp_apply, -Scheme.Hom.comp_base, H]

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

Goal state before:
pp: S : Type u_1
U : Set S
inst✝ : TopologicalSpace S
⊢ IsCompactOpenCovered (fun x ↦ id) U ↔ IsOpen U ∧ IsCompact U

Tactic:
rw [iff_of_unique]
  refine ⟨fun ⟨V, hV, heq⟩ ↦ ?_, fun ⟨ho, hc⟩ ↦ ⟨⟨U, ho⟩, hc, by simp⟩⟩
  simp only [id_eq, Set.image_id', carrier_eq_coe, ← heq] at heq ⊢
  exact ⟨V.2, hV⟩

Goal state after:
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 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:
intro i j hij

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.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.117} 𝒰.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.117} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
⊢ ∀ {i j : 𝒱.I₀} (hij : i ⟶ j),
    Cover.trans 𝒱 hij ≫
        ((d.isColimit j).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f j)).mapCocone s)).left ≫
          pullback.fst s.pt.hom (𝒰.f j) =
      ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)).left ≫
        pullback.fst s.pt.hom (𝒰.f i)

Tactic:
intro i j hij

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.117} 𝒰.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.117} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
i j : 𝒱.I₀
hij : i ⟶ j
⊢ Cover.trans 𝒱 hij ≫
      ((d.isColimit j).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f j)).mapCocone s)).left ≫
        pullback.fst s.pt.hom (𝒰.f j) =
    ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)).left ≫
      pullback.fst s.pt.hom (𝒰.f i)
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: 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
l : Fin n
m : ℕ
hlj : l = j
e : c.val j = 0
⊢ c.val i = 0

Tactic:
simpa [e] using hle

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

Goal state before:
pp: case refine_2
R : Type u_6
inst✝ : CommRing R
M : Submodule ℤ R
hM : 1 ∈ M
S : ConstructibleSetData R[X]
hS : ∀ C ∈ S, ∀ (j : Fin C.n) (k : ℕ), (C.g j).coeff k ∈ M
f : BasicConstructibleSetData R[X] → ConstructibleSetData R
hf₁ :
  ∀ (C : BasicConstructibleSetData R[X]),
    comap Polynomial.C '' (zeroLocus (Set.range { val := C.g }.val) \ zeroLocus {C.f}) = (f C).toSet
hf₂ : ∀ (C : BasicConstructibleSetData R[X]), ∀ C_1 ∈ f C, C_1.n ≤ { val := C.g }.degBound
hf₃ :
  ∀ (C : BasicConstructibleSetData R[X]),
    ∀ C_1 ∈ f C, ∀ (i : Fin C_1.n), C_1.g i ∈ coeffSubmodule ℤ { val := C.g } ^ { val := C.g }.powBound
⊢ ∀ C ∈ Finset.biUnion S f, C.n ≤ S.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ M ^ S.degBound ^ S.degBound

Tactic:
· simp only [Finset.mem_biUnion, forall_exists_index, and_imp]
    intro x y hy hx
    have H : degBound ⟨y.g⟩ ≤ S.degBound :=
      Finset.le_sup (f := fun e ↦ ∑ i, (e.g i).degree.succ) hy
    refine ⟨(hf₂ y x hx).trans H, fun i ↦ SetLike.le_def.mp ?_ (hf₃ y x hx i)⟩
    gcongr
    · simpa [Submodule.one_eq_span]
    · refine Submodule.span_le.mpr ?_
      simp [Set.subset_def, hM, forall_comm (α := R), hS y hy]
    · delta powBound
      by_cases h : S.degBound = 0
      · have : degBound ⟨y.g⟩ = 0 := by nlinarith
        rw [h, this]
      gcongr
      rwa [Nat.one_le_iff_ne_zero]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
⊢ evalEval 0 0 W.polynomialX = -W.a₄

Tactic:
simp only [evalEval_polynomialX, zero_add, zero_sub, mul_zero, zero_pow <| Nat.succ_ne_zero _]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
S : Type s
inst✝ : CommRing S
f : R →+* S
hf : Function.Injective ⇑f
x y : R
⊢ (W.map f).Equation (f x) (f y) ↔ W.Equation x y

Tactic:
by
  simp only [Equation, map_polynomial, map_mapRingHom_evalEval, map_eq_zero_iff f hf]

Goal state after: