awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
a b : ℝ
n : ℕ
ha : a ≠ 0
h :
  ∀ (a_1 : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 0 < x) x} x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ |
              (fun (x : ℝ) ↦
                  Eq (α := ℝ) (((fun (x : ℝ) ↦ x ^ n / (a * rexp x + b)) ∘ log) x)
                    ((fun (x : ℝ) ↦ log x ^ n / (a * x + b)) x))
                x}
            x}
      a_1
⊢ EventuallyEq (β := ℝ) atTop ((fun (x : ℝ) ↦ x ^ n / (a * rexp x + b)) ∘ log) fun (x : ℝ) ↦ log x ^ n / (a * x + b)
have h₁ : ∀ (a_1 : ℝ), 0 < a_1 → ((fun (x : ℝ) ↦ x ^ n / (a * rexp x + b)) ∘ log) a_1 = log a_1 ^ n / (a * a_1 + b)
Tactic: filter_upwards [eventually_gt_atTop (0 : ℝ)] with x hx using by simp [exp_log hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
n : ℕ
⊢ Asymptotics.IsLittleO (E := ℝ) atTop (fun (x : ℝ) ↦ log x ^ n) id
have rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x ^ n / id x) atTop (𝓝 0)
Tactic: rw [Asymptotics.isLittleO_iff_tendsto']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
n : ℕ
rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x ^ n / id x) atTop (𝓝 0)
⊢ Asymptotics.IsLittleO (E := ℝ) atTop (fun (x : ℝ) ↦ log x ^ n) id
have rw₁ : ∀ᶠ (x : ℝ) in atTop, id x = 0 → log x ^ n = 0
Tactic: rw [Asymptotics.isLittleO_iff_tendsto']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
n : ℕ
⊢ ∀ᶠ (x : ℝ) in atTop, id x = 0 → log x ^ n = 0
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ≠ 0) x} x →
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ id x = 0 → log x ^ n = 0) x} x}
    a
Tactic: filter_upwards [eventually_ne_atTop (0 : ℝ)] with x h₁ h₂ using (h₁ h₂).elim
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
n : ℕ
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ≠ 0) x} x →
          Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ id x = 0 → log x ^ n = 0) x} x}
      a
⊢ ∀ᶠ (x : ℝ) in atTop, id x = 0 → log x ^ n = 0
have h₁ : ∀ (a : ℝ), a ≠ 0 → id a = 0 → log a ^ n = 0
Tactic: filter_upwards [eventually_ne_atTop (0 : ℝ)] with x h₁ h₂ using (h₁ h₂).elim
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
c : ℝ
⊢ Asymptotics.IsLittleO (E := ℝ) atTop (fun (x : ℝ) ↦ c) log
have refine : ∀ᶠ (x : ℝ) in atTop, log x = 0 → c = 0
Tactic: refine Asymptotics.isLittleO_of_tendsto' ?_
    <| Tendsto.div_atTop (a := c) (by simp) tendsto_log_atTop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
c : ℝ
⊢ ∀ᶠ (x : ℝ) in atTop, log x = 0 → c = 0
have h : ∀ (x : ℝ) (hx : 1 < x), log x = 0 → c = 0
Tactic: filter_upwards [eventually_gt_atTop 1] with x hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
Goal:
y : ℝ
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ log (x + y) - log x) atTop (𝓝 0)
have this : Tendsto (fun (x : ℝ) ↦ 1 + y / x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 1 0))
Tactic: have : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0)) :=
    tendsto_const_nhds.add (tendsto_const_nhds.div_atTop tendsto_id)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
