linarith
case intro.intro.intro
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
l1 : ContinuousOn Real.log (Icc x (x + 1))
l2 : ∀ t ∈ Ioo x (x + 1), HasDerivAt Real.log t⁻¹ t
t : ℝ
ht1 : x < t
right✝ : t < x + 1
htx : t⁻¹ = (x + 1).log - x.log
⊢ x ≤ t
no goals