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 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
ha_pos : 0 < a
⊢ EventuallyEq (β := ℝ) atTop (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑(s (ψ n)) : ℝ) * (↑(s (ψ n)) : ℝ)) 1

Tactic:
have h : (fun n : ℕ => (1 : ℝ) / (s (ψ n) : ℝ) * (s (ψ n) : ℝ)) =ᶠ[atTop] 1 := by
        apply Filter.EventuallyEq.div_mul_cancel_atTop
        exact (tendsto_natCast_atTop_atTop.comp hψ_mono.tendsto_atTop).num ha_pos hψ_lim
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
ha_pos : 0 < a
h : EventuallyEq (β := ℝ) atTop (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑(s (ψ n)) : ℝ) * (↑(s (ψ n)) : ℝ)) 1
simp_rw :
  EventuallyEq (β := ℝ) atTop
    (fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ)
        (HDiv.hDiv (α := ℝ) 1 (↑(s (ψ n)) : ℝ) * (↑(s (ψ n)) : ℝ) / (↑(ψ n) : ℝ)))
    fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))
⊢ EventuallyEq (β := ℝ) atTop
    (fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(s (ψ n)) : ℝ)) ^
        HDiv.hDiv (α := ℝ) (↑(s (ψ n)) : ℝ) (↑(ψ n) : ℝ))
    fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))

Tactic:
simp_rw [← rpow_mul (apply_nonneg μ _), mul_div]

Premises used: mul_div, NonnegHomClass.apply_nonneg, Real.rpow_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
ha_pos : 0 < a
h : EventuallyEq (β := ℝ) atTop (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑(s (ψ n)) : ℝ) * (↑(s (ψ n)) : ℝ)) 1
⊢ EventuallyEq (β := ℝ) atTop
    (fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ)
        (HDiv.hDiv (α := ℝ) 1 (↑(s (ψ n)) : ℝ) * (↑(s (ψ n)) : ℝ) / (↑(ψ n) : ℝ)))
    fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))

Tactic:
EventuallyEq.comp₂ EventuallyEq.rfl HPow.hPow (h.div EventuallyEq.rfl)

Premises used: Filter.EventuallyEq.div, Filter.EventuallyEq.comp₂, HPow.hPow, Filter.EventuallyEq.rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
ha_pos : 0 < a
h : EventuallyEq (β := ℝ) atTop (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑(s (ψ n)) : ℝ) * (↑(s (ψ n)) : ℝ)) 1
⊢ EventuallyEq (β := ℝ) atTop
    (fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ)
        (HDiv.hDiv (α := ℝ) 1 (↑(s (ψ n)) : ℝ) * (↑(s (ψ n)) : ℝ) / (↑(ψ n) : ℝ)))
    fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))

Tactic:
exact EventuallyEq.comp₂ EventuallyEq.rfl HPow.hPow (h.div EventuallyEq.rfl)

Premises used: Filter.EventuallyEq.div, Filter.EventuallyEq.comp₂, HPow.hPow, Filter.EventuallyEq.rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
ha_pos : 0 < a
⊢ EventuallyEq (β := ℝ) atTop
    (fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(s (ψ n)) : ℝ)) ^
        HDiv.hDiv (α := ℝ) (↑(s (ψ n)) : ℝ) (↑(ψ n) : ℝ))
    fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))

Tactic:
have h_eq : (fun n : ℕ =>
        (μ (x ^ s (ψ n)) ^ (1 / (s (ψ n) : ℝ))) ^ ((s (ψ n) : ℝ) / (ψ n : ℝ))) =ᶠ[atTop]
        fun n : ℕ => μ (x ^ s (ψ n)) ^ (1 / (ψ n : ℝ)) := by
      have h : (fun n : ℕ => (1 : ℝ) / (s (ψ n) : ℝ) * (s (ψ n) : ℝ)) =ᶠ[atTop] 1 := by
        apply Filter.EventuallyEq.div_mul_cancel_atTop
        exact (tendsto_natCast_atTop_atTop.comp hψ_mono.tendsto_atTop).num ha_pos hψ_lim
      simp_rw [← rpow_mul (apply_nonneg μ _), mul_div]
      exact EventuallyEq.comp₂ EventuallyEq.rfl HPow.hPow (h.div EventuallyEq.rfl)
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
ha_pos : 0 < a
h_eq :
  EventuallyEq (β := ℝ) atTop
    (fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(s (ψ n)) : ℝ)) ^
        HDiv.hDiv (α := ℝ) (↑(s (ψ n)) : ℝ) (↑(ψ n) : ℝ))
    fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))
⊢ limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a

Tactic:
((tendsto_smoothingFun_of_map_one_le_one μ hμ1 x |>.comp <|
      tendsto_natCast_atTop_iff.mp <| (tendsto_natCast_atTop_atTop.comp
        hψ_mono.tendsto_atTop).num ha_pos hψ_lim).rpow
          hψ_lim <| .inr ha_pos).congr' h_eq |>.limsup_eq.le

Premises used: Filter.Tendsto.limsup_eq, StrictMono.tendsto_atTop, Filter.Tendsto.num, Eq.le, tendsto_smoothingFun_of_map_one_le_one, Filter.Tendsto.rpow, tendsto_natCast_atTop_iff, tendsto_natCast_atTop_atTop, Iff.mp, Filter.Tendsto.comp, Filter.Tendsto.congr', Or.inr
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(s n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
ha_pos : 0 < a
h_eq :
  EventuallyEq (β := ℝ) atTop
    (fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(s (ψ n)) : ℝ)) ^
        HDiv.hDiv (α := ℝ) (↑(s (ψ n)) : ℝ) (↑(ψ n) : ℝ))
    fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))
⊢ limsup (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ s (ψ n)) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ)))
      atTop ≤
    smoothingFun μ x ^ a

Tactic:
exact ((tendsto_smoothingFun_of_map_one_le_one μ hμ1 x |>.comp <|
      tendsto_natCast_atTop_iff.mp <| (tendsto_natCast_atTop_atTop.comp
        hψ_mono.tendsto_atTop).num ha_pos hψ_lim).rpow
          hψ_lim <| .inr ha_pos).congr' h_eq |>.limsup_eq.le

Premises used: Filter.Tendsto.limsup_eq, StrictMono.tendsto_atTop, Filter.Tendsto.num, Eq.le, tendsto_smoothingFun_of_map_one_le_one, Filter.Tendsto.rpow, tendsto_natCast_atTop_iff, tendsto_natCast_atTop_atTop, Iff.mp, Filter.Tendsto.comp, Filter.Tendsto.congr', Or.inr
-- Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Goal:
R : Type u_1
inst : CommRing R
μ : RingSeminorm R
hμ1 : LE.le (α := ℝ) ((μ : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
x : R
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
⊢ Tendsto (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) ((μ : (a : R) → ℝ) (x ^ ψ n) : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑(ψ n) : ℝ))) atTop
    (𝓝 (smoothingFun μ x))

Tactic:
have hψ_lim' : Tendsto ψ atTop atTop := StrictMono.tendsto_atTop hψ_mono
  (tendsto_smoothingFun_of_map_one_le_one μ hμ1 x).comp hψ_lim'

Premises used: StrictMono.tendsto_atTop, tendsto_smoothingFun_of_map_one_le_one, Filter.Tendsto.comp
-- 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
⊢ ∀ (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 : ℝ)

Tactic:
have hn : ∀ n : ℕ, ∃ m < n + 1,
      μ ((x + y) ^ (n : ℕ)) ^ (1 / (n : ℝ)) ≤ (μ (x ^ m) * μ (y ^ (n - m : ℕ))) ^ (1 / (n : ℝ)) :=
    fun n => RingSeminorm.exists_index_pow_le μ hna x y n
-- 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
⊢ let nu : ℕ → ℕ := fun (n : ℕ) ↦ n - mu n;
  nu = fun (n : ℕ) ↦ n - mu n

Tactic:
set nu : ℕ → ℕ := fun n => n - mu n with hnu

Premises used: HSub.hSub
-- 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
⊢ ∀ (n : ℕ), mu n ≤ n

Tactic:
have hmu_le : ∀ n : ℕ, mu n ≤ n := fun n => mu_le μ hn n
-- 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
⊢ ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (HDiv.hDiv (α := ℝ) (↑(mu n) : ℝ) (↑n : ℝ))

Tactic:
have hmu_bdd : ∀ n : ℕ, (mu n : ℝ) / n ∈ Set.Icc (0 : ℝ) 1 := fun n => mu_bdd μ hn n
-- 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 : ℝ))
⊢ Bornology.IsBounded (α := ℝ) (Set.Icc 0 1)

Tactic:
have hs : Bornology.IsBounded (Set.Icc (0 : ℝ) 1) := Metric.isBounded_Icc 0 1
-- 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)
obtain :
  ∀ (a : ℝ) (a_in : Membership.mem (γ := Set ℝ) (closure (Set.Icc 0 1)) a) (ψ : ℕ → ℕ) (hψ_mono : StrictMono ψ)
    (hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(mu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)),
    smoothingFun μ (x + y) ≤ max (smoothingFun μ x) (smoothingFun μ y)
⊢ smoothingFun μ (x + y) ≤ max (smoothingFun μ x) (smoothingFun μ y)

Tactic:
obtain ⟨a, a_in, ψ, hψ_mono, hψ_lim⟩ := tendsto_subseq_of_bounded hs hmu_bdd

Premises used: tendsto_subseq_of_bounded
-- 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 ℝ) (closure (Set.Icc 0 1)) a
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(mu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 a)
rw :
  ∀ (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)),
    smoothingFun μ (x + y) ≤ max (smoothingFun μ x) (smoothingFun μ y)
⊢ smoothingFun μ (x + y) ≤ max (smoothingFun μ x) (smoothingFun μ y)

Tactic:
rw [closure_Icc] at a_in

Premises used: closure_Icc
-- 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)
⊢ let b := 1 - a;
  b = 1 - a

Tactic:
set b := 1 - a with hb
-- 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
apply :
  EventuallyEq (β := ℝ) atTop
    (fun (x : ℕ) ↦ HSub.hSub (α := ℝ) 1 (((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(mu n) : ℝ) (↑n : ℝ)) ∘ ψ) x))
    ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(nu n) : ℝ) (↑n : ℝ)) ∘ ψ)
⊢ Tendsto ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(nu n) : ℝ) (↑n : ℝ)) ∘ ψ) atTop (𝓝 b)

Tactic:
apply Tendsto.congr' _ (Tendsto.const_sub 1 hψ_lim)

Premises used: Filter.Tendsto.const_sub, Filter.Tendsto.congr', 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) → ℝ)
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
simp :
  ∃ (a : ℕ),
    ∀ (b : ℕ),
      a ≤ b → 1 - HDiv.hDiv (α := ℝ) (↑(mu (ψ b)) : ℝ) (↑(ψ b) : ℝ) = HDiv.hDiv (α := ℝ) (↑(nu (ψ b)) : ℝ) (↑(ψ b) : ℝ)
⊢ EventuallyEq (β := ℝ) atTop
    (fun (x : ℕ) ↦ HSub.hSub (α := ℝ) 1 (((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(mu n) : ℝ) (↑n : ℝ)) ∘ ψ) x))
    ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(nu n) : ℝ) (↑n : ℝ)) ∘ ψ)

Tactic:
simp only [EventuallyEq, Function.comp_apply, eventually_atTop, ge_iff_le]

Premises used: ge_iff_le, Filter.EventuallyEq, Function.comp_apply, Filter.eventually_atTop
-- 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
h :
  ∀ (b : ℕ),
    1 ≤ b → 1 - HDiv.hDiv (α := ℝ) (↑(mu (ψ b)) : ℝ) (↑(ψ b) : ℝ) = HDiv.hDiv (α := ℝ) (↑(nu (ψ b)) : ℝ) (↑(ψ b) : ℝ)
⊢ ∃ (a : ℕ),
    ∀ (b : ℕ),
      a ≤ b → 1 - HDiv.hDiv (α := ℝ) (↑(mu (ψ b)) : ℝ) (↑(ψ b) : ℝ) = HDiv.hDiv (α := ℝ) (↑(nu (ψ b)) : ℝ) (↑(ψ b) : ℝ)

Tactic:
use 1
-- 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
m : ℕ
hm : 1 ≤ m
⊢ Ne (α := ℝ) (↑(ψ m) : ℝ) 0

Tactic:
have h0 : (ψ m : ℝ) ≠ 0 := cast_ne_zero.mpr
      (hψ_mono (Nat.pos_of_ne_zero (one_le_iff_ne_zero.mp hm))).ne_zero
-- 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
m : ℕ
hm : 1 ≤ m
h0 : Ne (α := ℝ) (↑(ψ m) : ℝ) 0
h :
  HDiv.hDiv (α := ℝ) (↑(ψ m) : ℝ) (↑(ψ m) : ℝ) - HDiv.hDiv (α := ℝ) (↑(mu (ψ m)) : ℝ) (↑(ψ m) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑(nu (ψ m)) : ℝ) (↑(ψ m) : ℝ)
h₁ :
  HSub.hSub (α := ℝ) (↑(ψ m) : ℝ) (↑(mu (ψ m)) : ℝ) / (↑(ψ m) : ℝ) = HDiv.hDiv (α := ℝ) (↑(nu (ψ m)) : ℝ) (↑(ψ m) : ℝ)
h₂ h₃ :
  HSub.hSub (α := ℝ) (↑(ψ m) : ℝ) (↑(mu (ψ m)) : ℝ) / (↑(ψ m) : ℝ) =
    HSub.hSub (α := ℝ) (↑(ψ m) : ℝ) (↑(mu (ψ m)) : ℝ) / (↑(ψ m) : ℝ)
⊢ 1 - HDiv.hDiv (α := ℝ) (↑(mu (ψ m)) : ℝ) (↑(ψ m) : ℝ) = HDiv.hDiv (α := ℝ) (↑(nu (ψ m)) : ℝ) (↑(ψ m) : ℝ)

Tactic:
rw [← div_self h0, ← sub_div, cast_sub (hmu_le _)]

Premises used: Nat.cast_sub, sub_div, div_self