mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
hf₀ :
  Function.Surjective
    ⇑(Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))))
i : D.vars
⊢ ∃ p', p'.IsHomogeneous 1 ∧ (eval (Presentation.relationOfHasCoeffs ↥(subalgebra R D))) p' = p i - X i

Tactic:
have hinj : Function.Injective
        (MvPolynomial.map (σ := D.vars) (algebraMap (D.subalgebra R) A)) :=
      map_injective _ (FaithfulSMul.algebraMap_injective (D.subalgebra R) A)

Goal state after:
case refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
hf₀ :
  Function.Surjective
    ⇑(Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))))
i : D.vars
hinj : Function.Injective ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
⊢ ∃ p', p'.IsHomogeneous 1 ∧ (eval (Presentation.relationOfHasCoeffs ↥(subalgebra R D))) p' = p i - X i
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
a : ι → K
F : MvPolynomial ι k
hFa : (aeval a) F = 0
i : ι
⊢ (AlgHom.restrictScalars k (Polynomial.aeval (a i))) (F.toPolynomialAdjoinImageCompl a i) = (aeval a) F

Tactic:
toPolynomialAdjoinImageCompl,

Goal state after:
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
hFa : (aeval a) F = 0
i : ι
⊢ (AlgHom.restrictScalars k (Polynomial.aeval (a i)))
      ((Polynomial.mapAlgHom (aeval fun j ↦ ⟨a ↑j, ⋯⟩))
        ((optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F))) =
    (aeval a) 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
a : ι → K
F : MvPolynomial ι k
hF : Irreducible F
i : ι
H : AlgebraicIndependent k fun x ↦ a ↑x
⊢ Irreducible
    ((Polynomial.mapAlgHom (aeval fun j ↦ ⟨a ↑j, ⋯⟩))
      ((optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)))

Tactic:
have hc : a '' {i}ᶜ = Set.range (fun x : {j | j ≠ i} ↦ a x) := by ext; simp

Goal state after:
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 : Irreducible F
i : ι
H : AlgebraicIndependent k fun x ↦ a ↑x
hc : a '' {i}ᶜ = Set.range fun x ↦ a ↑x
⊢ Irreducible
    ((Polynomial.mapAlgHom (aeval fun j ↦ ⟨a ↑j, ⋯⟩))
      ((optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)))
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 ((F.toPolynomialAdjoinImageCompl a i).coeff (σ i)) =
    (Algebra.adjoin k (a '' {i}ᶜ)).val 0
⊢ (aeval a) ((rename Subtype.val) (F₀.coeff (σ i))) = 0

