mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
P : Ideal R
inst✝ : P.IsPrime
f : MonicDegreeEq P.ResidueField m
g : MonicDegreeEq P.ResidueField k
H : map (algebraMap R P.ResidueField) ↑p = ↑f * ↑g
Hpq : IsCoprime ↑f ↑g
φ : 𝓡' →ₐ[R] P.ResidueField := (homEquiv P.ResidueField m k hn p).symm ⟨(f, g), ⋯⟩
Q : Ideal 𝓡' := RingHom.ker φ.toRingHom
this✝ : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := Ideal.ResidueField.liftₐ Q φ ⋯ ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField := Ideal.ResidueField.mapₐ P Q (Algebra.ofId R 𝓡') ⋯
⊢ φ'.comp φi = AlgHom.id R P.ResidueField

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
p : R[X]
hp : p ∈ R[X]_m
q : R[X]
hq : q ∈ R[X]_n
hf' : ¬f = 0
⊢ f.degree ≠ ⊥

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
P : Ideal R
inst✝ : P.IsPrime
f : MonicDegreeEq P.ResidueField m
g : MonicDegreeEq P.ResidueField k
H : map (algebraMap R P.ResidueField) ↑p = ↑f * ↑g
Hpq : IsCoprime ↑f ↑g
φ : 𝓡' →ₐ[R] P.ResidueField := (homEquiv P.ResidueField m k hn p).symm ⟨(f, g), ⋯⟩
Q : Ideal 𝓡' := RingHom.ker φ.toRingHom
this✝ : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := Ideal.ResidueField.liftₐ Q φ ⋯ ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField := Ideal.ResidueField.mapₐ P Q (Algebra.ofId R 𝓡') ⋯
e : P.ResidueField ≃ₐ[R] Q.ResidueField := AlgEquiv.ofAlgHom φi φ' ⋯ ⋯
x : 𝓡'
⊢ ↑φ x = e.symm ((IsScalarTower.toAlgHom R 𝓡' Q.ResidueField) x)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
p : R[X]
hp : p ∈ R[X]_m
q : R[X]
hq : q ∈ R[X]_n
hf' : ¬f = 0
⊢ ?m.137 < ?m.139

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
p : R[X]
hp : p ∈ R[X]_m
q : R[X]
hq : q ∈ R[X]_n
hg' : ¬g = 0
⊢ g.degree ≠ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
p : R[X]
hp : p ∈ R[X]_m
q : R[X]
hq : q ∈ R[X]_n
hg' : ¬g = 0
⊢ (↑(⟨p, hp⟩, ⟨q, hq⟩).1).degree < ?m.186

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
pq : ↥R[X]_m × ↥R[X]_n
⊢ f * ↑pq.2 + g * ↑pq.1 ∈ R[X]_(m + n)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
x✝¹ x✝ : ↥R[X]_m × ↥R[X]_n
⊢ ⟨f * ↑(x✝¹ + x✝).2 + g * ↑(x✝¹ + x✝).1, ⋯⟩ = ⟨f * ↑x✝¹.2 + g * ↑x✝¹.1, ⋯⟩ + ⟨f * ↑x✝.2 + g * ↑x✝.1, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
x✝¹ : R
x✝ : ↥R[X]_m × ↥R[X]_n
⊢ ⟨f * ↑(x✝¹ • x✝).2 + g * ↑(x✝¹ • x✝).1, ⋯⟩ = (RingHom.id R) x✝¹ • ⟨f * ↑x✝.2 + g * ↑x✝.1, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
this : (if ↑j ≤ ↑i then g.coeff (↑i - ↑j) else 0) = if ↑j ≤ ↑i ∧ ↑i ≤ ↑j + n then g.coeff (↑i - ↑j) else 0
⊢ (LinearMap.toMatrix ((degreeLT.basis R m).prod (degreeLT.basis R n)) (degreeLT.basis R (m + n)))
      (f.sylvesterMap g hf hg) i (Sum.inl j) =
    (Matrix.reindex (Equiv.refl (Fin (m + n))) finSumFinEquiv.symm) (f.sylvester g m n) i (Sum.inl j)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
h₁ : ↑j ≤ ↑i
h₂ : ¬↑i ≤ ↑j + n
⊢ g.natDegree < ↑i - ↑j

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
this : (if ↑j ≤ ↑i then f.coeff (↑i - ↑j) else 0) = if ↑j ≤ ↑i ∧ ↑i ≤ ↑j + m then f.coeff (↑i - ↑j) else 0
⊢ (LinearMap.toMatrix ((degreeLT.basis R m).prod (degreeLT.basis R n)) (degreeLT.basis R (m + n)))
      (f.sylvesterMap g hf hg) i (Sum.inr j) =
    (Matrix.reindex (Equiv.refl (Fin (m + n))) finSumFinEquiv.symm) (f.sylvester g m n) i (Sum.inr j)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing R'
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R R'
inst✝³ : Algebra R S
p : Ideal R
q : Ideal R'
inst✝² : p.IsPrime
inst✝¹ : q.IsPrime
inst✝ : q.LiesOver p
H : Function.Bijective ⇑(ResidueField.mapₐ p q (Algebra.ofId R R') ⋯)
Q : ↑(p.primesOver S)
⊢ comap ↑Algebra.TensorProduct.includeRight ↑((fiberIsoOfBijectiveResidueField H).symm Q) = ↑Q

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
h₁ : ↑j ≤ ↑i
h₂ : ¬↑i ≤ ↑j + m
⊢ f.natDegree < ↑i - ↑j

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing R'
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R R'
inst✝³ : Algebra R S
p : Ideal R
q : Ideal R'
inst✝² : p.IsPrime
inst✝¹ : q.IsPrime
inst✝ : q.LiesOver p
H : Function.Bijective ⇑(ResidueField.mapₐ p q (Algebra.ofId R R') ⋯)
Q : ↑(q.primesOver (R' ⊗[R] S))
⊢ ↑((fiberIsoOfBijectiveResidueField H) Q) = comap Algebra.TensorProduct.includeRight ↑Q

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
⊢ (LinearMap.toMatrix ((degreeLT.basis R m).prod (degreeLT.basis R n)) (degreeLT.basis R (m + n)))
      (f.sylvesterMap g hf hg) =
    (Matrix.reindex (Equiv.refl (Fin (m + n))) finSumFinEquiv.symm) (f.sylvester g m n)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing R'
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R R'
inst✝⁷ : Algebra R S
p : Ideal R
q : Ideal R'
inst✝⁶ : p.IsPrime
inst✝⁵ : q.IsPrime
inst✝⁴ : q.LiesOver p
H : Function.Bijective ⇑(ResidueField.mapₐ p q (Algebra.ofId R R') ⋯)
P₁ P₂ : Ideal (R' ⊗[R] S)
inst✝³ : P₁.IsPrime
inst✝² : P₂.IsPrime
inst✝¹ : P₁.LiesOver q
inst✝ : P₂.LiesOver q
H₂ : comap Algebra.TensorProduct.includeRight.toRingHom P₁ = comap Algebra.TensorProduct.includeRight.toRingHom P₂
⊢ (fiberIsoOfBijectiveResidueField H) ⟨P₁, ⋯⟩ = (fiberIsoOfBijectiveResidueField H) ⟨P₂, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing R'
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R R'
inst✝⁷ : Algebra R S
p : Ideal R
q : Ideal R'
inst✝⁶ : p.IsPrime
inst✝⁵ : q.IsPrime
inst✝⁴ : q.LiesOver p
H : Function.Bijective ⇑(ResidueField.mapₐ p q (Algebra.ofId R R') ⋯)
P₁ P₂ : Ideal (R' ⊗[R] S)
inst✝³ : P₁.IsPrime
inst✝² : P₂.IsPrime
inst✝¹ : P₁.LiesOver q
inst✝ : P₂.LiesOver q
H₂ : comap Algebra.TensorProduct.includeRight.toRingHom P₁ = comap Algebra.TensorProduct.includeRight.toRingHom P₂
⊢ P₁ = P₂

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
⊢ (LinearMap.toMatrix (((degreeLT.basis R m).prod (degreeLT.basis R n)).reindex finSumFinEquiv)
        (degreeLT.basis R (m + n)))
      (f.sylvesterMap g hf hg) =
    f.sylvester g m n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u
S : Type v
T : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra.FiniteType R T
inst✝¹ : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg : Function.Surjective ⇑(awayMapₐ f g)
p : Ideal R
inst✝ : p.IsPrime
hgp : IsUnit (1 ⊗ₜ[R] g)
this : IsClosed (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})
⊢ { asIdeal := p, isPrime := inst✝ } ∈ (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u
S : Type v
T : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra.FiniteType R T
inst✝¹ : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg : Function.Surjective ⇑(awayMapₐ f g)
p : Ideal R
inst✝ : p.IsPrime
hgp : IsUnit (1 ⊗ₜ[R] g)
this : IsClosed (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})
r : R
hpr : { asIdeal := p, isPrime := inst✝ } ∈ ↑(PrimeSpectrum.basicOpen r)
hrg : ↑(PrimeSpectrum.basicOpen r) ⊆ (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})ᶜ
⊢ IsLocalization.Away (f.toRingHom ((algebraMap R S) r)) (Away ((algebraMap R T) r))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
⊢ f.sylvesterMap g hf hg ∘ₗ f.adjSylvester g = f.resultant g m n • LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u
S : Type v
T : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra.FiniteType R T
inst✝¹ : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg : Function.Surjective ⇑(awayMapₐ f g)
p : Ideal R
inst✝ : p.IsPrime
hgp : IsUnit (1 ⊗ₜ[R] g)
this✝¹ : IsClosed (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})
r : R
hpr : { asIdeal := p, isPrime := inst✝ } ∈ ↑(PrimeSpectrum.basicOpen r)
hrg : ↑(PrimeSpectrum.basicOpen r) ⊆ (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})ᶜ
this✝ : IsLocalization.Away (f.toRingHom ((algebraMap R S) r)) (Away ((algebraMap R T) r))
h₁ : (awayMap (algebraMap R S) r).IsIntegral
x : T
n : ℕ
this : ∃ a k l, (algebraMap R T) r ^ (l + n) * f a = (algebraMap R T) r ^ (l + k) * x
⊢ ∃ a,
    (IsLocalization.Away.map (Away ((algebraMap R S) r)) (Away ((algebraMap R T) r)) f.toRingHom ((algebraMap R S) r))
        a =
      IsLocalization.mk' (Away ((algebraMap R T) r)) x ⟨(fun x ↦ (algebraMap R T) r ^ x) n, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
⊢ f.adjSylvester g ∘ₗ f.sylvesterMap g hf hg = f.resultant g m n • LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u
S : Type v
T : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra.FiniteType R T
inst✝¹ : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg : Function.Surjective ⇑(awayMapₐ f g)
p : Ideal R
inst✝ : p.IsPrime
hgp : IsUnit (1 ⊗ₜ[R] g)
this✝ : IsClosed (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})
r : R
hpr : { asIdeal := p, isPrime := inst✝ } ∈ ↑(PrimeSpectrum.basicOpen r)
hrg : ↑(PrimeSpectrum.basicOpen r) ⊆ (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})ᶜ
this : IsLocalization.Away (f.toRingHom ((algebraMap R S) r)) (Away ((algebraMap R T) r))
h₁ : (awayMap (algebraMap R S) r).IsIntegral
x : T
n : ℕ
⊢ PrimeSpectrum.basicOpen ((algebraMap R S) r) ≤ PrimeSpectrum.basicOpen g

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
H : m ≠ 0 ∨ n ≠ 0
a✝ : Nontrivial R
⊢ 1 ∈ R[X]_(?m.85 + ?m.86)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
H : m ≠ 0 ∨ n ≠ 0
a✝ : Nontrivial R
X : ↥R[X]_m × ↥R[X]_n := (f.adjSylvester g) ⟨1, ⋯⟩
this : ↑((f.sylvesterMap g hf hg) X) = ↑((f.resultant g m n • LinearMap.id) ⟨1, ⋯⟩)
⊢ (↑X.2).degree < ↑n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u
S : Type v
T : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra.FiniteType R T
inst✝¹ : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg : Function.Surjective ⇑(awayMapₐ f g)
p : Ideal R
inst✝ : p.IsPrime
hgp : IsUnit (1 ⊗ₜ[R] g)
this✝ : IsClosed (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})
r : R
hpr : { asIdeal := p, isPrime := inst✝ } ∈ ↑(PrimeSpectrum.basicOpen r)
hrg : ↑(PrimeSpectrum.basicOpen r) ⊆ (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})ᶜ
this : IsLocalization.Away (f.toRingHom ((algebraMap R S) r)) (Away ((algebraMap R T) r))
h₁ : (awayMap (algebraMap R S) r).IsIntegral
x : T
n m' : ℕ
s : S
hs : (algebraMap R S) r ^ m' = g * s
b : S
m : ℕ
e : f b = f g ^ m * x
⊢ f (s ^ m * b) = f (g * s) ^ m * x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
H : m ≠ 0 ∨ n ≠ 0
a✝ : Nontrivial R
X : ↥R[X]_m × ↥R[X]_n := (f.adjSylvester g) ⟨1, ⋯⟩
this : ↑((f.sylvesterMap g hf hg) X) = ↑((f.resultant g m n • LinearMap.id) ⟨1, ⋯⟩)
⊢ (↑X.1).degree < ↑m

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
H : m ≠ 0 ∨ n ≠ 0
a✝ : Nontrivial R
X : ↥R[X]_m × ↥R[X]_n := (f.adjSylvester g) ⟨1, ⋯⟩
this : ↑((f.sylvesterMap g hf hg) X) = ↑((f.resultant g m n • LinearMap.id) ⟨1, ⋯⟩)
⊢ f * ↑X.2 + g * ↑X.1 = C (f.resultant g m n)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
P : Ideal R
inst✝ : P.IsPrime
f : MonicDegreeEq P.ResidueField m
g : MonicDegreeEq P.ResidueField k
H : map (algebraMap R P.ResidueField) ↑p = ↑f * ↑g
Hpq : IsCoprime ↑f ↑g
⊢ ∃ Q,
    ∃ (x : Q.IsPrime) (x_1 : Q.LiesOver P),
      Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Q (Algebra.ofId R 𝓡') ⋯) ∧
        f.map (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R 𝓡') ⋯).toRingHom =
            (factor₁ m k hn p).map (algebraMap 𝓡' Q.ResidueField) ∧
          g.map (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R 𝓡') ⋯).toRingHom =
            (factor₂ m k hn p).map (algebraMap 𝓡' Q.ResidueField)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
H : m ≠ 0 ∨ n ≠ 0
⊢ ∃ p q, p.degree < ↑n ∧ q.degree < ↑m ∧ f * p + g * q = C (f.resultant g m n)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
P : Ideal R
inst✝ : P.IsPrime
p : R[X]
f g : P.ResidueField[X]
hp : p.Monic
hf : f.Monic
hg : g.Monic
H : map (algebraMap R P.ResidueField) p = f * g
Hpq : IsCoprime f g
⊢ p.natDegree = f.natDegree + g.natDegree

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
H : IsUnit (f.resultant g)
⊢ f.natDegree ≠ 0 ∨ g.natDegree ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
H : IsUnit (f.resultant g)
p q : R[X]
hp : p.degree < ↑g.natDegree
hq : q.degree < ↑f.natDegree
e : f * p + g * q = C (f.resultant g)
⊢ C ↑H.unit⁻¹ * p * f + C ↑H.unit⁻¹ * q * g = 1

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
P : Ideal R
inst✝ : P.IsPrime
p : R[X]
f g : P.ResidueField[X]
hp : p.Monic
hf : f.Monic
hg : g.Monic
H : map (algebraMap R P.ResidueField) p = f * g
Hpq : IsCoprime f g
⊢ ∃ R' x x_1,
    ∃ (_ : Algebra.Etale R R'),
      ∃ Q,
        ∃ (x_3 : Q.IsPrime) (x_4 : Q.LiesOver P),
          ∃ f' g',
            Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') ⋯) ∧
              f'.Monic ∧
                g'.Monic ∧
                  map (algebraMap R R') p = f' * g' ∧
                    IsCoprime f' g' ∧
                      map (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') ⋯).toRingHom f =
                          map (algebraMap R' Q.ResidueField) f' ∧
                        map (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') ⋯).toRingHom g =
                          map (algebraMap R' Q.ResidueField) g'

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u
S : Type v
T : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra.FiniteType R T
inst✝¹ : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg : Function.Surjective ⇑(awayMapₐ f g)
p : Ideal R
inst✝ : p.IsPrime
hgp : IsUnit (1 ⊗ₜ[R] g)
this✝ : IsClosed (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})
r : R
hpr : { asIdeal := p, isPrime := inst✝ } ∈ ↑(PrimeSpectrum.basicOpen r)
hrg : ↑(PrimeSpectrum.basicOpen r) ⊆ (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})ᶜ
this : IsLocalization.Away (f.toRingHom ((algebraMap R S) r)) (Away ((algebraMap R T) r))
h₁ : (awayMap (algebraMap R S) r).IsIntegral
⊢ Function.Surjective
    ⇑(IsLocalization.Away.map (Away ((algebraMap R S) r)) (Away ((algebraMap R T) r)) f.toRingHom ((algebraMap R S) r))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsSeparated f
x : ↥X
s : ↥S
h : f x = s
hx : Scheme.Hom.QuasiFiniteAt f x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hUV : V ≤ f ⁻¹ᵁ U
this : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).FiniteType
algInst✝ : Algebra ↑Γ(S, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).toAlgebra
algebraizeInst✝ : Algebra.FiniteType ↑Γ(S, U) ↑Γ(X, V)
⊢ (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal.LiesOver (IsAffineOpen.primeIdealOf hU ⟨f x, hxU⟩).asIdeal

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: case e'_5
R : Type u
S : Type v
T : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra.FiniteType R T
inst✝¹ : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg : Function.Surjective ⇑(awayMapₐ f g)
p : Ideal R
inst✝ : p.IsPrime
hgp : IsUnit (1 ⊗ₜ[R] g)
this✝ : IsClosed (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})
r : R
hpr : { asIdeal := p, isPrime := inst✝ } ∈ ↑(PrimeSpectrum.basicOpen r)
hrg : ↑(PrimeSpectrum.basicOpen r) ⊆ (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})ᶜ
this : IsLocalization.Away (f.toRingHom ((algebraMap R S) r)) (Away ((algebraMap R T) r))
h₁ : (awayMap (algebraMap R S) r).IsIntegral
h₂ :
  Function.Surjective
    ⇑(IsLocalization.Away.map (Away ((algebraMap R S) r)) (Away ((algebraMap R T) r)) f.toRingHom ((algebraMap R S) r))
e_2✝ : Away ((Algebra.ofId R T) r) = Away ((algebraMap R T) r)
e_4✝ : OreLocalization.instCommRing.toRing ≍ OreLocalization.instCommRing.toRing
x : R
⊢ ((awayMapₐ (Algebra.ofId R T) r).comp (algebraMap R (Away r))) x =
    (((IsLocalization.Away.map (Away ((algebraMap R S) r)) (Away ((algebraMap R T) r)) f.toRingHom
                ((algebraMap R S) r)).comp
            (awayMap (algebraMap R S) r)).comp
        (algebraMap R (Away r)))
      x

Tactic:
simp [Localization.awayMap, IsLocalization.Away.map, ← IsScalarTower.algebraMap_apply R T]

Goal state after:
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u
S : Type v
T : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra.FiniteType R T
inst✝¹ : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg : Function.Surjective ⇑(awayMapₐ f g)
p : Ideal R
inst✝ : p.IsPrime
hgp : IsUnit (1 ⊗ₜ[R] g)
⊢ ∃ r ∉ p, (awayMapₐ (Algebra.ofId R T) r).Finite

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
⊢ IsUnit (f.resultant g) ↔ IsCoprime f g

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: K : Type u_2
inst✝ : Field K
f g : K[X]
hf : f ≠ 0
⊢ f.leadingCoeff⁻¹ ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: K : Type u_2
inst✝ : Field K
f g : K[X]
hf : f ≠ 0
⊢ (C f.leadingCoeff⁻¹ * f).Monic

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: K : Type u_2
inst✝ : Field K
f g : K[X]
hf : f ≠ 0
H : (C f.leadingCoeff⁻¹ * f).Monic
this :
  IsUnit (f.leadingCoeff⁻¹ ^ g.natDegree) ∧ IsUnit (f.resultant g (C f.leadingCoeff⁻¹ * f).natDegree) ↔
    IsCoprime (C f.leadingCoeff⁻¹ * f) g
⊢ f.leadingCoeff⁻¹ ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: K : Type u_2
inst✝ : Field K
f g : K[X]
hf : f ≠ 0
H : (C f.leadingCoeff⁻¹ * f).Monic
this : IsUnit (f.leadingCoeff⁻¹ ^ g.natDegree) ∧ IsUnit (f.resultant g) ↔ IsCoprime (C f.leadingCoeff⁻¹ * f) g
⊢ IsUnit f.leadingCoeff⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: K : Type u_2
inst✝ : Field K
f g : K[X]
⊢ f.resultant g = 0 ↔ (f ≠ 0 ∨ g ≠ 0) ∧ ¬IsCoprime f g

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
⊢ (C r).natDegree - 1 + (C r).natDegree = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
⊢ (C r).discr = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 1
⊢ f.natDegree - 1 + f.natDegree = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 1
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 1 := finCongr ⋯
⊢ f.natDegree - 1 + f.natDegree ≠ 0

Tactic:
by

Goal state after: