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

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
⊢ IsLocallyArtinian X ↔ ∀ (i : 𝒰.I₀), IsLocallyArtinian (𝒰.X i)

Tactic:
refine ⟨fun h ↦ inferInstance, fun H ↦ ?_⟩

Goal state after:
X : Scheme
𝒰 : X.OpenCover
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian (𝒰.X i)
⊢ IsLocallyArtinian X
Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

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

Tactic:
rw [isSchemeTheoreticallyDominant_iff, Scheme.Hom.ker_comp, f.ker_eq_bot,
    Scheme.IdealSheafData.map_bot, g.ker_eq_bot]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
⊢ UniversallyOpen f

Tactic:
by
  rw [eq]
  intro X' Y' i₁ i₂ f' hf
  have hf' : IsOpenImmersion f' := MorphismProperty.of_isPullback hf.flip inferInstance
  exact f'.isOpenEmbedding.isOpenMap

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

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

Tactic:
rw [eq]
  exact universally_isZariskiLocalAtSource _

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

Goal state before:
pp: ⊢ @GeometricallyIntegral = @GeometricallyReduced ⊓ @GeometricallyIrreducible

Tactic:
rw [eq_geometrically, GeometricallyReduced.eq_geometrically,
    GeometricallyIrreducible.eq_geometrically, ← geometrically_inf]
  eta_expand
  simp [isIntegral_iff_irreducibleSpace_and_isReduced, and_comm]

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

Goal state before:
pp: R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
int : (algebraMap R T).IsIntegral
⊢ (algebraMap S (S ⊗[R] T)).IsIntegral

Tactic:
algebraMap_isIntegral_iff

Goal state after:
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
int : Algebra.IsIntegral R T
⊢ Algebra.IsIntegral S (S ⊗[R] T)
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)
⊢ f ≫ pullback.snd (terminal.from S) (terminal.from (Spec ℤ[n])) =
    g ≫ pullback.snd (terminal.from S) (terminal.from (Spec ℤ[n]))

Tactic:
change f ≫ toSpecMvPoly _ _ = g ≫ toSpecMvPoly _ _

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)
⊢ f ≫ toSpecMvPoly n S = g ≫ toSpecMvPoly n S
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
R S : CommRingCat
φ : R ⟶ S
i✝ : n
| (ConcreteCategory.hom (Scheme.Hom.app (SpecIso n S).inv ⊤))
    ((ConcreteCategory.hom (Scheme.Hom.app (map n (Spec.map φ)) ⊤)) (coord (Spec R) i✝))

Tactic:
enter [2]

Goal state after:
n : Type u
R S : CommRingCat
φ : R ⟶ S
i✝ : n
| (ConcreteCategory.hom (Scheme.Hom.app (map n (Spec.map φ)) ⊤)) (coord (Spec R) i✝)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
R S : CommRingCat
φ : R ⟶ S
i✝ : n
| (ConcreteCategory.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ)))) ⊤))
    ((ConcreteCategory.hom (Scheme.Hom.app (SpecIso n R).inv ⊤)) (coord (Spec R) i✝))

Tactic:
enter [2]

Goal state after:
n : Type u
R S : CommRingCat
φ : R ⟶ S
i✝ : n
| (ConcreteCategory.hom (Scheme.Hom.app (SpecIso n R).inv ⊤)) (coord (Spec R) i✝)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case mp.inr
n : Type u
S : Scheme
h : IsIntegralHom (𝔸(n; S) ↘ S)
h✝ : Nonempty ↥S
⊢ IsEmpty ↥S ∨ IsEmpty n

Tactic:
refine .inr ?_

Goal state after:
case mp.inr
n : Type u
S : Scheme
h : IsIntegralHom (𝔸(n; S) ↘ S)
h✝ : Nonempty ↥S
⊢ IsEmpty n
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : Zero Y
f : X → Y
⊢ (LocallyFinite fun s ↦ {↑s}) ↔ LocallyFiniteSupport f