y : ℝ
this : Tendsto (fun (x : ℝ) ↦ 1 + y / x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 1 0))
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ log (x + y) - log x) atTop (𝓝 0)
have rw : Tendsto (α := ℝ) (rexp ∘ fun (x : ℝ) ↦ log (x + y) - log x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 1 0))
Tactic: rw [← comap_exp_nhds_exp, exp_zero, tendsto_comap_iff, ← add_zero (1 : ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
y : ℝ
this : Tendsto (fun (x : ℝ) ↦ 1 + y / x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 1 0))
⊢ Tendsto (α := ℝ) (rexp ∘ fun (x : ℝ) ↦ log (x + y) - log x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 1 0))
have refine : (fun (x : ℝ) ↦ 1 + y / x) =ᶠ[atTop] rexp ∘ fun (x : ℝ) ↦ log (x + y) - log x
Tactic: refine this.congr' ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
y : ℝ
this : Tendsto (fun (x : ℝ) ↦ 1 + y / x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 1 0))
⊢ (fun (x : ℝ) ↦ 1 + y / x) =ᶠ[atTop] rexp ∘ fun (x : ℝ) ↦ log (x + y) - log x
have h : ∀ (x : ℝ) (hx₀ : 0 < x) (hxy : -y < x), 1 + y / x = (rexp ∘ fun (x : ℝ) ↦ log (x + y) - log x) x
Tactic: filter_upwards [eventually_gt_atTop (0 : ℝ), eventually_gt_atTop (-y)] with x hx₀ hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
y : ℝ
this : Tendsto (fun (x : ℝ) ↦ 1 + y / x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 1 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 1 + y / x = (rexp ∘ fun (x : ℝ) ↦ log (x + y) - log x) x
have h : x ≠ 0
Tactic: rw [comp_apply, exp_sub, exp_log, exp_log, one_add_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
y : ℝ
this : Tendsto (fun (x : ℝ) ↦ 1 + y / x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 1 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
h : x ≠ 0
h₁ : 0 < x
⊢ 1 + y / x = (rexp ∘ fun (x : ℝ) ↦ log (x + y) - log x) x
have h₂ : 0 < x + y
Tactic: rw [comp_apply, exp_sub, exp_log, exp_log, one_add_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
y : ℝ
this : Tendsto (fun (x : ℝ) ↦ 1 + y / x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 1 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ x ≠ 0
have linarith : x = 0 → 0 - x + (x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
y : ℝ
this : Tendsto (fun (x : ℝ) ↦ 1 + y / x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 1 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 0 < x
have linarith : x ≤ 0 → 0 - x + (x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
y : ℝ
this : Tendsto (fun (x : ℝ) ↦ 1 + y / x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 1 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 0 < x + y
have linarith : x + y ≤ 0 → -y - x + (x + y - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
e : ℝ
n : ℕ
h : NormNum.IsNat e n
⊢ 0 ≤ Real.log e
have rw : 0 ≤ Real.log (↑n : ℝ)
Tactic: rw [NormNum.IsNat.to_eq h rfl]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
e : ℝ
n : ℕ
h : NormNum.IsNat e n
w : Nat.blt 1 n = true
⊢ 0 < Real.log e
have rw : 0 < Real.log (↑n : ℝ)
Tactic: rw [NormNum.IsNat.to_eq h rfl]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
e : ℝ
n : ℕ
h : NormNum.IsNat e n
w : Nat.blt 1 n = true
⊢ 0 < Real.log (↑n : ℝ)
have hx : LT.lt (α := ℝ) 1 (↑n : ℝ)
Tactic: apply Real.log_pos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
⊢ 0 ≤ Real.log e
have rw : 0 ≤ Real.log (-(↑n : ℝ))
Tactic: rw [NormNum.IsInt.neg_to_eq h rfl]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 0 < Real.log e
have rw : 0 < Real.log (-(↑n : ℝ))
Tactic: rw [NormNum.IsInt.neg_to_eq h rfl]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 0 < Real.log (-(↑n : ℝ))
have rw : 0 < Real.log (↑n : ℝ)
Tactic: rw [Real.log_neg_eq_log]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
Goal:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 0 < Real.log (↑n : ℝ)
have hx : LT.lt (α := ℝ) 1 (↑n : ℝ)
Tactic: apply Real.log_pos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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
⊢ 0 < Real.log e
have rw : 0 < Real.log (HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ))
Tactic: rw [eq, invOf_eq_inv, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
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
⊢ 0 < Real.log (HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ))
have this : 1 < HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)
Tactic: have : 1 < (n : ℝ) / d := by
      simpa using (Rat.cast_lt (K := ℝ)).2 (of_decide_eq_true h)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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
⊢ 0 < Real.log e
have rw : 0 < Real.log (HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ))
Tactic: rw [eq, invOf_eq_inv, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
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
⊢ 0 < Real.log (HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ))
have this : HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ) < -1
Tactic: have : (n : ℝ) / d < -1 := by exact_mod_cast of_decide_eq_true h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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
⊢ Real.log e ≠ 0
have rw : Real.log (HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)) ≠ 0
Tactic: rw [eq, invOf_eq_inv, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
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
⊢ Real.log (HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)) ≠ 0
have h₁' : 0 < HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)
Tactic: have h₁' : 0 < (n : ℝ) / d := by
      simpa using (Rat.cast_pos (K := ℝ)).2 (of_decide_eq_true h₁)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
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 : ℝ)
⊢ Real.log (HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)) ≠ 0
have h₂' : HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ) < 1
Tactic: have h₂' : (n : ℝ) / d < 1 := by
      simpa using (Rat.cast_lt (K := ℝ)).2 (of_decide_eq_true h₂)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (goal)
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
⊢ Real.log e ≠ 0
have rw : Real.log (HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)) ≠ 0
Tactic: rw [eq, invOf_eq_inv, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
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
⊢ Real.log (HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)) ≠ 0
have h₁' : HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ) < 0
Tactic: have h₁' : (n : ℝ) / d < 0 := by exact_mod_cast of_decide_eq_true h₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Basic (hypothesis)
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
⊢ Real.log (HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)) ≠ 0
have h₂' : -1 < HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)
Tactic: have h₂' : -1 < (n : ℝ) / d := by exact_mod_cast of_decide_eq_true h₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (hypothesis)
Goal:
x : ℝ
hx : 0 < x
⊢ HasStrictDerivAt log x⁻¹ x
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
hx : 0 < x
this : HasStrictDerivAt log (rexp (log x))⁻¹ x
⊢ HasStrictDerivAt log x⁻¹ x
have rwa : ∀ (this : HasStrictDerivAt log x⁻¹ x), HasStrictDerivAt log x⁻¹ x
Tactic: rwa [exp_log hx] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
hx : x ≠ 0
⊢ HasStrictDerivAt log x⁻¹ x
have inl : ∀ (hx : x < 0), HasStrictDerivAt log x⁻¹ x
Tactic: rcases hx.lt_or_gt with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
hx : x ≠ 0
inl : ∀ (hx : x < 0), HasStrictDerivAt log x⁻¹ x
⊢ HasStrictDerivAt log x⁻¹ x
have inr : ∀ (hx : 0 < x), HasStrictDerivAt log x⁻¹ x
Tactic: rcases hx.lt_or_gt with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt log x⁻¹ x
have h : log = log ∘ Neg.neg
Tactic: convert! (hasStrictDerivAt_log_of_pos (neg_pos.mpr hx)).comp x (hasStrictDerivAt_neg x) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : x < 0
h : log = log ∘ Neg.neg
⊢ HasStrictDerivAt log x⁻¹ x
have h₁ : x⁻¹ = (-x)⁻¹ * -1
Tactic: convert! (hasStrictDerivAt_log_of_pos (neg_pos.mpr hx)).comp x (hasStrictDerivAt_neg x) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : x < 0
⊢ log = log ∘ Neg.neg
have h : ∀ (y : ℝ), log y = (log ∘ Neg.neg) y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
hx : x = 0
⊢ deriv log x = x⁻¹
have rw : 0 = x⁻¹
Tactic: rw [deriv_zero_of_not_differentiableAt (differentiableAt_log_iff.not_left.2 hx), hx, inv_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
hx : x = 0
rw : 0 = x⁻¹
⊢ deriv log x = x⁻¹
have rw₁ : Eq (α := ℝ) 0 0⁻¹
Tactic: rw [deriv_zero_of_not_differentiableAt (differentiableAt_log_iff.not_left.2 hx), hx, inv_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
hx : x = 0
rw : 0 = x⁻¹
rw₁ : Eq (α := ℝ) 0 0⁻¹
⊢ deriv log x = x⁻¹
have rw₂ : Eq (α := ℝ) 0 0
Tactic: rw [deriv_zero_of_not_differentiableAt (differentiableAt_log_iff.not_left.2 hx), hx, inv_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
n : ℕ∞ω
x : ℝ
⊢ ContDiffAt ℝ n log x ↔ x ≠ 0
have refine : ∀ (hx : x ≠ 0), ContDiffAt ℝ n log x
Tactic: refine ⟨fun h ↦ continuousAt_log_iff.1 h.continuousAt, fun hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
n : ℕ∞ω
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
⊢ ContDiffAt ℝ n log y
have hf₀' : HasDerivAt (↑expPartialHomeomorph : ℝ → ℝ) y ((↑expPartialHomeomorph.symm : ℝ → ℝ) y)
Tactic: apply expPartialHomeomorph.contDiffAt_symm_deriv (f₀' := y) hy.ne' (by simpa)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
n : ℕ∞ω
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
hf₀' : HasDerivAt (↑expPartialHomeomorph : ℝ → ℝ) y ((↑expPartialHomeomorph.symm : ℝ → ℝ) y)
⊢ ContDiffAt ℝ n log y
have hf : ContDiffAt ℝ n (↑expPartialHomeomorph : ℝ → ℝ) ((↑expPartialHomeomorph.symm : ℝ → ℝ) y)
Tactic: apply expPartialHomeomorph.contDiffAt_symm_deriv (f₀' := y) hy.ne' (by simpa)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
n : ℕ∞ω
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
⊢ HasDerivAt (↑expPartialHomeomorph : ℝ → ℝ) y ((↑expPartialHomeomorph.symm : ℝ → ℝ) y)
have h : y = rexp (log y)
Tactic: convert! hasDerivAt_exp (log y)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
n : ℕ∞ω
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
⊢ y = rexp (log y)
have h : y = y
Tactic: rw [exp_log hy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (hypothesis)
Goal:
n : ℕ∞ω
x : ℝ
hx : x ≠ 0
⊢ ContDiffAt ℝ n log x
have A : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
n : ℕ∞ω
x : ℝ
hx : x ≠ 0
A : ∀ (y : ℝ) (hy : 0 < y), ContDiffAt ℝ n log y
⊢ ContDiffAt ℝ n log x
have inl : ∀ (hx : x < 0), ContDiffAt ℝ n log x
Tactic: rcases hx.lt_or_gt with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
n : ℕ∞ω
x : ℝ
hx : x ≠ 0
A : ∀ (y : ℝ) (hy : 0 < y), ContDiffAt ℝ n log y
inl : ∀ (hx : x < 0), ContDiffAt ℝ n log x
⊢ ContDiffAt ℝ n log x
have inr : ∀ (hx : 0 < x), ContDiffAt ℝ n log x
Tactic: rcases hx.lt_or_gt with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
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
have hg : ContDiffAt ℝ n log (-x)
Tactic: apply ContDiffAt.comp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
n : ℕ∞ω
x : ℝ
hx_1 : x ≠ 0
A : ∀ (y : ℝ) (hy : 0 < y), ContDiffAt ℝ n log y
hx : x < 0
hg : ContDiffAt ℝ n log (-x)
⊢ ContDiffAt ℝ n (log ∘ fun (y : ℝ) ↦ -y) x
have hf : ContDiffAt ℝ (F := ℝ) n (fun (y : ℝ) ↦ -y) x
Tactic: apply ContDiffAt.comp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (hypothesis)
Goal:
n : ℕ∞ω
x : ℝ
hx_1 : x ≠ 0
A : ∀ (y : ℝ) (hy : 0 < y), ContDiffAt ℝ n log y
hx : x < 0
⊢ ContDiffAt ℝ n log x
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
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 x
have h : log = log ∘ fun (y : ℝ) ↦ -y
Tactic: convert! this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
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
⊢ log = log ∘ fun (y : ℝ) ↦ -y
have h : ∀ (x : ℝ), log x = (log ∘ fun (y : ℝ) ↦ -y) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (hypothesis)
Goal:
n : ℕ∞ω
x : ℝ
hx : Membership.mem (γ := Set ℝ) {0}ᶜ x
⊢ ContDiffWithinAt ℝ n log {0}ᶜ x
have hx₁ : ¬x = 0
Tactic: push _ ∈ _ at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
f : ℝ → ℝ
x f' : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0
⊢ HasDerivWithinAt (fun (y : ℝ) ↦ Real.log (f y)) (f' / f x) s x
have rw : HasDerivWithinAt (fun (y : ℝ) ↦ Real.log (f y)) ((f x)⁻¹ * f') s x
Tactic: rw [div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
f : ℝ → ℝ
x f' : ℝ
hf : HasDerivAt f f' x
hx : f x ≠ 0
⊢ HasDerivAt (fun (y : ℝ) ↦ Real.log (f y)) (f' / f x) x
have 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
Tactic: rw [← hasDerivWithinAt_univ] at *
Cleared hypotheses: hf, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
f : ℝ → ℝ
x f' : ℝ
hf : HasStrictDerivAt f f' x
hx : f x ≠ 0
⊢ HasStrictDerivAt (fun (y : ℝ) ↦ Real.log (f y)) (f' / f x) x
have rw : HasStrictDerivAt (fun (y : ℝ) ↦ Real.log (f y)) ((f x)⁻¹ * f') x
Tactic: rw [div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (hypothesis)
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun (x : ℝ) ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)
F' : ℝ → ℝ := fun (x : ℝ) ↦ -x ^ n / (1 - x)
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y
⊢ HasDerivAt F (F' y) y
have this : HasDerivAt F (∑ i ∈ Finset.range n, (↑(i + 1) : ℝ) * y ^ i / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + -1 / (1 - y)) y
Tactic: have : HasDerivAt F ((∑ i ∈ range n, ↑(i + 1) * y ^ i / (↑i + 1)) + (-1) / (1 - y)) y :=
      .add (.fun_sum fun i _ ↦ (hasDerivAt_pow (i + 1) y).div_const ((i : ℝ) + 1))
        (((hasDerivAt_id y).const_sub _).log <| sub_ne_zero.2 hy.2.ne')
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun (x : ℝ) ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)
F' : ℝ → ℝ := fun (x : ℝ) ↦ -x ^ n / (1 - x)
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y
this : HasDerivAt F (∑ i ∈ Finset.range n, (↑(i + 1) : ℝ) * y ^ i / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + -1 / (1 - y)) y
⊢ HasDerivAt F (F' y) y
have h₁ : F' y = ∑ i ∈ Finset.range n, (↑(i + 1) : ℝ) * y ^ i / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + -1 / (1 - y)
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun (x : ℝ) ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)
F' : ℝ → ℝ := fun (x : ℝ) ↦ -x ^ n / (1 - x)
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y
this : HasDerivAt F (∑ i ∈ Finset.range n, (↑(i + 1) : ℝ) * y ^ i / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + -1 / (1 - y)) y
⊢ -y ^ n / (1 - y) = ∑ i ∈ Finset.range n, y ^ i + -1 / (1 - y)
have simp : -(y ^ n * (y - 1)) = y ^ n * (1 - y)
Tactic: simp [field, geom_sum_eq hy.2.ne, sub_ne_zero.2 hy.2.ne, sub_ne_zero.2 hy.2.ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun (x : ℝ) ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)
F' : ℝ → ℝ := fun (x : ℝ) ↦ -x ^ n / (1 - x)
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y
this : HasDerivAt F (∑ i ∈ Finset.range n, (↑(i + 1) : ℝ) * y ^ i / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + -1 / (1 - y)) y
⊢ ∑ i ∈ Finset.range n, y ^ i + -1 / (1 - y) =
    ∑ i ∈ Finset.range n, (↑(i + 1) : ℝ) * y ^ i / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + -1 / (1 - y)
have e_a : ∀ (i : ℕ), y ^ i = (↑(i + 1) : ℝ) * y ^ i / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
Tactic: congr with i
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun (x : ℝ) ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)
F' : ℝ → ℝ := fun (x : ℝ) ↦ -x ^ n / (1 - x)
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y
this : HasDerivAt F (∑ i ∈ Finset.range n, (↑(i + 1) : ℝ) * y ^ i / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + -1 / (1 - y)) y
i : ℕ
⊢ y ^ i = (↑(i + 1) : ℝ) * y ^ i / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
have e_a : y ^ i = HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * y ^ i / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
Tactic: rw [Nat.cast_succ, mul_div_cancel_left₀ _ (Nat.cast_add_one_pos i).ne']