mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Polynomial.Factorization

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : IsAlgClosed F
f : F[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 1)
⊢ 0 < f.natDegree

Tactic:
grind [IsMonicOfDegree.natDegree_eq]

Goal state after:
Module: Mathlib.Analysis.Polynomial.Factorization

Goal state before:
pp: f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 1)
⊢ 0 < f.natDegree

Tactic:
grind [IsMonicOfDegree.natDegree_eq]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝¹ : SeminormedRing R
inst✝ : SeminormedAddCommGroup M
x : tsze R M
⊢ ↑‖x‖₊ = ↑(‖x.fst‖₊ + ‖x.snd‖₊)

Tactic:
;

Goal state after:
R : Type u_3
M : Type u_4
inst✝¹ : SeminormedRing R
inst✝ : SeminormedAddCommGroup M
x : tsze R M
⊢ ↑‖x‖₊ = ↑(‖x.fst‖₊ + ‖x.snd‖₊)
Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Goal state before:
pp: case h₂.refine_1
𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst✝¹¹ : SeminormedCommRing S
inst✝¹⁰ : SeminormedRing R
inst✝⁹ : SeminormedAddCommGroup M
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsBoundedSMul S R
inst✝⁵ : IsBoundedSMul S M
inst✝⁴ : Module R M
inst✝³ : IsBoundedSMul R M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : IsBoundedSMul Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ ‖r₁ • m₂‖ ≤ ‖r₁‖ * ‖m₂‖

Tactic:
apply norm_smul_le

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Goal state before:
pp: case h₂.refine_2
𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst✝¹¹ : SeminormedCommRing S
inst✝¹⁰ : SeminormedRing R
inst✝⁹ : SeminormedAddCommGroup M
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsBoundedSMul S R
inst✝⁵ : IsBoundedSMul S M
inst✝⁴ : Module R M
inst✝³ : IsBoundedSMul R M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : IsBoundedSMul Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ ‖MulOpposite.op r₂ • m₁‖ ≤ ‖r₂‖ * ‖m₁‖

Tactic:
apply norm_smul_le

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Goal state before:
pp: 𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst✝¹² : SeminormedCommRing S
inst✝¹¹ : SeminormedRing R
inst✝¹⁰ : SeminormedAddCommGroup M
inst✝⁹ : Algebra S R
inst✝⁸ : Module S M
inst✝⁷ : IsBoundedSMul S R
inst✝⁶ : IsBoundedSMul S M
inst✝⁵ : Module R M
inst✝⁴ : IsBoundedSMul R M
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : IsBoundedSMul Rᵐᵒᵖ M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
inst✝ : NormOneClass R
⊢ ‖1‖ = 1

