awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ≥0
rw : HPow.hPow (β := ℝ) a (↑(Int.negOfNat n) : ℝ) = (a ^ n)⁻¹
rw₁ : a ^ Int.negOfNat n = (a ^ n)⁻¹
rw₂ : a ^ (-Int.ofNat n) = (a ^ n)⁻¹
⊢ a ^ b = (a ^ n)⁻¹
have rw₃ : (a ^ Int.ofNat n)⁻¹ = (a ^ n)⁻¹
Tactic: rw [h.1, NNReal.rpow_intCast, Int.negOfNat_eq, zpow_neg, Int.ofNat_eq_natCast, zpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ≥0
rw : HPow.hPow (β := ℝ) a (↑(Int.negOfNat n) : ℝ) = (a ^ n)⁻¹
rw₁ : a ^ Int.negOfNat n = (a ^ n)⁻¹
rw₂ : a ^ (-Int.ofNat n) = (a ^ n)⁻¹
rw₃ : (a ^ Int.ofNat n)⁻¹ = (a ^ n)⁻¹
⊢ a ^ b = (a ^ n)⁻¹
have rw₄ : (HPow.hPow (β := ℤ) a (↑n : ℤ))⁻¹ = (a ^ n)⁻¹
Tactic: rw [h.1, NNReal.rpow_intCast, Int.negOfNat_eq, zpow_neg, Int.ofNat_eq_natCast, zpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ≥0
rw : HPow.hPow (β := ℝ) a (↑(Int.negOfNat n) : ℝ) = (a ^ n)⁻¹
rw₁ : a ^ Int.negOfNat n = (a ^ n)⁻¹
rw₂ : a ^ (-Int.ofNat n) = (a ^ n)⁻¹
rw₃ : (a ^ Int.ofNat n)⁻¹ = (a ^ n)⁻¹
rw₄ : (HPow.hPow (β := ℤ) a (↑n : ℤ))⁻¹ = (a ^ n)⁻¹
⊢ a ^ b = (a ^ n)⁻¹
have rw₅ : (a ^ n)⁻¹ = (a ^ n)⁻¹
Tactic: rw [h.1, NNReal.rpow_intCast, Int.negOfNat_eq, zpow_neg, Int.ofNat_eq_natCast, zpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
a : ℝ≥0
b : ℝ
m n d r : ℕ
ha : IsNat a m
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
⊢ IsNat (a ^ b) r
have rcases : IsNat (HPow.hPow (α := ℝ≥0) (↑m : ℝ≥0) b) r
Tactic: rcases ha with ⟨rfl⟩
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
⊢ IsNat (HPow.hPow (α := ℝ≥0) (↑m : ℝ≥0) b) r
have out : HPow.hPow (α := ℝ≥0) (↑m : ℝ≥0) b = (↑r : ℝ≥0)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
⊢ HPow.hPow (α := ℝ≥0) (↑m : ℝ≥0) b = (↑r : ℝ≥0)
have this : d ≠ 0
Tactic: have : d ≠ 0 := mod_cast hb.den_nz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
a : ℝ≥0
b : ℝ
na da : ℕ
ha : IsNNRat a na da
nr dr : ℕ
hnum : IsNat (HPow.hPow (α := ℝ≥0) (↑na : ℝ≥0) b) nr
hden : IsNat (HPow.hPow (α := ℝ≥0) (↑da : ℝ≥0) b) dr
⊢ IsNNRat (a ^ b) nr dr
have suffices : IsNNRat (HDiv.hDiv (α := ℝ≥0) (↑nr : ℝ≥0) (↑dr : ℝ≥0)) nr dr
Tactic: suffices IsNNRat (nr / dr : ℝ≥0) nr dr by
    simpa [ha.to_eq, NNReal.div_rpow, hnum.1, hden.1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
a : ℝ≥0
b : ℝ
na da : ℕ
ha : IsNNRat a na da
nr dr : ℕ
hnum : IsNat (HPow.hPow (α := ℝ≥0) (↑na : ℝ≥0) b) nr
hden : IsNat (HPow.hPow (α := ℝ≥0) (↑da : ℝ≥0) b) dr
⊢ IsNNRat (HDiv.hDiv (α := ℝ≥0) (↑nr : ℝ≥0) (↑dr : ℝ≥0)) nr dr
have h : Ne (α := ℝ≥0) (↑dr : ℝ≥0) 0
Tactic: apply IsNNRat.of_raw
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
a : ℝ≥0
b : ℝ
n d : ℕ
hb : IsRat b (Int.negOfNat n) d
⊢ a ^ b = a⁻¹ ^ HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)
have rw : a ^ b = (a ^ HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ))⁻¹
Tactic: rw [NNReal.inv_rpow, ← NNReal.rpow_neg, hb.neg_to_eq rfl rfl]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
a : ℝ≥0
b : ℝ
n d : ℕ
hb : IsRat b (Int.negOfNat n) d
rw : a ^ b = (a ^ HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ))⁻¹
⊢ a ^ b = a⁻¹ ^ HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)
have rw₁ : a ^ b = a ^ (-HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ))
Tactic: rw [NNReal.inv_rpow, ← NNReal.rpow_neg, hb.neg_to_eq rfl rfl]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
a : ℝ≥0
b : ℝ
n d : ℕ
hb : IsRat b (Int.negOfNat n) d
rw : a ^ b = (a ^ HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ))⁻¹
rw₁ : a ^ b = a ^ (-HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ))
⊢ a ^ b = a⁻¹ ^ HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)
have rw₂ : a ^ (-HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)) = a ^ (-HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ))
Tactic: rw [NNReal.inv_rpow, ← NNReal.rpow_neg, hb.neg_to_eq rfl rfl]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
x : ℂ
⊢ HasStrictDerivAt sinh ((cexp x + cexp (-x)) * 2⁻¹) x
have h : (cexp x + cexp (-x)) * 2⁻¹ = (cexp x - cexp (-id x) * -1) * 2⁻¹
Tactic: convert!
    ((hasStrictDerivAt_exp x).sub (hasStrictDerivAt_id x).fun_neg.cexp).mul_const (2 : ℂ)⁻¹ using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
x : ℂ
⊢ (cexp x + cexp (-x)) * 2⁻¹ = (cexp x - cexp (-id x) * -1) * 2⁻¹
have h : (cexp x + cexp (-x)) * 2⁻¹ = (cexp x - cexp (-x) * -1) * 2⁻¹
Tactic: rw [id, mul_neg_one, sub_eq_add_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
x : ℂ
h : (cexp x + cexp (-x)) * 2⁻¹ = (cexp x - cexp (-x) * -1) * 2⁻¹
⊢ (cexp x + cexp (-x)) * 2⁻¹ = (cexp x - cexp (-id x) * -1) * 2⁻¹
have h₁ : (cexp x + cexp (-x)) * 2⁻¹ = (cexp x - -cexp (-x)) * 2⁻¹
Tactic: rw [id, mul_neg_one, sub_eq_add_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
x : ℂ
h : (cexp x + cexp (-x)) * 2⁻¹ = (cexp x - cexp (-x) * -1) * 2⁻¹
h₁ : (cexp x + cexp (-x)) * 2⁻¹ = (cexp x - -cexp (-x)) * 2⁻¹
⊢ (cexp x + cexp (-x)) * 2⁻¹ = (cexp x - cexp (-id x) * -1) * 2⁻¹
have h₂ : (cexp x + cexp (-x)) * 2⁻¹ = (cexp x + - -cexp (-x)) * 2⁻¹
Tactic: rw [id, mul_neg_one, sub_eq_add_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
x : ℂ
h : (cexp x + cexp (-x)) * 2⁻¹ = (cexp x - cexp (-x) * -1) * 2⁻¹
h₁ : (cexp x + cexp (-x)) * 2⁻¹ = (cexp x - -cexp (-x)) * 2⁻¹
h₂ : (cexp x + cexp (-x)) * 2⁻¹ = (cexp x + - -cexp (-x)) * 2⁻¹
⊢ (cexp x + cexp (-x)) * 2⁻¹ = (cexp x - cexp (-id x) * -1) * 2⁻¹
have h₃ : (cexp x + cexp (-x)) * 2⁻¹ = (cexp x + cexp (-x)) * 2⁻¹
Tactic: rw [id, mul_neg_one, sub_eq_add_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
x : ℂ
⊢ HasStrictDerivAt cosh ((cexp x - cexp (-x)) * 2⁻¹) x
have h : (cexp x - cexp (-x)) * 2⁻¹ = (cexp x + cexp (-id x) * -1) * 2⁻¹
Tactic: convert!
    ((hasStrictDerivAt_exp x).add (hasStrictDerivAt_id x).fun_neg.cexp).mul_const (2 : ℂ)⁻¹ using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
x : ℂ
⊢ (cexp x - cexp (-x)) * 2⁻¹ = (cexp x + cexp (-id x) * -1) * 2⁻¹
have h : (cexp x - cexp (-x)) * 2⁻¹ = (cexp x + cexp (-x) * -1) * 2⁻¹
Tactic: rw [id, mul_neg_one, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
x : ℂ
h : (cexp x - cexp (-x)) * 2⁻¹ = (cexp x + cexp (-x) * -1) * 2⁻¹
⊢ (cexp x - cexp (-x)) * 2⁻¹ = (cexp x + cexp (-id x) * -1) * 2⁻¹
have h₁ : (cexp x - cexp (-x)) * 2⁻¹ = (cexp x + -cexp (-x)) * 2⁻¹
Tactic: rw [id, mul_neg_one, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
x : ℂ
h : (cexp x - cexp (-x)) * 2⁻¹ = (cexp x + cexp (-x) * -1) * 2⁻¹
h₁ : (cexp x - cexp (-x)) * 2⁻¹ = (cexp x + -cexp (-x)) * 2⁻¹
⊢ (cexp x - cexp (-x)) * 2⁻¹ = (cexp x + cexp (-id x) * -1) * 2⁻¹
have h₂ : (cexp x + -cexp (-x)) * 2⁻¹ = (cexp x + -cexp (-x)) * 2⁻¹
Tactic: rw [id, mul_neg_one, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
⊢ ∀ (x : ℝ), 0 < deriv sinh x
have rw : ∀ (x : ℝ), 0 < cosh x
Tactic: rw [Real.deriv_sinh]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
x : ℝ
⊢ sinh x = 0 ↔ x = 0
have rw : sinh x = 0 ↔ sinh x = sinh 0
Tactic: rw [← @sinh_inj x, sinh_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
x : ℝ
rw : sinh x = 0 ↔ sinh x = sinh 0
⊢ sinh x = 0 ↔ x = 0
have rw₁ : sinh x = 0 ↔ sinh x = 0
Tactic: rw [← @sinh_inj x, sinh_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
x : ℝ
⊢ |sinh x| = sinh |x|
have inl : x ≤ 0 → |sinh x| = sinh |x|
Tactic: cases le_total x 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
x : ℝ
inl : x ≤ 0 → |sinh x| = sinh |x|
⊢ |sinh x| = sinh |x|
have inr : 0 ≤ x → |sinh x| = sinh |x|
Tactic: cases le_total x 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (hypothesis)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (interior (Ici 0)) x
⊢ 0 < deriv cosh x
have hx₁ : 0 < x
Tactic: rw [interior_Ici, mem_Ioi] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
x : ℝ
hx : 0 < x
⊢ 0 < deriv cosh x
have rwa : 0 < sinh x
Tactic: rwa [deriv_cosh, sinh_pos_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
x : ℝ
⊢ sinh (-x) - -x = -(sinh x - x)
have simp : -sinh x + x = x - sinh x
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
⊢ StrictMono (β := ℝ) fun (x : ℝ) ↦ sinh x - x
have refine : StrictMonoOn (β := ℝ) (fun (x : ℝ) ↦ sinh x - x) (Ici 0)
Tactic: refine strictMono_of_odd_strictMonoOn_nonneg (fun x => by simp; abel) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
⊢ StrictMonoOn (β := ℝ) (fun (x : ℝ) ↦ sinh x - x) (Ici 0)
have refine_1 : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ sinh x - x) (Ici 0)
Tactic: refine strictMonoOn_of_deriv_pos (convex_Ici _) ?_ fun x hx => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
refine_1 : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ sinh x - x) (Ici 0)
⊢ StrictMonoOn (β := ℝ) (fun (x : ℝ) ↦ sinh x - x) (Ici 0)
have refine_2 : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (interior (Ici 0)) x), LT.lt (α := ℝ) 0 (deriv (fun (x : ℝ) ↦ sinh x - x) x)
Tactic: refine strictMonoOn_of_deriv_pos (convex_Ici _) ?_ fun x hx => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (hypothesis)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (interior (Ici 0)) x
⊢ LT.lt (α := ℝ) 0 (deriv (fun (x : ℝ) ↦ sinh x - x) x)
have hx₁ : 0 < x
Tactic: rw [interior_Ici, mem_Ioi] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
x : ℝ
hx : 0 < x
⊢ LT.lt (α := ℝ) 0 (deriv (fun (x : ℝ) ↦ sinh x - x) x)
have refine_2 : x ≠ 0
Tactic: rw [deriv_fun_sub, deriv_sinh, deriv_id'', sub_pos, one_lt_cosh]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
x : ℝ
hx : 0 < x
refine_2 : x ≠ 0
⊢ LT.lt (α := ℝ) 0 (deriv (fun (x : ℝ) ↦ sinh x - x) x)
have refine_2₁ : DifferentiableAt ℝ sinh x
Tactic: rw [deriv_fun_sub, deriv_sinh, deriv_id'', sub_pos, one_lt_cosh]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
x : ℝ
hx : 0 < x
refine_2 : x ≠ 0
refine_2₁ : DifferentiableAt ℝ sinh x
⊢ LT.lt (α := ℝ) 0 (deriv (fun (x : ℝ) ↦ sinh x - x) x)
have refine_2₂ : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x) x
Tactic: rw [deriv_fun_sub, deriv_sinh, deriv_id'', sub_pos, one_lt_cosh]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
n : ℕ
ih : iteratedDeriv (n + 1) sinh = iteratedDeriv n cosh
⊢ iteratedDeriv (n + 1 + 1) sinh = iteratedDeriv (n + 1) cosh
have succ : deriv (iteratedDeriv (n + 1) sinh) = iteratedDeriv (n + 1) cosh
Tactic: rw [iteratedDeriv_succ, ih, iteratedDeriv_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
n : ℕ
ih : iteratedDeriv (n + 1) sinh = iteratedDeriv n cosh
succ : deriv (iteratedDeriv (n + 1) sinh) = iteratedDeriv (n + 1) cosh
⊢ iteratedDeriv (n + 1 + 1) sinh = iteratedDeriv (n + 1) cosh
have succ₁ : deriv (iteratedDeriv n cosh) = iteratedDeriv (n + 1) cosh
Tactic: rw [iteratedDeriv_succ, ih, iteratedDeriv_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
n : ℕ
ih : iteratedDeriv (n + 1) sinh = iteratedDeriv n cosh
succ : deriv (iteratedDeriv (n + 1) sinh) = iteratedDeriv (n + 1) cosh
succ₁ : deriv (iteratedDeriv n cosh) = iteratedDeriv (n + 1) cosh
⊢ iteratedDeriv (n + 1 + 1) sinh = iteratedDeriv (n + 1) cosh
have succ₂ : deriv (iteratedDeriv n cosh) = deriv (iteratedDeriv n cosh)
Tactic: rw [iteratedDeriv_succ, ih, iteratedDeriv_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
n : ℕ
⊢ iteratedDeriv (n + 1) sinh = iteratedDeriv n cosh
have zero : iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) sinh = iteratedDeriv 0 cosh
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rw [iteratedDeriv_succ, ih, iteratedDeriv_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
n : ℕ
zero : iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) sinh = iteratedDeriv 0 cosh
⊢ iteratedDeriv (n + 1) sinh = iteratedDeriv n cosh
have succ : ∀ (n : ℕ) (ih : iteratedDeriv (n + 1) sinh = iteratedDeriv n cosh),
  iteratedDeriv (n + 1 + 1) sinh = iteratedDeriv (n + 1) cosh
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rw [iteratedDeriv_succ, ih, iteratedDeriv_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
⊢ iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) cosh = iteratedDeriv 0 sinh
have zero : ∀ (x : ℂ), iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) cosh x = iteratedDeriv 0 sinh x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
n : ℕ
ih : iteratedDeriv (n + 1) cosh = iteratedDeriv n sinh
⊢ iteratedDeriv (n + 1 + 1) cosh = iteratedDeriv (n + 1) sinh
have succ : deriv (iteratedDeriv (n + 1) cosh) = iteratedDeriv (n + 1) sinh
Tactic: rw [iteratedDeriv_succ, ih, iteratedDeriv_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
n : ℕ
ih : iteratedDeriv (n + 1) cosh = iteratedDeriv n sinh
succ : deriv (iteratedDeriv (n + 1) cosh) = iteratedDeriv (n + 1) sinh
⊢ iteratedDeriv (n + 1 + 1) cosh = iteratedDeriv (n + 1) sinh
have succ₁ : deriv (iteratedDeriv n sinh) = iteratedDeriv (n + 1) sinh
Tactic: rw [iteratedDeriv_succ, ih, iteratedDeriv_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
n : ℕ
ih : iteratedDeriv (n + 1) cosh = iteratedDeriv n sinh
succ : deriv (iteratedDeriv (n + 1) cosh) = iteratedDeriv (n + 1) sinh
succ₁ : deriv (iteratedDeriv n sinh) = iteratedDeriv (n + 1) sinh
⊢ iteratedDeriv (n + 1 + 1) cosh = iteratedDeriv (n + 1) sinh
have succ₂ : deriv (iteratedDeriv n sinh) = deriv (iteratedDeriv n sinh)
Tactic: rw [iteratedDeriv_succ, ih, iteratedDeriv_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
n : ℕ
⊢ iteratedDeriv (n + 1) cosh = iteratedDeriv n sinh
have zero : iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) cosh = iteratedDeriv 0 sinh
Tactic: induction n with
  | zero => ext; simp
  | succ n ih =>
    rw [iteratedDeriv_succ, ih, iteratedDeriv_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
n : ℕ
zero : iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) cosh = iteratedDeriv 0 sinh
⊢ iteratedDeriv (n + 1) cosh = iteratedDeriv n sinh
have succ : ∀ (n : ℕ) (ih : iteratedDeriv (n + 1) cosh = iteratedDeriv n sinh),
  iteratedDeriv (n + 1 + 1) cosh = iteratedDeriv (n + 1) sinh
Tactic: induction n with
  | zero => ext; simp
  | succ n ih =>
    rw [iteratedDeriv_succ, ih, iteratedDeriv_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
n : ℕ
⊢ iteratedDeriv (2 * n) sinh = sinh
have zero : iteratedDeriv (HMul.hMul (α := ℕ) 2 0) sinh = sinh
Tactic: induction n with
  | zero => simp
  | succ n ih => simp_all [mul_add]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
n : ℕ
zero : iteratedDeriv (HMul.hMul (α := ℕ) 2 0) sinh = sinh
⊢ iteratedDeriv (2 * n) sinh = sinh
have succ : ∀ (n : ℕ) (ih : iteratedDeriv (2 * n) sinh = sinh), iteratedDeriv (2 * (n + 1)) sinh = sinh
Tactic: induction n with
  | zero => simp
  | succ n ih => simp_all [mul_add]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
n : ℕ
⊢ iteratedDeriv (2 * n) cosh = cosh
have zero : iteratedDeriv (HMul.hMul (α := ℕ) 2 0) cosh = cosh
Tactic: induction n with
  | zero => simp
  | succ n ih => simp_all [mul_add]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
n : ℕ
zero : iteratedDeriv (HMul.hMul (α := ℕ) 2 0) cosh = cosh
⊢ iteratedDeriv (2 * n) cosh = cosh
have succ : ∀ (n : ℕ) (ih : iteratedDeriv (2 * n) cosh = cosh), iteratedDeriv (2 * (n + 1)) cosh = cosh
Tactic: induction n with
  | zero => simp
  | succ n ih => simp_all [mul_add]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
⊢ iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) cosh = iteratedDeriv 0 sinh
have zero : ∀ (x : ℝ), iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) cosh x = iteratedDeriv 0 sinh x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
⊢ logDeriv cosh = tanh
have h : ∀ (x : ℂ), logDeriv cosh x = tanh x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
x : ℂ
⊢ logDeriv cosh x = tanh x
have h : (deriv cosh / cosh) x = tanh x
Tactic: rw [logDeriv, Complex.deriv_cosh, Pi.div_apply, Complex.tanh]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
x : ℂ
h : (deriv cosh / cosh) x = tanh x
⊢ logDeriv cosh x = tanh x
have h₁ : (sinh / cosh) x = tanh x
Tactic: rw [logDeriv, Complex.deriv_cosh, Pi.div_apply, Complex.tanh]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
x : ℂ
h : (deriv cosh / cosh) x = tanh x
h₁ : (sinh / cosh) x = tanh x
⊢ logDeriv cosh x = tanh x
have h₂ : sinh x / cosh x = tanh x
Tactic: rw [logDeriv, Complex.deriv_cosh, Pi.div_apply, Complex.tanh]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
x : ℂ
h : (deriv cosh / cosh) x = tanh x
h₁ : (sinh / cosh) x = tanh x
h₂ : sinh x / cosh x = tanh x
⊢ logDeriv cosh x = tanh x
have h₃ : sinh x / cosh x = sinh x / cosh x
Tactic: rw [logDeriv, Complex.deriv_cosh, Pi.div_apply, Complex.tanh]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
⊢ logDeriv cosh = tanh
have h : ∀ (x : ℝ), logDeriv cosh x = tanh x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
x : ℝ
⊢ logDeriv cosh x = tanh x
have h : (deriv cosh / cosh) x = tanh x
Tactic: rw [logDeriv, Real.deriv_cosh, Pi.div_apply, Real.tanh_eq_sinh_div_cosh]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
x : ℝ
h : (deriv cosh / cosh) x = tanh x
⊢ logDeriv cosh x = tanh x
have h₁ : (sinh / cosh) x = tanh x
Tactic: rw [logDeriv, Real.deriv_cosh, Pi.div_apply, Real.tanh_eq_sinh_div_cosh]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
x : ℝ
h : (deriv cosh / cosh) x = tanh x
h₁ : (sinh / cosh) x = tanh x
⊢ logDeriv cosh x = tanh x
have h₂ : sinh x / cosh x = tanh x
Tactic: rw [logDeriv, Real.deriv_cosh, Pi.div_apply, Real.tanh_eq_sinh_div_cosh]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp (goal)
Goal:
x : ℝ
h : (deriv cosh / cosh) x = tanh x
h₁ : (sinh / cosh) x = tanh x
h₂ : sinh x / cosh x = tanh x
⊢ logDeriv cosh x = tanh x
have h₃ : sinh x / cosh x = sinh x / cosh x
Tactic: rw [logDeriv, Real.deriv_cosh, Pi.div_apply, Real.tanh_eq_sinh_div_cosh]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc (goal)
Goal:
⊢ sinc = dslope sin 0
have h : ∀ (x : ℝ), sinc x = dslope sin 0 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc (goal)
Goal:
x : ℝ
⊢ sinc (-x) = sinc x
have pos : ∀ (hx : x = 0), sinc (-x) = sinc x
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc (goal)
Goal:
x : ℝ
pos : ∀ (hx : x = 0), sinc (-x) = sinc x
⊢ sinc (-x) = sinc x
have neg : ∀ (hx : ¬x = 0), sinc (-x) = sinc x
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc (goal)
Goal:
x : ℝ
⊢ |sinc x| ≤ 1
have pos : ∀ (hx : x = 0), |sinc x| ≤ 1
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc (goal)
Goal:
x : ℝ
pos : ∀ (hx : x = 0), |sinc x| ≤ 1
⊢ |sinc x| ≤ 1
have neg : ∀ (hx : ¬x = 0), |sinc x| ≤ 1
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc (goal)
Goal:
x : ℝ
hx : ¬x = 0
⊢ |sinc x| ≤ 1
have neg : |sin x| / |x| ≤ 1
Tactic: rw [sinc_of_ne_zero hx, abs_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc (goal)
Goal:
x : ℝ
hx : ¬x = 0
⊢ |sin x| / |x| ≤ 1
have neg : |sin x| ≤ 1 * |x|
Tactic: refine div_le_of_le_mul₀ (abs_nonneg _) zero_le_one ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc (goal)
Goal:
x : ℝ
hx : ¬x = 0
⊢ |sin x| ≤ 1 * |x|
have neg : |sin x| ≤ |x|
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc (goal)
Goal:
x : ℝ
⊢ sin x / x ≤ |x|⁻¹
have inl : ∀ (hx : x < 0), sin x / x ≤ |x|⁻¹
Tactic: rcases lt_trichotomy x 0 with hx | rfl | hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc (goal)
Goal:
x : ℝ
inl : ∀ (hx : x < 0), sin x / x ≤ |x|⁻¹
⊢ sin x / x ≤ |x|⁻¹
have inr : sin 0 / 0 ≤ |0|⁻¹
Tactic: rcases lt_trichotomy x 0 with hx | rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc (goal)
Goal:
x : ℝ
inl : ∀ (hx : x < 0), sin x / x ≤ |x|⁻¹
inr : sin 0 / 0 ≤ |0|⁻¹
⊢ sin x / x ≤ |x|⁻¹
have inr₁ : ∀ (hx : 0 < x), sin x / x ≤ |x|⁻¹
Tactic: rcases lt_trichotomy x 0 with hx | rfl | hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc (goal)
Goal:
x : ℝ
hx : x < 0
⊢ sin x / x ≤ |x|⁻¹
have inl : sin x * x⁻¹ * -x ≤ 1
Tactic: rw [abs_of_nonpos hx.le, ← one_div, le_div_iff₀, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc (goal)
Goal:
x : ℝ
hx : x < 0
inl : sin x * x⁻¹ * -x ≤ 1
⊢ sin x / x ≤ |x|⁻¹
have inl₁ : 0 < -x
Tactic: rw [abs_of_nonpos hx.le, ← one_div, le_div_iff₀, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc (goal)
Goal:
x : ℝ
hx : x < 0
⊢ sin x * x⁻¹ * -x ≤ 1
have inl : -(sin x * x * x⁻¹) ≤ 1
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc (goal)
Goal:
x : ℝ
hx : x < 0
⊢ -(sin x * x * x⁻¹) ≤ 1
have inl : -1 ≤ sin x
Tactic: rw [mul_assoc, mul_inv_cancel₀ hx.ne, mul_one, neg_le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc (goal)
Goal:
x : ℝ
hx : 0 < x
⊢ sin x / x ≤ |x|⁻¹
have inr : sin x ≤ 1
Tactic: rw [abs_of_nonneg hx.le, div_eq_mul_inv, mul_inv_le_iff₀ hx, inv_mul_cancel₀ hx.ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc (goal)
Goal:
x : ℝ
hx : x ≠ 0
⊢ sinc x ≤ |x|⁻¹
have rw : sin x / x ≤ |x|⁻¹
Tactic: rw [sinc_of_ne_zero hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc (goal)
Goal:
⊢ Continuous sinc
have refine : ∀ (x : ℝ), ContinuousAt sinc x
Tactic: refine continuous_iff_continuousAt.mpr fun x ↦ ?_