Tactic:
by
  dsimp only [LocallyFinite]
  peel with z t ht
  have aux1 : t ∩ f.support = {i : f.support | ↑i ∈ t} := by aesop
  have aux2 : InjOn Subtype.val {i : f.support | ↑i ∈ t} := by aesop
  simp only [singleton_inter_nonempty, aux1, finite_image_iff aux2]

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✝ : AddCommMonoid Y
ι : Type u_3
s : Finset ι
F : ι → locallyFinsuppWithin U Y
⊢ ⇑(∑ n ∈ s, F n) = ∑ n ∈ s, ⇑(F n)

Tactic:
induction s using Finset.induction with

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
D : locallyFinsupp X ℤ
h : (support D).Finite
w : X
s : Finset X := h.toFinset
hs : s = h.toFinset
hw : w ∉ s
this : w ∉ support D
⊢ 0 = D w

Tactic:
exact (notMem_support.mp this).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✝³ : 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))) }
this : Nonempty ↥c'.cone.pt
⊢ Nonempty ↥c.pt

Tactic:
let α : F ⟶ Over.forget _ ⋙ D := Functor.whiskerRight
      (Functor.whiskerLeft (Over.post D) (Over.mapPullbackAdj (𝒰.f j)).counit) (Over.forget _)

Goal state after:
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
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))) }
this : Nonempty ↥c'.cone.pt
α : F ⟶ Over.forget i ⋙ D :=
  Functor.whiskerRight ((Over.post D).whiskerLeft (Over.mapPullbackAdj (𝒰.f j)).counit) (Over.forget (D.obj i))
⊢ Nonempty ↥c.pt
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: X Y Z : Scheme
inst✝³ : PreirreducibleSpace ↥X
inst✝² : Nonempty ↥Y
f : X.PartialMap Y
inst✝¹ : IsDominant f.hom
g : Y.PartialMap Z
inst✝ : IsDominant g.hom
⊢ IsDominant (f.comp g).hom

Tactic:
by
  dsimp only [comp_domain, comp_hom]
  have := IsZariskiLocalAtTarget.restrict ‹IsDominant f.hom› g.domain
  infer_instance

Goal state after:
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⟩
this :
  (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X) g₁ =
    (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X) g₂
⊢ ↑σ₁ = ↑σ₂

Tactic:
rw [Equiv.apply_symm_apply, Equiv.apply_symm_apply] at this
      exact congr($(this).2.hom)

Goal state after:
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⟩
q : Spec (CommRingCat.of (AlgebraicClosure ↑(X.residueField x))) ⟶ pullback f f := pullback.lift g₁ g₂ ⋯
q_fst : q ≫ pullback.fst f f = g₁
q_snd : q ≫ pullback.snd f f = g₂
⊢ (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X) g₁ =
    (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X) g₂

Tactic:
Scheme.SpecToEquivOfField_eq_iff,

Goal state after:
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⟩
q : Spec (CommRingCat.of (AlgebraicClosure ↑(X.residueField x))) ⟶ pullback f f := pullback.lift g₁ g₂ ⋯
q_fst : q ≫ pullback.fst f f = g₁
q_snd : q ≫ pullback.snd f f = g₂
⊢ ∃ (e :
    ((Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X) g₁).fst =
      ((Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X) g₂).fst),
    ((Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X) g₁).snd =
      (Scheme.residueFieldCongr e).hom ≫ ((Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X) g₂).snd
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case ht
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
degBound_e₂_lt : e₂.degBound < e.degBound
H₁ : Statement R₀ (Localization.Away c) n e₁
H₂ : Statement R₀ (R ⧸ Ideal.span {c}) n e₂
f : R[X]
T₁ : ConstructibleSetData (Localization.Away c)
T₂ : ConstructibleSetData (R ⧸ Ideal.span {c})
hT₁ : comap Polynomial.C '' (zeroLocus (Set.range e₁.val) \ zeroLocus {(mapRingHom ↑q₁) f}) = T₁.toSet
hT₁deg : ∀ x ∈ T₁, x.n ≤ e₁.degBound
hT₂ : comap Polynomial.C '' (zeroLocus (Set.range e₂.val) \ zeroLocus {(mapRingHom ↑q₂) f}) = T₂.toSet
hT₂deg : ∀ x ∈ T₂, x.n ≤ e₂.degBound
x✝ : Invertible (q₁ c) := ⋯
he₁span :
  coeffSubmodule R₀ e₁ ^ e₁.powBound =
    ⅟(q₁ c ^ e₁.powBound) • Submodule.map q₁.toLinearMap (span R₀ ({c} ∪ ⋃ i, coeff(e.val i)) ^ e₁.powBound)
