awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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 : ¬smoothingFun μ x ≤ smoothingFun μ y
neg : smoothingFun μ x ^ a * smoothingFun μ x ^ (1 - a) ≤ smoothingFun μ x
neg₁ : smoothingFun μ x ^ (a + (1 - a)) ≤ smoothingFun μ x
neg₂ : smoothingFun μ x ^ (a + 1 - a) ≤ smoothingFun μ x
neg₃ : HPow.hPow (β := ℝ) (smoothingFun μ x) 1 ≤ smoothingFun μ x
neg₄ neg₅ : smoothingFun μ x ≤ smoothingFun μ x
⊢ smoothingFun μ x ^ a * smoothingFun μ x ^ b ≤ smoothingFun μ x

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

Premises used: Real.rpow_add_of_nonneg, Iff.mpr, add_sub_cancel_left, add_sub, smoothingFun_nonneg, Real.rpow_one, And.right, And.left, sub_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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 ^ 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]
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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) + ε
apply : smoothingFun μ (x + y) ≤ smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε
⊢ smoothingFun μ (x + y) ≤ max (smoothingFun μ x) (smoothingFun μ y) + ε

Tactic:
apply le_trans _ h_mul

Premises used: le_trans
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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 : ℕ
⊢ 0 n ≤ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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 : ℕ
⊢ 0 n ≤ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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 : ℕ+),
    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ε
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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 + ε
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 + ε
⊢ smoothingFun μ (x + y) ≤ smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε

Tactic:
obtain ⟨N, hN⟩ := hex
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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 + ε
apply :
  HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x + y) ^ (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (ψ (↑N : ℕ)) ⋯) : ℕ)) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑(↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (ψ (↑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 + y) ≤ smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε

Tactic:
apply (ciInf_le (smoothingSeminormSeq_bddBelow μ _)
    ⟨ψ N, (hψ_mono.lt_iff_lt.mpr N.pos).pos⟩).trans (hN.le.trans' _)

Premises used: PNat.val, Iff.mpr, LT.lt.pos, StrictMono.lt_iff_lt, LT.lt.le, Subtype.mk, ciInf_le, PNat.pos, smoothingSeminormSeq_bddBelow, LE.le.trans, LE.le.trans'
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
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 + ε
⊢ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) ((x + y) ^ (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (ψ (↑N : ℕ)) ⋯) : ℕ)) : ℝ)
      (HDiv.hDiv (α := ℝ) 1 (↑(↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (ψ (↑N : ℕ)) ⋯) : ℕ) : ℝ)) ≤
    HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ mu (ψ (↑N : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ (↑N : ℕ)) : ℝ)) *
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (y ^ nu (ψ (↑N : ℕ))) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ (↑N : ℕ)) : ℝ))

Tactic:
simpa [PNat.mk_coe, hnu, ← mul_rpow (apply_nonneg μ _) (apply_nonneg μ _)] using
    mu_property μ hn (ψ N)

Premises used: PNat.val, Real.mul_rpow, _private.0.mu_property, NonnegHomClass.apply_nonneg, PNat.mk_coe
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
apply : smoothingSeminormSeq μ 0 =ᶠ[atTop] fun (x : ℕ) ↦ 0
⊢ smoothingFun μ 0 = 0

Tactic:
apply tendsto_nhds_unique_of_eventuallyEq (tendsto_smoothingFun_of_map_one_le_one μ hμ1 0)
      tendsto_const_nhds

Premises used: tendsto_const_nhds, tendsto_nhds_unique_of_eventuallyEq, tendsto_smoothingFun_of_map_one_le_one, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑μ : (a : R) → ℝ)
simp : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → smoothingSeminormSeq μ 0 b = 0
⊢ smoothingSeminormSeq μ 0 =ᶠ[atTop] fun (x : ℕ) ↦ 0

Tactic:
simp only [EventuallyEq, eventually_atTop, ge_iff_le]

Premises used: ge_iff_le, Filter.EventuallyEq, Filter.eventually_atTop