awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
d n : ℕ
inv : Invertible (α := ℝ) (↑d : ℝ)
eq : e = HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _)
h : decide (1 < HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) = true
this : 1 < HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)
⊢ 0 < Real.log (HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ))

Tactic:
exact Real.log_pos this

Premises used: Real.log_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible (α := ℝ) (↑d : ℝ)
eq : e = HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _)
h : decide (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) < -1) = true
rw : 0 < Real.log (HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ))
⊢ 0 < Real.log e

Tactic:
rw [eq, invOf_eq_inv, ← div_eq_mul_inv]

Premises used: div_eq_mul_inv, invOf_eq_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible (α := ℝ) (↑d : ℝ)
eq : e = HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _)
h : decide (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) < -1) = true
⊢ HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ) < -1

Tactic:
exact_mod_cast of_decide_eq_true h

Premises used: of_decide_eq_true
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible (α := ℝ) (↑d : ℝ)
eq : e = HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _)
h : decide (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) < -1) = true
⊢ HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ) < -1

Tactic:
have : (n : ℝ) / d < -1 := by exact_mod_cast of_decide_eq_true h
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible (α := ℝ) (↑d : ℝ)
eq : e = HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _)
h : decide (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) < -1) = true
this : HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ) < -1
⊢ 0 < Real.log (HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ))

Tactic:
Real.log_pos_of_lt_neg_one this

Premises used: Real.log_pos_of_lt_neg_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible (α := ℝ) (↑d : ℝ)
eq : e = HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _)
h : decide (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) < -1) = true
this : HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ) < -1
⊢ 0 < Real.log (HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ))

Tactic:
exact Real.log_pos_of_lt_neg_one this

Premises used: Real.log_pos_of_lt_neg_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
d n : ℕ
inv : Invertible (α := ℝ) (↑d : ℝ)
eq : e = HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _)
h₁ : decide (0 < HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) = true
h₂ : decide (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) < 1) = true
rw : Real.log (HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)) ≠ 0
⊢ Real.log e ≠ 0

Tactic:
rw [eq, invOf_eq_inv, ← div_eq_mul_inv]

Premises used: div_eq_mul_inv, invOf_eq_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
d n : ℕ
inv : Invertible (α := ℝ) (↑d : ℝ)
eq : e = HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _)
h₁ : decide (0 < HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) = true
h₂ : decide (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) < 1) = true
⊢ 0 < HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)

Tactic:
simpa using (Rat.cast_pos (K := ℝ)).2 (of_decide_eq_true h₁)

Premises used: Iff.mpr, of_decide_eq_true, Rat.cast_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
d n : ℕ
inv : Invertible (α := ℝ) (↑d : ℝ)
eq : e = HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _)
h₁ : decide (0 < HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) = true
h₂ : decide (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) < 1) = true
⊢ 0 < HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)

Tactic:
have h₁' : 0 < (n : ℝ) / d := by
      simpa using (Rat.cast_pos (K := ℝ)).2 (of_decide_eq_true h₁)
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
d n : ℕ
inv : Invertible (α := ℝ) (↑d : ℝ)
eq : e = HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _)
h₁ : decide (0 < HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) = true
h₂ : decide (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) < 1) = true
h₁' : 0 < HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ) < 1

Tactic:
simpa using (Rat.cast_lt (K := ℝ)).2 (of_decide_eq_true h₂)

Premises used: Iff.mpr, of_decide_eq_true, Rat.cast_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
d n : ℕ
inv : Invertible (α := ℝ) (↑d : ℝ)
eq : e = HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _)
h₁ : decide (0 < HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) = true
h₂ : decide (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) < 1) = true
h₁' : 0 < HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ) < 1

Tactic:
have h₂' : (n : ℝ) / d < 1 := by
      simpa using (Rat.cast_lt (K := ℝ)).2 (of_decide_eq_true h₂)
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
d n : ℕ
inv : Invertible (α := ℝ) (↑d : ℝ)
eq : e = HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _)
h₁ : decide (0 < HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) = true
h₂ : decide (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) < 1) = true
h₁' : 0 < HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)
h₂' : HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ) < 1
⊢ Real.log (HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)) ≠ 0

