awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
hx :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
n : ℕ
hn : 1 ≤ n
hx0 : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
apply : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n ≤ 0
⊢ LE.le (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (0 : ℝ)

Tactic:
apply le_trans (map_pow_le_pow μ x (one_le_iff_ne_zero.mp hn))

Premises used: map_pow_le_pow, Iff.mp, Nat.one_le_iff_ne_zero, le_trans
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
hx :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
n : ℕ
hn : 1 ≤ n
hx0 : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
rw : HPow.hPow (α := ℝ) 0 n ≤ 0
rw₁ rw₂ : LE.le (α := ℝ) 0 0
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n ≤ 0

Tactic:
rw [hx0, zero_pow (pos_iff_ne_zero.mp hn)]

Premises used: Iff.mp, pos_iff_ne_zero, zero_pow
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
hx :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
n : ℕ
hn : 1 ≤ n
hx0 : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (0 : ℝ)

Tactic:
have hxn : μ (x ^ n) = 0 := by
      apply le_antisymm _ (apply_nonneg μ _)
      apply le_trans (map_pow_le_pow μ x (one_le_iff_ne_zero.mp hn))
      rw [hx0, zero_pow (pos_iff_ne_zero.mp hn)]
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
hx :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
n : ℕ
hn : 1 ≤ n
hx0 : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
hxn : Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (0 : ℝ)
pos : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = 0
pos₁ : HPow.hPow (α := ℝ) 0 (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = 0
pos₂ pos₃ : Eq (α := ℝ) 0 0
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x

Tactic:
rw [hx0, hxn, zero_rpow (one_div_cast_ne_zero (one_le_iff_ne_zero.mp hn))]

Premises used: Nat.one_div_cast_ne_zero, Real.zero_rpow, Iff.mp, Nat.one_le_iff_ne_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
hx :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
n : ℕ
hn : 1 ≤ n
hx0 : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
rw :
  HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) =
    HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
rw₁ : (μ : (a : R) → ℝ) (x * 1) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
rw₂ : (μ : (a : R) → ℝ) x = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
rw₃ rw₄ : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)

Tactic:
rw [← mul_right_inj' hx0, ← hx 1, mul_one, mul_one]

Premises used: mul_right_inj', mul_one, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
hx :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
n : ℕ
hn : 1 ≤ n
hx0 : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)

Tactic:
have h1 : μ 1 = 1 := by rw [← mul_right_inj' hx0, ← hx 1, mul_one, mul_one]
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
hx :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
n : ℕ
hn : 1 ≤ n
hx0 : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
h1 : Eq (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
have hn0 : (n : ℝ) ≠ 0 := cast_ne_zero.mpr (_root_.ne_of_gt (lt_of_lt_of_le zero_lt_one hn))
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
hx :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
n : ℕ
hn : 1 ≤ n
hx0 : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
h1 : Eq (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hn0 : Ne (α := ℝ) (↑n : ℝ) 0
neg : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n * 1) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
neg₁ :
  HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n) ((μ : (a : R) → ℝ) 1 : ℝ) ^
      HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (μ : (a : R) → ℝ) x
neg₂ :
  HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (↑n : ℝ)) ((μ : (a : R) → ℝ) 1 : ℝ) ^
      HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (μ : (a : R) → ℝ) x
neg₃ :
  (HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (↑n : ℝ) * 1) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (μ : (a : R) → ℝ) x
neg₄ :
  HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (↑n : ℝ) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = (μ : (a : R) → ℝ) x
neg₅ : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑n : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
neg₆ : HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 1 = (μ : (a : R) → ℝ) x
neg₇ neg₈ : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) x : ℝ)
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x

Tactic:
rw [← mul_one (x ^ n), pow_mul_apply_eq_pow_mul μ hx, ← rpow_natCast, h1, mul_one,
      ← rpow_mul (apply_nonneg μ _), mul_one_div_cancel hn0, rpow_one]

Premises used: pow_mul_apply_eq_pow_mul, Real.rpow_one, mul_one_div_cancel, HPow.hPow, mul_one, NonnegHomClass.apply_nonneg, Real.rpow_mul, DFunLike.coe, Real.rpow_natCast
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
x : R
hx :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
⊢ Eq (α := ℝ) ((smoothingSeminorm μ hμ1 hna : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) x : ℝ)

Tactic:
smoothingFun_apply_of_map_mul_eq_mul μ hμ1 hx

