awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (goal)
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
hn0 : Ne (α := ℝ) (↑n : ℝ) 0
h :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n * y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) =
    HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ)
      (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))
h₁ :
  HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) ^
      HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ)
      (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))
h₂ :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) =
    HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ)
      (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))
h₃ :
  HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (↑n : ℝ) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) =
    HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ)
      (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))
h₄ :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑n : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) =
    HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ)
      (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))
h₅ :
  HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 1 *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) =
    HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ)
      (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x * y) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) =
    HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ)
      (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))
have h₆ : HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ)
    (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))) =
  HMul.hMul (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ)
    (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))
Tactic: rw [mul_pow, pow_mul_apply_eq_pow_mul μ hx, mul_rpow (pow_nonneg (apply_nonneg μ _) _)
    (apply_nonneg μ _), ← rpow_natCast, ← rpow_mul (apply_nonneg μ _), mul_one_div_cancel hn0,
    rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : SeminormedRing R
p : R[X]
n : ℕ
⊢ 0 ≤ if n < p.natDegree then ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ)) else 0
have pos : ∀ (h : n < p.natDegree), 0 ≤ ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
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 : ℝ))
⊢ 0 ≤ if n < p.natDegree then ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ)) else 0
have neg : ∀ (h : ¬n < p.natDegree), LE.le (α := ℝ) 0 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
r : 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‖
have 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‖
Tactic: simp only [natDegree_X_sub_C, lt_one_iff, coeff_sub, cast_one, one_div]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
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 : ℕ),
      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‖
have 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)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
r : R
this : (⨆ (n : ℕ), if n = 0 then ‖r‖ else 0) = ‖r‖
⊢ 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)
have 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
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
r : R
this : (⨆ (n : ℕ), if n = 0 then ‖r‖ else 0) = ‖r‖
⊢ 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
have 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
Tactic: ext n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
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 : ℕ
⊢ (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
have 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
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
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
⊢ (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
have 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
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
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
⊢ (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
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
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
⊢ (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
have pos₁ : ‖HSub.hSub (α := R) (coeff X n) (coeff ((C : (a : R) → R[X]) r) n)‖ ^ (HSub.hSub (α := ℝ) 1 (↑n : ℝ))⁻¹ = ‖r‖
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
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‖
⊢ (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
have pos₂ : ‖HSub.hSub (α := R) (coeff X 0) (coeff ((C : (a : R) → R[X]) r) 0)‖ ^ (HSub.hSub (α := ℝ) 1 (↑0 : ℝ))⁻¹ = ‖r‖
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
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‖
⊢ (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
have pos₃ : ‖HSub.hSub (α := R) (coeff X 0) (coeff ((C : (a : R) → R[X]) r) 0)‖ ^ (HSub.hSub (α := ℝ) 1 0)⁻¹ = ‖r‖
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
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‖
⊢ (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
have pos₄ : HPow.hPow (β := ℝ) ‖HSub.hSub (α := R) (coeff X 0) (coeff ((C : (a : R) → R[X]) r) 0)‖ 1⁻¹ = ‖r‖
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
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‖
⊢ (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
have pos₅ : HPow.hPow (β := ℝ) ‖HSub.hSub (α := R) 0 (coeff ((C : (a : R) → R[X]) r) 0)‖ 1⁻¹ = ‖r‖
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
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‖
⊢ (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
have pos₆ : HPow.hPow (β := ℝ) ‖0 - r‖ 1⁻¹ = ‖r‖
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
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‖
⊢ (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
have pos₇ : HPow.hPow (β := ℝ) ‖-r‖ 1⁻¹ = ‖r‖
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
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‖
⊢ (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
have pos₈ : HPow.hPow (β := ℝ) ‖r‖ 1⁻¹ = ‖r‖
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
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‖
⊢ (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
have pos₉ : HPow.hPow (β := ℝ) ‖r‖ 1 = ‖r‖
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
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‖
⊢ (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
have pos₁₀ : ‖r‖ = ‖r‖
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
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
⊢ (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
have neg : 0 = if n = 0 then ‖r‖ else 0
Tactic: rw [if_neg hn, if_neg hn]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
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
⊢ (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
have neg₁ : Eq (α := ℝ) 0 0
Tactic: rw [if_neg hn, if_neg hn]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
r : 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‖
have suffices : (⨆ (n : ℕ), if n = 0 then ‖r‖ 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
r : R
⊢ (⨆ (n : ℕ), if n = 0 then ‖r‖ else 0) = ‖r‖
have apply : ∀ (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]⟩)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
r : R
n : ℕ
⊢ (if n = 0 then ‖r‖ else 0) ≤ ‖r‖
have pos : n = 0 → ‖r‖ ≤ ‖r‖
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
r : R
n : ℕ
pos : n = 0 → ‖r‖ ≤ ‖r‖
⊢ (if n = 0 then ‖r‖ else 0) ≤ ‖r‖
have neg : ¬n = 0 → 0 ≤ ‖r‖
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
n : ℕ
⊢ Eq (α := ℝ)
    (⨆ (n_1 : ℕ),
      if n_1 < (HPow.hPow (α := R[X]) X n).natDegree then
        ‖(HPow.hPow (α := R[X]) X n).coeff n_1‖ ^
          (1 / HSub.hSub (α := ℝ) (↑(HPow.hPow (α := R[X]) X n).natDegree : ℝ) (↑n_1 : ℝ))
      else 0)
    0
have simp_rw : Eq (α := ℝ)
  (⨆ (n_1 : ℕ),
    if n_1 < n then Norm.norm.{u_1} (E := R) (if n_1 = n then 1 else 0) ^ (1 / HSub.hSub (α := ℝ) (↑n : ℝ) (↑n_1 : ℝ))
    else 0)
  0
Tactic: simp_rw [coeff_X_pow n, natDegree_X_pow]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
n : ℕ
⊢ Eq (α := ℝ)
    (⨆ (n_1 : ℕ),
      if n_1 < n then Norm.norm.{u_1} (E := R) (if n_1 = n then 1 else 0) ^ (1 / HSub.hSub (α := ℝ) (↑n : ℝ) (↑n_1 : ℝ))
      else 0)
    0
have h : Eq (α := ℕ → ℝ)
  (fun (n_1 : ℕ) ↦
    if n_1 < n then Norm.norm.{u_1} (E := R) (if n_1 = n then 1 else 0) ^ (1 / HSub.hSub (α := ℝ) (↑n : ℝ) (↑n_1 : ℝ))
    else 0)
  fun (x : ℕ) ↦ 0
Tactic: convert! ciSup_const using 2