-- Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
theorem contDiffAt_log {n : WithTop ℕ∞} {x : ℝ} : ContDiffAt ℝ n log x ↔ x ≠ 0

Proof state:
n : WithTop ℕ∞
x : ℝ
hx✝ : x ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
hx : x < 0
⊢ ContDiffAt ℝ n (log ∘ fun y => -y) x

Tactic:
apply ContDiffAt.comp

Result:
case hg
n : WithTop ℕ∞
x : ℝ
hx✝ : x ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
hx : x < 0
⊢ ContDiffAt ℝ n log (-x)

case hf
n : WithTop ℕ∞
x : ℝ
hx✝ : x ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
hx : x < 0
⊢ ContDiffAt ℝ n (fun y => -y) x

Proof state:
case inr
n : WithTop ℕ∞
x : ℝ
hx✝ : x ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
hx : 0 < x
⊢ ContDiffAt ℝ n log x

Tactic:
exact A x hx

Result:
no goals

Proof state:
case inl
n : WithTop ℕ∞
x : ℝ
hx✝ : x ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
hx : x < 0
⊢ ContDiffAt ℝ n log x

Tactic:
have : ContDiffAt ℝ n (log ∘ (fun y ↦ -y)) x := by
  apply ContDiffAt.comp
  apply A _ (Left.neg_pos_iff.mpr hx)
  apply contDiffAt_id.neg

Result:
case inl
n : WithTop ℕ∞
x : ℝ
hx✝ : x ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
hx : x < 0
this : ContDiffAt ℝ n (log ∘ fun y => -y) x
⊢ ContDiffAt ℝ n log x

Proof state:
case h.e'_9
n : WithTop ℕ∞
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
⊢ y = rexp (log y)

Tactic:
rw [exp_log hy]

Result:
no goals

Proof state:
n : WithTop ℕ∞
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
⊢ ContDiffAt ℝ n log y

Tactic:
apply expPartialHomeomorph.contDiffAt_symm_deriv (f₀' := y) hy.ne' (by simpa)

Result:
case hf₀'
n : WithTop ℕ∞
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
⊢ HasDerivAt (↑expPartialHomeomorph) y (↑expPartialHomeomorph.symm y)

case hf
n : WithTop ℕ∞
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
⊢ ContDiffAt ℝ n (↑expPartialHomeomorph) (↑expPartialHomeomorph.symm y)

Proof state:
case hg
n : WithTop ℕ∞
x : ℝ
hx✝ : x ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
hx : x < 0
⊢ ContDiffAt ℝ n log (-x)

case hf
n : WithTop ℕ∞
x : ℝ
hx✝ : x ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
hx : x < 0
⊢ ContDiffAt ℝ n (fun y => -y) x

Tactic:
apply A _ (Left.neg_pos_iff.mpr hx)

Result:
case hf
n : WithTop ℕ∞
x : ℝ
hx✝ : x ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
hx : x < 0
⊢ ContDiffAt ℝ n (fun y => -y) x

Proof state:
case hf
n : WithTop ℕ∞
x : ℝ
hx✝ : x ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
hx : x < 0
⊢ ContDiffAt ℝ n (fun y => -y) x

Tactic:
apply contDiffAt_id.neg

Result:
no goals

Proof state:
n : WithTop ℕ∞
x : ℝ
hx : x ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
⊢ ContDiffAt ℝ n log x

Tactic:
rcases hx.lt_or_lt with hx | hx

Result:
case inl
n : WithTop ℕ∞
x : ℝ
hx✝ : x ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
hx : x < 0
⊢ ContDiffAt ℝ n log x

case inr
n : WithTop ℕ∞
x : ℝ
hx✝ : x ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
hx : 0 < x
⊢ ContDiffAt ℝ n log x

Proof state:
case h.e'_10.h
n : WithTop ℕ∞
x✝ : ℝ
hx✝ : x✝ ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
hx : x✝ < 0
this : ContDiffAt ℝ n (log ∘ fun y => -y) x✝
x : ℝ
⊢ log x = (log ∘ fun y => -y) x

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_10
n : WithTop ℕ∞
x : ℝ
hx✝ : x ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
hx : x < 0
this : ContDiffAt ℝ n (log ∘ fun y => -y) x
⊢ log = log ∘ fun y => -y

Tactic:
ext x

Result:
case h.e'_10.h
n : WithTop ℕ∞
x✝ : ℝ
hx✝ : x✝ ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
hx : x✝ < 0
this : ContDiffAt ℝ n (log ∘ fun y => -y) x✝
x : ℝ
⊢ log x = (log ∘ fun y => -y) x

Proof state:
case hf
n : WithTop ℕ∞
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
⊢ ContDiffAt ℝ n (↑expPartialHomeomorph) (↑expPartialHomeomorph.symm y)

Tactic:
exact analyticAt_rexp.contDiffAt

Result:
no goals

Proof state:
n : WithTop ℕ∞
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
⊢ y ∈ expPartialHomeomorph.target

Tactic:
simpa

Result:
no goals

Proof state:
n : WithTop ℕ∞
x : ℝ
⊢ ContDiffAt ℝ n log x ↔ x ≠ 0

Tactic:
refine ⟨fun h ↦ continuousAt_log_iff.1 h.continuousAt, fun hx ↦ ?_⟩

Result:
n : WithTop ℕ∞
x : ℝ
hx : x ≠ 0
⊢ ContDiffAt ℝ n log x

Proof state:
case inl
n : WithTop ℕ∞
x : ℝ
hx✝ : x ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
hx : x < 0
this : ContDiffAt ℝ n (log ∘ fun y => -y) x
⊢ ContDiffAt ℝ n log x

Tactic:
convert this

Result:
case h.e'_10
n : WithTop ℕ∞
x : ℝ
hx✝ : x ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
hx : x < 0
this : ContDiffAt ℝ n (log ∘ fun y => -y) x
⊢ log = log ∘ fun y => -y

Proof state:
case hf₀'
n : WithTop ℕ∞
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
⊢ HasDerivAt (↑expPartialHomeomorph) y (↑expPartialHomeomorph.symm y)

Tactic:
convert hasDerivAt_exp (log y)

Result:
case h.e'_9
n : WithTop ℕ∞
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
⊢ y = rexp (log y)