internlm/Lean-Github huggingface dataset:
Theorem: IsIntegral_of_isLocalization
Proof state before:
case isIntegral
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Algebra.IsIntegral R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : Sₚ
⊢ IsIntegral Rₚ x
Tactic:
obtain ⟨x, ⟨_, t, ht, rfl⟩, rfl⟩ := IsLocalization.mk'_surjective
  (Algebra.algebraMapSubmonoid S M) x
Proof state after:
case isIntegral.intro.intro.mk.intro.intro
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Algebra.IsIntegral R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
t : R
ht : t ∈ ↑M
⊢ IsIntegral Rₚ (IsLocalization.mk' Sₚ x ⟨(algebraMap R S) t, ⋯⟩)
Theorem: IsIntegral_of_isLocalization
Proof state before:
case isIntegral.intro.intro.mk.intro.intro
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Algebra.IsIntegral R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
t : R
ht : t ∈ ↑M
⊢ IsIntegral Rₚ (IsLocalization.mk' Sₚ x ⟨(algebraMap R S) t, ⋯⟩)
Tactic:
rw [IsLocalization.mk'_eq_mul_mk'_one]
Proof state after:
case isIntegral.intro.intro.mk.intro.intro
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Algebra.IsIntegral R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
t : R
ht : t ∈ ↑M
⊢ IsIntegral Rₚ ((algebraMap S Sₚ) x * IsLocalization.mk' Sₚ 1 ⟨(algebraMap R S) t, ⋯⟩)
Theorem: IsIntegral_of_isLocalization
Proof state before:
case isIntegral.intro.intro.mk.intro.intro
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Algebra.IsIntegral R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
t : R
ht : t ∈ ↑M
⊢ IsIntegral Rₚ ((algebraMap S Sₚ) x * IsLocalization.mk' Sₚ 1 ⟨(algebraMap R S) t, ⋯⟩)
Tactic:
apply RingHom.IsIntegralElem.mul
Proof state after:
case isIntegral.intro.intro.mk.intro.intro.hx
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Algebra.IsIntegral R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
t : R
ht : t ∈ ↑M
⊢ (algebraMap Rₚ Sₚ).IsIntegralElem ((algebraMap S Sₚ) x)

case isIntegral.intro.intro.mk.intro.intro.hy
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Algebra.IsIntegral R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
t : R
ht : t ∈ ↑M
⊢ (algebraMap Rₚ Sₚ).IsIntegralElem (IsLocalization.mk' Sₚ 1 ⟨(algebraMap R S) t, ⋯⟩)
Theorem: IsIntegral_of_isLocalization
Proof state before:
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Algebra.IsIntegral R S
⊢ algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
Tactic:
apply IsLocalization.ringHom_ext M
Proof state after:
case h
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Algebra.IsIntegral R S
⊢ (algebraMap Rₚ Sₚ).comp (algebraMap R Rₚ) = (IsLocalization.map Sₚ (algebraMap R S) ⋯).comp (algebraMap R Rₚ)
Theorem: IsIntegral_of_isLocalization
Proof state before:
case h
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Algebra.IsIntegral R S
⊢ (algebraMap Rₚ Sₚ).comp (algebraMap R Rₚ) = (IsLocalization.map Sₚ (algebraMap R S) ⋯).comp (algebraMap R Rₚ)
Tactic:
simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
Proof state after:
no goals
Theorem: IsIntegral_of_isLocalization
Proof state before:
case isIntegral.intro.intro.mk.intro.intro.hx
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Algebra.IsIntegral R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
t : R
ht : t ∈ ↑M
⊢ (algebraMap Rₚ Sₚ).IsIntegralElem ((algebraMap S Sₚ) x)
Tactic:
exact IsIntegral.tower_top (IsIntegral.map (IsScalarTower.toAlgHom R S Sₚ) (hRS.1 x))
Proof state after:
no goals
Theorem: IsIntegral_of_isLocalization
Proof state before:
case isIntegral.intro.intro.mk.intro.intro.hy
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Algebra.IsIntegral R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
t : R
ht : t ∈ ↑M
⊢ (algebraMap Rₚ Sₚ).IsIntegralElem (IsLocalization.mk' Sₚ 1 ⟨(algebraMap R S) t, ⋯⟩)
Tactic:
show IsIntegral _ _
Proof state after:
case isIntegral.intro.intro.mk.intro.intro.hy
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Algebra.IsIntegral R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
t : R
ht : t ∈ ↑M
⊢ IsIntegral Rₚ (IsLocalization.mk' Sₚ 1 ⟨(algebraMap R S) t, ⋯⟩)
Theorem: IsIntegral_of_isLocalization
Proof state before:
case isIntegral.intro.intro.mk.intro.intro.hy
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Algebra.IsIntegral R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
t : R
ht : t ∈ ↑M
⊢ IsIntegral Rₚ (IsLocalization.mk' Sₚ 1 ⟨(algebraMap R S) t, ⋯⟩)
Tactic:
convert isIntegral_algebraMap (x := IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
Proof state after:
case h.e'_6
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Algebra.IsIntegral R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
t : R
ht : t ∈ ↑M
⊢ IsLocalization.mk' Sₚ 1 ⟨(algebraMap R S) t, ⋯⟩ = (algebraMap Rₚ Sₚ) (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
Theorem: IsIntegral_of_isLocalization
Proof state before:
case h.e'_6
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Algebra.IsIntegral R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
t : R
ht : t ∈ ↑M
⊢ IsLocalization.mk' Sₚ 1 ⟨(algebraMap R S) t, ⋯⟩ = (algebraMap Rₚ Sₚ) (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
Tactic:
rw [this, IsLocalization.map_mk', _root_.map_one]
Proof state after:
no goals
Theorem: Polynomial.derivative_scaleRoots
Proof state before:
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
⊢ derivative (p.scaleRoots r) = r ^ (p.natDegree - ((derivative p).natDegree + 1)) • (derivative p).scaleRoots r
Tactic:
by_cases hp : natDegree p = 0
Proof state after:
case pos
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : p.natDegree = 0
⊢ derivative (p.scaleRoots r) = r ^ (p.natDegree - ((derivative p).natDegree + 1)) • (derivative p).scaleRoots r

case neg
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
⊢ derivative (p.scaleRoots r) = r ^ (p.natDegree - ((derivative p).natDegree + 1)) • (derivative p).scaleRoots r
Theorem: Polynomial.derivative_scaleRoots
Proof state before:
case neg
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
⊢ derivative (p.scaleRoots r) = r ^ (p.natDegree - ((derivative p).natDegree + 1)) • (derivative p).scaleRoots r
Tactic:
ext i
Proof state after:
case neg.a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
⊢ (derivative (p.scaleRoots r)).coeff i =
    (r ^ (p.natDegree - ((derivative p).natDegree + 1)) • (derivative p).scaleRoots r).coeff i
Theorem: Polynomial.derivative_scaleRoots
Proof state before:
case neg.a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
⊢ (derivative (p.scaleRoots r)).coeff i =
    (r ^ (p.natDegree - ((derivative p).natDegree + 1)) • (derivative p).scaleRoots r).coeff i
Tactic:
simp only [coeff_smul, coeff_scaleRoots, ge_iff_le, smul_eq_mul, coeff_derivative,
  mul_comm (r ^ (natDegree p - _)), mul_assoc, ← pow_add]
Proof state after:
case neg.a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
⊢ p.coeff (i + 1) * ((↑i + 1) * r ^ (p.natDegree - (i + 1))) =
    p.coeff (i + 1) * ((↑i + 1) * r ^ ((derivative p).natDegree - i + (p.natDegree - ((derivative p).natDegree + 1))))
Theorem: Polynomial.derivative_scaleRoots
Proof state before:
case neg.a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
⊢ p.coeff (i + 1) * ((↑i + 1) * r ^ (p.natDegree - (i + 1))) =
    p.coeff (i + 1) * ((↑i + 1) * r ^ ((derivative p).natDegree - i + (p.natDegree - ((derivative p).natDegree + 1))))
Tactic:
simp_rw [← mul_assoc, ← coeff_derivative]
Proof state after:
case neg.a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
⊢ (derivative p).coeff i * r ^ (p.natDegree - (i + 1)) =
    (derivative p).coeff i * r ^ ((derivative p).natDegree - i + (p.natDegree - ((derivative p).natDegree + 1)))
Theorem: Polynomial.derivative_scaleRoots
Proof state before:
case neg.a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
⊢ (derivative p).coeff i * r ^ (p.natDegree - (i + 1)) =
    (derivative p).coeff i * r ^ ((derivative p).natDegree - i + (p.natDegree - ((derivative p).natDegree + 1)))
Tactic:
cases lt_or_le (natDegree (derivative p)) i with
| inl h => simp only [coeff_eq_zero_of_natDegree_lt h, zero_mul]
| inr h =>
  congr
  have h' := natDegree_derivative_lt hp
  zify
  rw [Int.ofNat_sub h', Int.ofNat_sub h, Int.ofNat_sub (h.trans_lt h')]
  simp only [Nat.cast_succ]
  abel
Proof state after:
no goals
Theorem: Polynomial.derivative_scaleRoots
Proof state before:
case pos
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : p.natDegree = 0
⊢ derivative (p.scaleRoots r) = r ^ (p.natDegree - ((derivative p).natDegree + 1)) • (derivative p).scaleRoots r
Tactic:
rw [hp, Nat.zero_sub, pow_zero, one_smul]
Proof state after:
case pos
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : p.natDegree = 0
⊢ derivative (p.scaleRoots r) = (derivative p).scaleRoots r
Theorem: Polynomial.derivative_scaleRoots
Proof state before:
case pos
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : p.natDegree = 0
⊢ derivative (p.scaleRoots r) = (derivative p).scaleRoots r
Tactic:
rw [natDegree_eq_zero_iff_degree_le_zero, degree_le_zero_iff] at hp
Proof state after:
case pos
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : p = C (p.coeff 0)
⊢ derivative (p.scaleRoots r) = (derivative p).scaleRoots r
Theorem: Polynomial.derivative_scaleRoots
Proof state before:
case pos
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : p = C (p.coeff 0)
⊢ derivative (p.scaleRoots r) = (derivative p).scaleRoots r
Tactic:
rw [hp]
Proof state after:
case pos
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : p = C (p.coeff 0)
⊢ derivative ((C (p.coeff 0)).scaleRoots r) = (derivative (C (p.coeff 0))).scaleRoots r
Theorem: Polynomial.derivative_scaleRoots
Proof state before:
case pos
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : p = C (p.coeff 0)
⊢ derivative ((C (p.coeff 0)).scaleRoots r) = (derivative (C (p.coeff 0))).scaleRoots r
Tactic:
simp only [scaleRoots_C, derivative_C, zero_scaleRoots]
Proof state after:
no goals
Theorem: Polynomial.derivative_scaleRoots
Proof state before:
case neg.a.inl
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
h : (derivative p).natDegree < i
⊢ (derivative p).coeff i * r ^ (p.natDegree - (i + 1)) =
    (derivative p).coeff i * r ^ ((derivative p).natDegree - i + (p.natDegree - ((derivative p).natDegree + 1)))
Tactic:
simp only [coeff_eq_zero_of_natDegree_lt h, zero_mul]
Proof state after:
no goals
Theorem: Polynomial.derivative_scaleRoots
Proof state before:
case neg.a.inr
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
h : i ≤ (derivative p).natDegree
⊢ (derivative p).coeff i * r ^ (p.natDegree - (i + 1)) =
    (derivative p).coeff i * r ^ ((derivative p).natDegree - i + (p.natDegree - ((derivative p).natDegree + 1)))
Tactic:
congr
Proof state after:
case neg.a.inr.e_a.e_a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
h : i ≤ (derivative p).natDegree
⊢ p.natDegree - (i + 1) = (derivative p).natDegree - i + (p.natDegree - ((derivative p).natDegree + 1))
Theorem: Polynomial.derivative_scaleRoots
Proof state before:
case neg.a.inr.e_a.e_a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
h : i ≤ (derivative p).natDegree
⊢ p.natDegree - (i + 1) = (derivative p).natDegree - i + (p.natDegree - ((derivative p).natDegree + 1))
Tactic:
have h' := natDegree_derivative_lt hp
Proof state after:
case neg.a.inr.e_a.e_a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
h : i ≤ (derivative p).natDegree
h' : (derivative p).natDegree < p.natDegree
⊢ p.natDegree - (i + 1) = (derivative p).natDegree - i + (p.natDegree - ((derivative p).natDegree + 1))
Theorem: Polynomial.derivative_scaleRoots
Proof state before:
case neg.a.inr.e_a.e_a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
h : i ≤ (derivative p).natDegree
h' : (derivative p).natDegree < p.natDegree
⊢ p.natDegree - (i + 1) = (derivative p).natDegree - i + (p.natDegree - ((derivative p).natDegree + 1))
Tactic:
zify
Proof state after:
case neg.a.inr.e_a.e_a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
h : i ≤ (derivative p).natDegree
h' : (derivative p).natDegree < p.natDegree
⊢ ↑(p.natDegree - (i + 1)) = ↑((derivative p).natDegree - i) + ↑(p.natDegree - ((derivative p).natDegree + 1))
Theorem: Polynomial.derivative_scaleRoots
Proof state before:
case neg.a.inr.e_a.e_a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
h : i ≤ (derivative p).natDegree
h' : (derivative p).natDegree < p.natDegree
⊢ ↑(p.natDegree - (i + 1)) = ↑((derivative p).natDegree - i) + ↑(p.natDegree - ((derivative p).natDegree + 1))
Tactic:
rw [Int.ofNat_sub h', Int.ofNat_sub h, Int.ofNat_sub (h.trans_lt h')]
Proof state after:
case neg.a.inr.e_a.e_a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
h : i ≤ (derivative p).natDegree
h' : (derivative p).natDegree < p.natDegree
⊢ ↑p.natDegree - ↑i.succ = ↑(derivative p).natDegree - ↑i + (↑p.natDegree - ↑(derivative p).natDegree.succ)
Theorem: Polynomial.derivative_scaleRoots
Proof state before:
case neg.a.inr.e_a.e_a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
h : i ≤ (derivative p).natDegree
h' : (derivative p).natDegree < p.natDegree
⊢ ↑p.natDegree - ↑i.succ = ↑(derivative p).natDegree - ↑i + (↑p.natDegree - ↑(derivative p).natDegree.succ)
Tactic:
simp only [Nat.cast_succ]
Proof state after:
case neg.a.inr.e_a.e_a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
h : i ≤ (derivative p).natDegree
h' : (derivative p).natDegree < p.natDegree
⊢ ↑p.natDegree - (↑i + 1) = ↑(derivative p).natDegree - ↑i + (↑p.natDegree - (↑(derivative p).natDegree + 1))
Theorem: Polynomial.derivative_scaleRoots
Proof state before:
case neg.a.inr.e_a.e_a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
h : i ≤ (derivative p).natDegree
h' : (derivative p).natDegree < p.natDegree
⊢ ↑p.natDegree - (↑i + 1) = ↑(derivative p).natDegree - ↑i + (↑p.natDegree - (↑(derivative p).natDegree + 1))
Tactic:
abel
Proof state after:
no goals
Theorem: Polynomial.Separable.scaleRoots
Proof state before:
R : Type u_1
inst✝ : CommRing R
p : R[X]
hp : p.Separable
r : R
hr : IsUnit r
⊢ (p.scaleRoots r).Separable
Tactic:
delta Polynomial.Separable at hp ⊢
Proof state after:
R : Type u_1
inst✝ : CommRing R
p : R[X]
hp : IsCoprime p (derivative p)
r : R
hr : IsUnit r
⊢ IsCoprime (p.scaleRoots r) (derivative (p.scaleRoots r))
Theorem: Polynomial.Separable.scaleRoots
Proof state before:
R : Type u_1
inst✝ : CommRing R
p : R[X]
hp : IsCoprime p (derivative p)
r : R
hr : IsUnit r
⊢ IsCoprime (p.scaleRoots r) (derivative (p.scaleRoots r))
Tactic:
rw [Polynomial.derivative_scaleRoots, Algebra.smul_def]
Proof state after:
R : Type u_1
inst✝ : CommRing R
p : R[X]
hp : IsCoprime p (derivative p)
r : R
hr : IsUnit r
⊢ IsCoprime (p.scaleRoots r)
    ((algebraMap R R[X]) (r ^ (p.natDegree - ((derivative p).natDegree + 1))) * (derivative p).scaleRoots r)
Theorem: Polynomial.Separable.scaleRoots
Proof state before:
R : Type u_1
inst✝ : CommRing R
p : R[X]
hp : IsCoprime p (derivative p)
r : R
hr : IsUnit r
⊢ IsCoprime (p.scaleRoots r)
    ((algebraMap R R[X]) (r ^ (p.natDegree - ((derivative p).natDegree + 1))) * (derivative p).scaleRoots r)
Tactic:
refine (isCoprime_mul_unit_left_right ((hr.pow _).map _) _ _).mpr ?_
Proof state after:
R : Type u_1
inst✝ : CommRing R
p : R[X]
hp : IsCoprime p (derivative p)
r : R
hr : IsUnit r
⊢ IsCoprime (p.scaleRoots r) ((derivative p).scaleRoots r)
Theorem: Polynomial.Separable.scaleRoots
Proof state before:
R : Type u_1
inst✝ : CommRing R
p : R[X]
hp : IsCoprime p (derivative p)
r : R
hr : IsUnit r
⊢ IsCoprime (p.scaleRoots r) ((derivative p).scaleRoots r)
Tactic:
exact Polynomial.isCoprime_scaleRoots _ _ _ hr hp
Proof state after:
no goals
Theorem: IsSeparable_of_isLocalization
Proof state before:
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
⊢ IsSeparable Rₚ Sₚ
Tactic:
have : algebraMap Rₚ Sₚ = IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ
  (algebraMap R S) (Submonoid.le_comap_map M) := by
  apply IsLocalization.ringHom_ext M
  simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
Proof state after:
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
⊢ IsSeparable Rₚ Sₚ