Theorem: log_ratio_mono (Ray/Dynamics/Multibrot/Postcritical.lean)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ MonotoneOn (fun x => (x - 1).log / x.log) (Ici 2)
Tactic:
have hd : ∀ x, 2 ≤ x → HasDerivAt (fun x ↦ log (x-1) / log x)
    ((1 / (x-1) * log x - log (x-1) * x⁻¹) / (log x)^2) x := by
  intro x x2
  have l0 : 0 < log x := Real.log_pos (by linarith)
  refine HasDerivAt.div ?_ (Real.hasDerivAt_log (by positivity)) l0.ne'
  exact HasDerivAt.log ((hasDerivAt_id _).sub_const _) (by linarith)
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
⊢ MonotoneOn (fun x => (x - 1).log / x.log) (Ici 2)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
⊢ MonotoneOn (fun x => (x - 1).log / x.log) (Ici 2)
Tactic:
have d : DifferentiableOn ℝ (fun x ↦ log (x-1) / log x) (Ici 2) :=
  fun x m ↦ (hd x m).differentiableAt.differentiableWithinAt
State after:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
⊢ MonotoneOn (fun x => (x - 1).log / x.log) (Ici 2)

State before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
⊢ MonotoneOn (fun x => (x - 1).log / x.log) (Ici 2)
Tactic:
apply monotoneOn_of_deriv_nonneg (convex_Ici _)
State after:
case hf
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
⊢ ContinuousOn (fun x => (x - 1).log / x.log) (Ici 2)

case hf'
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
⊢ DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (interior (Ici 2))

case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
⊢ ∀ x ∈ interior (Ici 2), 0 ≤ deriv (fun x => (x - 1).log / x.log) x

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
Tactic:
intro x x2
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x2 : 2 ≤ x
⊢ HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x2 : 2 ≤ x
⊢ HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
Tactic:
have l0 : 0 < log x := Real.log_pos (by linarith)
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x2 : 2 ≤ x
l0 : 0 < x.log
⊢ HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x2 : 2 ≤ x
l0 : 0 < x.log
⊢ HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
Tactic:
refine HasDerivAt.div ?_ (Real.hasDerivAt_log (by positivity)) l0.ne'
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x2 : 2 ≤ x
l0 : 0 < x.log
⊢ HasDerivAt (fun x => (x - 1).log) (1 / (x - 1)) x

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x2 : 2 ≤ x
l0 : 0 < x.log
⊢ HasDerivAt (fun x => (x - 1).log) (1 / (x - 1)) x
Tactic:
exact HasDerivAt.log ((hasDerivAt_id _).sub_const _) (by linarith)
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x2 : 2 ≤ x
⊢ 1 < x
Tactic:
linarith
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x2 : 2 ≤ x
l0 : 0 < x.log
⊢ x ≠ 0
Tactic:
positivity
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x2 : 2 ≤ x
l0 : 0 < x.log
⊢ x - 1 ≠ 0
Tactic:
linarith
State after:
no goals

State before:
case hf
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
⊢ ContinuousOn (fun x => (x - 1).log / x.log) (Ici 2)
Tactic:
exact d.continuousOn
State after:
no goals

State before:
case hf'
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
⊢ DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (interior (Ici 2))
Tactic:
exact d.mono interior_subset
State after:
no goals

State before:
case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
⊢ ∀ x ∈ interior (Ici 2), 0 ≤ deriv (fun x => (x - 1).log / x.log) x
Tactic:
intro x m
State after:
case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : x ∈ interior (Ici 2)
⊢ 0 ≤ deriv (fun x => (x - 1).log / x.log) x

State before:
case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : x ∈ interior (Ici 2)
⊢ 0 ≤ deriv (fun x => (x - 1).log / x.log) x
Tactic:
simp only [nonempty_Iio, interior_Ici', mem_Ioi] at m
State after:
case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
⊢ 0 ≤ deriv (fun x => (x - 1).log / x.log) x

State before:
case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
⊢ 0 ≤ deriv (fun x => (x - 1).log / x.log) x
Tactic:
have l0 : 0 < log x := Real.log_pos (by linarith)
State after:
case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 0 ≤ deriv (fun x => (x - 1).log / x.log) x

State before:
case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 0 ≤ deriv (fun x => (x - 1).log / x.log) x
Tactic:
simp only [(hd x m.le).deriv, one_div]
State after:
case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 0 ≤ ((x - 1)⁻¹ * x.log - (x - 1).log * x⁻¹) / x.log ^ 2

State before:
case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 0 ≤ ((x - 1)⁻¹ * x.log - (x - 1).log * x⁻¹) / x.log ^ 2
Tactic:
refine div_nonneg ?_ (by positivity)
State after:
case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 0 ≤ (x - 1)⁻¹ * x.log - (x - 1).log * x⁻¹

State before:
case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 0 ≤ (x - 1)⁻¹ * x.log - (x - 1).log * x⁻¹
Tactic:
simp only [sub_nonneg, mul_comm]
State after:
case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ x⁻¹ * (x - 1).log ≤ (x - 1)⁻¹ * x.log

State before:
case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ x⁻¹ * (x - 1).log ≤ (x - 1)⁻¹ * x.log
Tactic:
apply mul_le_mul
State after:
case hf'_nonneg.h₁
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ x⁻¹ ≤ (x - 1)⁻¹

case hf'_nonneg.h₂
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ (x - 1).log ≤ x.log

case hf'_nonneg.c0
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 0 ≤ (x - 1).log

case hf'_nonneg.b0
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 0 ≤ (x - 1)⁻¹

State before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
⊢ 1 < x
Tactic:
linarith
State after:
no goals

State before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 0 ≤ x.log ^ 2
Tactic:
positivity
State after:
no goals

State before:
case hf'_nonneg.h₁
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ x⁻¹ ≤ (x - 1)⁻¹
Tactic:
exact inv_le_inv_of_le (by linarith) (by linarith)
State after:
no goals

State before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 0 < x - 1
Tactic:
linarith
State after:
no goals

State before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ x - 1 ≤ x
Tactic:
linarith
State after:
no goals

State before:
case hf'_nonneg.h₂
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ (x - 1).log ≤ x.log
Tactic:
exact Real.log_le_log (by linarith) (by linarith)
State after:
no goals

State before:
case hf'_nonneg.c0
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 0 ≤ (x - 1).log
Tactic:
exact Real.log_nonneg (by linarith)
State after:
no goals

State before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 1 ≤ x - 1
Tactic:
linarith
State after:
no goals

State before:
case hf'_nonneg.b0
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 0 ≤ (x - 1)⁻¹
Tactic:
exact inv_nonneg.mpr (by linarith)
State after:
no goals

State before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 0 ≤ x - 1
Tactic:
linarith
State after:
no goals