x : ℝ
n : ℕ∞
this : ContDiffOn ℝ ⊤ log ({0}ᶜ)
⊢ ContDiffOn ℝ n log ({0}ᶜ)

case this
x : ℝ
n : ℕ∞
⊢ ContDiffOn ℝ ⊤ log ({0}ᶜ)
x : ℝ
n : ℕ∞
⊢ ContDiffOn ℝ n log ({0}ᶜ)
suffices : ContDiffOn ℝ ⊤ log ({0}ᶜ)
case this
x : ℝ
n : ℕ∞
⊢ ContDiffOn ℝ ⊤ log ({0}ᶜ)
x : ℝ
n : ℕ∞
this : ContDiffOn ℝ ⊤ log ({0}ᶜ)
⊢ ContDiffOn ℝ n log ({0}ᶜ)

case this
x : ℝ
n : ℕ∞
⊢ ContDiffOn ℝ ⊤ log ({0}ᶜ)
exact this.of_le le_top
case this
x : ℝ
n : ℕ∞
⊢ DifferentiableOn ℝ log ({0}ᶜ) ∧ ContDiffOn ℝ ⊤ (deriv log) ({0}ᶜ)
case this
x : ℝ
n : ℕ∞
⊢ ContDiffOn ℝ ⊤ log ({0}ᶜ)
refine' (contDiffOn_top_iff_deriv_of_open isOpen_compl_singleton).2 _
no goals
case this
x : ℝ
n : ℕ∞
⊢ DifferentiableOn ℝ log ({0}ᶜ) ∧ ContDiffOn ℝ ⊤ (deriv log) ({0}ᶜ)
simp [differentiableOn_log, contDiffOn_inv]