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 : ∀ (n : ℕ) (_hn : 1 ≤ n), (μ : (a : R) → ℝ) (x ^ n) = HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → smoothingSeminormSeq μ x b = (μ : (a : R) → ℝ) x
have h : ∀ (b : ℕ), 1 ≤ b → smoothingSeminormSeq μ x b = (μ : (a : R) → ℝ) x
Tactic: use 1
-- 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 : ∀ (n : ℕ) (_hn : 1 ≤ n), (μ : (a : R) → ℝ) (x ^ n) = HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n
n : ℕ
hn : 1 ≤ n
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
have hn0 : Ne (α := ℝ) (↑n : ℝ) 0
Tactic: have hn0 : (n : ℝ) ≠ 0 := cast_ne_zero.mpr (one_le_iff_ne_zero.mp hn)
-- 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 : ∀ (n : ℕ) (_hn : 1 ≤ n), (μ : (a : R) → ℝ) (x ^ n) = HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n
n : ℕ
hn : 1 ≤ n
hn0 : Ne (α := ℝ) (↑n : ℝ) 0
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
have h : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = (μ : (a : R) → ℝ) x
Tactic: rw [hx n hn, ← rpow_natCast, ← rpow_mul (apply_nonneg μ _), mul_one_div_cancel hn0, rpow_one]
-- 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 : ∀ (n : ℕ) (_hn : 1 ≤ n), (μ : (a : R) → ℝ) (x ^ n) = HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n
n : ℕ
hn : 1 ≤ n
hn0 : Ne (α := ℝ) (↑n : ℝ) 0
h : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = (μ : (a : R) → ℝ) x
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
have h₁ : HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (↑n : ℝ) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = (μ : (a : R) → ℝ) x
Tactic: rw [hx n hn, ← rpow_natCast, ← rpow_mul (apply_nonneg μ _), mul_one_div_cancel hn0, rpow_one]
-- 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 : ∀ (n : ℕ) (_hn : 1 ≤ n), (μ : (a : R) → ℝ) (x ^ n) = HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n
n : ℕ
hn : 1 ≤ n
hn0 : Ne (α := ℝ) (↑n : ℝ) 0
h : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = (μ : (a : R) → ℝ) x
h₁ :
  HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (↑n : ℝ) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = (μ : (a : R) → ℝ) x
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
have h₂ : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑n : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
Tactic: rw [hx n hn, ← rpow_natCast, ← rpow_mul (apply_nonneg μ _), mul_one_div_cancel hn0, rpow_one]
-- 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 : ∀ (n : ℕ) (_hn : 1 ≤ n), (μ : (a : R) → ℝ) (x ^ n) = HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n
n : ℕ
hn : 1 ≤ n
hn0 : Ne (α := ℝ) (↑n : ℝ) 0
h : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = (μ : (a : R) → ℝ) x
h₁ :
  HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (↑n : ℝ) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = (μ : (a : R) → ℝ) x
h₂ : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑n : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
have h₃ : HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 1 = (μ : (a : R) → ℝ) x
Tactic: rw [hx n hn, ← rpow_natCast, ← rpow_mul (apply_nonneg μ _), mul_one_div_cancel hn0, rpow_one]
-- 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 : ∀ (n : ℕ) (_hn : 1 ≤ n), (μ : (a : R) → ℝ) (x ^ n) = HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n
n : ℕ
hn : 1 ≤ n
hn0 : Ne (α := ℝ) (↑n : ℝ) 0
h : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = (μ : (a : R) → ℝ) x
h₁ :
  HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (↑n : ℝ) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = (μ : (a : R) → ℝ) x
h₂ : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((↑n : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
h₃ : HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) 1 = (μ : (a : R) → ℝ) x
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
have h₄ : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) x : ℝ)
Tactic: rw [hx n hn, ← rpow_natCast, ← rpow_mul (apply_nonneg μ _), mul_one_div_cancel hn0, rpow_one]
-- 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 : ℝ)
⊢ smoothingFun μ x = (μ : (a : R) → ℝ) x
have apply : smoothingSeminormSeq μ x =ᶠ[atTop] fun (x_1 : ℕ) ↦ (μ : (a : R) → ℝ) x
Tactic: apply tendsto_nhds_unique_of_eventuallyEq (tendsto_smoothingFun_of_map_one_le_one μ hμ1 x)
    tendsto_const_nhds
-- 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 : ℝ)
⊢ smoothingSeminormSeq μ x =ᶠ[atTop] fun (x_1 : ℕ) ↦ (μ : (a : R) → ℝ) x
have simp : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → smoothingSeminormSeq μ x b = (μ : (a : R) → ℝ) x
Tactic: simp only [EventuallyEq, eventually_atTop, ge_iff_le]
-- 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 : ℝ)
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → smoothingSeminormSeq μ x b = (μ : (a : R) → ℝ) x
have h : ∀ (b : ℕ), 1 ≤ b → smoothingSeminormSeq μ x b = (μ : (a : R) → ℝ) x
Tactic: use 1
-- 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 : ℝ)
n : ℕ
hn : 1 ≤ n
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
have pos : ∀ (hx0 : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)),
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
Tactic: by_cases hx0 : μ x = 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 :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
n : ℕ
hn : 1 ≤ n
pos :
  ∀ (hx0 : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)),
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
have neg : ∀ (hx0 : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)),
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
Tactic: by_cases hx0 : μ x = 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 :
  ∀ (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 : ℝ)
have apply : LE.le (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (0 : ℝ)
Tactic: apply le_antisymm _ (apply_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 :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
n : ℕ
hn : 1 ≤ n
hx0 : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
⊢ LE.le (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (0 : ℝ)
have apply : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n ≤ 0
Tactic: apply le_trans (map_pow_le_pow μ x (one_le_iff_ne_zero.mp hn))
-- 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 : ℝ)
n : ℕ
hn : 1 ≤ n
hx0 : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n ≤ 0
have rw : HPow.hPow (α := ℝ) 0 n ≤ 0
Tactic: rw [hx0, zero_pow (pos_iff_ne_zero.mp hn)]
-- 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 : ℝ)
n : ℕ
hn : 1 ≤ n
hx0 : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
rw : HPow.hPow (α := ℝ) 0 n ≤ 0
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n ≤ 0
have rw₁ : LE.le (α := ℝ) 0 0
Tactic: rw [hx0, zero_pow (pos_iff_ne_zero.mp hn)]
-- 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 :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
n : ℕ
hn : 1 ≤ n
hx0 : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
have hxn : 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)]
-- 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 : ℝ)
n : ℕ
hn : 1 ≤ n
hx0 : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
hxn : Eq (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (0 : ℝ)
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
have pos : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = 0
Tactic: rw [hx0, hxn, zero_rpow (one_div_cast_ne_zero (one_le_iff_ne_zero.mp hn))]
-- 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 : ℝ)
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
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
have pos₁ : HPow.hPow (α := ℝ) 0 (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = 0
Tactic: rw [hx0, hxn, zero_rpow (one_div_cast_ne_zero (one_le_iff_ne_zero.mp hn))]
-- 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 : ℝ)
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
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
have pos₂ : Eq (α := ℝ) 0 0
Tactic: rw [hx0, hxn, zero_rpow (one_div_cast_ne_zero (one_le_iff_ne_zero.mp hn))]
-- 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 : ℝ)
n : ℕ
hn : 1 ≤ n
hx0 : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
have rw : HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) =
  HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
Tactic: rw [← mul_right_inj' hx0, ← hx 1, mul_one, mul_one]
-- 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 : ℝ)
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 : ℝ)
⊢ Eq (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
have rw₁ : (μ : (a : R) → ℝ) (x * 1) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
Tactic: rw [← mul_right_inj' hx0, ← hx 1, mul_one, mul_one]
-- 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 : ℝ)
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 : ℝ)
⊢ Eq (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
have rw₂ : (μ : (a : R) → ℝ) x = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (1 : ℝ)
Tactic: rw [← mul_right_inj' hx0, ← hx 1, mul_one, mul_one]
-- 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 : ℝ)
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 : ℝ)
⊢ Eq (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
have rw₃ : Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) x : ℝ)
Tactic: rw [← mul_right_inj' hx0, ← hx 1, mul_one, mul_one]
-- 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 :
  ∀ (y : R), (μ : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) ((μ : (a : R) → ℝ) y : ℝ)
n : ℕ
hn : 1 ≤ n
hx0 : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
have h1 : Eq (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
Tactic: have h1 : μ 1 = 1 := by rw [← mul_right_inj' hx0, ← hx 1, mul_one, mul_one]
-- 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 :
  ∀ (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 : ℝ)
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
have hn0 : 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))
-- 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 : ℝ)
n : ℕ
hn : 1 ≤ n
hx0 : ¬Eq (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (0 : ℝ)
h1 : Eq (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hn0 : Ne (α := ℝ) (↑n : ℝ) 0
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
have neg : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n * 1) : ℝ) (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]
-- 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 : ℝ)
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
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
have neg₁ : HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) x : ℝ) n) ((μ : (a : R) → ℝ) 1 : ℝ) ^
    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]
-- 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 : ℝ)
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
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
have neg₂ : HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (↑n : ℝ)) ((μ : (a : R) → ℝ) 1 : ℝ) ^
    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]
-- 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 : ℝ)
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
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = (μ : (a : R) → ℝ) x
have neg₃ : (HPow.hPow (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) x : ℝ) (↑n : ℝ) * 1) ^ 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]