Tactic:
ne_of_lt <| Real.log_neg h₁' h₂'

Premises used: Real.log_neg, ne_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
d n : ℕ
inv : Invertible (α := ℝ) (↑d : ℝ)
eq : e = HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _)
h₁ : decide (0 < HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) = true
h₂ : decide (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) < 1) = true
h₁' : 0 < HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)
h₂' : HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ) < 1
⊢ Real.log (HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)) ≠ 0

Tactic:
exact ne_of_lt <| Real.log_neg h₁' h₂'

Premises used: Real.log_neg, ne_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible (α := ℝ) (↑d : ℝ)
eq : e = HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _)
h₁ : decide (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) < 0) = true
h₂ : decide (-1 < HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) = true
rw : Real.log (HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)) ≠ 0
⊢ Real.log e ≠ 0

Tactic:
rw [eq, invOf_eq_inv, ← div_eq_mul_inv]

Premises used: div_eq_mul_inv, invOf_eq_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible (α := ℝ) (↑d : ℝ)
eq : e = HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _)
h₁ : decide (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) < 0) = true
h₂ : decide (-1 < HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) = true
⊢ HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ) < 0

Tactic:
exact_mod_cast of_decide_eq_true h₁

Premises used: of_decide_eq_true
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible (α := ℝ) (↑d : ℝ)
eq : e = HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _)
h₁ : decide (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) < 0) = true
h₂ : decide (-1 < HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) = true
⊢ HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ) < 0

Tactic:
have h₁' : (n : ℝ) / d < 0 := by exact_mod_cast of_decide_eq_true h₁
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible (α := ℝ) (↑d : ℝ)
eq : e = HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _)
h₁ : decide (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) < 0) = true
h₂ : decide (-1 < HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) = true
h₁' : HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ) < 0
⊢ -1 < HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)

Tactic:
exact_mod_cast of_decide_eq_true h₂

Premises used: of_decide_eq_true
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible (α := ℝ) (↑d : ℝ)
eq : e = HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _)
h₁ : decide (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) < 0) = true
h₂ : decide (-1 < HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) = true
h₁' : HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ) < 0
⊢ -1 < HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)

Tactic:
have h₂' : -1 < (n : ℝ) / d := by exact_mod_cast of_decide_eq_true h₂
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible (α := ℝ) (↑d : ℝ)
eq : e = HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _)
h₁ : decide (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) < 0) = true
h₂ : decide (-1 < HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) = true
h₁' : HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ) < 0
h₂' : -1 < HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)
⊢ Real.log (HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)) ≠ 0

Tactic:
ne_of_lt <| Real.log_neg_of_lt_zero h₁' h₂'

Premises used: Real.log_neg_of_lt_zero, ne_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Basic
Goal:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible (α := ℝ) (↑d : ℝ)
eq : e = HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _)
h₁ : decide (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) < 0) = true
h₂ : decide (-1 < HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)) = true
h₁' : HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ) < 0
h₂' : -1 < HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)
⊢ Real.log (HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)) ≠ 0

Tactic:
exact ne_of_lt <| Real.log_neg_of_lt_zero h₁' h₂'

Premises used: Real.log_neg_of_lt_zero, ne_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
hx : 0 < x
⊢ HasStrictDerivAt log (rexp (log x))⁻¹ x

Tactic:
have : HasStrictDerivAt log (exp <| log x)⁻¹ x :=
    (hasStrictDerivAt_exp <| log x).of_local_left_inverse (continuousAt_log hx.ne')
        (ne_of_gt <| exp_pos _) <|
      Eventually.mono (lt_mem_nhds hx) @exp_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
hx : 0 < x
this : HasStrictDerivAt log (rexp (log x))⁻¹ x
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : HasStrictDerivAt log x⁻¹ x), HasStrictDerivAt log x⁻¹ x
⊢ HasStrictDerivAt log x⁻¹ x

Tactic:
rwa [exp_log hx] at this

Premises used: Real.exp_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
hx : x ≠ 0
inl : ∀ (hx : x < 0), HasStrictDerivAt log x⁻¹ x
inr : ∀ (hx : 0 < x), HasStrictDerivAt log x⁻¹ x
⊢ HasStrictDerivAt log x⁻¹ x