Tactic:
toPolynomialAdjoinImageCompl,

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
      (((Polynomial.mapAlgHom (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
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}
h : AlgebraicIndependent k a
⊢ False

Tactic:
refine h.transcendental_adjoin (i := n) (s := {n}ᶜ) (by simp) ?_

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}
h : AlgebraicIndependent k a
⊢ IsAlgebraic (↥(Algebra.adjoin k (a '' {n}ᶜ))) (a n)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
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.addXYZ P Q = addU P Q • ![0, 1, 0]

Tactic:
by
  erw [addXYZ, addX_of_X_eq hP hQ hPz hQz hx, addY_of_X_eq hP hQ hPz hQz hx,
    addZ_of_X_eq hP hQ hPz hQz hx, smul_fin3, mul_zero, mul_one]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Projective R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).negY (⇑f ∘ P) = f ((W'⁄A).negY P)

Tactic:
by
  rw [← RingHom.coe_coe, ← map_negY, map_baseChange]

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

Goal state before:
pp: case refine_2
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
x✝¹ : (@Surjective ⊓ @Flat) (Spec.map φ)
hfst : UniversallyClosed (pullback.fst (Spec.map φ) g)
left✝ : Surjective (Spec.map φ)
right✝ : Flat (Spec.map φ)
T : Scheme
f : T ⟶ Spec R
x✝ : HasPullback f g
s : Set ↥(pullback f g)
hs : IsClosed s
p : pullback (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) ⟶ pullback (Spec.map φ) f :=
  pullback.fst (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g)
⊢ IsClosed (⇑(pullback.fst f g) '' s)

Tactic:
let r : pullback (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) ⟶ pullback f g :=
    pullback.map _ _ _ _ (pullback.snd _ _) (pullback.snd _ _) (Spec.map φ) (pullback.condition ..)
      (pullback.condition ..)

Goal state after:
case refine_2
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
x✝¹ : (@Surjective ⊓ @Flat) (Spec.map φ)
hfst : UniversallyClosed (pullback.fst (Spec.map φ) g)
left✝ : Surjective (Spec.map φ)
right✝ : Flat (Spec.map φ)
T : Scheme
f : T ⟶ Spec R
x✝ : HasPullback f g
s : Set ↥(pullback f g)
hs : IsClosed s
p : pullback (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) ⟶ pullback (Spec.map φ) f :=
  pullback.fst (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g)
r : pullback (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) ⟶ pullback f g :=
  pullback.map (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) f g (pullback.snd (Spec.map φ) f)
    (pullback.snd (Spec.map φ) g) (Spec.map φ) ⋯ ⋯
⊢ IsClosed (⇑(pullback.fst f g) '' s)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: case refine_2
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
x✝¹ : (@Surjective ⊓ @Flat) (Spec.map φ)
hfst : UniversallyOpen (pullback.fst (Spec.map φ) g)
left✝ : Surjective (Spec.map φ)
right✝ : Flat (Spec.map φ)
T : Scheme
f : T ⟶ Spec R
x✝ : HasPullback f g
s : Set ↥(pullback f g)
hs : IsOpen s
p : pullback (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) ⟶ pullback (Spec.map φ) f :=
  pullback.fst (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g)
⊢ IsOpen (⇑(pullback.fst f g) '' s)

Tactic:
let r : pullback (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) ⟶ pullback f g :=
    pullback.map _ _ _ _ (pullback.snd _ _) (pullback.snd _ _) (Spec.map φ) (pullback.condition ..)
      (pullback.condition ..)

Goal state after:
case refine_2
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
x✝¹ : (@Surjective ⊓ @Flat) (Spec.map φ)
hfst : UniversallyOpen (pullback.fst (Spec.map φ) g)
left✝ : Surjective (Spec.map φ)
right✝ : Flat (Spec.map φ)
T : Scheme
f : T ⟶ Spec R
x✝ : HasPullback f g
s : Set ↥(pullback f g)
hs : IsOpen s
p : pullback (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) ⟶ pullback (Spec.map φ) f :=
  pullback.fst (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g)
r : pullback (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) ⟶ pullback f g :=
  pullback.map (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) f g (pullback.snd (Spec.map φ) f)
    (pullback.snd (Spec.map φ) g) (Spec.map φ) ⋯ ⋯
⊢ IsOpen (⇑(pullback.fst f g) '' s)
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal

Goal state before:
pp: case inr.refine_1
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal R
x : S
h✝ : Nontrivial R
p : (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x}))[X]
hp : p.Monic
e : eval₂ (algebraMap (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) S[X]) (C x * X) p = 0
q : R[X] := ∑ i ∈ Finset.range (p.natDegree + 1), C ((↑(p.coeff i)).coeff (p.natDegree - i)) * X ^ i
hq : q.natDegree = p.natDegree
⊢ q.Monic

pp: case inr.refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal R
x : S
h✝ : Nontrivial R
p : (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x}))[X]
hp : p.Monic
e : eval₂ (algebraMap (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) S[X]) (C x * X) p = 0
q : R[X] := ∑ i ∈ Finset.range (p.natDegree + 1), C ((↑(p.coeff i)).coeff (p.natDegree - i)) * X ^ i
hq : q.natDegree = p.natDegree
⊢ (aeval x) q = 0

pp: case inr.refine_3
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal R
x : S
h✝ : Nontrivial R
p : (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x}))[X]
hp : p.Monic
e : eval₂ (algebraMap (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) S[X]) (C x * X) p = 0
q : R[X] := ∑ i ∈ Finset.range (p.natDegree + 1), C ((↑(p.coeff i)).coeff (p.natDegree - i)) * X ^ i
hq : q.natDegree = p.natDegree
⊢ ∀ (i : ℕ), q.coeff i ∈ I ^ (q.natDegree - i)

Tactic:
· simpa [← hq] using! show q.coeff p.natDegree = 1 by simp [q, hp]

Goal state after:
case inr.refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal R
x : S
h✝ : Nontrivial R
p : (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x}))[X]
hp : p.Monic
e : eval₂ (algebraMap (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) S[X]) (C x * X) p = 0
q : R[X] := ∑ i ∈ Finset.range (p.natDegree + 1), C ((↑(p.coeff i)).coeff (p.natDegree - i)) * X ^ i
hq : q.natDegree = p.natDegree
⊢ (aeval x) q = 0

