Theorem: Smooth1Properties_estimate (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
⊢ (1 - 2 ^ (-ε)) / ε < Real.log 2
Tactic:
apply (div_lt_iff' εpos).mpr
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
⊢ 1 - 2 ^ (-ε) < ε * Real.log 2

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
⊢ 1 - 2 ^ (-ε) < ε * Real.log 2
Tactic:
have : 1 - 1 / (2 : ℝ) ^ ε = ((2 : ℝ) ^ ε - 1) / (2 : ℝ) ^ ε := by
  rw [sub_div, div_self (by positivity)]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
this : 1 - 1 / 2 ^ ε = (2 ^ ε - 1) / 2 ^ ε
⊢ 1 - 2 ^ (-ε) < ε * Real.log 2

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
this : 1 - 1 / 2 ^ ε = (2 ^ ε - 1) / 2 ^ ε
⊢ 1 - 2 ^ (-ε) < ε * Real.log 2
Tactic:
rw [← Real.log_rpow (by norm_num), rpow_neg (by norm_num), inv_eq_one_div (2 ^ ε), this]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
this : 1 - 1 / 2 ^ ε = (2 ^ ε - 1) / 2 ^ ε
⊢ (2 ^ ε - 1) / 2 ^ ε < (2 ^ ε).log

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
this : 1 - 1 / 2 ^ ε = (2 ^ ε - 1) / 2 ^ ε
⊢ (2 ^ ε - 1) / 2 ^ ε < (2 ^ ε).log
Tactic:
set c := (2 : ℝ) ^ ε
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
⊢ (c - 1) / c < c.log

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
⊢ (c - 1) / c < c.log
Tactic:
have hc : 1 < c := by
  rw [← rpow_zero (2 : ℝ)]
  apply Real.rpow_lt_rpow_of_exponent_lt (by norm_num) εpos
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
⊢ (c - 1) / c < c.log

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
⊢ (c - 1) / c < c.log
Tactic:
apply (div_lt_iff' (by positivity)).mpr <| lt_sub_iff_add_lt'.mp ?_
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
⊢ -1 < c * c.log - c

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
⊢ -1 < c * c.log - c
Tactic:
let f := (fun x ↦ x * Real.log x - x)
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
⊢ -1 < c * c.log - c

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
⊢ -1 < c * c.log - c
Tactic:
rw [(by simp [f] : -1 = f 1), (by simp : c * Real.log c - c = f c)]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
⊢ f 1 < f c

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
mono : StrictMonoOn f (Ici 1)
⊢ f 1 < f c
Tactic:
exact mono (by rw [mem_Ici]) (mem_Ici.mpr <| le_of_lt hc) hc
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
⊢ 1 - 1 / 2 ^ ε = (2 ^ ε - 1) / 2 ^ ε
Tactic:
rw [sub_div, div_self (by positivity)]
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
⊢ 2 ^ ε ≠ 0
Tactic:
positivity
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
this : 1 - 1 / 2 ^ ε = (2 ^ ε - 1) / 2 ^ ε
⊢ 0 < 2
Tactic:
norm_num
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
this : 1 - 1 / 2 ^ ε = (2 ^ ε - 1) / 2 ^ ε
⊢ 0 ≤ 2
Tactic:
norm_num
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
⊢ 1 < c
Tactic:
rw [← rpow_zero (2 : ℝ)]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
⊢ 2 ^ 0 < c

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
⊢ 2 ^ 0 < c
Tactic:
apply Real.rpow_lt_rpow_of_exponent_lt (by norm_num) εpos
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
⊢ 1 < 2
Tactic:
norm_num
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
⊢ 0 < c
Tactic:
positivity
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
⊢ -1 = f 1
Tactic:
simp [f]
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
⊢ c * c.log - c = f c
Tactic:
simp
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
⊢ StrictMonoOn f (Ici 1)
Tactic:
refine strictMonoOn_of_deriv_pos (convex_Ici _) ?_ ?_
State after:
case refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
⊢ ContinuousOn f (Ici 1)

case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
⊢ ∀ x ∈ interior (Ici 1), 0 < deriv f x

State before:
case refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
⊢ ContinuousOn f (Ici 1)
Tactic:
apply continuousOn_id.mul (continuousOn_id.log ?_) |>.sub continuousOn_id
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
⊢ ∀ x ∈ Ici 1, id x ≠ 0

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
⊢ ∀ x ∈ Ici 1, id x ≠ 0
Tactic:
intro x hx
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : x ∈ Ici 1
⊢ id x ≠ 0

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : x ∈ Ici 1
⊢ id x ≠ 0
Tactic:
simp only [mem_Ici] at hx
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 ≤ x
⊢ id x ≠ 0

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 ≤ x
⊢ id x ≠ 0
Tactic:
simp only [id_eq, ne_eq]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 ≤ x
⊢ ¬x = 0

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 ≤ x
⊢ ¬x = 0
Tactic:
linarith
State after:
no goals

State before:
case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
⊢ ∀ x ∈ interior (Ici 1), 0 < deriv f x
Tactic:
intro x hx
State after:
case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : x ∈ interior (Ici 1)
⊢ 0 < deriv f x

State before:
case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : x ∈ interior (Ici 1)
⊢ 0 < deriv f x
Tactic:
simp only [nonempty_Iio, interior_Ici', mem_Ioi] at hx
State after:
case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ 0 < deriv f x

State before:
case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ 0 < deriv f x
Tactic:
dsimp only [f]
State after:
case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ 0 < deriv (fun x => x * x.log - x) x

State before:
case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ 0 < deriv (fun x => x * x.log - x) x
Tactic:
rw [deriv_sub, deriv_mul, deriv_log, deriv_id'', one_mul, mul_inv_cancel]
State after:
case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ 0 < x.log + 1 - (fun x => 1) x

case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ x ≠ 0

case refine_2.hc
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x) x

case refine_2.hd
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x.log) x

case refine_2.hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x * x.log) x

case refine_2.hg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x) x

State before:
case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ 0 < x.log + 1 - (fun x => 1) x

case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ x ≠ 0

case refine_2.hc
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x) x

case refine_2.hd
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x.log) x

case refine_2.hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x * x.log) x

case refine_2.hg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x) x
Tactic:
simp
State after:
case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ 0 < x.log

case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ x ≠ 0

case refine_2.hc
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x) x

case refine_2.hd
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x.log) x

case refine_2.hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x * x.log) x

case refine_2.hg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x) x

State before:
case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ 0 < x.log
Tactic:
exact log_pos hx
State after:
no goals

State before:
case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ x ≠ 0
Tactic:
linarith
State after:
no goals

State before:
case refine_2.hc
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x) x
Tactic:
simp only [differentiableAt_id']
State after:
no goals

State before:
case refine_2.hd
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x.log) x
Tactic:
simp only [differentiableAt_log_iff, ne_eq]
State after:
case refine_2.hd
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ ¬x = 0

State before:
case refine_2.hd
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ ¬x = 0
Tactic:
linarith
State after:
no goals

State before:
case refine_2.hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x * x.log) x
Tactic:
exact differentiableAt_id'.mul <| differentiableAt_id'.log (by linarith)
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ x ≠ 0
Tactic:
linarith
State after:
no goals

State before:
case refine_2.hg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x) x
Tactic:
simp only [differentiableAt_id']
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
mono : StrictMonoOn f (Ici 1)
⊢ 1 ∈ Ici 1
Tactic:
rw [mem_Ici]
State after:
no goals