awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
b : ℝ
ht : 0 < b
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b
have rw : b * log b - b - 0 = b * log b - b
Tactic: rw [integral_eq_sub_of_hasDerivAt_of_tendsto (f := fun x ↦ x * log x - x)
    (fa := 0) (fb := b * log b - b) (hint := intervalIntegrable_log')]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
b : ℝ
ht : 0 < b
rw : b * log b - b - 0 = b * log b - b
hab : 0 < b
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b
have hderiv : ∀ x ∈ Set.Ioo 0 b, HasDerivAt (fun (x : ℝ) ↦ x * log x - x) (log x) x
Tactic: rw [integral_eq_sub_of_hasDerivAt_of_tendsto (f := fun x ↦ x * log x - x)
    (fa := 0) (fb := b * log b - b) (hint := intervalIntegrable_log')]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
b : ℝ
ht : 0 < b
rw : b * log b - b - 0 = b * log b - b
hab : 0 < b
hderiv : ∀ x ∈ Set.Ioo 0 b, HasDerivAt (fun (x : ℝ) ↦ x * log x - x) (log x) x
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b
have ha : Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * log x - x) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
Tactic: rw [integral_eq_sub_of_hasDerivAt_of_tendsto (f := fun x ↦ x * log x - x)
    (fa := 0) (fb := b * log b - b) (hint := intervalIntegrable_log')]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
b : ℝ
ht : 0 < b
rw : b * log b - b - 0 = b * log b - b
hab : 0 < b
hderiv : ∀ x ∈ Set.Ioo 0 b, HasDerivAt (fun (x : ℝ) ↦ x * log x - x) (log x) x
ha : Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * log x - x) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b
have hb : Filter.Tendsto (fun (x : ℝ) ↦ x * log x - x) (nhdsWithin b (Set.Iio b)) (nhds (b * log b - b))
Tactic: rw [integral_eq_sub_of_hasDerivAt_of_tendsto (f := fun x ↦ x * log x - x)
    (fa := 0) (fb := b * log b - b) (hint := intervalIntegrable_log')]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
b : ℝ
ht : 0 < b
s : ℝ
⊢ s ∈ Set.Ioo 0 b → HasDerivAt (fun (x : ℝ) ↦ x * log x - x) (log s) s
have hderiv : ∀ (hs : 0 < s), s < b → HasDerivAt (fun (x : ℝ) ↦ x * log x - x) (log s) s
Tactic: ⟨hs, _ ⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
b : ℝ
ht : 0 < b
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x * log x - x) b
have funProp : b ≠ 0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
b : ℝ
ht : 0 < b
funProp : b ≠ 0
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x * log x - x) b
have funProp₁ : ∀ (x : ℝ), x ≠ 0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
b : ℝ
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b
have inl : ∀ (h : b < 0), ∫ (s : ℝ) in 0..b, log s = b * log b - b
Tactic: rcases lt_trichotomy b 0 with h | h | h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
b : ℝ
inl : ∀ (h : b < 0), ∫ (s : ℝ) in 0..b, log s = b * log b - b
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b
have inr : ∀ (h : b = 0), ∫ (s : ℝ) in 0..b, log s = b * log b - b
Tactic: rcases lt_trichotomy b 0 with h | h | h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
b : ℝ
inl : ∀ (h : b < 0), ∫ (s : ℝ) in 0..b, log s = b * log b - b
inr : ∀ (h : b = 0), ∫ (s : ℝ) in 0..b, log s = b * log b - b
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b
have inr₁ : ∀ (h : 0 < b), ∫ (s : ℝ) in 0..b, log s = b * log b - b
Tactic: rcases lt_trichotomy b 0 with h | h | h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
b : ℝ
h : b < 0
| ∫ (s : ℝ) in 0..b, log s = b * log b - b
have arg : ∫ (s : ℝ) in 0..b, log s
Tactic: arg 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
b : ℝ
h : b < 0
| ∫ (s : ℝ) in 0..b, log s
have arg : fun (s : ℝ) ↦ log s
Tactic: arg 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
b : ℝ
h : b < 0
t : ℝ
| log t
have h₁ : log (-t)
Tactic: rw [← log_neg_eq_log]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
b : ℝ
h : b < 0
| ∫ (s : ℝ) in 0..b, log s = b * log b - b
have h₁ : ∀ (t : ℝ), log (-t)
Tactic: arg 1; arg 1; intro t; rw [← log_neg_eq_log]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
b : ℝ
h : b < 0
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b
have inl : ∫ (t : ℝ) in 0..b, log (-t) = b * log b - b
Tactic: conv => arg 1; arg 1; intro t; rw [← log_neg_eq_log]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
b : ℝ
h : b < 0
⊢ ∫ (t : ℝ) in 0..b, log (-t) = b * log b - b
have inl : -(-b * log b - -b) = b * log b - b
Tactic: rw [intervalIntegral.integral_comp_neg, intervalIntegral.integral_symm, neg_zero,
      integral_log_from_zero_of_pos (Left.neg_pos_iff.mpr h), log_neg_eq_log]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
⊢ ∫ (s : ℝ) in a..b, log s = b * log b - a * log a - b + a
have rw : HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in a..0, log x) (∫ (x : ℝ) in 0..b, log x) = b * log b - a * log a - b + a
Tactic: rw [← intervalIntegral.integral_add_adjacent_intervals (b := 0)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
rw : HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in a..0, log x) (∫ (x : ℝ) in 0..b, log x) = b * log b - a * log a - b + a
⊢ ∫ (s : ℝ) in a..b, log s = b * log b - a * log a - b + a
have hab : IntervalIntegrable log MeasureTheory.volume a 0
Tactic: rw [← intervalIntegral.integral_add_adjacent_intervals (b := 0)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
rw : HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in a..0, log x) (∫ (x : ℝ) in 0..b, log x) = b * log b - a * log a - b + a
hab : IntervalIntegrable log MeasureTheory.volume a 0
⊢ ∫ (s : ℝ) in a..b, log s = b * log b - a * log a - b + a
have hbc : IntervalIntegrable log MeasureTheory.volume 0 b
Tactic: rw [← intervalIntegral.integral_add_adjacent_intervals (b := 0)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
⊢ HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in a..0, log x) (∫ (x : ℝ) in 0..b, log x) = b * log b - a * log a - b + a
have rw : -(a * log a - a) + (b * log b - b) = b * log b - a * log a - b + a
Tactic: rw [intervalIntegral.integral_symm, integral_log_from_zero, integral_log_from_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, sin x = cos a - cos b
have rw : -cos b - -cos a = cos a - cos b
Tactic: rw [integral_deriv_eq_sub' fun x => -cos x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
rw : -cos b - -cos a = cos a - cos b
⊢ ∫ (x : ℝ) in a..b, sin x = cos a - cos b
have hderiv : (deriv fun (x : ℝ) ↦ -cos x) = sin
Tactic: rw [integral_deriv_eq_sub' fun x => -cos x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
rw : -cos b - -cos a = cos a - cos b
hderiv : (deriv fun (x : ℝ) ↦ -cos x) = sin
⊢ ∫ (x : ℝ) in a..b, sin x = cos a - cos b
have hdiff : ∀ x ∈ [[a, b]], DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ -cos x) x
Tactic: rw [integral_deriv_eq_sub' fun x => -cos x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
rw : -cos b - -cos a = cos a - cos b
hderiv : (deriv fun (x : ℝ) ↦ -cos x) = sin
hdiff : ∀ x ∈ [[a, b]], DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ -cos x) x
⊢ ∫ (x : ℝ) in a..b, sin x = cos a - cos b
have hcont : ContinuousOn sin [[a, b]]
Tactic: rw [integral_deriv_eq_sub' fun x => -cos x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, cos x = sin b - sin a
have hderiv : deriv sin = cos
Tactic: rw [integral_deriv_eq_sub']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
hderiv : deriv sin = cos
⊢ ∫ (x : ℝ) in a..b, cos x = sin b - sin a
have hdiff : ∀ x ∈ [[a, b]], DifferentiableAt ℝ sin x
Tactic: rw [integral_deriv_eq_sub']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
hderiv : deriv sin = cos
hdiff : ∀ x ∈ [[a, b]], DifferentiableAt ℝ sin x
⊢ ∫ (x : ℝ) in a..b, cos x = sin b - sin a
have hcont : ContinuousOn cos [[a, b]]
Tactic: rw [integral_deriv_eq_sub']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, Complex.cos (z * (↑x : ℂ)) = Complex.sin (z * (↑b : ℂ)) / z - Complex.sin (z * (↑a : ℂ)) / z
have hderiv : ∀ x ∈ [[a, b]], HasDerivAt (fun (b : ℝ) ↦ Complex.sin (z * (↑b : ℂ)) / z) (Complex.cos (z * (↑x : ℂ))) x
Tactic: apply integral_eq_sub_of_hasDerivAt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
z : ℂ
hz : z ≠ 0
a b : ℝ
hderiv : ∀ x ∈ [[a, b]], HasDerivAt (fun (b : ℝ) ↦ Complex.sin (z * (↑b : ℂ)) / z) (Complex.cos (z * (↑x : ℂ))) x
⊢ ∫ (x : ℝ) in a..b, Complex.cos (z * (↑x : ℂ)) = Complex.sin (z * (↑b : ℂ)) / z - Complex.sin (z * (↑a : ℂ)) / z
have hint : IntervalIntegrable (ε := ℂ) (fun (y : ℝ) ↦ Complex.cos (z * (↑y : ℂ))) MeasureTheory.volume a b
Tactic: apply integral_eq_sub_of_hasDerivAt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
z : ℂ
hz : z ≠ 0
a b x : ℝ
h : x ∈ [[a, b]]
⊢ HasDerivAt (fun (b : ℝ) ↦ Complex.sin (z * (↑b : ℂ)) / z) (Complex.cos (z * (↑x : ℂ))) x
have a₁ : HasDerivAt Complex.sin (Complex.cos ((↑x : ℂ) * z)) ((↑x : ℂ) * z)
Tactic: have a := Complex.hasDerivAt_sin (↑x * z)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
z : ℂ
hz : z ≠ 0
a_1 b x : ℝ
h : x ∈ [[a_1, b]]
a : HasDerivAt Complex.sin (Complex.cos ((↑x : ℂ) * z)) ((↑x : ℂ) * z)
⊢ HasDerivAt (fun (b : ℝ) ↦ Complex.sin (z * (↑b : ℂ)) / z) (Complex.cos (z * (↑x : ℂ))) x
have b₁ : HasDerivAt (fun (y : ℂ) ↦ y * z) z (↑x : ℂ)
Tactic: have b : HasDerivAt (fun y => y * z : ℂ → ℂ) z ↑x := hasDerivAt_mul_const _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
z : ℂ
hz : z ≠ 0
a_1 b_1 x : ℝ
h : x ∈ [[a_1, b_1]]
a : HasDerivAt Complex.sin (Complex.cos ((↑x : ℂ) * z)) ((↑x : ℂ) * z)
b : HasDerivAt (fun (y : ℂ) ↦ y * z) z (↑x : ℂ)
⊢ HasDerivAt (fun (b : ℝ) ↦ Complex.sin (z * (↑b : ℂ)) / z) (Complex.cos (z * (↑x : ℂ))) x
have c : HasDerivAt (Complex.sin ∘ fun (y : ℂ) ↦ y * z) (Complex.cos ((↑x : ℂ) * z) * z) (↑x : ℂ)
Tactic: have c : HasDerivAt (Complex.sin ∘ fun y : ℂ => (y * z)) _ ↑x := HasDerivAt.comp (𝕜 := ℂ) x a b
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
z : ℂ
hz : z ≠ 0
a_1 b_1 x : ℝ
h : x ∈ [[a_1, b_1]]
a : HasDerivAt Complex.sin (Complex.cos ((↑x : ℂ) * z)) ((↑x : ℂ) * z)
b : HasDerivAt (fun (y : ℂ) ↦ y * z) z (↑x : ℂ)
c : HasDerivAt (Complex.sin ∘ fun (y : ℂ) ↦ y * z) (Complex.cos ((↑x : ℂ) * z) * z) (↑x : ℂ)
⊢ HasDerivAt (fun (b : ℝ) ↦ Complex.sin (z * (↑b : ℂ)) / z) (Complex.cos (z * (↑x : ℂ))) x
have d : HasDerivAt (fun (y : ℝ) ↦ (Complex.sin ∘ fun (y : ℂ) ↦ y * z) (↑y : ℂ) / z) (Complex.cos ((↑x : ℂ) * z) * z / z) x
Tactic: have d := HasDerivAt.comp_ofReal (c.div_const z)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, 1 / (1 + HPow.hPow (β := ℕ) x 2) = arctan b - arctan a
have refine_1 : Continuous (Y := ℝ) fun (x : ℝ) ↦ 1 + HPow.hPow (β := ℕ) x 2
Tactic: refine integral_deriv_eq_sub' _ Real.deriv_arctan (fun _ _ => differentiableAt_arctan _)
    (continuous_const.div ?_ fun x => ?_).continuousOn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
refine_1 : Continuous (Y := ℝ) fun (x : ℝ) ↦ 1 + HPow.hPow (β := ℕ) x 2
⊢ ∫ (x : ℝ) in a..b, 1 / (1 + HPow.hPow (β := ℕ) x 2) = arctan b - arctan a
have refine_2 : ∀ (x : ℝ), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
Tactic: refine integral_deriv_eq_sub' _ Real.deriv_arctan (fun _ _ => differentiableAt_arctan _)
    (continuous_const.div ?_ fun x => ?_).continuousOn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b x : ℝ
⊢ 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
have nlinarith : 1 + HPow.hPow (β := ℕ) x 2 = 0 → -1 + (0 - HPow.hPow (β := ℕ) x 2) + (1 + HPow.hPow (β := ℕ) x 2 - 0) = 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b c : ℝ
hc : c ≠ 0
⊢ ∫ (x : ℝ) in a..b, (HPow.hPow (β := ℕ) c 2)⁻¹ * (1 + HPow.hPow (β := ℕ) (x / c) 2)⁻¹ =
    c⁻¹ * (arctan (b / c) - arctan (a / c))
have simp : c * ((HPow.hPow (β := ℕ) c 2)⁻¹ * (arctan (b / c) - arctan (a / c))) = c⁻¹ * (arctan (b / c) - arctan (a / c))
Tactic: simp [integral_comp_div (fun x => (c ^ 2)⁻¹ * (1 + x ^ 2)⁻¹) hc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b c : ℝ
⊢ ∫ (x : ℝ) in a..b, c * (HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) x 2)⁻¹ = arctan (b / c) - arctan (a / c)
have pos : ∀ (hc : c = 0),
  ∫ (x : ℝ) in a..b, c * (HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) x 2)⁻¹ = arctan (b / c) - arctan (a / c)
Tactic: by_cases hc : c = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b c : ℝ
pos :
  ∀ (hc : c = 0),
    ∫ (x : ℝ) in a..b, c * (HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) x 2)⁻¹ = arctan (b / c) - arctan (a / c)
⊢ ∫ (x : ℝ) in a..b, c * (HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) x 2)⁻¹ = arctan (b / c) - arctan (a / c)
have neg : ∀ (hc : ¬c = 0),
  ∫ (x : ℝ) in a..b, c * (HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) x 2)⁻¹ = arctan (b / c) - arctan (a / c)
Tactic: by_cases hc : c = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b c : ℝ
hc : ¬c = 0
⊢ ∫ (x : ℝ) in a..b, c * (HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) x 2)⁻¹ = arctan (b / c) - arctan (a / c)
have neg : c * (c⁻¹ * (arctan (b / c) - arctan (a / c))) = arctan (b / c) - arctan (a / c)
Tactic: rw [integral_const_mul, integral_inv_sq_add_sq hc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
t : ℂ
ht : t ≠ -1
⊢ t + 1 ≠ 0
have contrapose : ∀ (ht : t + 1 = 0), t = -1
Tactic: contrapose ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
t : ℂ
ht : t + 1 = 0
⊢ t = -1
have rwa : ∀ (ht : t = -1), t = -1
Tactic: rwa [add_eq_zero_iff_eq_neg] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b : ℝ
t : ℂ
ht : t ≠ -1
⊢ ∫ (x : ℝ) in a..b, (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ t =
    (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ (t + 1) / (2 * (t + 1)) -
      (1 + HPow.hPow (β := ℕ) (↑a : ℂ) 2) ^ (t + 1) / (2 * (t + 1))
have this : t + 1 ≠ 0
Tactic: have : t + 1 ≠ 0 := by contrapose ht; rwa [add_eq_zero_iff_eq_neg] at ht
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ ∫ (x : ℝ) in a..b, (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ t =
    (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ (t + 1) / (2 * (t + 1)) -
      (1 + HPow.hPow (β := ℕ) (↑a : ℂ) 2) ^ (t + 1) / (2 * (t + 1))
have hderiv : ∀ x ∈ [[a, b]],
  HasDerivAt (fun {b : ℝ} ↦ (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ (t + 1) / (2 * (t + 1)))
    ((↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ t) x
Tactic: apply integral_eq_sub_of_hasDerivAt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
hderiv :
  ∀ x ∈ [[a, b]],
    HasDerivAt (fun {b : ℝ} ↦ (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ (t + 1) / (2 * (t + 1)))
      ((↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ t) x
⊢ ∫ (x : ℝ) in a..b, (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ t =
    (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ (t + 1) / (2 * (t + 1)) -
      (1 + HPow.hPow (β := ℕ) (↑a : ℂ) 2) ^ (t + 1) / (2 * (t + 1))
have hint : IntervalIntegrable (ε := ℂ) (fun (y : ℝ) ↦ (↑y : ℂ) * (1 + HPow.hPow (β := ℕ) (↑y : ℂ) 2) ^ t) MeasureTheory.volume a b
Tactic: apply integral_eq_sub_of_hasDerivAt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
h : x ∈ [[a, b]]
⊢ HasDerivAt (fun (y : ℂ) ↦ 1 + HPow.hPow (β := ℕ) y 2) (2 * (↑x : ℂ)) (↑x : ℂ)
have h : (↑x : ℂ) = (↑x : ℂ) ^ HSub.hSub (α := ℕ) 2 1
Tactic: convert! (hasDerivAt_pow 2 (x : ℂ)).const_add 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
h : x ∈ [[a, b]]
⊢ HasDerivAt (fun {b : ℝ} ↦ (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ (t + 1) / (2 * (t + 1)))
    ((↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ t) x
have f : HasDerivAt (fun (y : ℂ) ↦ 1 + HPow.hPow (β := ℕ) y 2) (2 * (↑x : ℂ)) (↑x : ℂ)
Tactic: have f : HasDerivAt (fun y : ℂ => 1 + y ^ 2) (2 * x : ℂ) x := by
      convert! (hasDerivAt_pow 2 (x : ℂ)).const_add 1
      simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
h : x ∈ [[a, b]]
f : HasDerivAt (fun (y : ℂ) ↦ 1 + HPow.hPow (β := ℕ) y 2) (2 * (↑x : ℂ)) (↑x : ℂ)
z : ℂ
hz : 0 < z.re
⊢ HasDerivAt (fun (z : ℂ) ↦ z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z
have h : z ^ t / 2 = (t + 1) * id z ^ (t + 1 - 1) * 1 / (2 * (t + 1))
Tactic: convert!
        (HasDerivAt.cpow_const (c := t + 1) (hasDerivAt_id _) (Or.inl hz)).div_const
          (2 * (t + 1)) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
h : x ∈ [[a, b]]
f : HasDerivAt (fun (y : ℂ) ↦ 1 + HPow.hPow (β := ℕ) y 2) (2 * (↑x : ℂ)) (↑x : ℂ)
⊢ HasDerivAt (fun {b : ℝ} ↦ (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ (t + 1) / (2 * (t + 1)))
    ((↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ t) x
have g : ∀ {z : ℂ}, 0 < z.re → HasDerivAt (fun (z : ℂ) ↦ z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z
Tactic: have g :
      ∀ {z : ℂ}, 0 < z.re → HasDerivAt (fun z => z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z := by
      intro z hz
      convert!
        (HasDerivAt.cpow_const (c := t + 1) (hasDerivAt_id _) (Or.inl hz)).div_const
          (2 * (t + 1)) using 1
      simp [field]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
h : x ∈ [[a, b]]
f : HasDerivAt (fun (y : ℂ) ↦ 1 + HPow.hPow (β := ℕ) y 2) (2 * (↑x : ℂ)) (↑x : ℂ)
g : ∀ {z : ℂ}, 0 < z.re → HasDerivAt (fun (z : ℂ) ↦ z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z
⊢ HasDerivAt (fun {b : ℝ} ↦ (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ (t + 1) / (2 * (t + 1)))
    ((↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ t) x
have h : (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ t = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ t / 2 * (2 * (↑x : ℂ))
Tactic: convert! (HasDerivAt.comp (↑x) (g _) f).comp_ofReal using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
h_1 : x ∈ [[a, b]]
f : HasDerivAt (fun (y : ℂ) ↦ 1 + HPow.hPow (β := ℕ) y 2) (2 * (↑x : ℂ)) (↑x : ℂ)
g : ∀ {z : ℂ}, 0 < z.re → HasDerivAt (fun (z : ℂ) ↦ z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z
h : (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ t = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ t / 2 * (2 * (↑x : ℂ))
⊢ HasDerivAt (fun {b : ℝ} ↦ (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ (t + 1) / (2 * (t + 1)))
    ((↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ t) x
have hderiv : 0 < (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2).re
Tactic: convert! (HasDerivAt.comp (↑x) (g _) f).comp_ofReal using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ IntervalIntegrable (ε := ℂ) (fun (y : ℝ) ↦ (↑y : ℂ) * (1 + HPow.hPow (β := ℕ) (↑y : ℂ) 2) ^ t) MeasureTheory.volume a
    b
have hint : Continuous (Y := ℂ) fun (y : ℝ) ↦ (↑y : ℂ) * (1 + HPow.hPow (β := ℕ) (↑y : ℂ) 2) ^ t
Tactic: apply Continuous.intervalIntegrable
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ Continuous (Y := ℂ) fun (y : ℝ) ↦ (↑y : ℂ) * (1 + HPow.hPow (β := ℕ) (↑y : ℂ) 2) ^ t
have hint : Continuous (Y := ℂ) fun (y : ℝ) ↦ (1 + HPow.hPow (β := ℕ) (↑y : ℂ) 2) ^ t
Tactic: refine continuous_ofReal.mul ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ Continuous (Y := ℂ) fun (y : ℝ) ↦ (1 + HPow.hPow (β := ℕ) (↑y : ℂ) 2) ^ t
have hint : ∀ (a : ℝ), 1 + HPow.hPow (β := ℕ) (↑a : ℂ) 2 ∈ slitPlane
Tactic: apply Continuous.cpow (by fun_prop) continuous_const
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a_1 b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
a : ℝ
⊢ 1 + HPow.hPow (β := ℕ) (↑a : ℂ) 2 ∈ slitPlane
have hint : (↑(1 + HPow.hPow (β := ℕ) a 2) : ℂ) ∈ slitPlane
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b t : ℝ
ht : t ≠ -1
x s : ℝ
⊢ (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑s : ℂ)
have norm_cast : (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (↑(1 + HPow.hPow (β := ℕ) x 2) : ℂ) ^ (↑s : ℂ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b t : ℝ
ht : t ≠ -1
x s : ℝ
⊢ (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (↑(1 + HPow.hPow (β := ℕ) x 2) : ℂ) ^ (↑s : ℂ)
have hx : 0 ≤ 1 + HPow.hPow (β := ℕ) x 2
Tactic: rw [ofReal_cpow, ofReal_add, ofReal_pow, ofReal_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b t : ℝ
ht : t ≠ -1
⊢ ∫ (x : ℝ) in a..b, x * (1 + HPow.hPow (β := ℕ) x 2) ^ t =
    (1 + HPow.hPow (β := ℕ) b 2) ^ (t + 1) / (2 * (t + 1)) - (1 + HPow.hPow (β := ℕ) a 2) ^ (t + 1) / (2 * (t + 1))
have this : ∀ (x s : ℝ), (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑s : ℂ)
Tactic: have : ∀ x s : ℝ, (((↑1 + x ^ 2) ^ s : ℝ) : ℂ) = (1 + (x : ℂ) ^ 2) ^ (s : ℂ) := by
    intro x s
    norm_cast
    rw [ofReal_cpow, ofReal_add, ofReal_pow, ofReal_one]
    exact add_nonneg zero_le_one (sq_nonneg x)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑s : ℂ)
⊢ ∫ (x : ℝ) in a..b, x * (1 + HPow.hPow (β := ℕ) x 2) ^ t =
    (1 + HPow.hPow (β := ℕ) b 2) ^ (t + 1) / (2 * (t + 1)) - (1 + HPow.hPow (β := ℕ) a 2) ^ (t + 1) / (2 * (t + 1))
have rw : (↑(∫ (x : ℝ) in a..b, x * (1 + HPow.hPow (β := ℕ) x 2) ^ t) : ℂ) =
  (↑((1 + HPow.hPow (β := ℕ) b 2) ^ (t + 1) / (2 * (t + 1)) - (1 + HPow.hPow (β := ℕ) a 2) ^ (t + 1) / (2 * (t + 1))) :
    ℂ)
Tactic: rw [← ofReal_inj]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑s : ℂ)
⊢ (↑(∫ (x : ℝ) in a..b, x * (1 + HPow.hPow (β := ℕ) x 2) ^ t) : ℂ) =
    (↑((1 + HPow.hPow (β := ℕ) b 2) ^ (t + 1) / (2 * (t + 1)) -
          (1 + HPow.hPow (β := ℕ) a 2) ^ (t + 1) / (2 * (t + 1))) :
      ℂ)
have h : (↑(∫ (x : ℝ) in a..b, x * (1 + HPow.hPow (β := ℕ) x 2) ^ t) : ℂ) =
  ∫ (x : ℝ) in a..b, (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑t : ℂ)
Tactic: convert! integral_mul_cpow_one_add_sq (_ : (t : ℂ) ≠ -1)