awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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 : ℂ)

Tactic:
have f : HasDerivAt (fun y : ℂ => 1 + y ^ 2) (2 * x : ℂ) x := by
      convert! (hasDerivAt_pow 2 (x : ℂ)).const_add 1
      simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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 (x : ℂ) ↦ id x ^ (t + 1) / (2 * (t + 1))) ((t + 1) * id z ^ (t + 1 - 1) * 1 / (2 * (t + 1))) z

Tactic:
(HasDerivAt.cpow_const (c := t + 1) (hasDerivAt_id _) (Or.inl hz)).div_const
          (2 * (t + 1))

Premises used: HMul.hMul, hasDerivAt_id, HAdd.hAdd, HasDerivAt.div_const, Or.inl, OfNat.ofNat, HasDerivAt.cpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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 : ℂ)
z : ℂ
hz : 0 < z.re
h : z ^ t / 2 = (t + 1) * id z ^ (t + 1 - 1) * 1 / (2 * (t + 1))
⊢ HasDerivAt (fun (z : ℂ) ↦ z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z

Tactic:
convert!
        (HasDerivAt.cpow_const (c := t + 1) (hasDerivAt_id _) (Or.inl hz)).div_const
          (2 * (t + 1)) using 1

Premises used: HMul.hMul, hasDerivAt_id, HAdd.hAdd, HasDerivAt.div_const, Or.inl, OfNat.ofNat, HasDerivAt.cpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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
⊢ z ^ t / 2 = (t + 1) * id z ^ (t + 1 - 1) * 1 / (2 * (t + 1))

Tactic:
simp [field]
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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 : ℂ}, 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]
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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 (y : ℝ) ↦ ((fun (z : ℂ) ↦ z ^ (t + 1) / (2 * (t + 1))) ∘ fun (y : ℂ) ↦ 1 + HPow.hPow (β := ℕ) y 2) (↑y : ℂ))
    ((1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ t / 2 * (2 * (↑x : ℂ))) x

Tactic:
(HasDerivAt.comp (↑x) (g _) f).comp_ofReal

Premises used: HasDerivAt.comp_ofReal, HasDerivAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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 : ℂ))
hderiv : 0 < (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2).re
⊢ HasDerivAt (fun {b : ℝ} ↦ (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ (t + 1) / (2 * (t + 1)))
    ((↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ t) x

Tactic:
convert! (HasDerivAt.comp (↑x) (g _) f).comp_ofReal using 1

Premises used: HasDerivAt.comp_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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
⊢ (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ t = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ t / 2 * (2 * (↑x : ℂ))

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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
⊢ 0 < (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2).re

Tactic:
mod_cast add_pos_of_pos_of_nonneg zero_lt_one (sq_nonneg x)

Premises used: congrArg, cast, Complex.ofReal_pow._simp_1, Complex.ofReal, Nat.cast, Complex.re, zero_lt_one, HPow.hPow, HAdd.hAdd, congr, sq_nonneg, LT.lt, congrFun', Nat.cast_zero, OfNat.ofNat, Eq.symm, Nat.cast_one, Complex.ofReal_add._simp_1, add_pos_of_pos_of_nonneg, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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
⊢ 0 < (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2).re

Tactic:
exact mod_cast add_pos_of_pos_of_nonneg zero_lt_one (sq_nonneg x)

Premises used: zero_lt_one, sq_nonneg, add_pos_of_pos_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
hint : Continuous (Y := ℂ) fun (y : ℝ) ↦ (↑y : ℂ) * (1 + HPow.hPow (β := ℕ) (↑y : ℂ) 2) ^ t
⊢ IntervalIntegrable (ε := ℂ) (fun (y : ℝ) ↦ (↑y : ℂ) * (1 + HPow.hPow (β := ℕ) (↑y : ℂ) 2) ^ t) MeasureTheory.volume a
    b

Tactic:
apply Continuous.intervalIntegrable

Premises used: Continuous.intervalIntegrable
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ Continuous (Y := ℂ) fun (y : ℝ) ↦ (↑y : ℂ) * (1 + HPow.hPow (β := ℕ) (↑y : ℂ) 2) ^ t

Tactic:
continuous_ofReal.mul ?_

Premises used: Continuous.mul, Complex.continuous_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
hint : Continuous (Y := ℂ) fun (y : ℝ) ↦ (1 + HPow.hPow (β := ℕ) (↑y : ℂ) 2) ^ t
⊢ Continuous (Y := ℂ) fun (y : ℝ) ↦ (↑y : ℂ) * (1 + HPow.hPow (β := ℕ) (↑y : ℂ) 2) ^ t

Tactic:
refine continuous_ofReal.mul ?_

Premises used: Continuous.mul, Complex.continuous_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ Continuous (Y := ℂ) fun (x : ℝ) ↦ 1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
hint : ∀ (a : ℝ), 1 + HPow.hPow (β := ℕ) (↑a : ℂ) 2 ∈ slitPlane
⊢ Continuous (Y := ℂ) fun (y : ℝ) ↦ (1 + HPow.hPow (β := ℕ) (↑y : ℂ) 2) ^ t

Tactic:
apply Continuous.cpow (by fun_prop) continuous_const

Premises used: continuous_const, Continuous.cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a_1 b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
a : ℝ
hint : (↑(1 + HPow.hPow (β := ℕ) a 2) : ℂ) ∈ slitPlane
⊢ 1 + HPow.hPow (β := ℕ) (↑a : ℂ) 2 ∈ slitPlane

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a_1 b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
a : ℝ
⊢ (↑(1 + HPow.hPow (β := ℕ) a 2) : ℂ) ∈ slitPlane

Tactic:
ofReal_mem_slitPlane.2 <| add_pos_of_pos_of_nonneg one_pos <| sq_nonneg a

Premises used: Iff.mpr, Complex.ofReal_mem_slitPlane, sq_nonneg, one_pos, add_pos_of_pos_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a_1 b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
a : ℝ
⊢ (↑(1 + HPow.hPow (β := ℕ) a 2) : ℂ) ∈ slitPlane

Tactic:
exact ofReal_mem_slitPlane.2 <| add_pos_of_pos_of_nonneg one_pos <| sq_nonneg a

Premises used: Iff.mpr, Complex.ofReal_mem_slitPlane, sq_nonneg, one_pos, add_pos_of_pos_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b t : ℝ
ht : t ≠ -1
x s : ℝ
norm_cast : (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (↑(1 + HPow.hPow (β := ℕ) x 2) : ℂ) ^ (↑s : ℂ)
⊢ (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑s : ℂ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b t : ℝ
ht : t ≠ -1
x s : ℝ
hx : 0 ≤ 1 + HPow.hPow (β := ℕ) x 2
⊢ (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (↑(1 + HPow.hPow (β := ℕ) x 2) : ℂ) ^ (↑s : ℂ)

Tactic:
rw [ofReal_cpow, ofReal_add, ofReal_pow, ofReal_one]

Premises used: Complex.ofReal_cpow, Complex.ofReal_add, Complex.ofReal_one, Complex.ofReal_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b t : ℝ
ht : t ≠ -1
x s : ℝ
⊢ 0 ≤ 1 + HPow.hPow (β := ℕ) x 2

Tactic:
add_nonneg zero_le_one (sq_nonneg x)

Premises used: add_nonneg, zero_le_one, sq_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b t : ℝ
ht : t ≠ -1
x s : ℝ
⊢ 0 ≤ 1 + HPow.hPow (β := ℕ) x 2

Tactic:
exact add_nonneg zero_le_one (sq_nonneg x)

Premises used: add_nonneg, zero_le_one, sq_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b t : ℝ
ht : t ≠ -1
⊢ ∀ (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)
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑s : ℂ)
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))) :
      ℂ)
⊢ ∫ (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]

Premises used: Complex.ofReal_inj
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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))

