awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
⊢ iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) cos = -iteratedDeriv 0 sin
have zero : ∀ (x : ℂ), iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) cos x = (-iteratedDeriv 0 sin) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
n : ℕ
ih : iteratedDeriv (n + 1) cos = -iteratedDeriv n sin
⊢ iteratedDeriv (n + 1 + 1) cos = -iteratedDeriv (n + 1) sin
have succ : (fun (x : ℂ) ↦ -deriv (iteratedDeriv n sin) x) = -deriv (iteratedDeriv n sin)
Tactic: rw [iteratedDeriv_succ, ih, iteratedDeriv_succ, deriv.neg']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
n : ℕ
ih : iteratedDeriv (n + 1) cos = -iteratedDeriv n sin
⊢ (fun (x : ℂ) ↦ -deriv (iteratedDeriv n sin) x) = -deriv (iteratedDeriv n sin)
have succ : ∀ (x : ℂ), -deriv (iteratedDeriv n sin) x = (-deriv (iteratedDeriv n sin)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
n : ℕ
⊢ iteratedDeriv (n + 1) cos = -iteratedDeriv n sin
have zero : iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) cos = -iteratedDeriv 0 sin
Tactic: induction n with
  | zero => ext; simp
  | succ n ih =>
    rw [iteratedDeriv_succ, ih, iteratedDeriv_succ, deriv.neg']
    ext x
    simp
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
n : ℕ
zero : iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) cos = -iteratedDeriv 0 sin
⊢ iteratedDeriv (n + 1) cos = -iteratedDeriv n sin
have succ : ∀ (n : ℕ) (ih : iteratedDeriv (n + 1) cos = -iteratedDeriv n sin),
  iteratedDeriv (n + 1 + 1) cos = -iteratedDeriv (n + 1) sin
Tactic: induction n with
  | zero => ext; simp
  | succ n ih =>
    rw [iteratedDeriv_succ, ih, iteratedDeriv_succ, deriv.neg']
    ext x
    simp
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
n : ℕ
⊢ iteratedDeriv (2 * n) sin = HPow.hPow (α := (x : ℂ) → ℂ) (-1) n * sin
have zero : iteratedDeriv (HMul.hMul (α := ℕ) 2 0) sin = HPow.hPow (α := (x : ℂ) → ℂ) (β := ℕ) (-1) 0 * sin
Tactic: induction n with
  | zero => simp
  | succ n ih => simp_all [mul_add, pow_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
n : ℕ
zero : iteratedDeriv (HMul.hMul (α := ℕ) 2 0) sin = HPow.hPow (α := (x : ℂ) → ℂ) (β := ℕ) (-1) 0 * sin
⊢ iteratedDeriv (2 * n) sin = HPow.hPow (α := (x : ℂ) → ℂ) (-1) n * sin
have succ : ∀ (n : ℕ) (ih : iteratedDeriv (2 * n) sin = HPow.hPow (α := (x : ℂ) → ℂ) (-1) n * sin),
  iteratedDeriv (2 * (n + 1)) sin = HPow.hPow (α := (x : ℂ) → ℂ) (-1) (n + 1) * sin
Tactic: induction n with
  | zero => simp
  | succ n ih => simp_all [mul_add, pow_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
n : ℕ
⊢ iteratedDeriv (2 * n) cos = HPow.hPow (α := (x : ℂ) → ℂ) (-1) n * cos
have zero : iteratedDeriv (HMul.hMul (α := ℕ) 2 0) cos = HPow.hPow (α := (x : ℂ) → ℂ) (β := ℕ) (-1) 0 * cos
Tactic: induction n with
  | zero => simp
  | succ n ih => simp_all [mul_add, pow_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
n : ℕ
zero : iteratedDeriv (HMul.hMul (α := ℕ) 2 0) cos = HPow.hPow (α := (x : ℂ) → ℂ) (β := ℕ) (-1) 0 * cos
⊢ iteratedDeriv (2 * n) cos = HPow.hPow (α := (x : ℂ) → ℂ) (-1) n * cos
have succ : ∀ (n : ℕ) (ih : iteratedDeriv (2 * n) cos = HPow.hPow (α := (x : ℂ) → ℂ) (-1) n * cos),
  iteratedDeriv (2 * (n + 1)) cos = HPow.hPow (α := (x : ℂ) → ℂ) (-1) (n + 1) * cos
Tactic: induction n with
  | zero => simp
  | succ n ih => simp_all [mul_add, pow_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
⊢ iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) cos = -iteratedDeriv 0 sin
have zero : ∀ (x : ℝ), iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) cos x = (-iteratedDeriv 0 sin) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
n : ℕ
ih : iteratedDeriv (n + 1) cos = -iteratedDeriv n sin
⊢ iteratedDeriv (n + 1 + 1) cos = -iteratedDeriv (n + 1) sin
have succ : (fun (x : ℝ) ↦ -deriv (iteratedDeriv n sin) x) = -deriv (iteratedDeriv n sin)
Tactic: rw [iteratedDeriv_succ, ih, iteratedDeriv_succ, deriv.neg']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
n : ℕ
ih : iteratedDeriv (n + 1) cos = -iteratedDeriv n sin
⊢ (fun (x : ℝ) ↦ -deriv (iteratedDeriv n sin) x) = -deriv (iteratedDeriv n sin)
have succ : ∀ (x : ℝ), -deriv (iteratedDeriv n sin) x = (-deriv (iteratedDeriv n sin)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
n : ℕ
⊢ iteratedDeriv (2 * n) sin = HPow.hPow (α := (x : ℝ) → ℝ) (-1) n * sin
have zero : iteratedDeriv (HMul.hMul (α := ℕ) 2 0) sin = HPow.hPow (α := (x : ℝ) → ℝ) (β := ℕ) (-1) 0 * sin
Tactic: induction n with
  | zero => simp
  | succ n ih => simp_all [mul_add, pow_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
n : ℕ
zero : iteratedDeriv (HMul.hMul (α := ℕ) 2 0) sin = HPow.hPow (α := (x : ℝ) → ℝ) (β := ℕ) (-1) 0 * sin
⊢ iteratedDeriv (2 * n) sin = HPow.hPow (α := (x : ℝ) → ℝ) (-1) n * sin
have succ : ∀ (n : ℕ) (ih : iteratedDeriv (2 * n) sin = HPow.hPow (α := (x : ℝ) → ℝ) (-1) n * sin),
  iteratedDeriv (2 * (n + 1)) sin = HPow.hPow (α := (x : ℝ) → ℝ) (-1) (n + 1) * sin
Tactic: induction n with
  | zero => simp
  | succ n ih => simp_all [mul_add, pow_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
n : ℕ
⊢ iteratedDeriv (2 * n) cos = HPow.hPow (α := (x : ℝ) → ℝ) (-1) n * cos
have zero : iteratedDeriv (HMul.hMul (α := ℕ) 2 0) cos = HPow.hPow (α := (x : ℝ) → ℝ) (β := ℕ) (-1) 0 * cos
Tactic: induction n with
  | zero => simp
  | succ n ih => simp_all [mul_add, pow_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
n : ℕ
zero : iteratedDeriv (HMul.hMul (α := ℕ) 2 0) cos = HPow.hPow (α := (x : ℝ) → ℝ) (β := ℕ) (-1) 0 * cos
⊢ iteratedDeriv (2 * n) cos = HPow.hPow (α := (x : ℝ) → ℝ) (-1) n * cos
have succ : ∀ (n : ℕ) (ih : iteratedDeriv (2 * n) cos = HPow.hPow (α := (x : ℝ) → ℝ) (-1) n * cos),
  iteratedDeriv (2 * (n + 1)) cos = HPow.hPow (α := (x : ℝ) → ℝ) (-1) (n + 1) * cos
Tactic: induction n with
  | zero => simp
  | succ n ih => simp_all [mul_add, pow_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
⊢ logDeriv sin = cot
have h : ∀ (x : ℂ), logDeriv sin x = x.cot
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
⊢ logDeriv sin x = x.cot
have h : (deriv sin / sin) x = x.cot
Tactic: rw [logDeriv, Complex.deriv_sin, Pi.div_apply, Complex.cot]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
h : (deriv sin / sin) x = x.cot
⊢ logDeriv sin x = x.cot
have h₁ : (cos / sin) x = x.cot
Tactic: rw [logDeriv, Complex.deriv_sin, Pi.div_apply, Complex.cot]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
h : (deriv sin / sin) x = x.cot
h₁ : (cos / sin) x = x.cot
⊢ logDeriv sin x = x.cot
have h₂ : cos x / sin x = x.cot
Tactic: rw [logDeriv, Complex.deriv_sin, Pi.div_apply, Complex.cot]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
h : (deriv sin / sin) x = x.cot
h₁ : (cos / sin) x = x.cot
h₂ : cos x / sin x = x.cot
⊢ logDeriv sin x = x.cot
have h₃ : cos x / sin x = cos x / sin x
Tactic: rw [logDeriv, Complex.deriv_sin, Pi.div_apply, Complex.cot]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
⊢ logDeriv sin = cot
have h : ∀ (x : ℝ), logDeriv sin x = x.cot
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℝ
⊢ logDeriv sin x = x.cot
have h : (deriv sin / sin) x = x.cot
Tactic: rw [logDeriv, Real.deriv_sin, Pi.div_apply, Real.cot_eq_cos_div_sin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℝ
h : (deriv sin / sin) x = x.cot
⊢ logDeriv sin x = x.cot
have h₁ : (cos / sin) x = x.cot
Tactic: rw [logDeriv, Real.deriv_sin, Pi.div_apply, Real.cot_eq_cos_div_sin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℝ
h : (deriv sin / sin) x = x.cot
h₁ : (cos / sin) x = x.cot
⊢ logDeriv sin x = x.cot
have h₂ : cos x / sin x = x.cot
Tactic: rw [logDeriv, Real.deriv_sin, Pi.div_apply, Real.cot_eq_cos_div_sin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℝ
h : (deriv sin / sin) x = x.cot
h₁ : (cos / sin) x = x.cot
h₂ : cos x / sin x = x.cot
⊢ logDeriv sin x = x.cot
have h₃ : cos x / sin x = cos x / sin x
Tactic: rw [logDeriv, Real.deriv_sin, Pi.div_apply, Real.cot_eq_cos_div_sin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
⊢ logDeriv cos = -tan
have h : ∀ (x : ℂ), logDeriv cos x = (-tan) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
⊢ logDeriv cos x = (-tan) x
have h : (deriv cos / cos) x = (-tan) x
Tactic: rw [logDeriv, Complex.deriv_cos', Pi.div_apply, Pi.neg_apply, Complex.tan, neg_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
h : (deriv cos / cos) x = (-tan) x
⊢ logDeriv cos x = (-tan) x
have h₁ : HDiv.hDiv (α := (x : ℂ) → ℂ) (fun (x : ℂ) ↦ -sin x) cos x = (-tan) x
Tactic: rw [logDeriv, Complex.deriv_cos', Pi.div_apply, Pi.neg_apply, Complex.tan, neg_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
h : (deriv cos / cos) x = (-tan) x
h₁ : HDiv.hDiv (α := (x : ℂ) → ℂ) (fun (x : ℂ) ↦ -sin x) cos x = (-tan) x
⊢ logDeriv cos x = (-tan) x
have h₂ : -sin x / cos x = (-tan) x
Tactic: rw [logDeriv, Complex.deriv_cos', Pi.div_apply, Pi.neg_apply, Complex.tan, neg_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
h : (deriv cos / cos) x = (-tan) x
h₁ : HDiv.hDiv (α := (x : ℂ) → ℂ) (fun (x : ℂ) ↦ -sin x) cos x = (-tan) x
h₂ : -sin x / cos x = (-tan) x
⊢ logDeriv cos x = (-tan) x
have h₃ : -sin x / cos x = -tan x
Tactic: rw [logDeriv, Complex.deriv_cos', Pi.div_apply, Pi.neg_apply, Complex.tan, neg_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
h : (deriv cos / cos) x = (-tan) x
h₁ : HDiv.hDiv (α := (x : ℂ) → ℂ) (fun (x : ℂ) ↦ -sin x) cos x = (-tan) x
h₂ : -sin x / cos x = (-tan) x
h₃ : -sin x / cos x = -tan x
⊢ logDeriv cos x = (-tan) x
have h₄ : -sin x / cos x = -(sin x / cos x)
Tactic: rw [logDeriv, Complex.deriv_cos', Pi.div_apply, Pi.neg_apply, Complex.tan, neg_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
h : (deriv cos / cos) x = (-tan) x
h₁ : HDiv.hDiv (α := (x : ℂ) → ℂ) (fun (x : ℂ) ↦ -sin x) cos x = (-tan) x
h₂ : -sin x / cos x = (-tan) x
h₃ : -sin x / cos x = -tan x
h₄ : -sin x / cos x = -(sin x / cos x)
⊢ logDeriv cos x = (-tan) x
have h₅ : -(sin x / cos x) = -(sin x / cos x)
Tactic: rw [logDeriv, Complex.deriv_cos', Pi.div_apply, Pi.neg_apply, Complex.tan, neg_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
⊢ logDeriv cos = -tan
have h : ∀ (x : ℝ), logDeriv cos x = (-tan) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℝ
⊢ logDeriv cos x = (-tan) x
have h : (deriv cos / cos) x = (-tan) x
Tactic: rw [logDeriv, Real.deriv_cos', Pi.div_apply, Pi.neg_apply, neg_div, Real.tan_eq_sin_div_cos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℝ
h : (deriv cos / cos) x = (-tan) x
⊢ logDeriv cos x = (-tan) x
have h₁ : HDiv.hDiv (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ -sin x) cos x = (-tan) x
Tactic: rw [logDeriv, Real.deriv_cos', Pi.div_apply, Pi.neg_apply, neg_div, Real.tan_eq_sin_div_cos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℝ
h : (deriv cos / cos) x = (-tan) x
h₁ : HDiv.hDiv (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ -sin x) cos x = (-tan) x
⊢ logDeriv cos x = (-tan) x
have h₂ : -sin x / cos x = (-tan) x
Tactic: rw [logDeriv, Real.deriv_cos', Pi.div_apply, Pi.neg_apply, neg_div, Real.tan_eq_sin_div_cos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℝ
h : (deriv cos / cos) x = (-tan) x
h₁ : HDiv.hDiv (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ -sin x) cos x = (-tan) x
h₂ : -sin x / cos x = (-tan) x
⊢ logDeriv cos x = (-tan) x
have h₃ : -sin x / cos x = -tan x
Tactic: rw [logDeriv, Real.deriv_cos', Pi.div_apply, Pi.neg_apply, neg_div, Real.tan_eq_sin_div_cos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℝ
h : (deriv cos / cos) x = (-tan) x
h₁ : HDiv.hDiv (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ -sin x) cos x = (-tan) x
h₂ : -sin x / cos x = (-tan) x
h₃ : -sin x / cos x = -tan x
⊢ logDeriv cos x = (-tan) x
have h₄ : -(sin x / cos x) = -tan x
Tactic: rw [logDeriv, Real.deriv_cos', Pi.div_apply, Pi.neg_apply, neg_div, Real.tan_eq_sin_div_cos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℝ
h : (deriv cos / cos) x = (-tan) x
h₁ : HDiv.hDiv (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ -sin x) cos x = (-tan) x
h₂ : -sin x / cos x = (-tan) x
h₃ : -sin x / cos x = -tan x
h₄ : -(sin x / cos x) = -tan x
⊢ logDeriv cos x = (-tan) x
have h₅ : -(sin x / cos x) = -(sin x / cos x)
Tactic: rw [logDeriv, Real.deriv_cos', Pi.div_apply, Pi.neg_apply, neg_div, Real.tan_eq_sin_div_cos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
⊢ logDeriv cexp = 1
have h : ∀ (x : ℂ), logDeriv cexp x = 1 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
⊢ logDeriv cexp x = 1 x
have h : (deriv cexp / cexp) x = 1 x
Tactic: rw [logDeriv, Complex.deriv_exp, Pi.div_apply, ← exp_sub, sub_self, exp_zero, Pi.one_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
h : (deriv cexp / cexp) x = 1 x
⊢ logDeriv cexp x = 1 x
have h₁ : (cexp / cexp) x = 1 x
Tactic: rw [logDeriv, Complex.deriv_exp, Pi.div_apply, ← exp_sub, sub_self, exp_zero, Pi.one_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
h : (deriv cexp / cexp) x = 1 x
h₁ : (cexp / cexp) x = 1 x
⊢ logDeriv cexp x = 1 x
have h₂ : cexp x / cexp x = 1 x
Tactic: rw [logDeriv, Complex.deriv_exp, Pi.div_apply, ← exp_sub, sub_self, exp_zero, Pi.one_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
h : (deriv cexp / cexp) x = 1 x
h₁ : (cexp / cexp) x = 1 x
h₂ : cexp x / cexp x = 1 x
⊢ logDeriv cexp x = 1 x
have h₃ : cexp (x - x) = 1 x
Tactic: rw [logDeriv, Complex.deriv_exp, Pi.div_apply, ← exp_sub, sub_self, exp_zero, Pi.one_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
h : (deriv cexp / cexp) x = 1 x
h₁ : (cexp / cexp) x = 1 x
h₂ : cexp x / cexp x = 1 x
h₃ : cexp (x - x) = 1 x
⊢ logDeriv cexp x = 1 x
have h₄ : cexp 0 = 1 x
Tactic: rw [logDeriv, Complex.deriv_exp, Pi.div_apply, ← exp_sub, sub_self, exp_zero, Pi.one_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
h : (deriv cexp / cexp) x = 1 x
h₁ : (cexp / cexp) x = 1 x
h₂ : cexp x / cexp x = 1 x
h₃ : cexp (x - x) = 1 x
h₄ : cexp 0 = 1 x
⊢ logDeriv cexp x = 1 x
have h₅ : Eq (α := ℂ) 1 (1 x)
Tactic: rw [logDeriv, Complex.deriv_exp, Pi.div_apply, ← exp_sub, sub_self, exp_zero, Pi.one_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
h : (deriv cexp / cexp) x = 1 x
h₁ : (cexp / cexp) x = 1 x
h₂ : cexp x / cexp x = 1 x
h₃ : cexp (x - x) = 1 x
h₄ : cexp 0 = 1 x
h₅ : Eq (α := ℂ) 1 (1 x)
⊢ logDeriv cexp x = 1 x
have h₆ : Eq (α := ℂ) 1 1
Tactic: rw [logDeriv, Complex.deriv_exp, Pi.div_apply, ← exp_sub, sub_self, exp_zero, Pi.one_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
⊢ logDeriv rexp = 1
have h : ∀ (x : ℝ), logDeriv rexp x = 1 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℝ
⊢ logDeriv rexp x = 1 x
have h : (deriv rexp / rexp) x = 1 x
Tactic: rw [logDeriv, Real.deriv_exp, Pi.div_apply, ← exp_sub, sub_self, exp_zero, Pi.one_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℝ
h : (deriv rexp / rexp) x = 1 x
⊢ logDeriv rexp x = 1 x
have h₁ : (rexp / rexp) x = 1 x
Tactic: rw [logDeriv, Real.deriv_exp, Pi.div_apply, ← exp_sub, sub_self, exp_zero, Pi.one_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℝ
h : (deriv rexp / rexp) x = 1 x
h₁ : (rexp / rexp) x = 1 x
⊢ logDeriv rexp x = 1 x
have h₂ : rexp x / rexp x = 1 x
Tactic: rw [logDeriv, Real.deriv_exp, Pi.div_apply, ← exp_sub, sub_self, exp_zero, Pi.one_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℝ
h : (deriv rexp / rexp) x = 1 x
h₁ : (rexp / rexp) x = 1 x
h₂ : rexp x / rexp x = 1 x
⊢ logDeriv rexp x = 1 x
have h₃ : rexp (x - x) = 1 x
Tactic: rw [logDeriv, Real.deriv_exp, Pi.div_apply, ← exp_sub, sub_self, exp_zero, Pi.one_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℝ
h : (deriv rexp / rexp) x = 1 x
h₁ : (rexp / rexp) x = 1 x
h₂ : rexp x / rexp x = 1 x
h₃ : rexp (x - x) = 1 x
⊢ logDeriv rexp x = 1 x
have h₄ : rexp 0 = 1 x
Tactic: rw [logDeriv, Real.deriv_exp, Pi.div_apply, ← exp_sub, sub_self, exp_zero, Pi.one_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℝ
h : (deriv rexp / rexp) x = 1 x
h₁ : (rexp / rexp) x = 1 x
h₂ : rexp x / rexp x = 1 x
h₃ : rexp (x - x) = 1 x
h₄ : rexp 0 = 1 x
⊢ logDeriv rexp x = 1 x
have h₅ : Eq (α := ℝ) 1 (1 x)
Tactic: rw [logDeriv, Real.deriv_exp, Pi.div_apply, ← exp_sub, sub_self, exp_zero, Pi.one_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℝ
h : (deriv rexp / rexp) x = 1 x
h₁ : (rexp / rexp) x = 1 x
h₂ : rexp x / rexp x = 1 x
h₃ : rexp (x - x) = 1 x
h₄ : rexp 0 = 1 x
h₅ : Eq (α := ℝ) 1 (1 x)
⊢ logDeriv rexp x = 1 x
have h₆ : Eq (α := ℝ) 1 1
Tactic: rw [logDeriv, Real.deriv_exp, Pi.div_apply, ← exp_sub, sub_self, exp_zero, Pi.one_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (hypothesis)
Goal:
z : ℂ
hz : z ≠ 0
x : ℝ
⊢ HasDerivAt (fun (y : ℝ) ↦ Complex.sin (2 * z * (↑y : ℂ)) / (2 * z)) (Complex.cos (2 * z * (↑x : ℂ))) x
have a : HasDerivAt (fun (y : ℂ) ↦ y * (2 * z)) (2 * z) (↑x : ℂ)
Tactic: have a : HasDerivAt (fun y : ℂ => y * (2 * z)) _ x := hasDerivAt_mul_const _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (hypothesis)
Goal:
z : ℂ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun (y : ℂ) ↦ y * (2 * z)) (2 * z) (↑x : ℂ)
⊢ HasDerivAt (fun (y : ℝ) ↦ Complex.sin (2 * z * (↑y : ℂ)) / (2 * z)) (Complex.cos (2 * z * (↑x : ℂ))) x
have b : HasDerivAt (Complex.sin ∘ fun (y : ℂ) ↦ y * (2 * z)) (Complex.cos ((↑x : ℂ) * (2 * z)) * (2 * z)) (↑x : ℂ)
Tactic: have b : HasDerivAt (Complex.sin ∘ fun y : ℂ => (y * (2 * z))) _ x :=
    HasDerivAt.comp (x : ℂ) (Complex.hasDerivAt_sin (x * (2 * z))) a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (hypothesis)
Goal:
z : ℂ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun (y : ℂ) ↦ y * (2 * z)) (2 * z) (↑x : ℂ)
b : HasDerivAt (Complex.sin ∘ fun (y : ℂ) ↦ y * (2 * z)) (Complex.cos ((↑x : ℂ) * (2 * z)) * (2 * z)) (↑x : ℂ)
⊢ HasDerivAt (fun (y : ℝ) ↦ Complex.sin (2 * z * (↑y : ℂ)) / (2 * z)) (Complex.cos (2 * z * (↑x : ℂ))) x
have c : HasDerivAt (fun (x : ℝ) ↦ (Complex.sin ∘ fun (y : ℂ) ↦ y * (2 * z)) (↑x : ℂ) / (2 * z))
  (Complex.cos ((↑x : ℂ) * (2 * z)) * (2 * z) / (2 * z)) x
Tactic: have c := b.comp_ofReal.div_const (2 * z)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (hypothesis)
Goal:
z : ℂ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun (y : ℂ) ↦ y * (2 * z)) (2 * z) (↑x : ℂ)
b : HasDerivAt (Complex.sin ∘ fun (y : ℂ) ↦ y * (2 * z)) (Complex.cos ((↑x : ℂ) * (2 * z)) * (2 * z)) (↑x : ℂ)
c :
  HasDerivAt (fun (x : ℝ) ↦ (Complex.sin ∘ fun (y : ℂ) ↦ y * (2 * z)) (↑x : ℂ) / (2 * z))
    (Complex.cos ((↑x : ℂ) * (2 * z)) * (2 * z) / (2 * z)) x
⊢ HasDerivAt (fun (y : ℝ) ↦ Complex.sin (2 * z * (↑y : ℂ)) / (2 * z)) (Complex.cos (2 * z * (↑x : ℂ))) x
have c₁ : HasDerivAt (fun (x : ℝ) ↦ (Complex.sin ∘ fun (y : ℂ) ↦ y * 2 * z) (↑x : ℂ) / (2 * z)) (Complex.cos (2 * z * (↑x : ℂ))) x
Tactic: field_simp at c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (hypothesis)
Goal:
z : ℂ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun (y : ℂ) ↦ y * (2 * z)) (2 * z) (↑x : ℂ)
b : HasDerivAt (Complex.sin ∘ fun (y : ℂ) ↦ y * (2 * z)) (Complex.cos ((↑x : ℂ) * (2 * z)) * (2 * z)) (↑x : ℂ)
c :
  HasDerivAt (fun (x : ℝ) ↦ (Complex.sin ∘ fun (y : ℂ) ↦ y * 2 * z) (↑x : ℂ) / (2 * z)) (Complex.cos (2 * z * (↑x : ℂ)))
    x
⊢ HasDerivAt (fun (y : ℝ) ↦ Complex.sin (2 * z * (↑y : ℂ)) / (2 * z)) (Complex.cos (2 * z * (↑x : ℂ))) x
have c₁ : HasDerivAt (fun (x : ℝ) ↦ (Complex.sin ∘ fun (y : ℂ) ↦ 2 * z * y) (↑x : ℂ) / (2 * z)) (Complex.cos (2 * z * (↑x : ℂ))) x
Tactic: simp only [mul_rotate _ 2 z] at c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (hypothesis)
Goal:
z : ℂ
hz : z ≠ 0
x : ℝ
⊢ HasDerivAt (fun (y : ℝ) ↦ -Complex.cos (2 * z * (↑y : ℂ)) / (2 * z)) (Complex.sin (2 * z * (↑x : ℂ))) x
have a : HasDerivAt (fun (y : ℂ) ↦ y * (2 * z)) (2 * z) (↑x : ℂ)
Tactic: have a : HasDerivAt (fun y : ℂ => y * (2 * z)) _ x := hasDerivAt_mul_const _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (hypothesis)
Goal:
z : ℂ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun (y : ℂ) ↦ y * (2 * z)) (2 * z) (↑x : ℂ)
⊢ HasDerivAt (fun (y : ℝ) ↦ -Complex.cos (2 * z * (↑y : ℂ)) / (2 * z)) (Complex.sin (2 * z * (↑x : ℂ))) x
have b : HasDerivAt (Complex.cos ∘ fun (y : ℂ) ↦ y * (2 * z)) (-Complex.sin ((↑x : ℂ) * (2 * z)) * (2 * z)) (↑x : ℂ)
Tactic: have b : HasDerivAt (Complex.cos ∘ fun y : ℂ => (y * (2 * z))) _ x :=
    HasDerivAt.comp (x : ℂ) (Complex.hasDerivAt_cos (x * (2 * z))) a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (hypothesis)
Goal:
z : ℂ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun (y : ℂ) ↦ y * (2 * z)) (2 * z) (↑x : ℂ)
b : HasDerivAt (Complex.cos ∘ fun (y : ℂ) ↦ y * (2 * z)) (-Complex.sin ((↑x : ℂ) * (2 * z)) * (2 * z)) (↑x : ℂ)
⊢ HasDerivAt (fun (y : ℝ) ↦ -Complex.cos (2 * z * (↑y : ℂ)) / (2 * z)) (Complex.sin (2 * z * (↑x : ℂ))) x
have c : HasDerivAt (fun (i : ℝ) ↦ -((Complex.cos ∘ fun (y : ℂ) ↦ y * (2 * z)) (↑i : ℂ) / (2 * z)))
  (-(-Complex.sin ((↑x : ℂ) * (2 * z)) * (2 * z) / (2 * z))) x
Tactic: have c := (b.comp_ofReal.div_const (2 * z)).fun_neg