-- Mathlib/Analysis/Normed/Ring/SmoothingSeminorm.lean
theorem μ_bddAbove (hμ1 : μ 1 ≤ 1) {s : ℕ → ℕ} (hs : ∀ n : ℕ, s n ≤ n) (x : R)
    (ψ : ℕ → ℕ) : BddAbove (Set.range fun n : ℕ => μ (x ^ s (ψ n)) ^ (1 / (ψ n : ℝ)))

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : ¬μ x ≤ 1
⊢ μ x ∈ upperBounds (Set.range fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n)))

Tactic:
simp only [mem_upperBounds, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff']

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : ¬μ x ≤ 1
⊢ ∀ (x_1 : ℝ) (x_2 : ℕ), μ (x ^ s (ψ x_2)) ^ (1 / ↑(ψ x_2)) = x_1 → x_1 ≤ μ x

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : ¬μ x ≤ 1
n : ℕ
⊢ ↑(s (ψ n)) / ↑(ψ n) ≤ 1

Tactic:
exact div_le_one_of_le₀ (cast_le.mpr (hs (ψ n))) (cast_nonneg _)

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : μ x ≤ 1
n : ℕ
⊢ μ x ^ (↑(s (ψ n)) / ↑(ψ n)) ≤ 1

Tactic:
exact rpow_le_one (apply_nonneg _ _) hx (div_nonneg (cast_nonneg _) (cast_nonneg _))

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : μ x ≤ 1
n : ℕ
⊢ (μ x ^ s (ψ n)) ^ (1 / ↑(ψ n)) ≤ 1

Tactic:
rw [← rpow_natCast, ← rpow_mul (apply_nonneg _ _), mul_one_div]

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : μ x ≤ 1
n : ℕ
⊢ μ x ^ (↑(s (ψ n)) / ↑(ψ n)) ≤ 1

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : ¬μ x ≤ 1
⊢ BddAbove (Set.range fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n)))

Tactic:
use μ x

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : ¬μ x ≤ 1
⊢ μ x ∈ upperBounds (Set.range fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n)))

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
⊢ BddAbove (Set.range fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n)))

Tactic:
by_cases hx : μ x ≤ 1

Result:
case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : μ x ≤ 1
⊢ BddAbove (Set.range fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n)))

case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : ¬μ x ≤ 1
⊢ BddAbove (Set.range fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n)))

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
⊢ BddAbove (Set.range fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n)))

Tactic:
have hψ : ∀ n, 0 ≤ 1 / (ψ n : ℝ) := fun _ ↦ by simp only [one_div, inv_nonneg, cast_nonneg]

Result:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
⊢ BddAbove (Set.range fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n)))

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : μ x ≤ 1
⊢ 1 ∈ upperBounds (Set.range fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n)))

Tactic:
simp only [mem_upperBounds, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff']

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : μ x ≤ 1
⊢ ∀ (x_1 : ℝ) (x_2 : ℕ), μ (x ^ s (ψ x_2)) ^ (1 / ↑(ψ x_2)) = x_1 → x_1 ≤ 1

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : ¬μ x ≤ 1
n : ℕ
⊢ μ x ^ (↑(s (ψ n)) / ↑(ψ n)) ≤ μ x ^ 1

Tactic:
rw [rpow_le_rpow_left_iff (not_le.mp hx)]

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : ¬μ x ≤ 1
n : ℕ
⊢ ↑(s (ψ n)) / ↑(ψ n) ≤ 1

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : μ x ≤ 1
⊢ BddAbove (Set.range fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n)))

Tactic:
use 1

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : μ x ≤ 1
⊢ 1 ∈ upperBounds (Set.range fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n)))

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : ¬μ x ≤ 1
n : ℕ
⊢ (μ x ^ s (ψ n)) ^ (1 / ↑(ψ n)) ≤ μ x

Tactic:
rw [← rpow_natCast, ← rpow_mul (apply_nonneg _ _), mul_one_div]

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : ¬μ x ≤ 1
n : ℕ
⊢ μ x ^ (↑(s (ψ n)) / ↑(ψ n)) ≤ μ x

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : ¬μ x ≤ 1
n : ℕ
⊢ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n)) ≤ μ x

Tactic:
apply le_trans (rpow_le_rpow (apply_nonneg _ _) (map_pow_le_pow' hμ1 _ _) (hψ n))

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : ¬μ x ≤ 1
n : ℕ
⊢ (μ x ^ s (ψ n)) ^ (1 / ↑(ψ n)) ≤ μ x

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
x✝ : ℕ
⊢ 0 ≤ 1 / ↑(ψ x✝)

Tactic:
simp only [one_div, inv_nonneg, cast_nonneg]

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : ¬μ x ≤ 1
⊢ ∀ (x_1 : ℝ) (x_2 : ℕ), μ (x ^ s (ψ x_2)) ^ (1 / ↑(ψ x_2)) = x_1 → x_1 ≤ μ x

Tactic:
rintro _ n rfl

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : ¬μ x ≤ 1
n : ℕ
⊢ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n)) ≤ μ x

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : ¬μ x ≤ 1
n : ℕ
⊢ μ x ^ (↑(s (ψ n)) / ↑(ψ n)) ≤ μ x

Tactic:
conv_rhs => rw [← rpow_one (μ x)]

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : ¬μ x ≤ 1
n : ℕ
⊢ μ x ^ (↑(s (ψ n)) / ↑(ψ n)) ≤ μ x ^ 1