Premises used: iInf, smoothingFun_apply_of_map_mul_eq_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
hx :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
y : R
rw :
  Tendsto (fun (n : ℕ) ↦ HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingSeminormSeq μ y n)) atTop
    (𝓝 (HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingFun μ y)))
⊢ Tendsto (fun (n : ℕ) ↦ HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingSeminormSeq μ y n)) atTop
    (𝓝 (smoothingFun μ x * smoothingFun μ y))

Tactic:
rw [smoothingFun_apply_of_map_mul_eq_mul μ hμ1 hx]

Premises used: smoothingFun_apply_of_map_mul_eq_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
hx :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
y : R
⊢ Tendsto (fun (n : ℕ) ↦ HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingSeminormSeq μ y n)) atTop
    (𝓝 (HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingFun μ y)))

Tactic:
Tendsto.const_mul _ (tendsto_smoothingFun_of_map_one_le_one μ hμ1 y)

Premises used: Filter.Tendsto.const_mul, tendsto_smoothingFun_of_map_one_le_one
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
hx :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
y : R
⊢ Tendsto (fun (n : ℕ) ↦ HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingSeminormSeq μ y n)) atTop
    (𝓝 (HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingFun μ y)))

Tactic:
exact Tendsto.const_mul _ (tendsto_smoothingFun_of_map_one_le_one μ hμ1 y)

Premises used: Filter.Tendsto.const_mul, tendsto_smoothingFun_of_map_one_le_one
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
hx :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
y : R
⊢ Tendsto (fun (n : ℕ) ↦ HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingSeminormSeq μ y n)) atTop
    (𝓝 (smoothingFun μ x * smoothingFun μ y))

Tactic:
have hlim : Tendsto (fun n => μ x * smoothingSeminormSeq μ y n) atTop
      (𝓝 (smoothingFun μ x * smoothingFun μ y)) := by
    rw [smoothingFun_apply_of_map_mul_eq_mul μ hμ1 hx]
    exact Tendsto.const_mul _ (tendsto_smoothingFun_of_map_one_le_one μ hμ1 y)
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
hx :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
y : R
hlim :
  Tendsto (fun (n : ℕ) ↦ HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingSeminormSeq μ y n)) atTop
    (𝓝 (smoothingFun μ x * smoothingFun μ y))
apply :
  smoothingSeminormSeq μ (x * y) =ᶠ[atTop] fun (n : ℕ) ↦
    HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingSeminormSeq μ y n)
⊢ smoothingFun μ (x * y) = smoothingFun μ x * smoothingFun μ y

Tactic:
apply tendsto_nhds_unique_of_eventuallyEq (tendsto_smoothingFun_of_map_one_le_one μ hμ1 (x * y))
    hlim

Premises used: HMul.hMul, tendsto_nhds_unique_of_eventuallyEq, tendsto_smoothingFun_of_map_one_le_one
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
hx :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
y : R
hlim :
  Tendsto (fun (n : ℕ) ↦ HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingSeminormSeq μ y n)) atTop
    (𝓝 (smoothingFun μ x * smoothingFun μ y))
simp :
  ∃ (a : ℕ),
    ∀ (b : ℕ),
      a ≤ b →
        smoothingSeminormSeq μ (x * y) b = HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingSeminormSeq μ y b)
⊢ smoothingSeminormSeq μ (x * y) =ᶠ[atTop] fun (n : ℕ) ↦
    HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingSeminormSeq μ y n)

Tactic:
simp only [EventuallyEq, eventually_atTop, ge_iff_le]

Premises used: ge_iff_le, Filter.EventuallyEq, Filter.eventually_atTop
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
hx :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
y : R
hlim :
  Tendsto (fun (n : ℕ) ↦ HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingSeminormSeq μ y n)) atTop
    (𝓝 (smoothingFun μ x * smoothingFun μ y))
h :
  ∀ (b : ℕ),
    1 ≤ b → smoothingSeminormSeq μ (x * y) b = HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingSeminormSeq μ y b)
⊢ ∃ (a : ℕ),
    ∀ (b : ℕ),
      a ≤ b →
        smoothingSeminormSeq μ (x * y) b = HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingSeminormSeq μ y b)

Tactic:
use 1
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
hx :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
y : R
hlim :
  Tendsto (fun (n : ℕ) ↦ HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (smoothingSeminormSeq μ y n)) atTop
    (𝓝 (smoothingFun μ x * smoothingFun μ y))
n : ℕ
hn1 : 1 ≤ n
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
have hn0 : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (_root_.ne_of_gt (lt_of_lt_of_le zero_lt_one hn1))
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
x : R
hx :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
y : R
⊢ (smoothingSeminorm μ hμ1 hna : (a : R) → ℝ) (x * y) =
    HMul.hMul (α := ℝ) (β := ℝ) ((smoothingSeminorm μ hμ1 hna : (a : R) → ℝ) x : ℝ)
      ((smoothingSeminorm μ hμ1 hna : (a : R) → ℝ) y : ℝ)

Tactic:
smoothingFun_of_map_mul_eq_mul μ hμ1 hx y

Premises used: iInf, smoothingFun_of_map_mul_eq_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
p : R[X]
n : ℕ
hn : n < p.natDegree
⊢ spectralValueTerms p n = ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))

Tactic:
simp [spectralValueTerms, if_pos hn]

Premises used: spectralValueTerms, if_pos
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ spectralValueTerms p n = 0

Tactic:
simp only [spectralValueTerms, if_neg (not_lt.mpr hn)]

Premises used: Iff.mpr, spectralValueTerms, not_lt, if_neg
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
p : R[X]
⊢ Set.range (spectralValueTerms p) ⊆
    {0} ∪ (fun (n : ℕ) ↦ ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) '' Set.Iio p.natDegree

Tactic:
aesop (add simp [Set.range_subset_iff, spectralValueTerms])

Premises used: spectralValueTerms, Set.range_subset_iff
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
p : R[X]
⊢ BddAbove (Set.range (spectralValueTerms p))

Tactic:
(spectralValueTerms_finite_range p).bddAbove

Premises used: spectralValueTerms_finite_range, Set.Finite.bddAbove
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
p : R[X]
n : ℕ
pos : ∀ (h : n < p.natDegree), 0 ≤ ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))
neg : ∀ (h : ¬n < p.natDegree), LE.le (α := ℝ) 0 0
⊢ 0 ≤ if n < p.natDegree then ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ)) else 0

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
p : R[X]
n : ℕ
h : n < p.natDegree
⊢ 0 ≤ ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
p : R[X]
n : ℕ
h : ¬n < p.natDegree
⊢ LE.le (α := ℝ) 0 0

Tactic:
le_refl _

Premises used: le_refl
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
p : R[X]
n : ℕ
h : ¬n < p.natDegree
⊢ LE.le (α := ℝ) 0 0

Tactic:
exact le_refl _

Premises used: le_refl
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
p : R[X]
⊢ 0 ≤ spectralValue p

Tactic:
iSup_nonneg (spectralValueTerms_nonneg p)

Premises used: spectralValueTerms_nonneg, spectralValue, Real.iSup_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
r : R
simp :
  (⨆ (n : ℕ),
      if n = 0 then
        ‖HSub.hSub (α := R) (coeff X n) (coeff ((C : (a : R) → R[X]) r) n)‖ ^ (HSub.hSub (α := ℝ) 1 (↑n : ℝ))⁻¹
      else 0) =
    ‖r‖
⊢ (⨆ (n : ℕ),
      if n < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).natDegree then
        ‖(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).coeff n‖ ^
          (1 /
            HSub.hSub (α := ℝ) (↑(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).natDegree : ℝ)
              (↑n : ℝ))
      else 0) =
    ‖r‖

Tactic:
simp only [natDegree_X_sub_C, lt_one_iff, coeff_sub, cast_one, one_div]

Premises used: Polynomial.natDegree_X_sub_C, Polynomial.coeff_sub, Nat.lt_one_iff, one_div, Nat.cast_one
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
r : R
this : (⨆ (n : ℕ), if n = 0 then ‖r‖ else 0) = ‖r‖
rw :
  Eq (α := ℝ)
    (⨆ (n : ℕ),
      if n = 0 then
        ‖HSub.hSub (α := R) (coeff X n) (coeff ((C : (a : R) → R[X]) r) n)‖ ^ (HSub.hSub (α := ℝ) 1 (↑n : ℝ))⁻¹
      else 0)
    (⨆ (n : ℕ), if n = 0 then ‖r‖ else 0)
⊢ (⨆ (n : ℕ),
      if n = 0 then
        ‖HSub.hSub (α := R) (coeff X n) (coeff ((C : (a : R) → R[X]) r) n)‖ ^ (HSub.hSub (α := ℝ) 1 (↑n : ℝ))⁻¹
      else 0) =
    ‖r‖

Tactic:
rw [← this]
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
r : R
this : (⨆ (n : ℕ), if n = 0 then ‖r‖ else 0) = ‖r‖
h :
  Eq (α := (n : ℕ) → ℝ)
    (fun (n : ℕ) ↦
      if n = 0 then
        ‖HSub.hSub (α := R) (coeff X n) (coeff ((C : (a : R) → R[X]) r) n)‖ ^ (HSub.hSub (α := ℝ) 1 (↑n : ℝ))⁻¹
      else 0)
    fun (n : ℕ) ↦ if n = 0 then ‖r‖ else 0
⊢ Eq (α := ℝ)
    (⨆ (n : ℕ),
      if n = 0 then
        ‖HSub.hSub (α := R) (coeff X n) (coeff ((C : (a : R) → R[X]) r) n)‖ ^ (HSub.hSub (α := ℝ) 1 (↑n : ℝ))⁻¹
      else 0)
    (⨆ (n : ℕ), if n = 0 then ‖r‖ else 0)

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
r : R
this : (⨆ (n : ℕ), if n = 0 then ‖r‖ else 0) = ‖r‖
h :
  ∀ (n : ℕ),
    (if n = 0 then
        ‖HSub.hSub (α := R) (coeff X n) (coeff ((C : (a : R) → R[X]) r) n)‖ ^ (HSub.hSub (α := ℝ) 1 (↑n : ℝ))⁻¹
      else 0) =
      if n = 0 then ‖r‖ else 0
⊢ Eq (α := (n : ℕ) → ℝ)
    (fun (n : ℕ) ↦
      if n = 0 then
        ‖HSub.hSub (α := R) (coeff X n) (coeff ((C : (a : R) → R[X]) r) n)‖ ^ (HSub.hSub (α := ℝ) 1 (↑n : ℝ))⁻¹
      else 0)
    fun (n : ℕ) ↦ if n = 0 then ‖r‖ else 0

Tactic:
ext n
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
r : R
this : (⨆ (n : ℕ), if n = 0 then ‖r‖ else 0) = ‖r‖
n : ℕ
pos :
  ∀ (hn : n = 0),
    (if n = 0 then
        ‖HSub.hSub (α := R) (coeff X n) (coeff ((C : (a : R) → R[X]) r) n)‖ ^ (HSub.hSub (α := ℝ) 1 (↑n : ℝ))⁻¹
      else 0) =
      if n = 0 then ‖r‖ else 0
neg :
  ∀ (hn : ¬n = 0),
    (if n = 0 then
        ‖HSub.hSub (α := R) (coeff X n) (coeff ((C : (a : R) → R[X]) r) n)‖ ^ (HSub.hSub (α := ℝ) 1 (↑n : ℝ))⁻¹
      else 0) =
      if n = 0 then ‖r‖ else 0
⊢ (if n = 0 then ‖HSub.hSub (α := R) (coeff X n) (coeff ((C : (a : R) → R[X]) r) n)‖ ^ (HSub.hSub (α := ℝ) 1 (↑n : ℝ))⁻¹
    else 0) =
    if n = 0 then ‖r‖ else 0

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
r : R
this : (⨆ (n : ℕ), if n = 0 then ‖r‖ else 0) = ‖r‖
n : ℕ
hn : n = 0
pos :
  ‖HSub.hSub (α := R) (coeff X n) (coeff ((C : (a : R) → R[X]) r) n)‖ ^ (HSub.hSub (α := ℝ) 1 (↑n : ℝ))⁻¹ =
    if n = 0 then ‖r‖ else 0
pos₁ : ‖HSub.hSub (α := R) (coeff X n) (coeff ((C : (a : R) → R[X]) r) n)‖ ^ (HSub.hSub (α := ℝ) 1 (↑n : ℝ))⁻¹ = ‖r‖
pos₂ : ‖HSub.hSub (α := R) (coeff X 0) (coeff ((C : (a : R) → R[X]) r) 0)‖ ^ (HSub.hSub (α := ℝ) 1 (↑0 : ℝ))⁻¹ = ‖r‖
pos₃ : ‖HSub.hSub (α := R) (coeff X 0) (coeff ((C : (a : R) → R[X]) r) 0)‖ ^ (HSub.hSub (α := ℝ) 1 0)⁻¹ = ‖r‖
pos₄ : HPow.hPow (β := ℝ) ‖HSub.hSub (α := R) (coeff X 0) (coeff ((C : (a : R) → R[X]) r) 0)‖ 1⁻¹ = ‖r‖
pos₅ : HPow.hPow (β := ℝ) ‖HSub.hSub (α := R) 0 (coeff ((C : (a : R) → R[X]) r) 0)‖ 1⁻¹ = ‖r‖
pos₆ : HPow.hPow (β := ℝ) ‖0 - r‖ 1⁻¹ = ‖r‖
pos₇ : HPow.hPow (β := ℝ) ‖-r‖ 1⁻¹ = ‖r‖
pos₈ : HPow.hPow (β := ℝ) ‖r‖ 1⁻¹ = ‖r‖
pos₉ : HPow.hPow (β := ℝ) ‖r‖ 1 = ‖r‖
pos₁₀ pos₁₁ : ‖r‖ = ‖r‖
⊢ (if n = 0 then ‖HSub.hSub (α := R) (coeff X n) (coeff ((C : (a : R) → R[X]) r) n)‖ ^ (HSub.hSub (α := ℝ) 1 (↑n : ℝ))⁻¹
    else 0) =
    if n = 0 then ‖r‖ else 0

Tactic:
rw [if_pos hn, if_pos hn, hn, cast_zero, sub_zero, coeff_X_zero, coeff_C_zero, zero_sub,
        norm_neg, inv_one, rpow_one]

Premises used: inv_one, sub_zero, Polynomial.coeff_X_zero, if_pos, Real.rpow_one, norm_neg, Nat.cast_zero, Polynomial.coeff_C_zero, zero_sub
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
r : R
this : (⨆ (n : ℕ), if n = 0 then ‖r‖ else 0) = ‖r‖
n : ℕ
hn : ¬n = 0
neg : 0 = if n = 0 then ‖r‖ else 0
neg₁ neg₂ : Eq (α := ℝ) 0 0
⊢ (if n = 0 then ‖HSub.hSub (α := R) (coeff X n) (coeff ((C : (a : R) → R[X]) r) n)‖ ^ (HSub.hSub (α := ℝ) 1 (↑n : ℝ))⁻¹
    else 0) =
    if n = 0 then ‖r‖ else 0

Tactic:
rw [if_neg hn, if_neg hn]

Premises used: if_neg
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
r : R
suffices : (⨆ (n : ℕ), if n = 0 then ‖r‖ else 0) = ‖r‖
⊢ (⨆ (n : ℕ),
      if n = 0 then
        ‖HSub.hSub (α := R) (coeff X n) (coeff ((C : (a : R) → R[X]) r) n)‖ ^ (HSub.hSub (α := ℝ) 1 (↑n : ℝ))⁻¹
      else 0) =
    ‖r‖

Tactic:
suffices (⨆ n : ℕ, ite (n = 0) ‖r‖ 0) = ‖r‖ by
    rw [← this]
    apply congr_arg
    ext n
    by_cases hn : n = 0
    · rw [if_pos hn, if_pos hn, hn, cast_zero, sub_zero, coeff_X_zero, coeff_C_zero, zero_sub,
        norm_neg, inv_one, rpow_one]
    · rw [if_neg hn, if_neg hn]
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
r : R
x : ℝ
hx : x < ‖r‖
⊢ x < if Eq (α := ℕ) 0 0 then ‖r‖ else 0

Tactic:
simp only [if_true, hx]

Premises used: if_true
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
r : R
apply : ∀ (n : ℕ), (if n = 0 then ‖r‖ else 0) ≤ ‖r‖
⊢ (⨆ (n : ℕ), if n = 0 then ‖r‖ else 0) = ‖r‖

Tactic:
apply ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun n ↦ ?_)
      (fun _ hx ↦ ⟨0, by simp only [if_true, hx]⟩)

Premises used: ciSup_eq_of_forall_le_of_forall_lt_exists_gt, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
r : R
n : ℕ
pos : n = 0 → ‖r‖ ≤ ‖r‖
neg : ¬n = 0 → 0 ≤ ‖r‖
⊢ (if n = 0 then ‖r‖ else 0) ≤ ‖r‖

Tactic:
split_ifs
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
r : R
n : ℕ
h : n = 0
⊢ ‖r‖ ≤ ‖r‖

Tactic:
le_refl _

Premises used: le_refl
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
r : R
n : ℕ
h : n = 0
⊢ ‖r‖ ≤ ‖r‖

Tactic:
exact le_refl _

Premises used: le_refl
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
r : R
n : ℕ
h : ¬n = 0
⊢ 0 ≤ ‖r‖

Tactic:
norm_nonneg _

Premises used: norm_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
r : R
n : ℕ
h : ¬n = 0
⊢ 0 ≤ ‖r‖

Tactic:
exact norm_nonneg _

Premises used: norm_nonneg