Tactic:
by rw [norm_def, fst_one, snd_one, norm_zero, norm_one, add_zero]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormOneClass F
inst✝¹ : NormMulClass F
inst✝ : NormedAlgebra ℂ F
x : F
z : ℂ
hz : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℂ F) x_1‖) univ z
H : ∀ (z' : ℂ), ‖x - (algebraMap ℂ F) z'‖ ≠ 0
c : ℂ
M : ℝ := ‖x - (algebraMap ℂ F) z‖
hMdef : M = ‖x - (algebraMap ℂ F) z‖
this : ‖x - (algebraMap ℂ F) z‖ ≠ 0
⊢ 0 < M

Tactic:
;

Goal state after:
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormOneClass F
inst✝¹ : NormMulClass F
inst✝ : NormedAlgebra ℂ F
x : F
z : ℂ
hz : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℂ F) x_1‖) univ z
H : ∀ (z' : ℂ), ‖x - (algebraMap ℂ F) z'‖ ≠ 0
c : ℂ
M : ℝ := ‖x - (algebraMap ℂ F) z‖
hMdef : M = ‖x - (algebraMap ℂ F) z‖
this : ‖x - (algebraMap ℂ F) z‖ ≠ 0
⊢ 0 < M
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: x✝¹ x✝ : ℍ
⊢ √(normSq (x✝¹ * x✝)) = √(normSq x✝¹) * √(normSq x✝)

Tactic:
;

Goal state after:
x✝¹ x✝ : ℍ
⊢ √(normSq (x✝¹ * x✝)) = √(normSq x✝¹) * √(normSq x✝)
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
HH : M * (1 + (‖φ x u - φ x w‖ / M) ^ n) = (M ^ n + ‖φ x u - φ x w‖ ^ n) / M ^ (n - 1)
⊢ ‖φ x u‖ * M ^ (n - 1) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n

Tactic:
;

Goal state after:
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
HH : M * (1 + (‖φ x u - φ x w‖ / M) ^ n) = (M ^ n + ‖φ x u - φ x w‖ ^ n) / M ^ (n - 1)
⊢ ‖φ x u‖ * M ^ (n - 1) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
q : ℝ × ℝ → ℝ[X] := fun y ↦ X ^ 2 - C y.1 * X + C y.2
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
⊢ X ^ 2 - C w.1 * X + C w.2 - (X ^ 2 - C u.1 * X + C u.2) = (C u.1 - C w.1) * X + C w.2 - C u.2

Tactic:
;

Goal state after:
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
q : ℝ × ℝ → ℝ[X] := fun y ↦ X ^ 2 - C y.1 * X + C y.2
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
⊢ X ^ 2 - C w.1 * X + C w.2 - (X ^ 2 - C u.1 * X + C u.2) = (C u.1 - C w.1) * X + C w.2 - C u.2
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
q : ℝ × ℝ → ℝ[X] := fun y ↦ X ^ 2 - C y.1 * X + C y.2
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
hsub : q w - q u = (C u.1 - C w.1) * X + C w.2 - C u.2
hdvd : q u ∣ q w ^ n - (q w - q u) ^ n
⊢ (((C u.1 - C w.1) * X + C w.2 - C u.2) ^ n).natDegree < 2 * n

Tactic:
;

Goal state after:
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
q : ℝ × ℝ → ℝ[X] := fun y ↦ X ^ 2 - C y.1 * X + C y.2
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
hsub : q w - q u = (C u.1 - C w.1) * X + C w.2 - C u.2
hdvd : q u ∣ q w ^ n - (q w - q u) ^ n
⊢ (((C u.1 - C w.1) * X + C w.2 - C u.2) ^ n).natDegree < 2 * n
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: case hbc
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
q : ℝ × ℝ → ℝ[X] := fun y ↦ X ^ 2 - C y.1 * X + C y.2
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
hsub : q w - q u = (C u.1 - C w.1) * X + C w.2 - C u.2
hdvd : q u ∣ q w ^ n - (q w - q u) ^ n
⊢ n < 2 * n

Tactic:
;

Goal state after:
case hbc
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
q : ℝ × ℝ → ℝ[X] := fun y ↦ X ^ 2 - C y.1 * X + C y.2
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
hsub : q w - q u = (C u.1 - C w.1) * X + C w.2 - C u.2
hdvd : q u ∣ q w ^ n - (q w - q u) ^ n
⊢ n < 2 * n
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
q : ℝ × ℝ → ℝ[X] := fun y ↦ X ^ 2 - C y.1 * X + C y.2
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
hsub : q w - q u = (C u.1 - C w.1) * X + C w.2 - C u.2
hdvd : q u ∣ q w ^ n - (q w - q u) ^ n
H' : ((q w - q u) ^ n).natDegree < 2 * n
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * n - 2)
hrel : q w ^ n = p * q u + (q w - q u) ^ n
⊢ ‖φ x u‖ * M ^ (n - 1) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n

Tactic:
;

Goal state after:
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
q : ℝ × ℝ → ℝ[X] := fun y ↦ X ^ 2 - C y.1 * X + C y.2
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
hsub : q w - q u = (C u.1 - C w.1) * X + C w.2 - C u.2
hdvd : q u ∣ q w ^ n - (q w - q u) ^ n
H' : ((q w - q u) ^ n).natDegree < 2 * n
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * n - 2)
hrel : q w ^ n = p * q u + (q w - q u) ^ n
⊢ ‖φ x u‖ * M ^ (n - 1) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: case hbc
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖x - (algebraMap ℝ F) r‖
this : Tendsto (fun y ↦ ‖y.1‖ * c) (cobounded ℝ ×ˢ ⊤) atTop
y : ℝ × ℝ
hy : y ∈ {0}ᶜ ×ˢ Set.univ
⊢ c ≤ ‖x - (algebraMap ℝ F) (y.1⁻¹ * y.2)‖

Tactic:
;

Goal state after:
case hbc
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖x - (algebraMap ℝ F) r‖
this : Tendsto (fun y ↦ ‖y.1‖ * c) (cobounded ℝ ×ˢ ⊤) atTop
y : ℝ × ℝ
hy : y ∈ {0}ᶜ ×ˢ Set.univ
⊢ c ≤ ‖x - (algebraMap ℝ F) (y.1⁻¹ * y.2)‖
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: case h.inr
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm✝ : max 1 (‖x‖ ^ m) = 1
hx : ‖x‖ ^ m ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
hm : m ≠ 0
⊢ ‖x‖ ^ i ≤ 1

Tactic:
· rw [pow_le_one_iff_of_nonneg (norm_nonneg _) hm] at hx
      exact pow_le_one₀ (norm_nonneg _) hx

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
h : p 1 = 1
⊢ 1 ≠ 0

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
h : p 1 = 1
⊢ 1 ≠ 0
Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Goal state before:
pp: case mk
R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f f' : AlgebraNorm R S
toRingNorm✝ : RingNorm S
smul'✝ : ∀ (a : R) (x : S), toRingNorm✝.toFun (a • x) = ‖a‖ * toRingNorm✝.toFun x
h : ⇑{ toRingNorm := toRingNorm✝, smul' := smul'✝ }.toRingSeminorm = ⇑f'.toRingSeminorm
⊢ { toRingNorm := toRingNorm✝, smul' := smul'✝ } = f'

Tactic:
;

Goal state after:
case mk
R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f f' : AlgebraNorm R S
toRingNorm✝ : RingNorm S
smul'✝ : ∀ (a : R) (x : S), toRingNorm✝.toFun (a • x) = ‖a‖ * toRingNorm✝.toFun x
h : ⇑{ toRingNorm := toRingNorm✝, smul' := smul'✝ }.toRingSeminorm = ⇑f'.toRingSeminorm
⊢ { toRingNorm := toRingNorm✝, smul' := smul'✝ } = f'
Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f : AlgebraNorm R S
toRingNorm✝¹ : RingNorm S
smul'✝¹ : ∀ (a : R) (x : S), toRingNorm✝¹.toFun (a • x) = ‖a‖ * toRingNorm✝¹.toFun x
toRingNorm✝ : RingNorm S
smul'✝ : ∀ (a : R) (x : S), toRingNorm✝.toFun (a • x) = ‖a‖ * toRingNorm✝.toFun x
h :
  ⇑{ toRingNorm := toRingNorm✝¹, smul' := smul'✝¹ }.toRingSeminorm =
    ⇑{ toRingNorm := toRingNorm✝, smul' := smul'✝ }.toRingSeminorm
⊢ { toRingNorm := toRingNorm✝¹, smul' := smul'✝¹ } = { toRingNorm := toRingNorm✝, smul' := smul'✝ }

Tactic:
;

Goal state after:
case mk.mk
R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f : AlgebraNorm R S
toRingNorm✝¹ : RingNorm S
smul'✝¹ : ∀ (a : R) (x : S), toRingNorm✝¹.toFun (a • x) = ‖a‖ * toRingNorm✝¹.toFun x
toRingNorm✝ : RingNorm S
smul'✝ : ∀ (a : R) (x : S), toRingNorm✝.toFun (a • x) = ‖a‖ * toRingNorm✝.toFun x
h :
  ⇑{ toRingNorm := toRingNorm✝¹, smul' := smul'✝¹ }.toRingSeminorm =
    ⇑{ toRingNorm := toRingNorm✝, smul' := smul'✝ }.toRingSeminorm
⊢ { toRingNorm := toRingNorm✝¹, smul' := smul'✝¹ } = { toRingNorm := toRingNorm✝, smul' := smul'✝ }
Module: Mathlib.Analysis.Normed.Field.Approximation

Goal state before:
pp: K : Type u_1
inst✝ : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
this : (Multiset.map (fun x ↦ ‖a - x‖) g.roots).prod < (↑f.natDegree + 1) * ε * max ‖a‖ 1 ^ ↑f.natDegree
h : ∀ b ∈ g.roots, ((↑f.natDegree + 1) * ε) ^ (↑f.natDegree)⁻¹ * max ‖a‖ 1 ≤ ‖a - b‖
i✝ : K
a✝ : i✝ ∈ g.roots
⊢ 0 ≤ ((↑f.natDegree + 1) * ε) ^ (↑f.natDegree)⁻¹ * max ‖a‖ 1

Tactic:
;

Goal state after:
K : Type u_1
inst✝ : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
this : (Multiset.map (fun x ↦ ‖a - x‖) g.roots).prod < (↑f.natDegree + 1) * ε * max ‖a‖ 1 ^ ↑f.natDegree
h : ∀ b ∈ g.roots, ((↑f.natDegree + 1) * ε) ^ (↑f.natDegree)⁻¹ * max ‖a‖ 1 ≤ ‖a - b‖
i✝ : K
a✝ : i✝ ∈ g.roots
⊢ 0 ≤ ((↑f.natDegree + 1) * ε) ^ (↑f.natDegree)⁻¹ * max ‖a‖ 1
Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Goal state before:
pp: R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f : AlgebraNorm R S
hf1 : f 1 = 1
a : R
⊢ f (a • 1) = ‖a‖

Tactic:
← mul_one ‖a‖,

Goal state after:
R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f : AlgebraNorm R S
hf1 : f 1 = 1
a : R
⊢ f (a • 1) = ‖a‖ * 1
Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Goal state before:
pp: R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f : AlgebraNorm R S
hf1 : f 1 = 1
a : R
⊢ f (a • 1) = ‖a‖ * f 1

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f : AlgebraNorm R S
hf1 : f 1 = 1
a : R
⊢ f (a • 1) = ‖a‖ * f 1
Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Goal state before:
pp: R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f : AlgebraNorm R S
hf1 : f 1 = 1
a : R
⊢ f (a • 1) = ‖a‖

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f : AlgebraNorm R S
hf1 : f 1 = 1
a : R
⊢ f (a • 1) = ‖a‖
Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Goal state before:
pp: R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f✝ : AlgebraNorm R S
A : Subalgebra R S
f : AlgebraNorm R S
x : ↥A
hx : f ↑x = 0
⊢ ↑x = 0

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f✝ : AlgebraNorm R S
A : Subalgebra R S
f : AlgebraNorm R S
x : ↥A
hx : f ↑x = 0
⊢ ↑x = 0
Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : SeminormedCommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
f : AlgebraNorm R S
f' : MulAlgebraNorm R S
toMulRingSeminorm✝ : MulRingSeminorm S
eq_zero_of_map_eq_zero'✝ : ∀ (x : S), toMulRingSeminorm✝.toFun x = 0 → x = 0
smul'✝ :
  ∀ (a : R) (x : S),
    { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }.toFun (a • x) =
      ‖a‖ * { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }.toFun x
h :
  { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝,
        smul' := smul'✝ }.toMulRingSeminorm =
    f'.toMulRingSeminorm
⊢ { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝, smul' := smul'✝ } = f'

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : SeminormedCommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
f : AlgebraNorm R S
f' : MulAlgebraNorm R S
toMulRingSeminorm✝ : MulRingSeminorm S
eq_zero_of_map_eq_zero'✝ : ∀ (x : S), toMulRingSeminorm✝.toFun x = 0 → x = 0
smul'✝ :
  ∀ (a : R) (x : S),
    { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }.toFun (a • x) =
      ‖a‖ * { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }.toFun x
h :
  { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝,
        smul' := smul'✝ }.toMulRingSeminorm =
    f'.toMulRingSeminorm
⊢ { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝, smul' := smul'✝ } = f'
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
h_le : ∀ (m : ℕ), p (x ^ s (ψ m)) ^ (1 / ↑(ψ m)) ≤ p x ^ (↑(s (ψ m)) / ↑(ψ m))
hfx : 1 < p x
⊢ ∃ b, ∀ (x_1 : ℕ), p (x ^ s (ψ x_1)) ^ (1 / ↑(ψ x_1)) ≤ b

Tactic:
use p x
    refine fun m ↦ le_trans (h_le m) <| rpow_le_self_of_one_le hfx.le ?_
    exact div_le_one_of_le₀ (mod_cast hs_le _) (cast_nonneg _)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : SeminormedCommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
f : AlgebraNorm R S
toMulRingSeminorm✝¹ : MulRingSeminorm S
eq_zero_of_map_eq_zero'✝¹ : ∀ (x : S), toMulRingSeminorm✝¹.toFun x = 0 → x = 0
smul'✝¹ :
  ∀ (a : R) (x : S),
    { toMulRingSeminorm := toMulRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ }.toFun (a • x) =
      ‖a‖ * { toMulRingSeminorm := toMulRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ }.toFun x
toMulRingSeminorm✝ : MulRingSeminorm S
eq_zero_of_map_eq_zero'✝ : ∀ (x : S), toMulRingSeminorm✝.toFun x = 0 → x = 0
smul'✝ :
  ∀ (a : R) (x : S),
    { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }.toFun (a • x) =
      ‖a‖ * { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }.toFun x
h :
  { toMulRingSeminorm := toMulRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹,
        smul' := smul'✝¹ }.toMulRingSeminorm =
    { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝,
        smul' := smul'✝ }.toMulRingSeminorm
⊢ { toMulRingSeminorm := toMulRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹, smul' := smul'✝¹ } =
    { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝, smul' := smul'✝ }

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : SeminormedCommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
f : AlgebraNorm R S
toMulRingSeminorm✝¹ : MulRingSeminorm S
eq_zero_of_map_eq_zero'✝¹ : ∀ (x : S), toMulRingSeminorm✝¹.toFun x = 0 → x = 0
smul'✝¹ :
  ∀ (a : R) (x : S),
    { toMulRingSeminorm := toMulRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ }.toFun (a • x) =
      ‖a‖ * { toMulRingSeminorm := toMulRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ }.toFun x
toMulRingSeminorm✝ : MulRingSeminorm S
eq_zero_of_map_eq_zero'✝ : ∀ (x : S), toMulRingSeminorm✝.toFun x = 0 → x = 0
smul'✝ :
  ∀ (a : R) (x : S),
    { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }.toFun (a • x) =
      ‖a‖ * { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }.toFun x
h :
  { toMulRingSeminorm := toMulRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹,
        smul' := smul'✝¹ }.toMulRingSeminorm =
    { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝,
        smul' := smul'✝ }.toMulRingSeminorm
⊢ { toMulRingSeminorm := toMulRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹, smul' := smul'✝¹ } =
    { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝, smul' := smul'✝ }
Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : SeminormedCommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
f : MulAlgebraNorm R S
a : R
⊢ f (a • 1) = ‖a‖

Tactic:
← mul_one ‖a‖,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : SeminormedCommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
f : MulAlgebraNorm R S
a : R
⊢ f (a • 1) = ‖a‖ * 1
Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : SeminormedCommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
f : MulAlgebraNorm R S
a : R
⊢ f (a • 1) = ‖a‖

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : SeminormedCommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
f : MulAlgebraNorm R S
a : R
⊢ f (a • 1) = ‖a‖
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: R✝ : Type u_1
inst✝⁵ : NonAssocRing R✝
inst✝⁴ : DecidableEq R✝
inst✝³ : NoZeroDivisors R✝
inst✝² : Nontrivial R✝
R : Type u_2
inst✝¹ : Ring R
inst✝ : Nontrivial R
v : AbsoluteValue R ℝ
x : R
⊢ ((fun N ↦ { toFun := N.toFun, map_mul' := ⋯, nonneg' := ⋯, eq_zero' := ⋯, add_le' := ⋯ })
        ((fun v ↦
            { toFun := v.toFun, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, map_one' := ⋯, map_mul' := ⋯,
              eq_zero_of_map_eq_zero' := ⋯ })
          v))
      x =
    v x

Tactic:
;

Goal state after:
R✝ : Type u_1
inst✝⁵ : NonAssocRing R✝
inst✝⁴ : DecidableEq R✝
inst✝³ : NoZeroDivisors R✝
inst✝² : Nontrivial R✝
R : Type u_2
inst✝¹ : Ring R
inst✝ : Nontrivial R
v : AbsoluteValue R ℝ
x : R
⊢ ((fun N ↦ { toFun := N.toFun, map_mul' := ⋯, nonneg' := ⋯, eq_zero' := ⋯, add_le' := ⋯ })
        ((fun v ↦
            { toFun := v.toFun, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, map_one' := ⋯, map_mul' := ⋯,
              eq_zero_of_map_eq_zero' := ⋯ })
          v))
      x =
    v x
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: R✝ : Type u_1
R : Type u_2
inst✝ : NormedRing R
x : R
hx : ‖x‖ = 0
⊢ ‖x‖ = 0

Tactic:
;

Goal state after:
R✝ : Type u_1
R : Type u_2
inst✝ : NormedRing R
x : R
hx : ‖x‖ = 0
⊢ ‖x‖ = 0
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: R✝ : Type u_1
R : Type u_2
inst✝ : NormedField R
x : R
hx : ‖x‖ = 0
⊢ ‖x‖ = 0

Tactic:
;

Goal state after:
R✝ : Type u_1
R : Type u_2
inst✝ : NormedField R
x : R
hx : ‖x‖ = 0
⊢ ‖x‖ = 0
Module: Mathlib.Topology.Algebra.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
F : Filter ι
inst✝³ : F.NeBot
inst✝² : Add R
inst✝¹ : ContinuousAdd R
inst✝ : AddLeftMono R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) F f
cobdd : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) F f
x✝¹ x✝ : R
h : x✝¹ ≤ x✝
⊢ c + x✝¹ ≤ c + x✝

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_4
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
F : Filter ι
inst✝³ : F.NeBot
inst✝² : Add R
inst✝¹ : ContinuousAdd R
inst✝ : AddLeftMono R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) F f
cobdd : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) F f
x✝¹ x✝ : R
h : x✝¹ ≤ x✝
⊢ c + x✝¹ ≤ c + x✝