g₁ : (x : BasicConstructibleSetData (Localization.Away c)) → Fin x.n → R
hg₁ : ∀ x ∈ T₁, ∀ (i : Fin x.n), g₁ x i ∈ ↑(span R₀ ({c} ∪ ⋃ i, coeff(e.val i)) ^ e₁.powBound)
hq₁g₁ : ∀ x ∈ T₁, ∀ (i : Fin x.n), q₁.toLinearMap (g₁ x i) = q₁ c ^ e₁.powBound * x.g i
n₁ : Localization.Away c → ℕ
f₁ : Localization.Away c → R
hf₁ : ∀ (x : Localization.Away c), x * q₁ c ^ n₁ x = q₁ (f₁ x)
g₂ : (x : BasicConstructibleSetData (R ⧸ Ideal.span {c})) → Fin x.n → R
hg₂ : ∀ x ∈ T₂, ∀ (i : Fin x.n), g₂ x i ∈ ↑(coeffSubmodule R₀ e ^ e₂.powBound)
hq₂g₂ : ∀ x ∈ T₂, ∀ (i : Fin x.n), q₂.toLinearMap (g₂ x i) = x.g i
f₂ : R ⧸ Ideal.span {c} → R
hf₂ : ∀ (x : R ⧸ Ideal.span {c}), q₂ (f₂ x) = x
S₁ : Finset (BasicConstructibleSetData R) := ⋯
S₂ : Finset (BasicConstructibleSetData R) := ⋯
x : BasicConstructibleSetData (Localization.Away c)
hx : x ∈ T₁
k : Fin x.n
⊢ 1 ≤ e.degBound

Tactic:
· lia

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

Goal state before:
pp: case ht
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
degBound_e₂_lt : e₂.degBound < e.degBound
H₁ : Statement R₀ (Localization.Away c) n e₁
H₂ : Statement R₀ (R ⧸ Ideal.span {c}) n e₂
f : R[X]
T₁ : ConstructibleSetData (Localization.Away c)
T₂ : ConstructibleSetData (R ⧸ Ideal.span {c})
hT₁ : comap Polynomial.C '' (zeroLocus (Set.range e₁.val) \ zeroLocus {(mapRingHom ↑q₁) f}) = T₁.toSet
hT₁deg : ∀ x ∈ T₁, x.n ≤ e₁.degBound
hT₂ : comap Polynomial.C '' (zeroLocus (Set.range e₂.val) \ zeroLocus {(mapRingHom ↑q₂) f}) = T₂.toSet
hT₂deg : ∀ x ∈ T₂, x.n ≤ e₂.degBound
x✝ : Invertible (q₁ c) := ⋯
he₁span :
  coeffSubmodule R₀ e₁ ^ e₁.powBound =
    ⅟(q₁ c ^ e₁.powBound) • Submodule.map q₁.toLinearMap (span R₀ ({c} ∪ ⋃ i, coeff(e.val i)) ^ e₁.powBound)
g₁ : (x : BasicConstructibleSetData (Localization.Away c)) → Fin x.n → R
hg₁ : ∀ x ∈ T₁, ∀ (i : Fin x.n), g₁ x i ∈ ↑(span R₀ ({c} ∪ ⋃ i, coeff(e.val i)) ^ e₁.powBound)
hq₁g₁ : ∀ x ∈ T₁, ∀ (i : Fin x.n), q₁.toLinearMap (g₁ x i) = q₁ c ^ e₁.powBound * x.g i
n₁ : Localization.Away c → ℕ
f₁ : Localization.Away c → R
hf₁ : ∀ (x : Localization.Away c), x * q₁ c ^ n₁ x = q₁ (f₁ x)
g₂ : (x : BasicConstructibleSetData (R ⧸ Ideal.span {c})) → Fin x.n → R
hg₂ : ∀ x ∈ T₂, ∀ (i : Fin x.n), g₂ x i ∈ ↑(coeffSubmodule R₀ e ^ e₂.powBound)
hq₂g₂ : ∀ x ∈ T₂, ∀ (i : Fin x.n), q₂.toLinearMap (g₂ x i) = x.g i
f₂ : R ⧸ Ideal.span {c} → R
hf₂ : ∀ (x : R ⧸ Ideal.span {c}), q₂ (f₂ x) = x
S₁ : Finset (BasicConstructibleSetData R) := ⋯
S₂ : Finset (BasicConstructibleSetData R) := ⋯
x : BasicConstructibleSetData (R ⧸ Ideal.span {c})
hx : x ∈ T₂
k : Fin x.n
⊢ 1 ≤ e.degBound

Tactic:
· lia

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] {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R],
    Statement R₀ R n { val := 0 }

Tactic:
intro R

Goal state after:
case hP₁
R✝ : Type u_2
inst✝ : CommRing R✝
n : ℕ
R : Type u_2
⊢ ∀ [inst : CommRing R] {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n { val := 0 }
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] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic →
      (∀ (j : Fin n), j ≠ i → e.val j = 0) →
        ∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n e

Tactic:
intro R

Goal state after:
case hP₂
R✝ : Type u_2
inst✝ : CommRing R✝
n : ℕ
R : Type u_2
⊢ ∀ [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic →
      (∀ (j : Fin n), j ≠ i → e.val j = 0) →
        ∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n e
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] (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree →
        i ≠ j →
          (∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R],
              Statement R₀ R n { val := Function.update e.val j (e.val j %ₘ e.val i) }) →
            ∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n e

Tactic:
intro R

Goal state after:
case hP₃
R✝ : Type u_2
inst✝ : CommRing R✝
n : ℕ
R : Type u_2
⊢ ∀ [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 →
          (∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R],
              Statement R₀ R n { val := Function.update e.val j (e.val j %ₘ e.val i) }) →
            ∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n e
Module: Mathlib.AlgebraicGeometry.Cover.Sigma

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : UnivLE.{v, u}
inst✝ : P.IsMultiplicative
𝒰✝ 𝒱 𝒰 : Cover (precoverage P) S
⊢ (Hom.sigma (𝟙 𝒰)).h₀ ≍ (𝟙 𝒰.sigma).h₀

Tactic:
simp only [sigma_I₀, sigma_X, heq_eq_eq]
    ext j : 1
    exact Sigma.hom_ext _ _ (by simp)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Sigma

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : UnivLE.{v, u}
inst✝ : P.IsMultiplicative
𝒰 𝒱 X✝ Y✝ Z✝ : Cover (precoverage P) S
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (Hom.sigma (f ≫ g)).h₀ ≍ (Hom.sigma f ≫ Hom.sigma g).h₀

Tactic:
simp only [sigma_I₀, sigma_X, heq_eq_eq]
    ext j : 1
    exact Sigma.hom_ext _ _ (by simp)

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 : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        (∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : 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_1 : CommRing R₀] [inst_2 : 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_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n e

Tactic:
intro R

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),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        (∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : 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_1 : CommRing R₀] [inst_2 : 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_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n e
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
⊢ Irreducible W.polynomial

Tactic:
by_contra h
  rcases (monic_polynomial.not_irreducible_iff_exists_add_mul_eq_coeff natDegree_polynomial).mp h
    with ⟨f, g, h0, h1⟩
  simp only [polynomial_eq, Cubic.coeff_eq_c, Cubic.coeff_eq_d] at h0 h1
  apply_fun degree at h0 h1
  rw [Cubic.degree_of_a_ne_zero' <| neg_ne_zero.mpr <| one_ne_zero' R, degree_mul] at h0
  apply (h1.symm.le.trans Cubic.degree_of_b_eq_zero').not_gt
  rcases Nat.WithBot.add_eq_three_iff.mp h0.symm with h | h | h | h
  iterate 2 rw [degree_add_eq_right_of_degree_lt] <;> simp only [h] <;> decide
  iterate 2 rw [degree_add_eq_left_of_degree_lt] <;> simp only [h] <;> decide

Goal state after: