mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Minpoly.IsConjRoot

Goal state before:
pp: K : Type u_2
S : Type u_4
inst✝³ : CommRing S
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : IsDomain S
x y : S
h : IsIntegral K x
⊢ y ∈ (minpoly K x).aroots S ↔ y ∈ (minpoly K x).rootSet S

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.IsConjRoot

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R S
r : R
x : S
h : X - C r = minpoly R x
hf : Function.Injective ⇑(algebraMap R S)
⊢ x ∈ (X - C r).aroots S

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.IsConjRoot

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R S
r : R
x : S
h : IsConjRoot R ((algebraMap R S) r) x
hf : Function.Injective ⇑(algebraMap R S)
⊢ x = (algebraMap R S) r

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.IsConjRoot

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : IsSeparable K x
sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
⊢ x ∉ ⊥ ↔ ∃ y, x ≠ y ∧ IsConjRoot K x y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hlim : Tendsto (fun n ↦ seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' c f x))
⊢ seminormFromConst_seq c f (c * x) = fun n ↦ f c * seminormFromConst_seq c f x (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
⊢ seminormFromConst' c f (c * x) = seminormFromConst' c f c * seminormFromConst' c f x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: K : Type u_1
inst✝ : Field K
k : K
g : RingSeminorm K
hg1 : g 1 ≤ 1
hg_k : g k ≠ 0
hg_pm : IsPowMul ⇑g
⊢ (seminormFromConst hg1 hg_k hg_pm) k ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Krasner

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁵ : NormedField L
inst✝⁴ : NontriviallyNormedField K
inst✝³ : CompleteSpace K
inst✝² : IsUltrametricDist K
inst✝¹ : NormedAlgebra K L
inst✝ : Normal K L
x y : L
xsep : IsSeparable K x
sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
this✝¹ : FiniteDimensional K ↥K⟮y⟯
this✝ : IsUltrametricDist L
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
zsep : IsSeparable (↥K⟮y⟯) z
this : z ∈ K⟮y⟯
⊢ x ∈ K⟮y⟯

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Krasner

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁵ : NormedField L
inst✝⁴ : NontriviallyNormedField K
inst✝³ : CompleteSpace K
inst✝² : IsUltrametricDist K
inst✝¹ : NormedAlgebra K L
inst✝ : Normal K L
x y : L
xsep : IsSeparable K x
sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
this✝ : FiniteDimensional K ↥K⟮y⟯
this : IsUltrametricDist L
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
zsep : IsSeparable (↥K⟮y⟯) z
⊢ z ∈ K⟮y⟯ ↔ z ∈ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Krasner

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁵ : NormedField L
inst✝⁴ : NontriviallyNormedField K
inst✝³ : CompleteSpace K
inst✝² : IsUltrametricDist K
inst✝¹ : NormedAlgebra K L
inst✝ : Normal K L
x y : L
xsep : IsSeparable K x
sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
this✝¹ : FiniteDimensional K ↥K⟮y⟯
this✝ : IsUltrametricDist L
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
zsep : IsSeparable (↥K⟮y⟯) z
this : z ∈ K⟮y⟯ ↔ z ∈ ⊥
hz : z ∉ ⊥
z' : L
hne : z ≠ z'
h1 : IsConjRoot (↥K⟮y⟯) z z'
σ : Gal(L/↥K⟮y⟯)
hσ : z' = σ.symm z
⊢ ‖z - z'‖ ≤ max ‖z‖ ‖z'‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Krasner

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁵ : NormedField L
inst✝⁴ : NontriviallyNormedField K
inst✝³ : CompleteSpace K
inst✝² : IsUltrametricDist K
inst✝¹ : NormedAlgebra K L
inst✝ : Normal K L
x y : L
xsep : IsSeparable K x
sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
this✝¹ : FiniteDimensional K ↥K⟮y⟯
this✝ : IsUltrametricDist L
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
zsep : IsSeparable (↥K⟮y⟯) z
this : z ∈ K⟮y⟯ ↔ z ∈ ⊥
hz : z ∉ ⊥
z' : L
hne : z ≠ z'
h1 : IsConjRoot (↥K⟮y⟯) z z'
σ : Gal(L/↥K⟮y⟯)
hσ : z' = σ.symm z
⊢ max ‖z‖ ‖z'‖ ≤ ‖x - y‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Krasner

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁵ : NormedField L
inst✝⁴ : NontriviallyNormedField K
inst✝³ : CompleteSpace K
inst✝² : IsUltrametricDist K
inst✝¹ : NormedAlgebra K L
inst✝ : Normal K L
x y : L
xsep : IsSeparable K x
sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
this✝¹ : FiniteDimensional K ↥K⟮y⟯
this✝ : IsUltrametricDist L
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
zsep : IsSeparable (↥K⟮y⟯) z
this : z ∈ K⟮y⟯ ↔ z ∈ ⊥
hz : z ∉ ⊥
z' : L
hne : z ≠ z'
h1 : IsConjRoot (↥K⟮y⟯) z z'
σ : Gal(L/↥K⟮y⟯)
hσ : z' = σ.symm z
⊢ ‖x - y‖ < ‖x - (z' + y)‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Krasner

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁵ : NormedField L
inst✝⁴ : NontriviallyNormedField K
inst✝³ : CompleteSpace K
inst✝² : IsUltrametricDist K
inst✝¹ : NormedAlgebra K L
inst✝ : Normal K L
x y : L
xsep : IsSeparable K x
sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
this✝¹ : FiniteDimensional K ↥K⟮y⟯
this✝ : IsUltrametricDist L
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
zsep : IsSeparable (↥K⟮y⟯) z
this : z ∈ K⟮y⟯ ↔ z ∈ ⊥
hz : z ∉ ⊥
z' : L
hne : z ≠ z'
h1 : IsConjRoot (↥K⟮y⟯) z z'
σ : Gal(L/↥K⟮y⟯)
hσ : z' = σ.symm z
⊢ ‖x - (z' + y)‖ = ‖z - z'‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Krasner

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁵ : NormedField L
inst✝⁴ : NontriviallyNormedField K
inst✝³ : CompleteSpace K
inst✝² : IsUltrametricDist K
inst✝¹ : NormedAlgebra K L
inst✝ : Normal K L
x y : L
xsep : IsSeparable K x
sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
⊢ x ∈ K⟮y⟯

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : μ x ≠ 0
L : ℝ := ⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 : μ (x ^ ↑m1) ^ (1 / ↑↑m1) < (⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)) + ε / 2
m2 : ℕ
hm2 : ∀ n ≥ m2, (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬μ (x ^ (n % ↑m1)) = 0
hxn' : 0 < μ (x ^ (n % ↑m1))
h : μ (x ^ (↑m1 * (n / ↑m1))) ^ (1 / ↑n) ≤ (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n)
hL0' : 0 < L + ε / 2
⊢ (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n) < (L + ε / 2) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Krasner

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁵ : NormedField L
inst✝⁴ : NontriviallyNormedField K
inst✝³ : CompleteSpace K
inst✝² : IsUltrametricDist K
inst✝¹ : NormedAlgebra K L
inst✝ : Algebra.IsAlgebraic K L
x y : L
xsep : IsSeparable K x
sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
C : Type u_1 := AlgebraicClosure K
this✝³ : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this✝² : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst✝ : Algebra L C := iL.toAlgebra
this✝¹ : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this✝ : IsKrasner K C := of_completeSpace_of_normal K C
norm_iL : ∀ (x : L), ‖iL x‖ = ‖x‖
this : iL x ∈ K⟮iL y⟯
⊢ x ∈ K⟮y⟯

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Krasner

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁵ : NormedField L
inst✝⁴ : NontriviallyNormedField K
inst✝³ : CompleteSpace K
inst✝² : IsUltrametricDist K
inst✝¹ : NormedAlgebra K L
inst✝ : Algebra.IsAlgebraic K L
x y : L
xsep : IsSeparable K x
sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
C : Type u_1 := AlgebraicClosure K
this✝² : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this✝¹ : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst✝ : Algebra L C := iL.toAlgebra
this✝ : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := of_completeSpace_of_normal K C
norm_iL : ∀ (x : L), ‖iL x‖ = ‖x‖
⊢ minpoly K (iL x) ∣ minpoly K x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Krasner

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁵ : NormedField L
inst✝⁴ : NontriviallyNormedField K
inst✝³ : CompleteSpace K
inst✝² : IsUltrametricDist K
inst✝¹ : NormedAlgebra K L
inst✝ : Algebra.IsAlgebraic K L
x y : L
xsep : IsSeparable K x
sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
C : Type u_1 := AlgebraicClosure K
this✝² : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this✝¹ : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst✝ : Algebra L C := iL.toAlgebra
this✝ : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := of_completeSpace_of_normal K C
norm_iL : ∀ (x : L), ‖iL x‖ = ‖x‖
xC' : C
hx' : IsConjRoot K (iL x) xC'
hne : iL x ≠ xC'
⊢ xC' ∈ (minpoly K x).rootSet C

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : μ x ≠ 0
L : ℝ := ⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 : μ (x ^ ↑m1) ^ (1 / ↑↑m1) < (⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)) + ε / 2
m2 : ℕ
hm2 : ∀ n ≥ m2, (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬μ (x ^ (n % ↑m1)) = 0
hxn' : 0 < μ (x ^ (n % ↑m1))
h : μ (x ^ (↑m1 * (n / ↑m1))) ^ (1 / ↑n) ≤ (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n)
hL0' : 0 < L + ε / 2
h1 : (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n) < (L + ε / 2) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n))
⊢ μ (x ^ (n % ↑m1)) ^ (1 / ↑n) ≤ (μ x ^ (n % ↑m1)) ^ (1 / ↑n)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
inst✝ : SeminormedRing R
p : R[X]
n : ℕ
hn : n < p.natDegree
⊢ spectralValueTerms p n = ‖p.coeff n‖ ^ (1 / (↑p.natDegree - ↑n))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
inst✝ : SeminormedRing R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ spectralValueTerms p n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
inst✝ : SeminormedRing R
p : R[X]
⊢ Set.range (spectralValueTerms p) ⊆ {0} ∪ (fun n ↦ ‖p.coeff n‖ ^ (1 / (↑p.natDegree - ↑n))) '' Set.Iio p.natDegree

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
inst✝ : SeminormedRing R
p : R[X]
n : ℕ
⊢ 0 ≤ spectralValueTerms p n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Krasner

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁵ : NormedField L
inst✝⁴ : NontriviallyNormedField K
inst✝³ : CompleteSpace K
inst✝² : IsUltrametricDist K
inst✝¹ : NormedAlgebra K L
inst✝ : Algebra.IsAlgebraic K L
x y : L
xsep : IsSeparable K x
sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
⊢ x ∈ K⟮y⟯

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : μ x ≠ 0
L : ℝ := ⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 : μ (x ^ ↑m1) ^ (1 / ↑↑m1) < (⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)) + ε / 2
m2 : ℕ
hm2 : ∀ n ≥ m2, (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬μ (x ^ (n % ↑m1)) = 0
hxn' : 0 < μ (x ^ (n % ↑m1))
h : μ (x ^ (↑m1 * (n / ↑m1))) ^ (1 / ↑n) ≤ (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n)
hL0' : 0 < L + ε / 2
h1 : (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n) < (L + ε / 2) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n))
h2 : μ (x ^ (n % ↑m1)) ^ (1 / ↑n) ≤ (μ x ^ (n % ↑m1)) ^ (1 / ↑n)
⊢ L + ε = L + ε / 2 + ε / 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Instances

