mathlib-initiative/mathlib-tactics huggingface dataset:
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₂‖

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:
<;>

Goal state after:
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₂‖

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₁‖
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: case a
z w : ℂ
⊢ (↑(z + w)).re = (↑z + ↑w).re

pp: case a
z w : ℂ
⊢ (↑(z + w)).imI = (↑z + ↑w).imI

pp: case a
z w : ℂ
⊢ (↑(z + w)).imJ = (↑z + ↑w).imJ

pp: case a
z w : ℂ
⊢ (↑(z + w)).imK = (↑z + ↑w).imK

Tactic:
<;>

Goal state after:
case a
z w : ℂ
⊢ (↑(z + w)).re = (↑z + ↑w).re

case a
z w : ℂ
⊢ (↑(z + w)).imI = (↑z + ↑w).imI

case a
z w : ℂ
⊢ (↑(z + w)).imJ = (↑z + ↑w).imJ

case a
z w : ℂ
⊢ (↑(z + w)).imK = (↑z + ↑w).imK
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: case a
z w : ℂ
⊢ (↑(z * w)).re = (↑z * ↑w).re

pp: case a
z w : ℂ
⊢ (↑(z * w)).imI = (↑z * ↑w).imI

pp: case a
z w : ℂ
⊢ (↑(z * w)).imJ = (↑z * ↑w).imJ

pp: case a
z w : ℂ
⊢ (↑(z * w)).imK = (↑z * ↑w).imK

Tactic:
<;>

Goal state after:
case a
z w : ℂ
⊢ (↑(z * w)).re = (↑z * ↑w).re

case a
z w : ℂ
⊢ (↑(z * w)).imI = (↑z * ↑w).imI

case a
z w : ℂ
⊢ (↑(z * w)).imJ = (↑z * ↑w).imJ

case a
z w : ℂ
⊢ (↑(z * w)).imK = (↑z * ↑w).imK
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: case a
r : ℝ
z : ℂ
⊢ (r • ↑z).re = (↑r * ↑z).re

pp: case a
r : ℝ
z : ℂ
⊢ (r • ↑z).imI = (↑r * ↑z).imI

pp: case a
r : ℝ
z : ℂ
⊢ (r • ↑z).imJ = (↑r * ↑z).imJ

pp: case a
r : ℝ
z : ℂ
⊢ (r • ↑z).imK = (↑r * ↑z).imK

Tactic:
<;>

Goal state after:
case a
r : ℝ
z : ℂ
⊢ (r • ↑z).re = (↑r * ↑z).re

case a
r : ℝ
z : ℂ
⊢ (r • ↑z).imI = (↑r * ↑z).imI

case a
r : ℝ
z : ℂ
⊢ (r • ↑z).imJ = (↑r * ↑z).imJ

case a
r : ℝ
z : ℂ
⊢ (r • ↑z).imK = (↑r * ↑z).imK
Module: Mathlib.Analysis.Normed.Ring.Ultra

Goal state before:
pp: case ofNat
R : Type u_1
inst✝² : SeminormedRing R
inst✝¹ : NormOneClass R
inst✝ : IsUltrametricDist R
a✝ : ℕ
⊢ ‖↑(Int.ofNat a✝)‖₊ ≤ 1

pp: case negSucc
R : Type u_1
inst✝² : SeminormedRing R
inst✝¹ : NormOneClass R
inst✝ : IsUltrametricDist R
a✝ : ℕ
⊢ ‖↑(Int.negSucc a✝)‖₊ ≤ 1

Tactic:
<;>

Goal state after:
case ofNat
R : Type u_1
inst✝² : SeminormedRing R
inst✝¹ : NormOneClass R
inst✝ : IsUltrametricDist R
a✝ : ℕ
⊢ ‖↑(Int.ofNat a✝)‖₊ ≤ 1

case negSucc
R : Type u_1
inst✝² : SeminormedRing R
inst✝¹ : NormOneClass R
inst✝ : IsUltrametricDist R
a✝ : ℕ
⊢ ‖↑(Int.negSucc a✝)‖₊ ≤ 1
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: case inl
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
⊢ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k ≤ ∑ _x ∈ Finset.range (m + 1), max 1 (‖x‖ ^ m)

pp: case inr
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
⊢ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k ≤ ∑ _x ∈ Finset.range (m + 1), max 1 (‖x‖ ^ m)

Tactic:
<;>

Goal state after:
case inl
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
⊢ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k ≤ ∑ _x ∈ Finset.range (m + 1), max 1 (‖x‖ ^ m)

case inr
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
⊢ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k ≤ ∑ _x ∈ Finset.range (m + 1), max 1 (‖x‖ ^ m)
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: case inl
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
⊢ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k ≤ ∑ _x ∈ Finset.range (m + 1), 1

pp: case inr
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
⊢ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k ≤ ∑ _x ∈ Finset.range (m + 1), ‖x‖ ^ m

Tactic:
<;>

Goal state after:
case inl
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
⊢ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k ≤ ∑ _x ∈ Finset.range (m + 1), 1

case inr
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
⊢ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k ≤ ∑ _x ∈ Finset.range (m + 1), ‖x‖ ^ m
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: case e'_3.e'_5
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
H : φ x z ≠ 0
M : ℝ := ‖φ x z‖
r : ℝ
⊢ 2 * x * (algebraMap ℝ F) r = (2 * r, r ^ 2).1 • x

pp: case e'_3.e'_6
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
H : φ x z ≠ 0
M : ℝ := ‖φ x z‖
r : ℝ
⊢ (algebraMap ℝ F) r ^ 2 = (algebraMap ℝ F) (2 * r, r ^ 2).2

Tactic:
<;>

Goal state after:
case e'_3.e'_5
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
H : φ x z ≠ 0
M : ℝ := ‖φ x z‖
r : ℝ
⊢ 2 * x * (algebraMap ℝ F) r = (2 * r, r ^ 2).1 • x

case e'_3.e'_6
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
H : φ x z ≠ 0
M : ℝ := ‖φ x z‖
r : ℝ
⊢ (algebraMap ℝ F) r ^ 2 = (algebraMap ℝ F) (2 * r, r ^ 2).2
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case pos.refine_1
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
x y : R
h : x * y = 0
⊢ 0 ≤ AddGroupSeminorm.toFun 1 x

pp: case pos.refine_2
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
x y : R
h : x * y = 0
⊢ 0 ≤ AddGroupSeminorm.toFun 1 y

Tactic:
<;>

Goal state after:
case pos.refine_1
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
x y : R
h : x * y = 0
⊢ 0 ≤ AddGroupSeminorm.toFun 1 x

case pos.refine_2
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
x y : R
h : x * y = 0
⊢ 0 ≤ AddGroupSeminorm.toFun 1 y
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
⊢ (Multiset.map (fun x ↦ a - x) g.roots).prod = eval a g

Tactic:
hg.eval_eq_prod_roots_of_monic hgm

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
⊢ (Multiset.map (fun x ↦ a - x) g.roots).prod = (Multiset.map (fun x ↦ a - x) g.roots).prod
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : f x = 0
⊢ 0 / 0 ≤ 1

Tactic:
div_zero

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : f x = 0
⊢ 0 ≤ 1
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
hna : IsNonarchimedean f
x y z : R
hz : f z = 0
⊢ f ((x + y) * z) / f z ≤ f (x * z) / f z ∨ f ((x + y) * z) / f z ≤ f (y * z) / f z

Tactic:
simp only [hz, div_zero, le_refl, or_self_iff]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
hy : f y = 0
⊢ f (x * y) / 0 ≤ f x

Tactic:
div_zero

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
hy : f y = 0
⊢ 0 ≤ f x
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
h_bdd : BddAbove (Set.range fun y ↦ f (x * y) / f y)
h0 : f x = 0
⊢ f x = f x / f 1

Tactic:
h0,

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
h_bdd : BddAbove (Set.range fun y ↦ f (x * y) / f y)
h0 : f x = 0
⊢ 0 = 0 / f 1
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: case f
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
hna : IsNonarchimedean ⇑f
x y : R
n : ℕ
hmax : f ((x + y) * c ^ n) ≤ f (x * c ^ n) ∨ f ((x + y) * c ^ n) ≤ f (y * c ^ n)
⊢ f ((x + y) * c ^ n) ≤ f (x * c ^ n) → f ((x + y) * c ^ n) / f c ^ n ≤ f (x * c ^ n) / f c ^ n

pp: case g
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
hna : IsNonarchimedean ⇑f
x y : R
n : ℕ
hmax : f ((x + y) * c ^ n) ≤ f (x * c ^ n) ∨ f ((x + y) * c ^ n) ≤ f (y * c ^ n)
⊢ f ((x + y) * c ^ n) ≤ f (y * c ^ n) → f ((x + y) * c ^ n) / f c ^ n ≤ f (y * c ^ n) / f c ^ n

Tactic:
<;>

Goal state after:
case f
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
hna : IsNonarchimedean ⇑f
x y : R
n : ℕ
hmax : f ((x + y) * c ^ n) ≤ f (x * c ^ n) ∨ f ((x + y) * c ^ n) ≤ f (y * c ^ n)
⊢ f ((x + y) * c ^ n) ≤ f (x * c ^ n) → f ((x + y) * c ^ n) / f c ^ n ≤ f (x * c ^ n) / f c ^ n

case g
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
hna : IsNonarchimedean ⇑f
x y : R
n : ℕ
hmax : f ((x + y) * c ^ n) ≤ f (x * c ^ n) ∨ f ((x + y) * c ^ n) ≤ f (y * c ^ n)
⊢ f ((x + y) * c ^ n) ≤ f (y * c ^ n) → f ((x + y) * c ^ n) / f c ^ n ≤ f (y * c ^ n) / f c ^ n
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: case f
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
hna : IsNonarchimedean ⇑f
x y : R
n : ℕ
hmax : f ((x + y) * c ^ n) ≤ f (x * c ^ n) ∨ f ((x + y) * c ^ n) ≤ f (y * c ^ n)
a✝ : f ((x + y) * c ^ n) ≤ f (x * c ^ n)
⊢ f ((x + y) * c ^ n) / f c ^ n ≤ f (x * c ^ n) / f c ^ n

pp: case g
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
hna : IsNonarchimedean ⇑f
x y : R
n : ℕ
hmax : f ((x + y) * c ^ n) ≤ f (x * c ^ n) ∨ f ((x + y) * c ^ n) ≤ f (y * c ^ n)
a✝ : f ((x + y) * c ^ n) ≤ f (y * c ^ n)
⊢ f ((x + y) * c ^ n) / f c ^ n ≤ f (y * c ^ n) / f c ^ n

Tactic:
<;>

Goal state after:
case f
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
hna : IsNonarchimedean ⇑f
x y : R
n : ℕ
hmax : f ((x + y) * c ^ n) ≤ f (x * c ^ n) ∨ f ((x + y) * c ^ n) ≤ f (y * c ^ n)
a✝ : f ((x + y) * c ^ n) ≤ f (x * c ^ n)
⊢ f ((x + y) * c ^ n) / f c ^ n ≤ f (x * c ^ n) / f c ^ n

case g
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
hna : IsNonarchimedean ⇑f
x y : R
n : ℕ
hmax : f ((x + y) * c ^ n) ≤ f (x * c ^ n) ∨ f ((x + y) * c ^ n) ≤ f (y * c ^ n)
a✝ : f ((x + y) * c ^ n) ≤ f (y * c ^ n)
⊢ f ((x + y) * c ^ n) / f c ^ n ≤ f (y * c ^ n) / f c ^ n
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:
rw [add_assoc, add_halves]

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
  refine ⟨fun h ↦ ?_, fun h ↦ h ▸ spectralValue_X_pow p.natDegree⟩
  refine hp.eq_X_pow_iff_natDegree_le_natTrailingDegree.mpr <|
    le_natTrailingDegree hp.ne_zero fun n hn ↦ ?_
  have h0 : spectralValueTerms p n = 0 := by
    apply le_antisymm ((le_ciSup (spectralValueTerms_bddAbove p) n).trans h.le)
    exact spectralValueTerms_nonneg _ _
  rw [spectralValueTerms_of_lt_natDegree _ hn,
    Real.rpow_eq_zero_iff_of_nonneg (norm_nonneg _)] at h0
  exact norm_eq_zero.mp h0.1

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : ∀ (n : ℕ), ‖P.coeff n‖ ≤ 1
n : ℕ
hn : n < P.natDegree
⊢ ‖P.coeff n‖ ^ (1 / (↑P.natDegree - ↑n)) ≤ 1

Tactic:
apply Real.rpow_le_one (norm_nonneg _) (h n)

Goal state after:
case pos
R : Type u_1
inst✝ : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : ∀ (n : ℕ), ‖P.coeff n‖ ≤ 1
n : ℕ
hn : n < P.natDegree
⊢ 0 ≤ 1 / (↑P.natDegree - ↑n)
Module: Mathlib.Analysis.Normed.Field.Dense

Goal state before:
pp: case pos
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 ⋯ ⋯
fa0 : (aeval a) f = 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ else 1
a' : F
conj : IsConjRoot L a a'
ne : a ≠ a'
hS : S.Nonempty
⊢ δ ≤ ‖a - a'‖

pp: case neg
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 ⋯ ⋯
fa0 : (aeval a) f = 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ else 1
a' : F
conj : IsConjRoot L a a'
ne : a ≠ a'
hS : ¬S.Nonempty
⊢ δ ≤ ‖a - a'‖

Tactic:
<;>

Goal state after:
case pos
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 ⋯ ⋯
fa0 : (aeval a) f = 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ else 1
a' : F
conj : IsConjRoot L a a'
ne : a ≠ a'
hS : S.Nonempty
⊢ δ ≤ ‖a - a'‖

case neg
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 ⋯ ⋯
fa0 : (aeval a) f = 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ else 1
a' : F
conj : IsConjRoot L a a'
ne : a ≠ a'
hS : ¬S.Nonempty
⊢ δ ≤ ‖a - a'‖
Module: Mathlib.Analysis.Normed.Field.Dense

Goal state before:
pp: case pos
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 ⋯ ⋯
fa0 : (aeval a) f = 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ else 1
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
hS : S.Nonempty
⊢ δ > 0

pp: case neg
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 ⋯ ⋯
fa0 : (aeval a) f = 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ else 1
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
hS : ¬S.Nonempty
⊢ δ > 0

Tactic:
<;>

Goal state after:
case pos
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 ⋯ ⋯
fa0 : (aeval a) f = 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ else 1
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
hS : S.Nonempty
⊢ δ > 0

case neg
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 ⋯ ⋯
fa0 : (aeval a) f = 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ else 1
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
hS : ¬S.Nonempty
⊢ δ > 0
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
n : ℕ
hn0 : n = 0
⊢ ↑(mu μ hn 0) / 0 ≤ 1

Tactic:
div_zero

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
n : ℕ
hn0 : n = 0
⊢ 0 ≤ 1
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
inst✝ : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf1 : f 1 = 1
p : K[X]
s : Multiset L
hp : (mapAlg K L) p = (Multiset.map (fun a ↦ X - C a) s).prod
h_le : 0 ≤ ⨆ x, if x ∈ s then f x else 0
m : ℕ
hm : m < p.natDegree
h✝ : 0 < ↑p.natDegree - ↑m
hps : s.card = p.natDegree
hc : ‖p.coeff m‖ = f (((mapAlg K L) p).coeff m)
h : f ((-1) ^ (s.card - m) * s.esymm (s.card - m)) = f (s.esymm (s.card - m))
t : Multiset L
ht_card : t.card = s.card - m
hts : ∀ x ∈ t, x ∈ s
ht_ge : f (Multiset.map prod (powersetCard (s.card - m) s)).sum ≤ f t.prod
h_pr : f t.prod ≤ (Multiset.map (⇑f) t).prod
hs_ne : s ≠ 0
y : L
hyx : y ∈ s
hy_max : ∀ z ∈ s, f z ≤ f y
this : (Multiset.map (⇑f) t).prod ≤ f y ^ (p.natDegree - m)
h_bdd : BddAbove (Set.range fun x ↦ if x ∈ s then f x else 0)
⊢ f y ≤ if y ∈ s then f y else 0

Tactic:
by rw [if_pos hyx]

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

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : ∀ (x : M), ‖x‖ = 0
x : M
⊢ normedMk x = 0 x

Tactic:
simpa [← norm_eq_zero] using h x

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
n✝ : R
n : ℕ+
hpos : (-1) ^ ↑n = 1
⊢ μ ((-1) ^ ↑n * n✝ ^ ↑n) ^ (1 / ↑↑n) = μ (n✝ ^ ↑n) ^ (1 / ↑↑n)

pp: case inr
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
n✝ : R
n : ℕ+
hneg : (-1) ^ ↑n = -1
⊢ μ ((-1) ^ ↑n * n✝ ^ ↑n) ^ (1 / ↑↑n) = μ (n✝ ^ ↑n) ^ (1 / ↑↑n)

Tactic:
· rw [hpos, one_mul]

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
n✝ : R
n : ℕ+
hneg : (-1) ^ ↑n = -1
⊢ μ ((-1) ^ ↑n * n✝ ^ ↑n) ^ (1 / ↑↑n) = μ (n✝ ^ ↑n) ^ (1 / ↑↑n)