Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (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 : ℕ), ↑(mu n) / ↑n ∈ Set.Icc 0 1
hs : Bornology.IsBounded (Set.Icc 0 1)
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(mu n) / ↑n) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
hb_lim : Tendsto ((fun n ↦ ↑(nu n) / ↑n) ∘ ψ) atTop (𝓝 b)
b_in : b ∈ Set.Icc 0 1
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx : limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a
hy : limsup (fun n ↦ μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ y ^ b
hxy :
  limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n)) * μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b
ε : ℝ
hε : ε > 0
h : smoothingFun μ x ≤ smoothingFun μ y
⊢ smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε ≤ smoothingFun μ y + ε

pp: case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (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 : ℕ), ↑(mu n) / ↑n ∈ Set.Icc 0 1
hs : Bornology.IsBounded (Set.Icc 0 1)
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(mu n) / ↑n) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
hb_lim : Tendsto ((fun n ↦ ↑(nu n) / ↑n) ∘ ψ) atTop (𝓝 b)
b_in : b ∈ Set.Icc 0 1
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx : limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a
hy : limsup (fun n ↦ μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ y ^ b
hxy :
  limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n)) * μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b
ε : ℝ
hε : ε > 0
h : ¬smoothingFun μ x ≤ smoothingFun μ y
⊢ smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε ≤ smoothingFun μ x + ε

Tactic:
· 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]

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (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 : ℕ), ↑(mu n) / ↑n ∈ Set.Icc 0 1
hs : Bornology.IsBounded (Set.Icc 0 1)
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(mu n) / ↑n) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
hb_lim : Tendsto ((fun n ↦ ↑(nu n) / ↑n) ∘ ψ) atTop (𝓝 b)
b_in : b ∈ Set.Icc 0 1
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx : limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a
hy : limsup (fun n ↦ μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ y ^ b
hxy :
  limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n)) * μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b
ε : ℝ
hε : ε > 0
h : ¬smoothingFun μ x ≤ smoothingFun μ y
⊢ smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε ≤ smoothingFun μ x + ε