Goal state before:
pp: F : Type u_1
inst✝ : NormedField F
f : Filter F
hc : Cauchy f
hn : nhds 0 ⊓ f = ⊥
δ : ℝ
δ_pos : δ > 0
hδ : ∀ᶠ (y : F) in f, δ ≤ ‖y‖
y : F
hy : δ ≤ ‖y‖
⊢ δ ≤ ((fun x ↦ ‖x⁻¹‖) y)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Instances

Goal state before:
pp: F : Type u_1
inst✝ : NormedField F
f : Filter F
hc : Cauchy f
hn : nhds 0 ⊓ f = ⊥
δ : ℝ
δ_pos : δ > 0
hδ : ∀ᶠ (y : F) in f, δ ≤ ‖y‖
f_bdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ ‖x⁻¹‖
y : F
hy : δ ≤ ‖y‖
⊢ y ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Instances

Goal state before:
pp: F : Type u_1
inst✝ : NormedField F
f : Filter F
hc : Cauchy f
hn : nhds 0 ⊓ f = ⊥
δ : ℝ
δ_pos : δ > 0
hδ : ∀ᶠ (y : F) in f, δ ≤ ‖y‖
f_bdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ ‖x⁻¹‖
h₀ : ∀ᶠ (y : F) in f, y ≠ 0
x✝¹ : F × F
x y : F
x✝ : (x, y).1 ≠ 0 ∧ (x, y).2 ≠ 0
hx : (x, y).1 ≠ 0
hy : (x, y).2 ≠ 0
⊢ (x, y).1⁻¹ - (x, y).2⁻¹ = (x, y).1⁻¹ * ((x, y).2 - (x, y).1) * (x, y).2⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
r : R
this : (⨆ n, if n = 0 then ‖r‖ else 0) = ‖r‖
⊢ (⨆ n, if n = 0 then ‖X.coeff n - (C r).coeff n‖ ^ (1 - ↑n)⁻¹ else 0) = ‖r‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
r : R
x✝ : ℝ
hx : x✝ < ‖r‖
⊢ x✝ < if 0 = 0 then ‖r‖ else 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
r : R
⊢ spectralValue (X - C r) = ‖r‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Instances