case inr.refine_3
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal R
x : S
h✝ : Nontrivial R
p : (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x}))[X]
hp : p.Monic
e : eval₂ (algebraMap (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) S[X]) (C x * X) p = 0
q : R[X] := ∑ i ∈ Finset.range (p.natDegree + 1), C ((↑(p.coeff i)).coeff (p.natDegree - i)) * X ^ i
hq : q.natDegree = p.natDegree
⊢ ∀ (i : ℕ), q.coeff i ∈ I ^ (q.natDegree - i)
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} [p.IsPrime] (Q : Ideal S) [Q.IsPrime], p < Ideal.under R Q → ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
intro p _ Q _ hpQ

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
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
H : IsIntegral R s
t : R
ht : t ∈ R⁰
ht' : t • s ∈ (algebraMap R S).range
i : ℕ
hi : i < (minpoly R s).natDegree
⊢ t ^ ((minpoly R s).natDegree - i) • (t • s) ^ i ∈ (algebraMap R S).range

Tactic:
exact (AlgHom.range (Algebra.ofId _ _)).smul_mem (Subalgebra.pow_mem _ ht' _) _

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsNoetherianRing R
inst✝¹ : IsDomain S
inst✝ : FaithfulSMul R S
s : S
H : IsAlmostIntegral R s
this : IsDomain R
⊢ IsIntegral R s

Tactic:
exact H.isIntegral_of_nonZeroDivisors_le_comap fun _ ↦ by simp

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsNoetherianRing R
inst✝¹ : IsDomain S
inst✝ : FaithfulSMul R S
s : S
H : IsAlmostIntegral R s
⊢ IsIntegral R s

Tactic:
have := IsDomain.of_faithfulSMul R S
  exact H.isIntegral_of_nonZeroDivisors_le_comap fun _ ↦ by simp

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
σ : 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 →₀ ℕ
⊢ (((↑(rename Subtype.val)).comp (map (algebraMap R S))).comp ↑(killCompl ⋯)).IsIntegralElem f

Tactic:
convert!
          H.map
            ((rename Subtype.val).comp
                (killCompl (f := ((↑) : f.vars → σ)) Subtype.val_injective)).toRingHom

Goal state after:
case e'_5
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 →₀ ℕ
⊢ ((↑(rename Subtype.val)).comp (map (algebraMap R S))).comp ↑(killCompl ⋯) =
    ((rename Subtype.val).comp (killCompl ⋯)).comp (algebraMap (MvPolynomial σ R) (MvPolynomial σ S))

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
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ C (q / (C a.leadingCoeff⁻¹ * gcd p q)).leadingCoeff⁻¹ * (p / (C a.leadingCoeff⁻¹ * gcd p q)) =
      C (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹ * (p / gcd p q) ∧
    C (q / (C a.leadingCoeff⁻¹ * gcd p q)).leadingCoeff⁻¹ * (q / (C a.leadingCoeff⁻¹ * gcd p q)) =
      C (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹ * (q / gcd p q)

Tactic:
leadingCoeff_div hdeg',

Goal state after:
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ C (q.leadingCoeff / (C a.leadingCoeff⁻¹ * gcd p q).leadingCoeff)⁻¹ * (p / (C a.leadingCoeff⁻¹ * gcd p q)) =
      C (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹ * (p / gcd p q) ∧
    C (q.leadingCoeff / (C a.leadingCoeff⁻¹ * gcd p q).leadingCoeff)⁻¹ * (q / (C a.leadingCoeff⁻¹ * gcd p q)) =
      C (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹ * (q / gcd p q)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case f.hd
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) q ≠ 0

pp: case f.hc
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) (C (q / gcd p q).leadingCoeff⁻¹) ≠ 0

Tactic:
· exact algebraMap_ne_zero hq

Goal state after:
case f.hc
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) (C (q / gcd p q).leadingCoeff⁻¹) ≠ 0
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case h
K : Type u
inst✝ : Field K
x : K⟮X⟯
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) q ≠ 0

Tactic:
· exact algebraMap_ne_zero hq

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

Goal state before:
pp: R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
T : Type u_4
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
H : Function.Bijective ⇑(toIntegralClosure R S B)
H' : Function.Bijective ⇑(toIntegralClosure S T (S ⊗[R] B))
e : T ⊗[R] ↥(integralClosure R B) ≃ₐ[T] ↥(integralClosure T (T ⊗[R] B)) :=
  (Algebra.TensorProduct.cancelBaseChange R S T T ↥(integralClosure R B)).symm.trans
    ((Algebra.TensorProduct.congr AlgEquiv.refl (AlgEquiv.ofBijective (toIntegralClosure R S B) H)).trans
      ((AlgEquiv.ofBijective (toIntegralClosure S T (S ⊗[R] B)) H').trans
        (Algebra.TensorProduct.cancelBaseChange R S T T B).mapIntegralClosure))
⊢ ⇑(toIntegralClosure R T B) = ⇑e

Tactic:
← e.coe_toAlgHom

Goal state after:
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
T : Type u_4
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
H : Function.Bijective ⇑(toIntegralClosure R S B)
H' : Function.Bijective ⇑(toIntegralClosure S T (S ⊗[R] B))
e : T ⊗[R] ↥(integralClosure R B) ≃ₐ[T] ↥(integralClosure T (T ⊗[R] B)) :=
  (Algebra.TensorProduct.cancelBaseChange R S T T ↥(integralClosure R B)).symm.trans
    ((Algebra.TensorProduct.congr AlgEquiv.refl (AlgEquiv.ofBijective (toIntegralClosure R S B) H)).trans
      ((AlgEquiv.ofBijective (toIntegralClosure S T (S ⊗[R] B)) H').trans
        (Algebra.TensorProduct.cancelBaseChange R S T T B).mapIntegralClosure))
⊢ ⇑(toIntegralClosure R T B) = ⇑↑e
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
P : Ideal R
inst✝⁵ : P.IsPrime
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Q.LiesOver P
inst✝² : IsUnramifiedAt R Q
x : S
p : R[X]
inst✝¹ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ : Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
hp₂ : R[x] = ⊤
Q' : Ideal (P.Fiber S) := ((PrimeSpectrum.primesOverOrderIsoFiber R S P) ⟨Q, ⋯⟩).asIdeal
this✝⁴ : Q'.LiesOver Q
this✝³ : Q'.LiesOver P
this✝² : Algebra (Localization.AtPrime Q) (Localization.AtPrime Q') := Localization.AtPrime.algebraOfLiesOver Q Q'
this✝¹ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q') := Localization.AtPrime.algebraOfLiesOver P Q'
this✝ : IsUnramifiedAt P.ResidueField Q'
this : Function.Surjective ⇑(aeval (1 ⊗ₜ[R] x))
⊢ ¬minpoly P.ResidueField ((algebraMap S Q.ResidueField) x) ^ 2 ∣ Polynomial.map (algebraMap R P.ResidueField) p

Tactic:
convert! IsUnramifiedAt.not_minpoly_sq_dvd (A := P.Fiber S) Q' (1 ⊗ₜ x) _ hp₁ this

Goal state after:
R : Type u_1
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
P : Ideal R
inst✝⁵ : P.IsPrime
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Q.LiesOver P
inst✝² : IsUnramifiedAt R Q
x : S
p : R[X]
inst✝¹ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ : Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
hp₂ : R[x] = ⊤
Q' : Ideal (P.Fiber S) := ((PrimeSpectrum.primesOverOrderIsoFiber R S P) ⟨Q, ⋯⟩).asIdeal
this✝⁴ : Q'.LiesOver Q
this✝³ : Q'.LiesOver P
this✝² : Algebra (Localization.AtPrime Q) (Localization.AtPrime Q') := Localization.AtPrime.algebraOfLiesOver Q Q'
this✝¹ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q') := Localization.AtPrime.algebraOfLiesOver P Q'
this✝ : IsUnramifiedAt P.ResidueField Q'
this : Function.Surjective ⇑(aeval (1 ⊗ₜ[R] x))
⊢ minpoly P.ResidueField ((algebraMap S Q.ResidueField) x) =
    minpoly P.ResidueField ((algebraMap (P.Fiber S) Q'.ResidueField) (1 ⊗ₜ[R] x))
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: case inl
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
H : ∃ x, R[x] = ⊤
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt R Q
h✝ : Subsingleton S
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
cases Ideal.IsPrime.ne_top' (Subsingleton.elim Q ⊤)

Goal state after: