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

Goal state before:
pp: case inl
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
⊢ (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)

pp: case inr
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
⊢ (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:
·

Goal state after:
case inl
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
⊢ (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)
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 := ⋯
Q : Ideal 𝓡' := ⋯
this✝ : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField := ⋯
e : P.ResidueField ≃ₐ[R] Q.ResidueField := ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
⊢ (↑((homEquiv Q.ResidueField m k hn p) (φi.comp φ))).1 = (factor₁ m k hn p).map (algebraMap 𝓡' Q.ResidueField)

Tactic:
·

Goal state after:
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 := ⋯
Q : Ideal 𝓡' := ⋯
this✝ : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField := ⋯
e : P.ResidueField ≃ₐ[R] Q.ResidueField := ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
⊢ (↑((homEquiv Q.ResidueField m k hn p) (φi.comp φ))).1 = (factor₁ m k hn p).map (algebraMap 𝓡' Q.ResidueField)
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 lia

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

Goal state before:
pp: case inr
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
⊢ (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:
·

Goal state after:
case inr
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
⊢ (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)
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 lia

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

Goal state before:
pp: case refine_2
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 φ' ⋯ ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
⊢ g.map (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R 𝓡') ⋯).toRingHom =
    (factor₂ m k hn p).map (algebraMap 𝓡' Q.ResidueField)

Tactic:
·

Goal state after:
case refine_2
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 φ' ⋯ ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
⊢ g.map (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R 𝓡') ⋯).toRingHom =
    (factor₂ m k hn p).map (algebraMap 𝓡' Q.ResidueField)
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 := ⋯
Q : Ideal 𝓡' := ⋯
this✝ : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField := ⋯
e : P.ResidueField ≃ₐ[R] Q.ResidueField := ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
⊢ g.map (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R 𝓡') ⋯).toRingHom =
    (↑((homEquiv Q.ResidueField m k hn p) (φi.comp φ))).2

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 := ⋯
Q : Ideal 𝓡' := ⋯
this✝ : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField := ⋯
e : P.ResidueField ≃ₐ[R] Q.ResidueField := ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
⊢ (↑((homEquiv Q.ResidueField m k hn p) (φi.comp φ))).2 = (factor₂ m k hn p).map (algebraMap 𝓡' Q.ResidueField)

Tactic:
·

Goal state after:
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 := ⋯
Q : Ideal 𝓡' := ⋯
this✝ : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField := ⋯
e : P.ResidueField ≃ₐ[R] Q.ResidueField := ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
⊢ g.map (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R 𝓡') ⋯).toRingHom =
    (↑((homEquiv Q.ResidueField m k hn p) (φi.comp φ))).2
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: case refine_1
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})ᶜ
⊢ (awayMapₐ (Algebra.ofId R T) r).IsIntegral

pp: case refine_2
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})ᶜ
⊢ (awayMapₐ (Algebra.ofId R T) r).FiniteType

Tactic:
·

Goal state after:
case refine_1
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})ᶜ
⊢ (awayMapₐ (Algebra.ofId R T) r).IsIntegral
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 := ⋯
Q : Ideal 𝓡' := ⋯
this✝ : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField := ⋯
e : P.ResidueField ≃ₐ[R] Q.ResidueField := ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
⊢ (↑((homEquiv Q.ResidueField m k hn p) (φi.comp φ))).2 = (factor₂ m k hn p).map (algebraMap 𝓡' Q.ResidueField)

Tactic:
·

Goal state after:
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 := ⋯
Q : Ideal 𝓡' := ⋯
this✝ : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField := ⋯
e : P.ResidueField ≃ₐ[R] Q.ResidueField := ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
⊢ (↑((homEquiv Q.ResidueField m k hn p) (φi.comp φ))).2 = (factor₂ m k hn p).map (algebraMap 𝓡' Q.ResidueField)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

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

pp: case neg
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
⊢ IsUnit (f.resultant g) ↔ IsCoprime f g

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : f.natDegree = 0
⊢ IsUnit (f.resultant g) ↔ IsCoprime f g
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

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

pp: case neg.refine_2
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
⊢ IsCoprime f g → IsUnit (f.resultant g)

Tactic:
·

Goal state after:
case neg.refine_1
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
H : IsUnit (f.resultant g)
⊢ IsCoprime f g
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg.refine_2
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
⊢ IsCoprime f g → IsUnit (f.resultant g)

Tactic:
·

Goal state after:
case neg.refine_2
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
⊢ IsCoprime f g → IsUnit (f.resultant g)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg.refine_2.inl
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
b : R[X]
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
e : 0 * f + b * g = 1
⊢ 1 = f.resultant b * f.resultant g

pp: case neg.refine_2.inr
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
⊢ 1 = f.resultant b * f.resultant g

Tactic:
·

Goal state after:
case neg.refine_2.inl
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
b : R[X]
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
e : 0 * f + b * g = 1
⊢ 1 = f.resultant b * f.resultant g
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg.refine_2.inr
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
⊢ 1 = f.resultant b * f.resultant g

Tactic:
·

Goal state after:
case neg.refine_2.inr
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
⊢ 1 = f.resultant b * f.resultant g
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg.refine_2.inr
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (C 1) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
⊢ 1 = f.resultant b * f.resultant g

pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
⊢ a.natDegree + f.natDegree ≤ b.natDegree + g.natDegree

Tactic:
·

Goal state after:
case neg.refine_2.inr
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (C 1) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
⊢ 1 = f.resultant b * f.resultant g
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: case refine_2
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})ᶜ
⊢ (awayMapₐ (Algebra.ofId R T) r).FiniteType

Tactic:
·

Goal state after:
case refine_2
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})ᶜ
⊢ (awayMapₐ (Algebra.ofId R T) r).FiniteType
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
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
⊢ a.natDegree + f.natDegree ≤ b.natDegree + g.natDegree

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
⊢ a.natDegree + f.natDegree ≤ b.natDegree + g.natDegree
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

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

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

Tactic:
·

Goal state after:
case inl
K : Type u_2
inst✝ : Field K
g : K[X]
⊢ resultant 0 g = 0 ↔ (0 ≠ 0 ∨ g ≠ 0) ∧ ¬IsCoprime 0 g
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inl.inl
K : Type u_2
inst✝ : Field K
⊢ resultant 0 0 = 0 ↔ (0 ≠ 0 ∨ 0 ≠ 0) ∧ ¬IsCoprime 0 0

pp: case inl.inr
K : Type u_2
inst✝ : Field K
g : K[X]
hg : g ≠ 0
⊢ resultant 0 g = 0 ↔ (0 ≠ 0 ∨ g ≠ 0) ∧ ¬IsCoprime 0 g

Tactic:
·

Goal state after:
case inl.inl
K : Type u_2
inst✝ : Field K
⊢ resultant 0 0 = 0 ↔ (0 ≠ 0 ∨ 0 ≠ 0) ∧ ¬IsCoprime 0 0
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 lia

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 lia

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 ⋯
this : NeZero (f.natDegree - 1 + f.natDegree)
i : ℕ
hi : i < 1
j : ℕ
hj : j < 1
⊢ i = 0

Tactic:
by lia

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 ⋯
this : NeZero (f.natDegree - 1 + f.natDegree)
j : ℕ
hj : j < 1
hi : 0 < 1
⊢ j = 0

Tactic:
by lia

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 = 2
⊢ f.natDegree - 1 + f.natDegree = 3

Tactic:
by lia

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

Goal state before:
pp: R : Type u_2
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✝¹ : FiniteType R S
inst✝ : QuasiFiniteAt R q
s₁ : S
hs₁q : s₁ ∉ q
hs₁ : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s₁ ∈ q'
s₂ : ↥(integralClosure R S)
hs₂q : ↑s₂ ∉ q
hs₂ : Function.Bijective ⇑(Localization.awayMap (integralClosure R S).val.toRingHom s₂)
s₃ : ↥(integralClosure R S)
n : ℕ
hs₃ :
  (Localization.awayMap (integralClosure R S).val.toRingHom s₂)
      (IsLocalization.mk' (Localization.Away s₂) s₃ ⟨(fun x ↦ s₂ ^ x) n, ⋯⟩) =
    (algebraMap S (Localization.Away ((integralClosure R S).val.toRingHom s₂))) s₁
m : ℕ
hm : ↑s₂ ^ m * ↑s₃ = ↑s₂ ^ m * (s₁ * ↑s₂ ^ n)
hm0 : 0 < m
hs₃q : ↑s₃ ∉ q
q' : Ideal ↥(integralClosure R S)
x✝¹ : q'.IsPrime
hq'q : q' ≠ Ideal.under (↥(integralClosure R S)) q
x✝ : q'.LiesOver p
this✝¹ : Algebra (↥(integralClosure R S)) (Localization.Away ↑s₂) := OreLocalization.instAlgebra
e : Localization.Away s₂ ≃ₐ[↥(integralClosure R S)] Localization.Away ↑s₂ :=
  AlgEquiv.ofBijective (Localization.awayMapₐ (ofId (↥(integralClosure R S)) S) s₂) hs₂
q's : Ideal (Localization.Away s₂) := Ideal.map (algebraMap (↥(integralClosure R S)) (Localization.Away s₂)) q'
H : ¬⟨↑s₂ ^ m * ↑s₃, ⋯⟩ ∈ q'
hq's : Disjoint ↑(Submonoid.powers s₂) ↑q'
this✝ : q's.IsPrime
this : q's.LiesOver q'
⊢ False

Tactic:
have : q's.LiesOver p := .trans _ q' _

Goal state after:
R : Type u_2
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✝¹ : FiniteType R S
inst✝ : QuasiFiniteAt R q
s₁ : S
hs₁q : s₁ ∉ q
hs₁ : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s₁ ∈ q'
s₂ : ↥(integralClosure R S)
hs₂q : ↑s₂ ∉ q
hs₂ : Function.Bijective ⇑(Localization.awayMap (integralClosure R S).val.toRingHom s₂)
s₃ : ↥(integralClosure R S)
n : ℕ
hs₃ :
  (Localization.awayMap (integralClosure R S).val.toRingHom s₂)
      (IsLocalization.mk' (Localization.Away s₂) s₃ ⟨(fun x ↦ s₂ ^ x) n, ⋯⟩) =
    (algebraMap S (Localization.Away ((integralClosure R S).val.toRingHom s₂))) s₁
m : ℕ
hm : ↑s₂ ^ m * ↑s₃ = ↑s₂ ^ m * (s₁ * ↑s₂ ^ n)
hm0 : 0 < m
hs₃q : ↑s₃ ∉ q
q' : Ideal ↥(integralClosure R S)
x✝¹ : q'.IsPrime
hq'q : q' ≠ Ideal.under (↥(integralClosure R S)) q
x✝ : q'.LiesOver p
this✝² : Algebra (↥(integralClosure R S)) (Localization.Away ↑s₂) := OreLocalization.instAlgebra
e : Localization.Away s₂ ≃ₐ[↥(integralClosure R S)] Localization.Away ↑s₂ :=
  AlgEquiv.ofBijective (Localization.awayMapₐ (ofId (↥(integralClosure R S)) S) s₂) hs₂
q's : Ideal (Localization.Away s₂) := Ideal.map (algebraMap (↥(integralClosure R S)) (Localization.Away s₂)) q'
H : ¬⟨↑s₂ ^ m * ↑s₃, ⋯⟩ ∈ q'
hq's : Disjoint ↑(Submonoid.powers s₂) ↑q'
this✝¹ : q's.IsPrime
this✝ : q's.LiesOver q'
this : q's.LiesOver p
⊢ False