mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
⊢ ∀ r ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1},
    ∀ s ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1},
      r * s ∈ RingHom.ker (compLocalizationAwayAlgHom T g P)

Tactic:
intro x

Goal state after:
case a
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
x : ((localizationAway T g).comp P).Ring
⊢ x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} →
    ∀ s ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1},
      x * s ∈ RingHom.ker (compLocalizationAwayAlgHom T g P)
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ D.presLeft.ker ≤ P.ker

Tactic:
intro x

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
x : D.presLeft.Ring
⊢ x ∈ D.presLeft.ker → x ∈ P.ker
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : (algebraMap R T).IsStandardSmooth
⊢ Algebra.IsStandardSmooth R T

Tactic:
RingHom.IsStandardSmooth

Goal state after:
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmooth R T
⊢ Algebra.IsStandardSmooth R T
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmooth R T
this : Algebra.IsStandardSmooth S (S ⊗[R] T)
⊢ (algebraMap S (S ⊗[R] T)).IsStandardSmooth

Tactic:
RingHom.IsStandardSmooth

Goal state after:
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmooth R T
this : Algebra.IsStandardSmooth S (S ⊗[R] T)
⊢ Algebra.IsStandardSmooth S (S ⊗[R] T)
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: case h₂
⊢ ∀ ⦃R S T : Type u_2⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], (algebraMap R T).IsStandardSmooth → (algebraMap S (S ⊗[R] T)).IsStandardSmooth

Tactic:
· introv h
    replace h : Algebra.IsStandardSmooth R T := by
      rw [RingHom.IsStandardSmooth] at h; convert! h; ext; simp_rw [Algebra.smul_def]; rfl
    suffices Algebra.IsStandardSmooth S (S ⊗[R] T) by
      rw [RingHom.IsStandardSmooth]; convert! this; ext; simp_rw [Algebra.smul_def]; rfl
    infer_instance

Goal state after:
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
hQ : W'.Equation Q
hQz : Q z = 0
⊢ W'.addX P Q = -(Q y ^ 2 * P z) * P x

Tactic:
by
  rw [addX, hQz, X_eq_zero_of_Z_eq_zero hQ hQz]
  ring1

Goal state after:
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
⊢ W'.addX P Q * (P z * Q z) ^ 2 = 0

Tactic:
rw [addX_eq' hP hQ, 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.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: n : ℕ
X Y : Scheme
f : X ⟶ Y
inst✝ : SmoothOfRelativeDimension n f
⊢ ∀ (x : ↥X),
    ∃ U,
      ∃ (_ : IsAffineOpen U),
        ∃ V,
          ∃ (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ f ⁻¹ᵁ U),
            (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth

Tactic:
intro x

Goal state after:
n : ℕ
X Y : Scheme
f : X ⟶ Y
inst✝ : SmoothOfRelativeDimension n f
x : ↥X
⊢ ∃ U,
    ∃ (_ : IsAffineOpen U),
      ∃ V,
        ∃ (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ f ⁻¹ᵁ U),
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: case inr
X : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
this :
  ∀ {X : Scheme} [IsReduced X] (f : X ⟶ Spec (CommRingCat.of K)) [inst : LocallyOfFinitePresentation f],
    CompactSpace ↥X → Dense ↑(smoothLocus f)
H : ¬CompactSpace ↥X
⊢ ∀ (x : ↥X), x ∈ closure ↑(smoothLocus f)

Tactic:
intro x

Goal state after:
case inr
X : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
this :
  ∀ {X : Scheme} [IsReduced X] (f : X ⟶ Spec (CommRingCat.of K)) [inst : LocallyOfFinitePresentation f],
    CompactSpace ↥X → Dense ↑(smoothLocus f)
H : ¬CompactSpace ↥X
x : ↥X
⊢ x ∈ closure ↑(smoothLocus f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X✝ : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
X : Scheme
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
H : CompactSpace ↥X
this : IsNoetherian X
⊢ ∀ (x : ↥X), x ∈ closure ↑(smoothLocus f)

Tactic:
intro x

Goal state after:
X✝ : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
X : Scheme
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
H : CompactSpace ↥X
this : IsNoetherian X
x : ↥X
⊢ x ∈ closure ↑(smoothLocus f)
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
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
n : ι
inst✝ : ExpChar k p
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
S : Set (MvPolynomial ι k) := {F | F ≠ 0 ∧ (aeval a) F = 0}
F : MvPolynomial ι k
hFmin : ∀ (G : MvPolynomial ι k), G ≠ 0 → (aeval a) G = 0 → F.totalDegree ≤ G.totalDegree
hF₀ : F ≠ 0
hFa : (aeval a) F = 0
hFirr : Irreducible F
i : ι
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hi : ¬p ∣ σ i
hσi : σ i ≠ 0
alg : IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)
Hi : IsTranscendenceBasis k fun x ↦ a ↑x
k' : IntermediateField k K := adjoin k (a '' {i}ᶜ)
hF₁irr : Irreducible (F.toPolynomialAdjoinImageCompl a i)
this✝ : UniqueFactorizationMonoid ↥(Algebra.adjoin k (a '' {i}ᶜ))
hF₂irr :
  Irreducible (Polynomial.map (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k') (F.toPolynomialAdjoinImageCompl a i))
Hsep : ¬IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
this : CharP (↥k') p
g : Polynomial ↥k'
hg : Irreducible g
eq : ((Polynomial.expand (↥k') p) g).coeff (σ i) = (minpoly (↥k') (a i)).coeff (σ i)
⊢ (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0

Tactic:
← minpoly.eq_of_irreducible hF₂irr ((Polynomial.aeval_map_algebraMap ..).trans
    (aeval_toPolynomialAdjoinImageCompl_eq_zero hFa i)),

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
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
n : ι
inst✝ : ExpChar k p
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
S : Set (MvPolynomial ι k) := {F | F ≠ 0 ∧ (aeval a) F = 0}
F : MvPolynomial ι k
hFmin : ∀ (G : MvPolynomial ι k), G ≠ 0 → (aeval a) G = 0 → F.totalDegree ≤ G.totalDegree
hF₀ : F ≠ 0
hFa : (aeval a) F = 0
hFirr : Irreducible F
i : ι
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hi : ¬p ∣ σ i
hσi : σ i ≠ 0
alg : IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)
Hi : IsTranscendenceBasis k fun x ↦ a ↑x
k' : IntermediateField k K := adjoin k (a '' {i}ᶜ)
hF₁irr : Irreducible (F.toPolynomialAdjoinImageCompl a i)
this✝ : UniqueFactorizationMonoid ↥(Algebra.adjoin k (a '' {i}ᶜ))
hF₂irr :
  Irreducible (Polynomial.map (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k') (F.toPolynomialAdjoinImageCompl a i))
Hsep : ¬IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
this : CharP (↥k') p
g : Polynomial ↥k'
hg : Irreducible g
eq :
  ((Polynomial.expand (↥k') p) g).coeff (σ i) =
    (Polynomial.map (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k') (F.toPolynomialAdjoinImageCompl a i) *
          Polynomial.C
            (Polynomial.map (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k')
                  (F.toPolynomialAdjoinImageCompl a i)).leadingCoeff⁻¹).coeff
      (σ i)
⊢ (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst✝¹ : IsClosedImmersion i
f : X ⟶ Y
inst✝ : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this✝¹ : IsDominant i
x : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f (g₁ x) ∈ ↑U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : g₁ x ∈ ↑V
hVU : V ≤ f ⁻¹ᵁ U
this✝ : g₁.base = g₂.base
W : Opens ↥Z
hW : W ∈ Z.affineOpens
hxW : x ∈ ↑W
hWV : W ≤ g₁ ⁻¹ᵁ V ⊓ g₂ ⁻¹ᵁ V
this : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FormallyUnramified
algInst✝¹ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algInst✝ : Algebra ↑Γ(Y, U) ↑Γ(Z, W) := (CommRingCat.Hom.hom (Scheme.Hom.appLE (g₁ ≫ f) U W ⋯)).toAlgebra
algebraizeInst✝ : Algebra.FormallyUnramified ↑Γ(Y, U) ↑Γ(X, V)
ψ₁ : ↑Γ(X, V) →ₐ[↑Γ(Y, U)] ↑Γ(Z, W) := { toRingHom := CommRingCat.Hom.hom (Scheme.Hom.appLE g₁ V W ⋯), commutes' := ⋯ }
ψ₂ : ↑Γ(X, V) →ₐ[↑Γ(Y, U)] ↑Γ(Z, W) := { toRingHom := CommRingCat.Hom.hom (Scheme.Hom.appLE g₂ V W ⋯), commutes' := ⋯ }
⊢ Scheme.Opens.ι W ≫ g₁ = Scheme.Opens.ι W ≫ g₂

Tactic:
suffices ψ₁ = ψ₂ by
    simpa [ψ₁, ψ₂, -Iso.cancel_iso_hom_left, IsAffineOpen.isoSpec_hom] using
      congr(hW.isoSpec.hom ≫ Spec.map (CommRingCat.ofHom ($this).toRingHom) ≫ hV.fromSpec)

Goal state after:
X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst✝¹ : IsClosedImmersion i
f : X ⟶ Y
inst✝ : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this✝¹ : IsDominant i
x : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f (g₁ x) ∈ ↑U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : g₁ x ∈ ↑V
hVU : V ≤ f ⁻¹ᵁ U
this✝ : g₁.base = g₂.base
W : Opens ↥Z
hW : W ∈ Z.affineOpens
hxW : x ∈ ↑W
hWV : W ≤ g₁ ⁻¹ᵁ V ⊓ g₂ ⁻¹ᵁ V
this : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FormallyUnramified
algInst✝¹ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algInst✝ : Algebra ↑Γ(Y, U) ↑Γ(Z, W) := (CommRingCat.Hom.hom (Scheme.Hom.appLE (g₁ ≫ f) U W ⋯)).toAlgebra
algebraizeInst✝ : Algebra.FormallyUnramified ↑Γ(Y, U) ↑Γ(X, V)
ψ₁ : ↑Γ(X, V) →ₐ[↑Γ(Y, U)] ↑Γ(Z, W) := { toRingHom := CommRingCat.Hom.hom (Scheme.Hom.appLE g₁ V W ⋯), commutes' := ⋯ }
ψ₂ : ↑Γ(X, V) →ₐ[↑Γ(Y, U)] ↑Γ(Z, W) := { toRingHom := CommRingCat.Hom.hom (Scheme.Hom.appLE g₂ V W ⋯), commutes' := ⋯ }
⊢ ψ₁ = ψ₂
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)
⊢ ↑s ⊆ ↑(restrictScalars k (separableClosure (↥(adjoin k (insert n ↑s \ {i}))) K))

Tactic:
intro x

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
⊢ 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
inst✝³ : CommRing R
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : FaithfulSMul R K
x : K
h : Transcendental R x
⊢ IsStronglyTranscendental R x

Tactic:
simpa [IsStronglyTranscendental, or_imp, forall_and, @forall_comm K, ← subsingleton_iff_forall_eq,
    not_subsingleton, ext_iff, forall_or_left, ← imp_iff_or_not, transcendental_iff] using h

Goal state after:
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
⊢ Ideal.comap (algebraMap R SQ) (Ideal.map (algebraMap R SQ) p) ≤ p

Tactic:
intro x

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
⊢ x ∈ Ideal.comap (algebraMap R SQ) (Ideal.map (algebraMap R SQ) p) → x ∈ p
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: case refine_2.hf
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
f : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I →+* S ⧸ Ideal.map (algebraMap R S) I :=
  Ideal.Quotient.lift (Ideal.map (algebraMap R ↥R[x]) I)
    ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) ⋯
y : S ⧸ Ideal.map (algebraMap R S) I
z : S
hz : (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) z = y
this : y ∈ Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) (conductor R x)
⊢ Function.Surjective ⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) I))

Tactic:
· exact Ideal.Quotient.mk_surjective

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:
intro x

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
⊢ (map (algebraMap S T) q).IsRoot x → IsIntegral R x
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: case e'_6
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S},
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f →
      ∀ (n : σ →₀ ℕ), Finite σ → IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial (↥f.vars) S
hg : (rename Subtype.val) g = f
n : ↥f.vars →₀ ℕ
⊢ f = ((rename Subtype.val).comp (killCompl ⋯)).toRingHom f

Tactic:
nth_rw 1 12 [← hg]; simp

Goal state after:
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]
⊢ ∀ (a : I.ResidueField[X]), (aeval ((algebraMap R[X] J.ResidueField) X)) a = 0 → a = 0

Tactic:
intro x

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]
⊢ (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
⊢ Ideal.under R p ≤ Ideal.under R q

Tactic:
intro x

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
⊢ 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
⊢ RingHom.ker f ≤ Ideal.comap (mapRingHom (algebraMap R p.ResidueField)) ⊥

Tactic:
intro x

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]
⊢ x ∈ RingHom.ker f → x ∈ Ideal.comap (mapRingHom (algebraMap R p.ResidueField)) ⊥
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : p.IsPrime
inst✝² : q.LiesOver p
Q : Ideal (p.Fiber S)
inst✝¹ : Q.IsPrime
hQ : Ideal.comap TensorProduct.includeRight.toRingHom Q = q
inst✝ : QuasiFiniteAt p.ResidueField Q
Sq : Type u_2 := Localization.AtPrime q
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
φ₁ : p.ResidueField →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  Ideal.quotientMapₐ (Ideal.map (algebraMap R Sq) p) (IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) ⋯
φ₂ : p.Fiber S →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  TensorProduct.lift φ₁ (IsScalarTower.toAlgHom R S (Sq ⧸ Ideal.map (algebraMap R Sq) p)) ⋯
φ₃ : Localization.AtPrime Q →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p := IsLocalization.liftAlgHom ⋯
⊢ Function.Surjective ⇑φ₃

Tactic:
intro x

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : p.IsPrime
inst✝² : q.LiesOver p
Q : Ideal (p.Fiber S)
inst✝¹ : Q.IsPrime
hQ : Ideal.comap TensorProduct.includeRight.toRingHom Q = q
inst✝ : QuasiFiniteAt p.ResidueField Q
Sq : Type u_2 := Localization.AtPrime q
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
φ₁ : p.ResidueField →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  Ideal.quotientMapₐ (Ideal.map (algebraMap R Sq) p) (IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) ⋯
φ₂ : p.Fiber S →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  TensorProduct.lift φ₁ (IsScalarTower.toAlgHom R S (Sq ⧸ Ideal.map (algebraMap R Sq) p)) ⋯
φ₃ : Localization.AtPrime Q →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p := IsLocalization.liftAlgHom ⋯
x : Sq ⧸ Ideal.map (algebraMap R Sq) p
⊢ ∃ a, φ₃ a = x