Goal state before:
pp: F : Type u_1
inst✝ : NormedField F
f : Filter F
hc : Cauchy f
hn : nhds 0 ⊓ f = ⊥
⊢ Cauchy (map (fun x ↦ x⁻¹) f)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.ProperSpace

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
h : c = 0
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.ProperSpace

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
this : c ^ n ≠ 0
x✝ : 𝕜
⊢ 0 < ?m.159

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.ProperSpace

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
⊢ IsCompact (closedBall 0 (‖c‖ ^ n * r))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.ProperSpace

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : WeaklyLocallyCompactSpace 𝕜
⊢ ProperSpace 𝕜

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.CocompactMap

Goal state before:
pp: E : Type u_2
F : Type u_3
𝓕 : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
f : 𝓕
inst✝² : ProperSpace F
inst✝¹ : FunLike 𝓕 E F
inst✝ : CocompactMapClass 𝓕 E F
ε : ℝ
h : ⇑f ⁻¹' (closedBall 0 ε)ᶜ ∈ cocompact E
r : ℝ
hr : (closedBall 0 r)ᶜ ⊆ ⇑f ⁻¹' (closedBall 0 ε)ᶜ
x : E
hx : r < ‖x‖
this : x ∈ ⇑f ⁻¹' (closedBall 0 ε)ᶜ
⊢ ε < ‖f x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.CocompactMap

