mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ ((P y * Q z - Q y * P z) ^ 2 * P z * Q z + W'.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z) -
            W'.a₂ * P z * Q z * (P x * Q z - Q x * P z) ^ 2 -
          P x * Q z * (P x * Q z - Q x * P z) ^ 2 -
        Q x * P z * (P x * Q z - Q x * P z) ^ 2) *
      (P x * Q z - Q x * P z) =
    0

Tactic:
hx

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ ((P y * Q z - Q y * P z) ^ 2 * P z * Q z + W'.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (Q x * P z - Q x * P z) -
            W'.a₂ * P z * Q z * (Q x * P z - Q x * P z) ^ 2 -
          Q x * P z * (Q x * P z - Q x * P z) ^ 2 -
        Q x * P z * (Q x * P z - Q x * P z) ^ 2) *
      (Q x * P z - Q x * P z) =
    0
Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.Smooth
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.Smooth R S
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth) f

Tactic:
obtain ⟨s, hs, h⟩ := Algebra.Smooth.exists_span_eq_top_isStandardSmooth R S

Goal state after:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.Smooth
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.Smooth R S
s : Set S
hs : Ideal.span s = ⊤
h : ∀ x ∈ s, Algebra.IsStandardSmooth R (Localization.Away x)
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth) f
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ⇑f ⁻¹' U.carrier
⊢ ∃ U,
    ∃ (_ : IsAffineOpen U),
      ∃ V, ∃ (_ : IsAffineOpen V) (hVU : V ≤ f ⁻¹ᵁ U), x ∈ V ∧ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).Smooth

Tactic:
have := f.finitePresentation_appLE hU hV hVU

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ⇑f ⁻¹' U.carrier
this : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
⊢ ∃ U,
    ∃ (_ : IsAffineOpen U),
      ∃ V, ∃ (_ : IsAffineOpen V) (hVU : V ≤ f ⁻¹ᵁ U), x ∈ V ∧ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).Smooth
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case refine_2
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H :
  (Algebra.adjoin k (a '' {i}ᶜ)).val
      ((aeval fun j ↦ ⟨a ↑j, ⋯⟩)
        (((optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)).coeff (σ i))) =
    (Algebra.adjoin k (a '' {i}ᶜ)).val 0
⊢ (aeval a) ((rename Subtype.val) (F₀.coeff (σ i))) = 0

Tactic:
map_zero

Goal state after:
case refine_2
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H :
  (Algebra.adjoin k (a '' {i}ᶜ)).val
      ((aeval fun j ↦ ⟨a ↑j, ⋯⟩)
        (((optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)).coeff (σ i))) =
    0
⊢ (aeval a) ((rename Subtype.val) (F₀.coeff (σ i))) = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z = Q x * P z
⊢ (P y * Q z - Q y * P z) *
        ((P y * Q z - Q y * P z) ^ 2 * P z * Q z +
                  W'.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z) -
                W'.a₂ * P z * Q z * (P x * Q z - Q x * P z) ^ 2 -
              P x * Q z * (P x * Q z - Q x * P z) ^ 2 -
            Q x * P z * (P x * Q z - Q x * P z) ^ 2 -
          P x * Q z * (P x * Q z - Q x * P z) ^ 2) +
      P y * Q z * (P x * Q z - Q x * P z) ^ 3 =
    (P y * Q z - Q y * P z) ^ 3 * (P z * Q z)

Tactic:
hx

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z = Q x * P z
⊢ (P y * Q z - Q y * P z) *
        ((P y * Q z - Q y * P z) ^ 2 * P z * Q z +
                  W'.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (Q x * P z - Q x * P z) -
                W'.a₂ * P z * Q z * (Q x * P z - Q x * P z) ^ 2 -
              Q x * P z * (Q x * P z - Q x * P z) ^ 2 -
            Q x * P z * (Q x * P z - Q x * P z) ^ 2 -
          Q x * P z * (Q x * P z - Q x * P z) ^ 2) +
      P y * Q z * (Q x * P z - Q x * P z) ^ 3 =
    (P y * Q z - Q y * P z) ^ 3 * (P z * Q z)
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
p : ℕ
hp : Nat.Prime p
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
F' : ↥F.support →₀ k
hF' : (Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) F' = 0
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (fun s ↦ σ' ↑s) F')
hF'' : coeff 0 F'' = 0
hpm : p * F''.totalDegree ≤ F.totalDegree
hF''0 : F''.totalDegree = 0
⊢ C 0 = 0

Tactic:
map_zero

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
p : ℕ
hp : Nat.Prime p
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
F' : ↥F.support →₀ k
hF' : (Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) F' = 0
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (fun s ↦ σ' ↑s) F')
hF'' : coeff 0 F'' = 0
hpm : p * F''.totalDegree ≤ F.totalDegree
hF''0 : F''.totalDegree = 0
⊢ 0 = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
⊢ IsOpenImmersion (Spec.map (CommRingCat.ofHom (TensorProduct.lmul' R).toRingHom))

Tactic:
rw [isOpenImmersion_SpecMap_iff_of_surjective _ (fun x ↦ ⟨1 ⊗ₜ x, by simp⟩)]
  apply (Ideal.isIdempotentElem_iff_of_fg _ (KaehlerDifferential.ideal_fg R S)).mp
  apply (Ideal.cotangent_subsingleton_iff _).mp
  exact inferInstanceAs <| Subsingleton Ω[S⁄R]

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

Goal state before:
pp: case refine_2
W P Q : MorphismProperty Scheme
X Y : Scheme
inst✝³ : W.IsStableUnderBaseChange
inst✝² : Scheme.IsJointlySurjectivePreserving W
inst✝¹ : P.RespectsIso
inst✝ : P.RespectsLeft IsOpenImmersion
X✝ Y✝ : Scheme
f : X✝ ⟶ Y✝
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X✝
h : ∀ (i : 𝒰.I₀), sourceLocalClosure IsOpenImmersion P (𝒰.f i ≫ f)
⊢ sourceLocalClosure IsOpenImmersion P f

Tactic:
choose 𝒱 h𝒱 using h

Goal state after:
case refine_2
W P Q : MorphismProperty Scheme
X Y : Scheme
inst✝³ : W.IsStableUnderBaseChange
inst✝² : Scheme.IsJointlySurjectivePreserving W
inst✝¹ : P.RespectsIso
inst✝ : P.RespectsLeft IsOpenImmersion
X✝ Y✝ : Scheme
f : X✝ ⟶ Y✝
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X✝
𝒱 : (i : 𝒰.I₀) → Scheme.Cover (Scheme.precoverage IsOpenImmersion) (𝒰.X i)
h𝒱 : ∀ (i : 𝒰.I₀) (i_1 : (𝒱 i).I₀), P ((𝒱 i).f i_1 ≫ 𝒰.f i ≫ f)
⊢ sourceLocalClosure IsOpenImmersion P f
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case refine_1
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
inst✝¹ : ExpChar k p
inst✝ : Algebra.EssFiniteType k K
s : Finset K
hs : (fun t ↦ IsTranscendenceBasis k Subtype.val) ↑s
Hs :
  ∀ ⦃j : Set K⦄,
    (fun t ↦ IsTranscendenceBasis k Subtype.val) j →
      (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) ↑s ≤
          (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) j →
        (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) j ≤
          (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) ↑s
n : K
hn : ¬IsSeparable (↥(adjoin k ↑s)) n
hns : n ∉ s
i : K
hi₁ : IsTranscendenceBasis k fun j ↦ id ↑j
hi₂ : IsSeparable (↥(adjoin k (insert n ↑s \ {i}))) (id i)
x : K
⊢ x ∈ ↑s → x ∈ ↑(restrictScalars k (separableClosure (↥(adjoin k (insert n ↑s \ {i}))) K))

Tactic:
hx

Goal state after:
case refine_1
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
inst✝¹ : ExpChar k p
inst✝ : Algebra.EssFiniteType k K
s : Finset K
hs : (fun t ↦ IsTranscendenceBasis k Subtype.val) ↑s
Hs :
  ∀ ⦃j : Set K⦄,
    (fun t ↦ IsTranscendenceBasis k Subtype.val) j →
      (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) ↑s ≤
          (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) j →
        (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) j ≤
          (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) ↑s
n : K
hn : ¬IsSeparable (↥(adjoin k ↑s)) n
hns : n ∉ s
i : K
hi₁ : IsTranscendenceBasis k fun j ↦ id ↑j
hi₂ : IsSeparable (↥(adjoin k (insert n ↑s \ {i}))) (id i)
x : K
hx : x ∈ ↑s
⊢ x ∈ ↑(restrictScalars k (separableClosure (↥(adjoin k (insert n ↑s \ {i}))) K))
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
x : S
f : S →ₐ[R] T
hf : Function.Injective ⇑f
h : IsStronglyTranscendental R (f x)
u : S
p : R[X]
hp : (aeval x) p * u = 0
⊢ f 0 = 0

Tactic:
map_zero

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
x : S
f : S →ₐ[R] T
hf : Function.Injective ⇑f
h : IsStronglyTranscendental R (f x)
u : S
p : R[X]
hp : (aeval x) p * u = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
M : Submonoid R
inst✝¹ : IsLocalization M S
inst✝ : IsScalarTower R S T
x : T
h : IsStronglyTranscendental R x
t : T
p : S[X]
hp : (aeval x) p * t = 0
a : R
ha₁ : a ∈ M
ha₂ : map (algebraMap R S) (IsLocalization.integerNormalization M p) = a • p
⊢ (aeval x) (IsLocalization.integerNormalization M p) = a • (aeval x) p

Tactic:
simpa [AlgHom.map_smul_of_tower] using congr(aeval x $ha₂)

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.GoingDown

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i : ℕ
hi : i ≠ q.natDegree
⊢ q.coeff i ∈ (Ideal.span {x | ∃ i < p.natDegree, p.coeff i = x}).radical

Tactic:
Ideal.radical_eq_sInf,

Goal state after:
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i : ℕ
hi : i ≠ q.natDegree
⊢ q.coeff i ∈ sInf {J | Ideal.span {x | ∃ i < p.natDegree, p.coeff i = x} ≤ J ∧ J.IsPrime}
Module: Mathlib.RingTheory.IntegralClosure.GoingDown

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Algebra.IsIntegral R S
inst✝² : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst✝¹ : p.IsPrime
Q : Ideal S
inst✝ : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
x : R
⊢ x ∈ Ideal.comap (algebraMap R SQ) (Ideal.map (algebraMap R SQ) p) → x ∈ p

Tactic:
hx

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Algebra.IsIntegral R S
inst✝² : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst✝¹ : p.IsPrime
Q : Ideal S
inst✝ : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
x : R
hx : x ∈ Ideal.comap (algebraMap R SQ) (Ideal.map (algebraMap R SQ) p)
⊢ x ∈ p
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hv : IsTrivialOn K v
hle : v RatFunc.X ≤ 1
p : K[X]
⊢ v ↑p ≤ 1

Tactic:
by
  rw [as_sum_range p, RatFunc.coePolynomial, map_sum]
  apply map_sum_le v
  intro i
  by_cases h0 : p.coeff i = 0
  · simp_all
  · rw [← RatFunc.coePolynomial]
    simp_all [pow_le_one', ← RatFunc.algebraMap_eq_C, hv.eq_one _ h0]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R[X]
q : S[X]
hp : p.Monic
hq : q.Monic
H : q ∣ map (algebraMap R S) p
i : ℕ
a✝ : Nontrivial S
T : Type u_2
w✝⁴ : CommRing T
w✝³ : Algebra S T
w✝² : Module.Finite S T
w✝¹ : Module.Free S T
w✝ : Nontrivial T
hqT : (map (algebraMap S T) q).Splits
algInst✝ : Algebra R T := ((algebraMap S T).comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
x : T
⊢ (map (algebraMap S T) q).IsRoot x → IsIntegral R x

Tactic:
hx

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R[X]
q : S[X]
hp : p.Monic
hq : q.Monic
H : q ∣ map (algebraMap R S) p
i : ℕ
a✝ : Nontrivial S
T : Type u_2
w✝⁴ : CommRing T
w✝³ : Algebra S T
w✝² : Module.Finite S T
w✝¹ : Module.Free S T
w✝ : Nontrivial T
hqT : (map (algebraMap S T) q).Splits
algInst✝ : Algebra R T := ((algebraMap S T).comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
x : T
hx : (map (algebraMap S T) q).IsRoot x
⊢ IsIntegral R x
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hp : IsIntegral R[X] p
i : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun i ↦ (q.coeff i).natDegree) + p.natDegree + 1
⊢ IsIntegral R (p.coeff i)

Tactic:
have hm₁ (i) : (q.coeff i).natDegree < m := by
    by_cases hi : i ∈ q.support
    · exact (Finset.le_sup (f := fun i ↦ (q.coeff i).natDegree) hi).trans_lt (by lia)
    · simp_all [m]

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hp : IsIntegral R[X] p
i : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun i ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
⊢ IsIntegral R (p.coeff i)
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField))) ⋯ ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
x✝ : I.ResidueField[X]
x : I.ResidueField[X]
⊢ (aeval ((algebraMap R[X] J.ResidueField) X)) x = 0 → x = 0

Tactic:
hx

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField))) ⋯ ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
x✝ : I.ResidueField[X]
x : I.ResidueField[X]
hx : (aeval ((algebraMap R[X] J.ResidueField) X)) x = 0
⊢ x = 0
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : QuasiFinite R (Localization.AtPrime p ⧸ Ideal.map (algebraMap R (Localization.AtPrime p)) (Ideal.under R p))
q : Ideal T
inst✝ : q.IsPrime
f : Localization.AtPrime p →ₐ[R] Localization.AtPrime q
hf : Function.Surjective ⇑f
x : R
⊢ x ∈ Ideal.under R p → x ∈ Ideal.under R q

Tactic:
hx

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : QuasiFinite R (Localization.AtPrime p ⧸ Ideal.map (algebraMap R (Localization.AtPrime p)) (Ideal.under R p))
q : Ideal T
inst✝ : q.IsPrime
f : Localization.AtPrime p →ₐ[R] Localization.AtPrime q
hf : Function.Surjective ⇑f
x : R
hx : x ∈ Ideal.under R p
⊢ x ∈ Ideal.under R q
Module: Mathlib.RingTheory.QuasiFinite.Polynomial

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R[X] →ₐ[R] S
hf : Function.Surjective ⇑f
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : Algebra.WeaklyQuasiFiniteAt R P
H : RingHom.ker f ≤ Ideal.map C (Ideal.under R P)
algInst✝ : Algebra R[X] S := f.toAlgebra
p : Ideal R := Ideal.under R P
x : R[X]
⊢ x ∈ RingHom.ker f → x ∈ Ideal.comap (mapRingHom (algebraMap R p.ResidueField)) ⊥

Tactic:
hx

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R[X] →ₐ[R] S
hf : Function.Surjective ⇑f
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : Algebra.WeaklyQuasiFiniteAt R P
H : RingHom.ker f ≤ Ideal.map C (Ideal.under R P)
algInst✝ : Algebra R[X] S := f.toAlgebra
p : Ideal R := Ideal.under R P
x : R[X]
hx : x ∈ RingHom.ker f
⊢ x ∈ Ideal.comap (mapRingHom (algebraMap R p.ResidueField)) ⊥
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
I : Ideal R
inst✝⁵ : I.IsPrime
J : Ideal R[X]
inst✝⁴ : J.IsPrime
inst✝³ : J.LiesOver I
inst✝² : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra I J
f : R[X] →ₐ[R] S
hf : Function.Surjective ⇑f
p : Ideal R
inst✝ : p.IsPrime
this :
  (AlgHom.restrictScalars R (aeval (1 ⊗ₜ[R] f X))).comp (mapAlgHom (Algebra.ofId R p.ResidueField)) =
    Algebra.TensorProduct.includeRight.comp f
⊢ RingHom.ker ↑f ≤ RingHom.ker (Algebra.TensorProduct.includeRight.comp f)

Tactic:
intro; aesop

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyQuasiFinite f
inst✝ : IsLocallyArtinian Y
⊢ IsLocallyArtinian X

Tactic:
change id _

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyQuasiFinite f
inst✝ : IsLocallyArtinian Y
⊢ id (IsLocallyArtinian X)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyQuasiFinite f
inst✝¹ : QuasiCompact f
inst✝ : IsLocallyArtinian Y
⊢ IsFinite f

Tactic:
change id _

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyQuasiFinite f
inst✝¹ : QuasiCompact f
inst✝ : IsLocallyArtinian Y
⊢ id (IsFinite f)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
⊢ LocallyQuasiFinite f

Tactic:
change id _

Goal state after:
X Y : Scheme
f : X ⟶ Y
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
⊢ id (LocallyQuasiFinite f)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this✝ :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    (∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)) → (∃ R, Y = Spec R) → id (LocallyQuasiFinite f)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
x : ↥(Y.affineCover.X i)
this : ∀ (x : ↥Y), IsLocallyArtinian (Hom.fiber f x)
⊢ LocallyQuasiFinite
    (Hom.fiberToSpecResidueField (pullback.snd f (Y.affineCover.f i)) x ≫
      Spec.map (Hom.residueFieldMap (Y.affineCover.f i) x))

Tactic:
let g : (pullback.snd f (Y.affineCover.f i)).fiber x ⟶ f.fiber (Y.affineCover.f i x) :=
      pullback.map _ _ _ _ (pullback.fst _ _) (Spec.map ((Y.affineCover.f i).residueFieldMap _))
        (Y.affineCover.f i) (by simp [pullback.condition]) (by simp)

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this✝ :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    (∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)) → (∃ R, Y = Spec R) → id (LocallyQuasiFinite f)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
x : ↥(Y.affineCover.X i)
this : ∀ (x : ↥Y), IsLocallyArtinian (Hom.fiber f x)
g : Hom.fiber (pullback.snd f (Y.affineCover.f i)) x ⟶ Hom.fiber f ((Y.affineCover.f i) x) :=
  pullback.map (pullback.snd f (Y.affineCover.f i)) ((Y.affineCover.X i).fromSpecResidueField x) f
    (Y.fromSpecResidueField ((Y.affineCover.f i) x)) (pullback.fst f (Y.affineCover.f i))
    (Spec.map (Hom.residueFieldMap (Y.affineCover.f i) x)) (Y.affineCover.f i) ⋯ ⋯
⊢ LocallyQuasiFinite
    (Hom.fiberToSpecResidueField (pullback.snd f (Y.affineCover.f i)) x ≫
      Spec.map (Hom.residueFieldMap (Y.affineCover.f i) x))
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
U V : X.AffineZariskiSite
h : (toOpensFunctor X).obj U ⟶ (toOpensFunctor X).obj V
x : ↥X
⊢ x ∈ (toOpensFunctor X).obj U →
    ∃ U_1 f, (Sieve.functorPushforward (toOpensFunctor X) ((toOpensFunctor X).imageSieve h)).arrows f ∧ x ∈ U_1

Tactic:
hx

Goal state after:
X : Scheme
U V : X.AffineZariskiSite
h : (toOpensFunctor X).obj U ⟶ (toOpensFunctor X).obj V
x : ↥X
hx : x ∈ (toOpensFunctor X).obj U
⊢ ∃ U_1 f, (Sieve.functorPushforward (toOpensFunctor X) ((toOpensFunctor X).imageSieve h)).arrows f ∧ x ∈ U_1