Tactic:
rcases hx.lt_or_gt with hx | hx

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt (log ∘ Neg.neg) ((-x)⁻¹ * -1) x

Tactic:
(hasStrictDerivAt_log_of_pos (neg_pos.mpr hx)).comp x (hasStrictDerivAt_neg x)

Premises used: Iff.mpr, neg_pos, HasStrictDerivAt.comp, Real.hasStrictDerivAt_log_of_pos, hasStrictDerivAt_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : x < 0
h : log = log ∘ Neg.neg
h₁ : x⁻¹ = (-x)⁻¹ * -1
⊢ HasStrictDerivAt log x⁻¹ x

Tactic:
convert! (hasStrictDerivAt_log_of_pos (neg_pos.mpr hx)).comp x (hasStrictDerivAt_neg x) using 1

Premises used: Iff.mpr, neg_pos, HasStrictDerivAt.comp, Real.hasStrictDerivAt_log_of_pos, hasStrictDerivAt_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : x < 0
h : ∀ (y : ℝ), log y = (log ∘ Neg.neg) y
⊢ log = log ∘ Neg.neg

Tactic:
ext y
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : x < 0
y : ℝ
⊢ log y = (log ∘ Neg.neg) y

Tactic:
(log_neg_eq_log y).symm

Premises used: Real.log_neg_eq_log, Real.log, dite, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : x < 0
y : ℝ
⊢ log y = (log ∘ Neg.neg) y

Tactic:
exact (log_neg_eq_log y).symm

Premises used: Real.log_neg_eq_log, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : x < 0
⊢ x⁻¹ = (-x)⁻¹ * -1

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : 0 < x
⊢ HasStrictDerivAt log x⁻¹ x

Tactic:
hasStrictDerivAt_log_of_pos hx

Premises used: Real.hasStrictDerivAt_log_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : 0 < x
⊢ HasStrictDerivAt log x⁻¹ x

Tactic:
exact hasStrictDerivAt_log_of_pos hx

Premises used: Real.hasStrictDerivAt_log_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
hx : x ≠ 0
⊢ HasDerivAt log x⁻¹ x

Tactic:
(hasStrictDerivAt_log hx).hasDerivAt

Premises used: Real.hasStrictDerivAt_log, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
hx : x ≠ 0
⊢ DifferentiableAt ℝ log x

Tactic:
(hasDerivAt_log hx).differentiableAt

Premises used: HasDerivAt.differentiableAt, Real.hasDerivAt_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
⊢ DifferentiableOn ℝ log {0}ᶜ

Tactic:
fun _x hx =>
  (differentiableAt_log hx).differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, Real.differentiableAt_log, DifferentiableOn
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
⊢ DifferentiableAt ℝ log x ↔ x ≠ 0

Tactic:
⟨fun h => continuousAt_log_iff.1 h.continuousAt, differentiableAt_log⟩

Premises used: DifferentiableAt.continuousAt, Real.differentiableAt_log, Real.continuousAt_log_iff, Iff.intro, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
hx : x = 0
rw : 0 = x⁻¹
rw₁ : Eq (α := ℝ) 0 0⁻¹
rw₂ rw₃ : Eq (α := ℝ) 0 0
⊢ deriv log x = x⁻¹

Tactic:
rw [deriv_zero_of_not_differentiableAt (differentiableAt_log_iff.not_left.2 hx), hx, inv_zero]

Premises used: Iff.mpr, deriv_zero_of_not_differentiableAt, inv_zero, Real.differentiableAt_log_iff, Iff.not_left
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
⊢ deriv log = Inv.inv

Tactic:
funext deriv_log

Premises used: Real.deriv_log, funext
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
n : ℕ∞ω
x : ℝ
⊢ ContDiffAt ℝ n log x ↔ x ≠ 0

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

Premises used: Real.continuousAt_log_iff, Iff.intro, Iff.mp, ContDiffAt.continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
n : ℕ∞ω
x : ℝ
refine : ∀ (hx : x ≠ 0), ContDiffAt ℝ n log x
⊢ ContDiffAt ℝ n log x ↔ x ≠ 0

