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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
x y : R
hn :
  ∀ (n : ℕ),
    ∃ m < n + 1,
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x + y) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
        HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) (x ^ m) : ℝ) ((μ : (a : R) → ℝ) (y ^ (n - m)) : ℝ) ^
          HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
mu : ℕ → ℕ := fun (n : ℕ) ↦ _root_.mu μ hn n
nu : ℕ → ℕ := fun (n : ℕ) ↦ n - mu n
hnu : nu = fun (n : ℕ) ↦ n - mu n
hmu_le : ∀ (n : ℕ), mu n ≤ n
hmu_bdd : ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (HDiv.hDiv (α := ℝ) (↑(mu n) : ℝ) (↑n : ℝ))
hs : Bornology.IsBounded (α := ℝ) (Set.Icc 0 1)
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(mu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
hb_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(nu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 b)
b_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) b
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a
hy :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ y ^ b
hxy :
  limsup
      (fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b
ε : ℝ
hε : ε > 0
⊢ smoothingFun μ (x + y) ≤ max (smoothingFun μ x) (smoothingFun μ y) + ε
have h_mul : smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε ≤ max (smoothingFun μ x) (smoothingFun μ y) + ε
Tactic: have h_mul : smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε ≤
      max (smoothingFun μ x) (smoothingFun μ y) + ε := by
    rw [max_def]
    split_ifs with h
    · rw [add_le_add_iff_right]
      apply le_trans (mul_le_mul_of_nonneg_right
        (rpow_le_rpow (smoothingFun_nonneg μ hμ1 _) h a_in.1)
        (rpow_nonneg (smoothingFun_nonneg μ hμ1 _) _))
      rw [hb, ← rpow_add_of_nonneg (smoothingFun_nonneg μ hμ1 _) a_in.1
        (sub_nonneg.mpr a_in.2), add_sub, add_sub_cancel_left, rpow_one]
    · rw [add_le_add_iff_right]
      apply le_trans (mul_le_mul_of_nonneg_left
        (rpow_le_rpow (smoothingFun_nonneg μ hμ1 _) (le_of_lt (not_le.mp h)) b_in.1)
        (rpow_nonneg (smoothingFun_nonneg μ hμ1 _) _))
      rw [hb, ← rpow_add_of_nonneg (smoothingFun_nonneg μ hμ1 _) a_in.1
        (sub_nonneg.mpr a_in.2), add_sub, add_sub_cancel_left, 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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
x y : R
hn :
  ∀ (n : ℕ),
    ∃ m < n + 1,
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x + y) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
        HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) (x ^ m) : ℝ) ((μ : (a : R) → ℝ) (y ^ (n - m)) : ℝ) ^
          HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
mu : ℕ → ℕ := fun (n : ℕ) ↦ _root_.mu μ hn n
nu : ℕ → ℕ := fun (n : ℕ) ↦ n - mu n
hnu : nu = fun (n : ℕ) ↦ n - mu n
hmu_le : ∀ (n : ℕ), mu n ≤ n
hmu_bdd : ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (HDiv.hDiv (α := ℝ) (↑(mu n) : ℝ) (↑n : ℝ))
hs : Bornology.IsBounded (α := ℝ) (Set.Icc 0 1)
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(mu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
hb_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(nu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 b)
b_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) b
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a
hy :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ y ^ b
hxy :
  limsup
      (fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b
ε : ℝ
hε : ε > 0
h_mul : smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε ≤ max (smoothingFun μ x) (smoothingFun μ y) + ε
⊢ smoothingFun μ (x + y) ≤ max (smoothingFun μ x) (smoothingFun μ y) + ε
have apply : smoothingFun μ (x + y) ≤ smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε
Tactic: apply le_trans _ h_mul
-- 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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
x y : R
hn :
  ∀ (n : ℕ),
    ∃ m < n + 1,
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x + y) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
        HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) (x ^ m) : ℝ) ((μ : (a : R) → ℝ) (y ^ (n - m)) : ℝ) ^
          HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
mu : ℕ → ℕ := fun (n : ℕ) ↦ _root_.mu μ hn n
nu : ℕ → ℕ := fun (n : ℕ) ↦ n - mu n
hnu : nu = fun (n : ℕ) ↦ n - mu n
hmu_le : ∀ (n : ℕ), mu n ≤ n
hmu_bdd : ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (HDiv.hDiv (α := ℝ) (↑(mu n) : ℝ) (↑n : ℝ))
hs : Bornology.IsBounded (α := ℝ) (Set.Icc 0 1)
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(mu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
hb_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(nu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 b)
b_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) b
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a
hy :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ y ^ b
hxy :
  limsup
      (fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b
ε : ℝ
hε : ε > 0
h_mul : smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε ≤ max (smoothingFun μ x) (smoothingFun μ y) + ε
⊢ smoothingFun μ (x + y) ≤ smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε
have hex : ∃ (n : ℕ+),
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ (↑n : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ (↑n : ℕ)) : ℝ)) *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ (↑n : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ (↑n : ℕ)) : ℝ)) <
    smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε
Tactic: have hex : ∃ n : PNat, μ (x ^ mu (ψ n)) ^ (1 / (ψ n : ℝ)) * μ (y ^ nu (ψ n)) ^ (1 / (ψ n : ℝ)) <
      smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε :=
    Filter.exists_lt_of_limsup_le (bddAbove_range_mul (μ_bddAbove μ hμ1 hmu_le _ _)
      (fun n ↦ by positivity) (μ_bddAbove μ hμ1 hnu_le _ _)
      (fun n ↦ by positivity)).isBoundedUnder_of_range hxy hε
-- 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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
x y : R
hn :
  ∀ (n : ℕ),
    ∃ m < n + 1,
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x + y) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
        HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) (x ^ m) : ℝ) ((μ : (a : R) → ℝ) (y ^ (n - m)) : ℝ) ^
          HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
mu : ℕ → ℕ := fun (n : ℕ) ↦ _root_.mu μ hn n
nu : ℕ → ℕ := fun (n : ℕ) ↦ n - mu n
hnu : nu = fun (n : ℕ) ↦ n - mu n
hmu_le : ∀ (n : ℕ), mu n ≤ n
hmu_bdd : ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (HDiv.hDiv (α := ℝ) (↑(mu n) : ℝ) (↑n : ℝ))
hs : Bornology.IsBounded (α := ℝ) (Set.Icc 0 1)
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(mu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
hb_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(nu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 b)
b_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) b
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a
hy :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ y ^ b
hxy :
  limsup
      (fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b
ε : ℝ
hε : ε > 0
h_mul : smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε ≤ max (smoothingFun μ x) (smoothingFun μ y) + ε
hex :
  ∃ (n : ℕ+),
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ (↑n : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ (↑n : ℕ)) : ℝ)) *
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ (↑n : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ (↑n : ℕ)) : ℝ)) <
      smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε
⊢ smoothingFun μ (x + y) ≤ smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε
have obtain : ∀ (N : ℕ+)
  (hN :
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ (↑N : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ (↑N : ℕ)) : ℝ)) *
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ (↑N : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ (↑N : ℕ)) : ℝ)) <
      smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε),
  smoothingFun μ (x + y) ≤ smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε
Tactic: obtain ⟨N, hN⟩ := hex
Cleared hypotheses: hex
-- 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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
x y : R
hn :
  ∀ (n : ℕ),
    ∃ m < n + 1,
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x + y) ^ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤
        HMul.hMul (α := ℝ) (β := ℝ) ((μ : (a : R) → ℝ) (x ^ m) : ℝ) ((μ : (a : R) → ℝ) (y ^ (n - m)) : ℝ) ^
          HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
mu : ℕ → ℕ := fun (n : ℕ) ↦ _root_.mu μ hn n
nu : ℕ → ℕ := fun (n : ℕ) ↦ n - mu n
hnu : nu = fun (n : ℕ) ↦ n - mu n
hmu_le : ∀ (n : ℕ), mu n ≤ n
hmu_bdd : ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (HDiv.hDiv (α := ℝ) (↑(mu n) : ℝ) (↑n : ℝ))
hs : Bornology.IsBounded (α := ℝ) (Set.Icc 0 1)
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(mu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
hb_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(nu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 b)
b_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) b
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a
hy :
  limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ y ^ b
hxy :
  limsup
      (fun (n : ℕ) ↦
        HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)) *
          HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b
ε : ℝ
hε : ε > 0
h_mul : smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε ≤ max (smoothingFun μ x) (smoothingFun μ y) + ε
N : ℕ+
hN :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ (↑N : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ (↑N : ℕ)) : ℝ)) *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ (↑N : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ (↑N : ℕ)) : ℝ)) <
    smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε
⊢ smoothingFun μ (x + y) ≤ smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε
have apply : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x + y) ^ (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (ψ (↑N : ℕ)) sorry) : ℕ)) : ℝ)
    (HDiv.hDiv (α := ℝ) 1 (↑(↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (ψ (↑N : ℕ)) sorry) : ℕ) : ℝ)) ≤
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ (↑N : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ (↑N : ℕ)) : ℝ)) *
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ (↑N : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ (↑N : ℕ)) : ℝ))
Tactic: apply (ciInf_le (smoothingSeminormSeq_bddBelow μ _)
    ⟨ψ N, (hψ_mono.lt_iff_lt.mpr N.pos).pos⟩).trans (hN.le.trans' _)
-- 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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
⊢ smoothingFun μ 0 = 0
have apply : smoothingSeminormSeq μ 0 =ᶠ[atTop] fun (x : ℕ) ↦ 0
Tactic: apply tendsto_nhds_unique_of_eventuallyEq (tendsto_smoothingFun_of_map_one_le_one μ hμ1 0)
      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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
⊢ smoothingSeminormSeq μ 0 =ᶠ[atTop] fun (x : ℕ) ↦ 0
have simp : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → smoothingSeminormSeq μ 0 b = 0
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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → smoothingSeminormSeq μ 0 b = 0
have h : ∀ (b : ℕ), 1 ≤ b → smoothingSeminormSeq μ 0 b = 0
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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
n : ℕ
hn : 1 ≤ n
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (HPow.hPow (α := R) 0 n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = 0
have h : HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≠ 0
Tactic: rw [zero_pow (pos_iff_ne_zero.mp hn), map_zero, zero_rpow]
-- 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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
n : R
⊢ Eq (α := ℝ)
    (⨅ (n_1 : ℕ+),
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((-n) ^ (↑n_1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n_1 : ℕ) : ℝ)))
    (⨅ (n_1 : ℕ+), HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n ^ (↑n_1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n_1 : ℕ) : ℝ)))
have e_s : Eq (α := ℕ+ → ℝ)
  (fun (n_1 : ℕ+) ↦
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((-n) ^ (↑n_1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n_1 : ℕ) : ℝ)))
  fun (n_1 : ℕ+) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n ^ (↑n_1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n_1 : ℕ) : ℝ))
Tactic: congr
-- 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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
n : R
⊢ Eq (α := ℕ+ → ℝ)
    (fun (n_1 : ℕ+) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((-n) ^ (↑n_1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n_1 : ℕ) : ℝ)))
    fun (n_1 : ℕ+) ↦
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n ^ (↑n_1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n_1 : ℕ) : ℝ))
have e_s : ∀ (n_1 : ℕ+),
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((-n) ^ (↑n_1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n_1 : ℕ) : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n ^ (↑n_1 : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n_1 : ℕ) : ℝ))
Tactic: ext n
-- 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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
n_1 : R
n : ℕ+
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((-n_1) ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
have e_s : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (HPow.hPow (α := R) (-1) (↑n : ℕ) * n_1 ^ (↑n : ℕ)) : ℝ)
    (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ)) =
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
Tactic: rw [neg_pow]
-- 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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
n_1 : R
n : ℕ+
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (HPow.hPow (α := R) (-1) (↑n : ℕ) * n_1 ^ (↑n : ℕ)) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
have e_s : ∀ (hpos : HPow.hPow (α := R) (-1) (↑n : ℕ) = 1),
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (HPow.hPow (α := R) (-1) (↑n : ℕ) * n_1 ^ (↑n : ℕ)) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
Tactic: rcases neg_one_pow_eq_or R n with hpos | hneg
-- 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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
n_1 : R
n : ℕ+
e_s :
  ∀ (hpos : HPow.hPow (α := R) (-1) (↑n : ℕ) = 1),
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (HPow.hPow (α := R) (-1) (↑n : ℕ) * n_1 ^ (↑n : ℕ)) : ℝ)
        (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ)) =
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (HPow.hPow (α := R) (-1) (↑n : ℕ) * n_1 ^ (↑n : ℕ)) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
have e_s₁ : ∀ (hneg : HPow.hPow (α := R) (-1) (↑n : ℕ) = -1),
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (HPow.hPow (α := R) (-1) (↑n : ℕ) * n_1 ^ (↑n : ℕ)) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
Tactic: rcases neg_one_pow_eq_or R n with hpos | hneg
-- 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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
n_1 : R
n : ℕ+
hpos : HPow.hPow (α := R) (-1) (↑n : ℕ) = 1
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (HPow.hPow (α := R) (-1) (↑n : ℕ) * n_1 ^ (↑n : ℕ)) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
have e_s : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (1 * n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ)) =
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
Tactic: rw [hpos, one_mul]
-- 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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
n_1 : R
n : ℕ+
hpos : HPow.hPow (α := R) (-1) (↑n : ℕ) = 1
e_s :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (1 * n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (HPow.hPow (α := R) (-1) (↑n : ℕ) * n_1 ^ (↑n : ℕ)) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
have e_s₁ : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ)) =
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
Tactic: rw [hpos, one_mul]
-- 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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
n_1 : R
n : ℕ+
hneg : HPow.hPow (α := R) (-1) (↑n : ℕ) = -1
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (HPow.hPow (α := R) (-1) (↑n : ℕ) * n_1 ^ (↑n : ℕ)) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
have e_s : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (-1 * n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ)) =
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
Tactic: rw [hneg, neg_one_mul, map_neg_eq_map μ]
-- 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 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
n_1 : R
n : ℕ+
hneg : HPow.hPow (α := R) (-1) (↑n : ℕ) = -1
e_s :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (-1 * n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (HPow.hPow (α := R) (-1) (↑n : ℕ) * n_1 ^ (↑n : ℕ)) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ)) =
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
have e_s₁ : HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (-n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ)) =
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (n_1 ^ (↑n : ℕ)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(↑n : ℕ) : ℝ))
Tactic: rw [hneg, neg_one_mul, map_neg_eq_map μ]