awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 : (μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) < HPow.hPow (β := ℝ) (L + ε / 2) (↑(↑m1 : ℕ) : ℝ)
m2 : ℕ
hm2 :
  ∀ n ≥ m2,
    (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
        1 ≤
      ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1 : ℕ) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)
hxn' : LT.lt (α := ℝ) (0 : ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ)
h :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
hL0' : 0 < L + ε / 2
hm10 : Ne (α := ℝ) (↑(↑m1 : ℕ) : ℝ) 0
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) <
    HPow.hPow (β := ℝ) (L + ε / 2) 1 * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
have this : HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ) = 1
Tactic: have : (n : ℝ) / n = (1 : ℝ) := div_self (cast_ne_zero.mpr (_root_.ne_of_gt hn0))
-- 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 : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 : (μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) < HPow.hPow (β := ℝ) (L + ε / 2) (↑(↑m1 : ℕ) : ℝ)
m2 : ℕ
hm2 :
  ∀ n ≥ m2,
    (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
        1 ≤
      ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1 : ℕ) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)
hxn' : LT.lt (α := ℝ) (0 : ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ)
h :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
hL0' : 0 < L + ε / 2
hm10 : Ne (α := ℝ) (↑(↑m1 : ℕ) : ℝ) 0
this : HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ) = 1
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) <
    HPow.hPow (β := ℝ) (L + ε / 2) 1 * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
have nth_rw : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) <
  (L + ε / 2) ^ HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ) *
    (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
Tactic: nth_rw 2 [← this]
-- 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 : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 : (μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) < HPow.hPow (β := ℝ) (L + ε / 2) (↑(↑m1 : ℕ) : ℝ)
m2 : ℕ
hm2 :
  ∀ n ≥ m2,
    (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
        1 ≤
      ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1 : ℕ) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)
hxn' : LT.lt (α := ℝ) (0 : ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ)
h :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
hL0' : 0 < L + ε / 2
hm10 : Ne (α := ℝ) (↑(↑m1 : ℕ) : ℝ) 0
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) <
    (L + ε / 2) ^ HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ) *
      (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
have nth_rw : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) <
  (L + ε / 2) ^ HDiv.hDiv (α := ℝ) (↑((↑m1 : ℕ) * (n / (↑m1 : ℕ)) + n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ) *
    (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
Tactic: nth_rw 3 [← div_add_mod n m1]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 : (μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) < HPow.hPow (β := ℝ) (L + ε / 2) (↑(↑m1 : ℕ) : ℝ)
m2 : ℕ
hm2 :
  ∀ n ≥ m2,
    (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
        1 ≤
      ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1 : ℕ) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)
hxn' : LT.lt (α := ℝ) (0 : ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ)
h :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
hL0' : 0 < L + ε / 2
hm10 : Ne (α := ℝ) (↑(↑m1 : ℕ) : ℝ) 0
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) <
    (L + ε / 2) ^ HDiv.hDiv (α := ℝ) (↑((↑m1 : ℕ) * (n / (↑m1 : ℕ)) + n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ) *
      (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
have h_lt : 0 < HDiv.hDiv (α := ℝ) (↑(n / (↑m1 : ℕ)) : ℝ) (↑n : ℝ)
Tactic: have h_lt : 0 < ((n / m1 : ℕ) : ℝ) / (n : ℝ) :=
        div_pos (cast_pos.mpr (Nat.div_pos (le_trans (le_max_left _ _) hn) (PNat.pos m1)))
          (cast_pos.mpr hn0)
-- 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 : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 : (μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) < HPow.hPow (β := ℝ) (L + ε / 2) (↑(↑m1 : ℕ) : ℝ)
m2 : ℕ
hm2 :
  ∀ n ≥ m2,
    (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
        1 ≤
      ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1 : ℕ) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)
hxn' : LT.lt (α := ℝ) (0 : ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ)
h :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
hL0' : 0 < L + ε / 2
hm10 : Ne (α := ℝ) (↑(↑m1 : ℕ) : ℝ) 0
h_lt : 0 < HDiv.hDiv (α := ℝ) (↑(n / (↑m1 : ℕ)) : ℝ) (↑n : ℝ)
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) <
    (L + ε / 2) ^ HDiv.hDiv (α := ℝ) (↑((↑m1 : ℕ) * (n / (↑m1 : ℕ)) + n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ) *
      (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
have rw : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) (↑(n / (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) <
  HPow.hPow (β := ℝ) (L + ε / 2) (↑(↑m1 : ℕ) : ℝ) ^ HDiv.hDiv (α := ℝ) (↑(n / (↑m1 : ℕ)) : ℝ) (↑n : ℝ)
Tactic: rw [← rpow_natCast, ← rpow_add hL0', ← neg_div, ← add_div, Nat.cast_add,
        add_neg_cancel_right, Nat.cast_mul, ← rpow_mul (apply_nonneg μ _), mul_one_div,
        mul_div_assoc, rpow_mul (le_of_lt hL0')]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
    (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
      ε / 2
m2 : ℕ
hm2 :
  ∀ n ≥ m2,
    (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
        1 ≤
      ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1 : ℕ) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)
hxn' : LT.lt (α := ℝ) (0 : ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ)
h :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
hL0' : 0 < L + ε / 2
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)) + n % (↑m1 : ℕ))) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) <
    L + ε
have h1 : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) <
  (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
Tactic: have h1 : (μ (x ^ (m1 : ℕ)) ^ (n / (m1 : ℕ))) ^ (1 / (n : ℝ)) <
        (L + ε / 2) * (L + ε / 2) ^ (-(((n % m1 : ℕ) : ℝ) / (n : ℝ))) := by
      have hm10 : (m1 : ℝ) ≠ 0 := cast_ne_zero.mpr (_root_.ne_of_gt (PNat.pos m1))
      rw [← rpow_lt_rpow_iff (rpow_nonneg (apply_nonneg μ _) _) (le_of_lt hL0')
        (cast_pos.mpr (PNat.pos m1)), ← rpow_mul (apply_nonneg μ _), one_div_mul_cancel hm10,
        rpow_one] at hm1
      nth_rw 1 [← rpow_one (L + ε / 2)]
      have : (n : ℝ) / n = (1 : ℝ) := div_self (cast_ne_zero.mpr (_root_.ne_of_gt hn0))
      nth_rw 2 [← this]; clear this
      nth_rw 3 [← div_add_mod n m1]
      have h_lt : 0 < ((n / m1 : ℕ) : ℝ) / (n : ℝ) :=
        div_pos (cast_pos.mpr (Nat.div_pos (le_trans (le_max_left _ _) hn) (PNat.pos m1)))
          (cast_pos.mpr hn0)
      rw [← rpow_natCast, ← rpow_add hL0', ← neg_div, ← add_div, Nat.cast_add,
        add_neg_cancel_right, Nat.cast_mul, ← rpow_mul (apply_nonneg μ _), mul_one_div,
        mul_div_assoc, rpow_mul (le_of_lt hL0')]
      exact rpow_lt_rpow (apply_nonneg μ _) hm1 h_lt
-- 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 : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
    (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
      ε / 2
m2 : ℕ
hm2 :
  ∀ n ≥ m2,
    (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
        1 ≤
      ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1 : ℕ) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)
hxn' : LT.lt (α := ℝ) (0 : ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ)
h :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
hL0' : 0 < L + ε / 2
h1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) <
    (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
have pos : ∀ (hnm1 : n % (↑m1 : ℕ) = 0),
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
Tactic: by_cases hnm1 : n % m1 = 0
-- 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 : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
    (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
      ε / 2
m2 : ℕ
hm2 :
  ∀ n ≥ m2,
    (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
        1 ≤
      ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1 : ℕ) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)
hxn' : LT.lt (α := ℝ) (0 : ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ)
h :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
hL0' : 0 < L + ε / 2
h1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) <
    (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
pos :
  ∀ (hnm1 : n % (↑m1 : ℕ) = 0),
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
have neg : ∀ (hnm1 : ¬n % (↑m1 : ℕ) = 0),
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
Tactic: by_cases hnm1 : n % m1 = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
    (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
      ε / 2
m2 : ℕ
hm2 :
  ∀ n ≥ m2,
    (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
        1 ≤
      ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1 : ℕ) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)
hxn' : LT.lt (α := ℝ) (0 : ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ)
h :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
hL0' : 0 < L + ε / 2
h1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) <
    (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)) + n % (↑m1 : ℕ))) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) <
    L + ε
have h2 : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
Tactic: have h2 : μ (x ^ (n % m1)) ^ (1 / (n : ℝ)) ≤ (μ x ^ (n % m1)) ^ (1 / (n : ℝ)) := by
      by_cases hnm1 : n % m1 = 0
      · simpa [hnm1, pow_zero] using rpow_le_rpow (apply_nonneg μ _) hμ1 (one_div_cast_nonneg _)
      · exact rpow_le_rpow (apply_nonneg μ _) (map_pow_le_pow μ _ hnm1) (one_div_cast_nonneg _)
-- 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 : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
    (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
      ε / 2
m2 : ℕ
hm2 :
  ∀ n ≥ m2,
    (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
        1 ≤
      ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1 : ℕ) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)
hxn' : LT.lt (α := ℝ) (0 : ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ)
h :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
hL0' : 0 < L + ε / 2
h1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) <
    (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
h2 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
⊢ L + ε = L + ε / 2 + ε / 2
have rw : L + ε = L + (ε / 2 + ε / 2)
Tactic: rw [add_assoc, add_halves]
-- 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 : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
    (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
      ε / 2
m2 : ℕ
hm2 :
  ∀ n ≥ m2,
    (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
        1 ≤
      ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1 : ℕ) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)
hxn' : LT.lt (α := ℝ) (0 : ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ)
h :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
hL0' : 0 < L + ε / 2
h1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) <
    (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
h2 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
rw : L + ε = L + (ε / 2 + ε / 2)
⊢ L + ε = L + ε / 2 + ε / 2
have rw₁ : L + ε = L + ε
Tactic: rw [add_assoc, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
hx : Ne (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
L : ℝ := ⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑m1 : ℕ) : ℝ)) <
    (⨅ (n : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))) +
      ε / 2
m2 : ℕ
hm2 :
  ∀ n ≥ m2,
    (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) -
        1 ≤
      ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1 : ℕ) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (0 : ℝ)
hxn' : LT.lt (α := ℝ) (0 : ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ)
h :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ((↑m1 : ℕ) * (n / (↑m1 : ℕ)))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
hL0' : 0 < L + ε / 2
h1 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (↑m1 : ℕ)) : ℝ) (n / (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) <
    (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ))
h2 :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ (n % (↑m1 : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
⊢ (L + ε / 2) * (L + ε / 2) ^ (-HDiv.hDiv (α := ℝ) (↑(n % (↑m1 : ℕ)) : ℝ) (↑n : ℝ)) *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (n % (↑m1 : ℕ)) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤
    L + ε
have heq : L + ε = L + ε / 2 + ε / 2
Tactic: have heq : L + ε = L + ε / 2 + ε / 2 := by rw [add_assoc, add_halves]