Tactic:
refine ⟨fun h ↦ continuousAt_log_iff.1 h.continuousAt, fun hx ↦ ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
n : ℕ∞ω
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
⊢ y ∈ expPartialHomeomorph.target

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
n : ℕ∞ω
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
hf₀' : HasDerivAt (↑expPartialHomeomorph : ℝ → ℝ) y ((↑expPartialHomeomorph.symm : ℝ → ℝ) y)
hf : ContDiffAt ℝ n (↑expPartialHomeomorph : ℝ → ℝ) ((↑expPartialHomeomorph.symm : ℝ → ℝ) y)
⊢ ContDiffAt ℝ n log y

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

Premises used: OpenPartialHomeomorph.contDiffAt_symm_deriv, LT.lt.ne', Real.expPartialHomeomorph
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
n : ℕ∞ω
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
⊢ HasDerivAt rexp (rexp (log y)) (log y)

Tactic:
hasDerivAt_exp (log y)

Premises used: Real.log, Real.hasDerivAt_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
n : ℕ∞ω
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
h : y = rexp (log y)
⊢ HasDerivAt (↑expPartialHomeomorph : ℝ → ℝ) y ((↑expPartialHomeomorph.symm : ℝ → ℝ) y)

Tactic:
convert! hasDerivAt_exp (log y)

Premises used: Real.log, Real.hasDerivAt_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
n : ℕ∞ω
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
h h₁ : y = y
⊢ y = rexp (log y)

Tactic:
rw [exp_log hy]

Premises used: Real.exp_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
n : ℕ∞ω
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
⊢ ContDiffAt ℝ n (↑expPartialHomeomorph : ℝ → ℝ) ((↑expPartialHomeomorph.symm : ℝ → ℝ) y)

Tactic:
analyticAt_rexp.contDiffAt

Premises used: analyticAt_rexp, OpenPartialHomeomorph.toFun', Real.exp, AnalyticAt.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
n : ℕ∞ω
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
⊢ ContDiffAt ℝ n (↑expPartialHomeomorph : ℝ → ℝ) ((↑expPartialHomeomorph.symm : ℝ → ℝ) y)

Tactic:
exact analyticAt_rexp.contDiffAt

Premises used: analyticAt_rexp, AnalyticAt.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
n : ℕ∞ω
x : ℝ
hx : x ≠ 0
⊢ ∀ (y : ℝ) (hy : 0 < y), ContDiffAt ℝ n log y