Goal state before:
pp: E : Type u_2
F : Type u_3
𝓕 : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
f : 𝓕
inst✝² : ProperSpace F
inst✝¹ : FunLike 𝓕 E F
inst✝ : CocompactMapClass 𝓕 E F
ε : ℝ
⊢ ∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
n : ℕ
⊢ spectralValue (X ^ n) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : Nontrivial R
p : R[X]
hp : p.Monic
h : spectralValue p = 0
n : ℕ
hn : n < p.natDegree
⊢ spectralValueTerms p n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : Nontrivial R
p : R[X]
hp : p.Monic
⊢ spectralValue p = 0 ↔ p = X ^ p.natDegree

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
inst✝ : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : iSup (spectralValueTerms P) ≤ 1
n : ℕ
hPn : n < P.natDegree
this : 1 < ‖P.coeff n‖
⊢ 0 < 1 / (↑P.natDegree - ↑n)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.CocompactMap

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), ∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
⊢ Tendsto f (cocompact E) (cocompact F)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Completeness

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
n : ℕ
⊢ 0 < (1 / 2) ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Completeness

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < (1 / 2) ^ n
n : ℕ
⊢ 0 ≤ dist (u (f (n + 1))) (u (f n))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Completeness

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
⊢ ∃ f, StrictMono f ∧ Summable fun i ↦ dist (u (f (i + 1))) (u (f i))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Completeness

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
h : ∀ (u : ℕ → E), (Summable fun x ↦ ‖u x‖) → ∃ a, Tendsto (fun n ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable fun i ↦ ‖u (f (i + 1)) - u (f i)‖
v : ℕ → E := fun n ↦ u (f (n + 1)) - u (f n)
⊢ (fun n ↦ ∑ i ∈ range n, v i) = fun n ↦ u (f n) - u (f 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
inst✝ : NormedDivisionRing R
P : R[X]
hP : P.Monic
⊢ spectralValue P ≤ 1 ↔ ∀ (n : ℕ), ‖P.coeff n‖ ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Completeness

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
h : ∀ (u : ℕ → E), (Summable fun x ↦ ‖u x‖) → ∃ a, Tendsto (fun n ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)
⊢ CompleteSpace E

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Completeness

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
u : ℕ → E
hu : Summable fun x ↦ ‖u x‖
⊢ ∃ a, Tendsto (fun n ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Dense

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this✝ : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
⊢ (map (algebraMap L f.SplittingField) f).degree ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Dense

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this✝ : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
⊢ (map (algebraMap L f.SplittingField) f).degree ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Dense

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this✝ : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
⊢ (aeval a) f = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
p : K[X]
hp : p.Monic
x : L
hx : (aeval x) p = 0
hx0 : ¬f x = 0
h_ge : ¬f x ≤ spectralValue p
n : ℕ
hn : n < p.natDegree
⊢ (‖p.coeff n‖ ^ (1 / (↑p.natDegree - ↑n))) ^ (p.natDegree - n) = ‖p.coeff n‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : μ x ≠ 0
L : ℝ := ⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 : μ (x ^ ↑m1) ^ (1 / ↑↑m1) < (⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)) + ε / 2
m2 : ℕ
hm2 : ∀ n ≥ m2, (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬μ (x ^ (n % ↑m1)) = 0
hxn' : 0 < μ (x ^ (n % ↑m1))
h : μ (x ^ (↑m1 * (n / ↑m1))) ^ (1 / ↑n) ≤ (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n)
hL0' : 0 < L + ε / 2
h1 : (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n) < (L + ε / 2) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n))
h2 : μ (x ^ (n % ↑m1)) ^ (1 / ↑n) ≤ (μ x ^ (n % ↑m1)) ^ (1 / ↑n)
⊢ (L + ε / 2) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) ≤ L + ε

Tactic:
by

Goal state after: