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

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

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝ : NonUnitalRing R
toRingSeminorm✝¹ : RingSeminorm R
eq_zero_of_map_eq_zero'✝¹ : ∀ (x : R), toRingSeminorm✝¹.toFun x = 0 → x = 0
toRingSeminorm✝ : RingSeminorm R
eq_zero_of_map_eq_zero'✝ : ∀ (x : R), toRingSeminorm✝.toFun x = 0 → x = 0
h :
  (fun f ↦ f.toFun) { toRingSeminorm := toRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    (fun f ↦ f.toFun) { toRingSeminorm := toRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
⊢ { toRingSeminorm := toRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    { toRingSeminorm := toRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }

Tactic:
congr

Goal state after:
case mk.mk
R : Type u_1
inst✝ : NonUnitalRing R
toRingSeminorm✝¹ : RingSeminorm R
eq_zero_of_map_eq_zero'✝¹ : ∀ (x : R), toRingSeminorm✝¹.toFun x = 0 → x = 0
toRingSeminorm✝ : RingSeminorm R
eq_zero_of_map_eq_zero'✝ : ∀ (x : R), toRingSeminorm✝.toFun x = 0 → x = 0
h :
  (fun f ↦ f.toFun) { toRingSeminorm := toRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    (fun f ↦ f.toFun) { toRingSeminorm := toRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
⊢ toRingSeminorm✝¹ = toRingSeminorm✝
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝ : NonAssocRing R
toAddGroupSeminorm✝¹ : AddGroupSeminorm R
map_one'✝¹ : toAddGroupSeminorm✝¹.toFun 1 = 1
map_mul'✝¹ :
  ∀ (x y : R), toAddGroupSeminorm✝¹.toFun (x * y) = toAddGroupSeminorm✝¹.toFun x * toAddGroupSeminorm✝¹.toFun y
toAddGroupSeminorm✝ : AddGroupSeminorm R
map_one'✝ : toAddGroupSeminorm✝.toFun 1 = 1
map_mul'✝ : ∀ (x y : R), toAddGroupSeminorm✝.toFun (x * y) = toAddGroupSeminorm✝.toFun x * toAddGroupSeminorm✝.toFun y
h :
  (fun f ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun f ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
⊢ { toAddGroupSeminorm := toAddGroupSeminorm✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    { toAddGroupSeminorm := toAddGroupSeminorm✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }

Tactic:
congr

Goal state after:
case mk.mk
R : Type u_1
inst✝ : NonAssocRing R
toAddGroupSeminorm✝¹ : AddGroupSeminorm R
map_one'✝¹ : toAddGroupSeminorm✝¹.toFun 1 = 1
map_mul'✝¹ :
  ∀ (x y : R), toAddGroupSeminorm✝¹.toFun (x * y) = toAddGroupSeminorm✝¹.toFun x * toAddGroupSeminorm✝¹.toFun y
toAddGroupSeminorm✝ : AddGroupSeminorm R
map_one'✝ : toAddGroupSeminorm✝.toFun 1 = 1
map_mul'✝ : ∀ (x y : R), toAddGroupSeminorm✝.toFun (x * y) = toAddGroupSeminorm✝.toFun x * toAddGroupSeminorm✝.toFun y
h :
  (fun f ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun f ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
⊢ toAddGroupSeminorm✝¹ = toAddGroupSeminorm✝
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝ : NonAssocRing R
toMulRingSeminorm✝¹ : MulRingSeminorm R
eq_zero_of_map_eq_zero'✝¹ : ∀ (x : R), toMulRingSeminorm✝¹.toFun x = 0 → x = 0
toMulRingSeminorm✝ : MulRingSeminorm R
eq_zero_of_map_eq_zero'✝ : ∀ (x : R), toMulRingSeminorm✝.toFun x = 0 → x = 0
h :
  (fun f ↦ f.toFun) { toMulRingSeminorm := toMulRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    (fun f ↦ f.toFun) { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
⊢ { toMulRingSeminorm := toMulRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }

Tactic:
congr

Goal state after:
case mk.mk
R : Type u_1
inst✝ : NonAssocRing R
toMulRingSeminorm✝¹ : MulRingSeminorm R
eq_zero_of_map_eq_zero'✝¹ : ∀ (x : R), toMulRingSeminorm✝¹.toFun x = 0 → x = 0
toMulRingSeminorm✝ : MulRingSeminorm R
eq_zero_of_map_eq_zero'✝ : ∀ (x : R), toMulRingSeminorm✝.toFun x = 0 → x = 0
h :
  (fun f ↦ f.toFun) { toMulRingSeminorm := toMulRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    (fun f ↦ f.toFun) { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
⊢ toMulRingSeminorm✝¹ = toMulRingSeminorm✝
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
f_mul : f x ≤ c * f x * f 1
hx : 0 < f x
⊢ 0 ≤ c

Tactic:
show c * f x * f 1 = c * f 1 * f x by ring,

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
f_mul : f x ≤ c * f 1 * f x
hx : 0 < f x
⊢ 0 ≤ c
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:
congr

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 = eval a g
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
⊢ ‖eval a (∑ i ∈ Finset.range (g.natDegree + 1), (monomial i) ((g - f).coeff i))‖ =
    ‖eval a (∑ i ∈ Finset.range (g.natDegree + 1), C (g.coeff i - f.coeff i) * X ^ i)‖

Tactic:
congr

Goal state after:
case e_p.e_f
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
⊢ (fun i ↦ (monomial i) ((g - f).coeff i)) = fun i ↦ C (g.coeff i - f.coeff i) * X ^ i
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_neg : ∀ (x : R), f (-x) = f x
x : R
⊢ ⨆ y, f (-x * y) / f y = ⨆ y, f (x * y) / f y

Tactic:
congr

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_neg : ∀ (x : R), f (-x) = f x
x : R
⊢ (fun y ↦ f (-x * y) / f y) = fun y ↦ f (x * y) / f y
Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension

Goal state before:
pp: case h.h
K : Type u_1
L : Type u_2
inst✝⁴ : NormedField K
inst✝³ : Ring L
inst✝² : Algebra K L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
B : Basis ι K L
i : ι
hBi : B i = 1
hna : IsNonarchimedean Norm.norm
c : ι × ι
left✝ : c ∈ univ
hc : (univ.sup' ⋯ fun i ↦ B.norm (B i.1 * B i.2)) = B.norm (B c.1 * B c.2)
x : L
⊢ ∀ (y : L), B.norm (x * y) ≤ B.norm (B c.1 * B c.2) * B.norm x * B.norm y

Tactic:
y

Goal state after:
case h.h
K : Type u_1
L : Type u_2
inst✝⁴ : NormedField K
inst✝³ : Ring L
inst✝² : Algebra K L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
B : Basis ι K L
i : ι
hBi : B i = 1
hna : IsNonarchimedean Norm.norm
c : ι × ι
left✝ : c ∈ univ
hc : (univ.sup' ⋯ fun i ↦ B.norm (B i.1 * B i.2)) = B.norm (B c.1 * B c.2)
x y : L
⊢ B.norm (x * y) ≤ B.norm (B c.1 * B c.2) * B.norm x * B.norm y
Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension

Goal state before:
pp: case h.h
K : Type u_1
L : Type u_2
inst✝⁴ : NormedField K
inst✝³ : Ring L
inst✝² : Algebra K L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
B : Basis ι K L
i : ι
hBi : B i = 1
hna : IsNonarchimedean Norm.norm
c : ι × ι
left✝¹ : c ∈ univ
hc : (univ.sup' ⋯ fun i ↦ B.norm (B i.1 * B i.2)) = B.norm (B c.1 * B c.2)
x y : L
ixy : ι
left✝ : ixy ∈ univ
hixy_def : (univ.sup' ⋯ fun i ↦ ‖(B.repr (x * y)) i‖) = ‖(B.repr (x * y)) ixy‖
hna' : IsNonarchimedean ⇑(NormedField.toMulRingNorm K)
k : ι
hk :
  ‖∑ x_1, (B.repr x) x_1 * ∑ x, (B.repr y) x * (B.repr (B x_1 * B x)) ixy‖ ≤
    ‖(B.repr x) k‖ * ‖∑ x, (B.repr y) x * (B.repr (B k * B x)) ixy‖
⊢ ‖(B.repr x) k‖ * ‖∑ x, (B.repr y) x * (B.repr (B k * B x)) ixy‖ ≤ B.norm (B c.1 * B c.2) * B.norm x * B.norm y

Tactic:
obtain ⟨k', hk'⟩ : ∃ (k' : ι),
        ‖∑ j : ι, B.repr y j • B.repr (B k * B j) ixy‖ ≤
          ‖B.repr y k' • B.repr (B k * B k') ixy‖ := by
      obtain ⟨k, hk0, hk⟩ := IsNonarchimedean.finset_image_add (map_zero _) (apply_nonneg _) hna'
        (fun i ↦ B.repr y i • B.repr (B k * B i) ixy) (univ : Finset ι)
      exact ⟨k, hk⟩

Goal state after:
case h.h
K : Type u_1
L : Type u_2
inst✝⁴ : NormedField K
inst✝³ : Ring L
inst✝² : Algebra K L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
B : Basis ι K L
i : ι
hBi : B i = 1
hna : IsNonarchimedean Norm.norm
c : ι × ι
left✝¹ : c ∈ univ
hc : (univ.sup' ⋯ fun i ↦ B.norm (B i.1 * B i.2)) = B.norm (B c.1 * B c.2)
x y : L
ixy : ι
left✝ : ixy ∈ univ
hixy_def : (univ.sup' ⋯ fun i ↦ ‖(B.repr (x * y)) i‖) = ‖(B.repr (x * y)) ixy‖
hna' : IsNonarchimedean ⇑(NormedField.toMulRingNorm K)
k : ι
hk :
  ‖∑ x_1, (B.repr x) x_1 * ∑ x, (B.repr y) x * (B.repr (B x_1 * B x)) ixy‖ ≤
    ‖(B.repr x) k‖ * ‖∑ x, (B.repr y) x * (B.repr (B k * B x)) ixy‖
k' : ι
hk' : ‖∑ j, (B.repr y) j • (B.repr (B k * B j)) ixy‖ ≤ ‖(B.repr y) k' • (B.repr (B k * B k')) ixy‖
⊢ ‖(B.repr x) k‖ * ‖∑ x, (B.repr y) x * (B.repr (B k * B x)) ixy‖ ≤ B.norm (B c.1 * B c.2) * B.norm x * B.norm y
Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension

Goal state before:
pp: K : Type u_1
inst✝² : NormedField K
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
σ : L ≃ₐ[K] L
x : L
⊢ ∀ (b : L), (algNormOfAlgEquiv σ) (x + b) ≤ max ((algNormOfAlgEquiv σ) x) ((algNormOfAlgEquiv σ) b)

Tactic:
y

Goal state after:
K : Type u_1
inst✝² : NormedField K
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
σ : L ≃ₐ[K] L
x y : L
⊢ (algNormOfAlgEquiv σ) (x + y) ≤ max ((algNormOfAlgEquiv σ) x) ((algNormOfAlgEquiv σ) y)
Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension

Goal state before:
pp: K : Type u_1
inst✝² : NormedField K
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
σ : L ≃ₐ[K] L
x : K
⊢ (algNormOfAlgEquiv σ) ((algebraMap K L) x) = ‖x‖

Tactic:
simp only [algNormOfAlgEquiv_apply, AlgEquiv.commutes]
  exact (Classical.choose_spec (exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional
    h_fin hu.isNonarchimedean_norm)).2.1 _

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

Goal state before:
pp: K : Type u_1
inst✝² : NormedField K
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
r : K
x : L
⊢ ⨆ σ, (algNormOfAlgEquiv σ) (r • x) = ‖r‖ * ⨆ σ, (algNormOfAlgEquiv σ) x

Tactic:
simp only [AlgebraNormClass.map_smul_eq_mul,
      Real.mul_iSup_of_nonneg (norm_nonneg _)]

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

Goal state before:
pp: case pos
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
⊢ smoothingSeminormSeq μ x n < L + ε

Tactic:
simp only [smoothingSeminormSeq]

Goal state after:
case pos
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
⊢ μ (x ^ n) ^ (1 / ↑n) < L + ε
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case neg
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))
⊢ smoothingSeminormSeq μ x n < L + ε

Tactic:
simp only [smoothingSeminormSeq]

Goal state after:
case neg
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))
⊢ μ (x ^ n) ^ (1 / ↑n) < L + ε
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
hm10 : ↑↑m1 ≠ 0
⊢ (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n) < (L + ε / 2) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n))

Tactic:
← rpow_lt_rpow_iff (rpow_nonneg (apply_nonneg μ _) _) (le_of_lt hL0')
        (cast_pos.mpr (PNat.pos m1)),

Goal state after:
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)) ^ ↑↑m1 < (L + ε / 2) ^ ↑↑m1
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
hm10 : ↑↑m1 ≠ 0
⊢ (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n) < (L + ε / 2) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n))
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))
hterm : seminormFromConst_seq c f (c * x) = fun n ↦ f c * seminormFromConst_seq c f x (n + 1)
⊢ Tendsto (seminormFromConst_seq c f (c * x)) atTop (𝓝 (f c * seminormFromConst' c f x))

Tactic:
simpa [hterm] using tendsto_const_nhds.mul hlim

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:
rwa [seminormFromConst_def hg1 hg_k, seminormFromConst_apply_c hg1 hg_k hg_pm]

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

Goal state before:
pp: case refine_2
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'
⊢ ‖iL x - iL y‖ < ‖iL x - xC'‖

Tactic:
have : xC' ∈ (minpoly K x).rootSet C := by
        rwa [isConjRoot_iff_mem_minpoly_rootSet (xsep.isIntegral.map _),
          minpoly.algHom_eq iL iL.injective x] at hx'

Goal state after:
case refine_2
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'
this : xC' ∈ (minpoly K x).rootSet C
⊢ ‖iL x - iL y‖ < ‖iL x - xC'‖
Module: Mathlib.Analysis.Normed.Field.ProperSpace

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

Tactic:
rcases exists_isCompact_closedBall (0 : 𝕜) with ⟨r, rpos, hr⟩

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
⊢ ProperSpace 𝕜
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✝ : 𝕜
⊢ x✝ ∈ closedBall 0 (‖c‖ ^ n * r) ↔ x✝ ∈ c ^ n • closedBall 0 r

Tactic:
simp only [mem_closedBall, dist_zero_right, Set.mem_smul_set_iff_inv_smul_mem₀ this,
      smul_eq_mul, norm_mul, norm_inv, norm_pow,
      inv_mul_le_iff₀ (by simpa only [norm_pow] using norm_pos_iff.mpr this)]

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

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
n : ℕ
hn : 1 ≤ n
⊢ smoothingSeminormSeq μ 1 n ≤ 1

Tactic:
simp only [smoothingSeminormSeq]

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
n : ℕ
hn : 1 ≤ n
⊢ μ (1 ^ n) ^ (1 / ↑n) ≤ 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
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
hn_lt : ∀ n < p.natDegree, ‖p.coeff n‖ < f x ^ (p.natDegree - n)
h_deg : 0 < p.natDegree
h_lt : f (∑ i ∈ Finset.range p.natDegree, p.coeff i • x ^ i) < f (x ^ p.natDegree)
⊢ f 0 = f (x ^ p.natDegree)

Tactic:
rw [← hx, aeval_eq_sum_range, Finset.sum_range_succ, add_comm, hp.coeff_natDegree,
          one_smul, ← max_eq_left_of_lt h_lt]

Goal state after:
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
hn_lt : ∀ n < p.natDegree, ‖p.coeff n‖ < f x ^ (p.natDegree - n)
h_deg : 0 < p.natDegree
h_lt : f (∑ i ∈ Finset.range p.natDegree, p.coeff i • x ^ i) < f (x ^ p.natDegree)
⊢ f (x ^ p.natDegree + ∑ x_1 ∈ Finset.range p.natDegree, p.coeff x_1 • x ^ x_1) =
    max (f (x ^ p.natDegree)) (f (∑ i ∈ Finset.range p.natDegree, p.coeff i • x ^ i))
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
ha : a = 0
b : ℝ
m : ℕ
hm : ∀ (b_1 : ℕ), m ≤ b_1 → μ x ^ (↑(s (ψ b_1)) * (1 / ↑(ψ b_1))) ≤ b
k : ℕ
hkm : m ≤ k
⊢ μ (x ^ s (ψ k)) ^ (1 / ↑(ψ k)) ≤ μ x ^ (↑(s (ψ k)) * (1 / ↑(ψ k)))

Tactic:
rpow_mul (apply_nonneg μ x),

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
ha : a = 0
b : ℝ
m : ℕ
hm : ∀ (b_1 : ℕ), m ≤ b_1 → μ x ^ (↑(s (ψ b_1)) * (1 / ↑(ψ b_1))) ≤ b
k : ℕ
hkm : m ≤ k
⊢ μ (x ^ s (ψ k)) ^ (1 / ↑(ψ k)) ≤ (μ x ^ ↑(s (ψ k))) ^ (1 / ↑(ψ k))