Tactic:
have A y (hy : 0 < y) : ContDiffAt ℝ n log y := by
    apply expPartialHomeomorph.contDiffAt_symm_deriv (f₀' := y) hy.ne' (by simpa)
    · convert! hasDerivAt_exp (log y)
      rw [exp_log hy]
    · exact analyticAt_rexp.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
n : ℕ∞ω
x : ℝ
hx : x ≠ 0
A : ∀ (y : ℝ) (hy : 0 < y), ContDiffAt ℝ n log y
inl : ∀ (hx : x < 0), ContDiffAt ℝ n log x
inr : ∀ (hx : 0 < x), ContDiffAt ℝ n log x
⊢ ContDiffAt ℝ n log x

Tactic:
rcases hx.lt_or_gt with hx | hx

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
n : ℕ∞ω
x : ℝ
hx_1 : x ≠ 0
A : ∀ (y : ℝ) (hy : 0 < y), ContDiffAt ℝ n log y
hx : x < 0
hg : ContDiffAt ℝ n log (-x)
hf : ContDiffAt ℝ (F := ℝ) n (fun (y : ℝ) ↦ -y) x
⊢ ContDiffAt ℝ n (log ∘ fun (y : ℝ) ↦ -y) x

Tactic:
apply ContDiffAt.comp

Premises used: ContDiffAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
n : ℕ∞ω
x : ℝ
hx_1 : x ≠ 0
A : ∀ (y : ℝ) (hy : 0 < y), ContDiffAt ℝ n log y
hx : x < 0
⊢ ContDiffAt ℝ n log (-x)

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

Premises used: Iff.mpr, Left.neg_pos_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
n : ℕ∞ω
x : ℝ
hx_1 : x ≠ 0
A : ∀ (y : ℝ) (hy : 0 < y), ContDiffAt ℝ n log y
hx : x < 0
⊢ ContDiffAt ℝ (F := ℝ) n (fun (y : ℝ) ↦ -y) x

Tactic:
apply contDiffAt_id.neg

Premises used: contDiffAt_id, ContDiffAt.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
n : ℕ∞ω
x : ℝ
hx_1 : x ≠ 0
A : ∀ (y : ℝ) (hy : 0 < y), ContDiffAt ℝ n log y
hx : x < 0
⊢ ContDiffAt ℝ n (log ∘ fun (y : ℝ) ↦ -y) 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
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
n : ℕ∞ω
x : ℝ
hx_1 : x ≠ 0
A : ∀ (y : ℝ) (hy : 0 < y), ContDiffAt ℝ n log y
hx : x < 0
this : ContDiffAt ℝ n (log ∘ fun (y : ℝ) ↦ -y) x
⊢ ContDiffAt ℝ n (log ∘ fun (y : ℝ) ↦ -y) x

Tactic:
this
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
n : ℕ∞ω
x : ℝ
hx_1 : x ≠ 0
A : ∀ (y : ℝ) (hy : 0 < y), ContDiffAt ℝ n log y
hx : x < 0
this : ContDiffAt ℝ n (log ∘ fun (y : ℝ) ↦ -y) x
h : log = log ∘ fun (y : ℝ) ↦ -y
⊢ ContDiffAt ℝ n log x

Tactic:
convert! this
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
n : ℕ∞ω
x : ℝ
hx_1 : x ≠ 0
A : ∀ (y : ℝ) (hy : 0 < y), ContDiffAt ℝ n log y
hx : x < 0
this : ContDiffAt ℝ n (log ∘ fun (y : ℝ) ↦ -y) x
h : ∀ (x : ℝ), log x = (log ∘ fun (y : ℝ) ↦ -y) x
⊢ log = log ∘ fun (y : ℝ) ↦ -y

Tactic:
ext x
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
n : ℕ∞ω
x_1 : ℝ
hx_1 : x_1 ≠ 0
A : ∀ (y : ℝ) (hy : 0 < y), ContDiffAt ℝ n log y
hx : x_1 < 0
this : ContDiffAt ℝ n (log ∘ fun (y : ℝ) ↦ -y) x_1
x : ℝ
⊢ log x = (log ∘ fun (y : ℝ) ↦ -y) x

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
n : ℕ∞ω
x : ℝ
hx_1 : x ≠ 0
A : ∀ (y : ℝ) (hy : 0 < y), ContDiffAt ℝ n log y
hx : 0 < x
⊢ ContDiffAt ℝ n log x

Tactic:
A x hx
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
n : ℕ∞ω
x : ℝ
hx_1 : x ≠ 0
A : ∀ (y : ℝ) (hy : 0 < y), ContDiffAt ℝ n log y
hx : 0 < x
⊢ ContDiffAt ℝ n log x

Tactic:
exact A x hx
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
n : ℕ∞ω
x : ℝ
hx : Membership.mem (γ := Set ℝ) {0}ᶜ x
⊢ ¬x = 0

Tactic:
push _ ∈ _ at hx
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
n : ℕ∞ω
x : ℝ
hx : ¬x = 0
⊢ ContDiffWithinAt ℝ n log {0}ᶜ x

Tactic:
(contDiffAt_log.2 hx).contDiffWithinAt

Premises used: Iff.mpr, Real.contDiffAt_log, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
n : ℕ∞ω
x : ℝ
hx : ¬x = 0
⊢ ContDiffWithinAt ℝ n log {0}ᶜ x

Tactic:
exact (contDiffAt_log.2 hx).contDiffWithinAt

Premises used: Iff.mpr, Real.contDiffAt_log, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
f : ℝ → ℝ
x f' : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0
rw : HasDerivWithinAt (fun (y : ℝ) ↦ Real.log (f y)) ((f x)⁻¹ * f') s x
⊢ HasDerivWithinAt (fun (y : ℝ) ↦ Real.log (f y)) (f' / f x) s x

Tactic:
rw [div_eq_inv_mul]

Premises used: div_eq_inv_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
f : ℝ → ℝ
x f' : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0
⊢ HasDerivWithinAt (fun (y : ℝ) ↦ Real.log (f y)) ((f x)⁻¹ * f') s x

Tactic:
(hasDerivAt_log hx).comp_hasDerivWithinAt x hf

Premises used: Real.log, dite, Real.hasDerivAt_log, HasDerivAt.comp_hasDerivWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
f : ℝ → ℝ
x f' : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0
⊢ HasDerivWithinAt (fun (y : ℝ) ↦ Real.log (f y)) ((f x)⁻¹ * f') s x

Tactic:
exact (hasDerivAt_log hx).comp_hasDerivWithinAt x hf

Premises used: Real.hasDerivAt_log, HasDerivAt.comp_hasDerivWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
f : ℝ → ℝ
x f' : ℝ
hf : HasDerivAt f f' x
hx : f x ≠ 0
rw :
  ∀ (hf : HasDerivWithinAt f f' Set.univ x) (hx : f x ≠ 0),
    HasDerivWithinAt (fun (y : ℝ) ↦ Real.log (f y)) (f' / f x) Set.univ x
⊢ HasDerivAt (fun (y : ℝ) ↦ Real.log (f y)) (f' / f x) x

Tactic:
rw [← hasDerivWithinAt_univ] at *

Premises used: hasDerivWithinAt_univ
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
f : ℝ → ℝ
x f' : ℝ
hf : HasDerivWithinAt f f' Set.univ x
hx : f x ≠ 0
⊢ HasDerivWithinAt (fun (y : ℝ) ↦ Real.log (f y)) (f' / f x) Set.univ x

Tactic:
hf.log hx

Premises used: HasDerivWithinAt.log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
f : ℝ → ℝ
x f' : ℝ
hf : HasDerivWithinAt f f' Set.univ x
hx : f x ≠ 0
⊢ HasDerivWithinAt (fun (y : ℝ) ↦ Real.log (f y)) (f' / f x) Set.univ x

Tactic:
exact hf.log hx

Premises used: HasDerivWithinAt.log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
f : ℝ → ℝ
x f' : ℝ
hf : HasStrictDerivAt f f' x
hx : f x ≠ 0
rw : HasStrictDerivAt (fun (y : ℝ) ↦ Real.log (f y)) ((f x)⁻¹ * f') x
⊢ HasStrictDerivAt (fun (y : ℝ) ↦ Real.log (f y)) (f' / f x) x

Tactic:
rw [div_eq_inv_mul]

Premises used: div_eq_inv_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
f : ℝ → ℝ
x f' : ℝ
hf : HasStrictDerivAt f f' x
hx : f x ≠ 0
⊢ HasStrictDerivAt (fun (y : ℝ) ↦ Real.log (f y)) ((f x)⁻¹ * f') x

Tactic:
(hasStrictDerivAt_log hx).comp x hf

Premises used: Real.hasStrictDerivAt_log, Real.log, dite, HasStrictDerivAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
f : ℝ → ℝ
x f' : ℝ
hf : HasStrictDerivAt f f' x
hx : f x ≠ 0
⊢ HasStrictDerivAt (fun (y : ℝ) ↦ Real.log (f y)) ((f x)⁻¹ * f') x

Tactic:
exact (hasStrictDerivAt_log hx).comp x hf

Premises used: Real.hasStrictDerivAt_log, HasStrictDerivAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
f : ℝ → ℝ
x : ℝ
s : Set ℝ
hf : DifferentiableWithinAt ℝ f s x
hx : f x ≠ 0
hxs : UniqueDiffWithinAt ℝ s x
⊢ derivWithin (fun (x : ℝ) ↦ Real.log (f x)) s x = derivWithin f s x / f x

Tactic:
(hf.hasDerivWithinAt.log hx).derivWithin hxs

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
f : ℝ → ℝ
x : ℝ
hf : DifferentiableAt ℝ f x
hx : f x ≠ 0
⊢ deriv (fun (x : ℝ) ↦ Real.log (f x)) x = deriv f x / f x

Tactic:
(hf.hasDerivAt.log hx).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.log