Tactic:
integral_mul_cpow_one_add_sq (_ : (t : ℂ) ≠ -1)

Premises used: integral_mul_cpow_one_add_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑s : ℂ)
h :
  (↑(∫ (x : ℝ) in a..b, x * (1 + HPow.hPow (β := ℕ) x 2) ^ t) : ℂ) =
    ∫ (x : ℝ) in a..b, (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑t : ℂ)
h₁ :
  (↑((1 + HPow.hPow (β := ℕ) b 2) ^ (t + 1) / (2 * (t + 1)) - (1 + HPow.hPow (β := ℕ) a 2) ^ (t + 1) / (2 * (t + 1))) :
      ℂ) =
    (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1)) -
      (1 + HPow.hPow (β := ℕ) (↑a : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1))
convert_1 convert_2 : ℝ
convert_3 : (↑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))) :
      ℂ)

Tactic:
convert! integral_mul_cpow_one_add_sq (_ : (t : ℂ) ≠ -1)

Premises used: integral_mul_cpow_one_add_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑s : ℂ)
h :
  Eq (α := ℂ) (∫ (x : ℝ) in a..b, (↑(x * (1 + HPow.hPow (β := ℕ) x 2) ^ t) : ℂ))
    (∫ (x : ℝ) in a..b, (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑t : ℂ))
⊢ (↑(∫ (x : ℝ) in a..b, x * (1 + HPow.hPow (β := ℕ) x 2) ^ t) : ℂ) =
    ∫ (x : ℝ) in a..b, (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑t : ℂ)

Tactic:
rw [← intervalIntegral.integral_ofReal]

Premises used: intervalIntegral.integral_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑s : ℂ)
h : ∀ (x : ℝ), (↑(x * (1 + HPow.hPow (β := ℕ) x 2) ^ t) : ℂ) = (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑t : ℂ)
⊢ Eq (α := ℂ) (∫ (x : ℝ) in a..b, (↑(x * (1 + HPow.hPow (β := ℕ) x 2) ^ t) : ℂ))
    (∫ (x : ℝ) in a..b, (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑t : ℂ))

Tactic:
congr with x : 1
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑s : ℂ)
x : ℝ
h : (↑x : ℂ) * (↑((1 + HPow.hPow (β := ℕ) x 2) ^ t) : ℂ) = (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑t : ℂ)
h₁ h₂ :
  (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑t : ℂ) = (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑t : ℂ)
⊢ (↑(x * (1 + HPow.hPow (β := ℕ) x 2) ^ t) : ℂ) = (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑t : ℂ)

Tactic:
rw [ofReal_mul, this x t]

Premises used: Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑s : ℂ)
h :
  (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ (↑(t + 1) : ℂ) / (↑(2 * (t + 1)) : ℂ) -
      (1 + HPow.hPow (β := ℕ) (↑a : ℂ) 2) ^ (↑(t + 1) : ℂ) / (↑(2 * (t + 1)) : ℂ) =
    (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1)) -
      (1 + HPow.hPow (β := ℕ) (↑a : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1))
⊢ (↑((1 + HPow.hPow (β := ℕ) b 2) ^ (t + 1) / (2 * (t + 1)) - (1 + HPow.hPow (β := ℕ) a 2) ^ (t + 1) / (2 * (t + 1))) :
      ℂ) =
    (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1)) -
      (1 + HPow.hPow (β := ℕ) (↑a : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1))

Tactic:
simp_rw [ofReal_sub, ofReal_div, this a (t + 1), this b (t + 1)]

Premises used: HAdd.hAdd, Complex.ofReal_div, Complex.ofReal_sub, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑s : ℂ)
h :
  (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1)) -
      (1 + HPow.hPow (β := ℕ) (↑a : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1)) =
    (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1)) -
      (1 + HPow.hPow (β := ℕ) (↑a : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1))
⊢ (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ (↑(t + 1) : ℂ) / (↑(2 * (t + 1)) : ℂ) -
      (1 + HPow.hPow (β := ℕ) (↑a : ℂ) 2) ^ (↑(t + 1) : ℂ) / (↑(2 * (t + 1)) : ℂ) =
    (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1)) -
      (1 + HPow.hPow (β := ℕ) (↑a : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1))

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑s : ℂ)
⊢ (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1)) -
      (1 + HPow.hPow (β := ℕ) (↑a : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1)) =
    (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1)) -
      (1 + HPow.hPow (β := ℕ) (↑a : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1))

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑s : ℂ)
convert_3 : ¬t = -1
⊢ (↑t : ℂ) ≠ -1

Tactic:
rw [← ofReal_one, ← ofReal_neg, Ne, ofReal_inj]

Premises used: Complex.ofReal_neg, Complex.ofReal_one, Ne, Complex.ofReal_inj
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑s : ℂ)
⊢ ¬t = -1

Tactic:
ht
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑s : ℂ)
⊢ ¬t = -1

Tactic:
exact ht
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
α β γ : ℝ
⊢ β * α * γ * α = β * (α * α * γ)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
⊢ ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)

Tactic:
have h : ∀ α β γ : ℝ, β * α * γ * α = β * (α * α * γ) := fun α β γ => by ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
x : ℝ
h_1 : x ∈ [[a, b]]
⊢ HasDerivAt (fun (y : ℝ) ↦ sin y ^ (n + 1)) ((↑(n + 1) : ℝ) * cos x * sin x ^ n) x

Tactic:
simpa only [mul_right_comm] using (hasDerivAt_sin x).pow (n + 1)

Premises used: Real.hasDerivAt_sin, HasDerivAt.pow, HAdd.hAdd, mul_right_comm, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
⊢ ∀ x ∈ [[a, b]], HasDerivAt (fun (y : ℝ) ↦ sin y ^ (n + 1)) ((↑(n + 1) : ℝ) * cos x * sin x ^ n) x

Tactic:
have hu : ∀ x ∈ [[a, b]],
      HasDerivAt (fun y => sin y ^ (n + 1)) ((n + 1 : ℕ) * cos x * sin x ^ n) x :=
    fun x _ => by simpa only [mul_right_comm] using (hasDerivAt_sin x).pow (n + 1)
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun (y : ℝ) ↦ sin y ^ (n + 1)) ((↑(n + 1) : ℝ) * cos x * sin x ^ n) x
x : ℝ
h_1 : x ∈ [[a, b]]
⊢ HasDerivAt (-cos) (sin x) x

Tactic:
simpa only [neg_neg] using (hasDerivAt_cos x).neg

Premises used: HasDerivAt.neg, neg_neg, Real.hasDerivAt_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun (y : ℝ) ↦ sin y ^ (n + 1)) ((↑(n + 1) : ℝ) * cos x * sin x ^ n) x
⊢ ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x

Tactic:
have hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x := fun x _ => by
    simpa only [neg_neg] using (hasDerivAt_cos x).neg
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun (y : ℝ) ↦ sin y ^ (n + 1)) ((↑(n + 1) : ℝ) * cos x * sin x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x
refine_3 :
  ∀
    (H :
      ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
        sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a -
          ∫ (x : ℝ) in a..b, (↑(n + 1) : ℝ) * cos x * sin x ^ n * (-cos) x),
    ∫ (x : ℝ) in a..b, sin x ^ (n + 2) =
      (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b +
          HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ n) -
        HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
refine_1 : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (↑(n + 1) : ℝ) * cos x * sin x ^ n) MeasureTheory.volume a b
refine_2 : IntervalIntegrable sin MeasureTheory.volume a b
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ n) -
      HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)

Tactic:
have H := integral_mul_deriv_eq_deriv_mul hu hv ?_ ?_
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun (y : ℝ) ↦ sin y ^ (n + 1)) ((↑(n + 1) : ℝ) * cos x * sin x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a -
      ∫ (x : ℝ) in a..b, (↑(n + 1) : ℝ) * cos x * sin x ^ n * (-cos) x
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) (∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x)

Tactic:
simp only [_root_.pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun (y : ℝ) ↦ sin y ^ (n + 1)) ((↑(n + 1) : ℝ) * cos x * sin x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a -
      ∫ (x : ℝ) in a..b, (↑(n + 1) : ℝ) * cos x * sin x ^ n * (-cos) x
simp : -(sin b ^ (n + 1) * cos b) + sin a ^ (n + 1) * cos a = C
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (cos x) 2 * sin x ^ n

Tactic:
simp [H, h, sq]

Premises used: sq
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun (y : ℝ) ↦ sin y ^ (n + 1)) ((↑(n + 1) : ℝ) * cos x * sin x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a -
      ∫ (x : ℝ) in a..b, (↑(n + 1) : ℝ) * cos x * sin x ^ n * (-cos) x
⊢ -(sin b ^ (n + 1) * cos b) + sin a ^ (n + 1) * cos a = C

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun (y : ℝ) ↦ sin y ^ (n + 1)) ((↑(n + 1) : ℝ) * cos x * sin x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a -
      ∫ (x : ℝ) in a..b, (↑(n + 1) : ℝ) * cos x * sin x ^ n * (-cos) x
⊢ C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (cos x) 2 * sin x ^ n =
    C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ n - sin x ^ (n + 2)

Tactic:
simp [cos_sq', sub_mul, ← pow_add, add_comm]

Premises used: pow_add, add_comm, sub_mul, Real.cos_sq'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun (y : ℝ) ↦ sin y ^ (n + 1)) ((↑(n + 1) : ℝ) * cos x * sin x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a -
      ∫ (x : ℝ) in a..b, (↑(n + 1) : ℝ) * cos x * sin x ^ n * (-cos) x
hf : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ sin x ^ n) MeasureTheory.volume a b
hg : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ sin x ^ (n + 2)) MeasureTheory.volume a b
⊢ C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ n - sin x ^ (n + 2) =
    (C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ n) -
      HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)

Tactic:
rw [integral_sub, mul_sub, add_sub_assoc]

Premises used: add_sub_assoc, mul_sub, intervalIntegral.integral_sub