-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_mul_cpow_one_add_sq {t : ℂ} (ht : t ≠ -1) :
    (∫ x : ℝ in a..b, (x : ℂ) * ((1 : ℂ) + ↑x ^ 2) ^ t) =
      ((1 : ℂ) + (b : ℂ) ^ 2) ^ (t + 1) / (2 * (t + ↑1)) -
      ((1 : ℂ) + (a : ℂ) ^ 2) ^ (t + 1) / (2 * (t + ↑1))

Proof state:
case hint.hu
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ Continuous fun y => ↑y * (1 + ↑y ^ 2) ^ t

Tactic:
refine continuous_ofReal.mul ?_

Result:
case hint.hu
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ Continuous fun y => (1 + ↑y ^ 2) ^ t

Proof state:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y => 1 + y ^ 2) (2 * ↑x) ↑x
⊢ ∀ {z : ℂ}, 0 < z.re → HasDerivAt (fun z => z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z

Tactic:
intro z hz

Result:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y => 1 + y ^ 2) (2 * ↑x) ↑x
z : ℂ
hz : 0 < z.re
⊢ HasDerivAt (fun z => z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z

Proof state:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y => 1 + y ^ 2) (2 * ↑x) ↑x
z : ℂ
hz : 0 < z.re
⊢ 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

Result:
case h.e'_9
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y => 1 + y ^ 2) (2 * ↑x) ↑x
z : ℂ
hz : 0 < z.re
⊢ z ^ t / 2 = (t + 1) * id z ^ (t + 1 - 1) * 1 / (2 * (t + 1))

Proof state:
a b : ℝ
t : ℂ
ht : t + 1 = 0
⊢ t = -1

Tactic:
rwa [add_eq_zero_iff_eq_neg] at ht

Result:
no goals

Proof state:
case hint.hu.hf
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ Continuous fun x => 1 + ↑x ^ 2

Tactic:
exact continuous_const.add (continuous_ofReal.pow 2)

Result:
no goals

Proof state:
case hderiv
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ ∀ x ∈ [[a, b]], HasDerivAt (fun {b} => (1 + ↑b ^ 2) ^ (t + 1) / (2 * (t + 1))) (↑x * (1 + ↑x ^ 2) ^ t) x

Tactic:
intro x _

Result:
case hderiv
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
⊢ HasDerivAt (fun {b} => (1 + ↑b ^ 2) ^ (t + 1) / (2 * (t + 1))) (↑x * (1 + ↑x ^ 2) ^ t) x

Proof state:
case hderiv
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y => 1 + 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 + ↑x ^ 2).re

Tactic:
exact mod_cast add_pos_of_pos_of_nonneg zero_lt_one (sq_nonneg x)

Result:
no goals

Proof state:
a b : ℝ
t : ℂ
ht : t ≠ -1
⊢ ∫ (x : ℝ) in a..b, ↑x * (1 + ↑x ^ 2) ^ t =
    (1 + ↑b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + ↑a ^ 2) ^ (t + 1) / (2 * (t + 1))

Tactic:
have : t + 1 ≠ 0 := by contrapose! ht; rwa [add_eq_zero_iff_eq_neg] at ht

Result:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ ∫ (x : ℝ) in a..b, ↑x * (1 + ↑x ^ 2) ^ t =
    (1 + ↑b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + ↑a ^ 2) ^ (t + 1) / (2 * (t + 1))

Proof state:
case hderiv
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
⊢ HasDerivAt (fun {b} => (1 + ↑b ^ 2) ^ (t + 1) / (2 * (t + 1))) (↑x * (1 + ↑x ^ 2) ^ t) x

Tactic:
have f : HasDerivAt (fun y : ℂ => 1 + y ^ 2) (2 * x : ℂ) x := by
  convert (hasDerivAt_pow 2 (x : ℂ)).const_add 1
  simp

Result:
case hderiv
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y => 1 + y ^ 2) (2 * ↑x) ↑x
⊢ HasDerivAt (fun {b} => (1 + ↑b ^ 2) ^ (t + 1) / (2 * (t + 1))) (↑x * (1 + ↑x ^ 2) ^ t) x

Proof state:
case hint.hu.h0
a✝ b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
a : ℝ
⊢ 1 + ↑a ^ 2 ∈ slitPlane

Tactic:
norm_cast

Result:
case hint.hu.h0
a✝ b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
a : ℝ
⊢ ↑(1 + a ^ 2) ∈ slitPlane

Proof state:
case hint.hu.h0
a✝ b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
a : ℝ
⊢ ↑(1 + a ^ 2) ∈ slitPlane

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

Result:
no goals

Proof state:
case h.e'_9.h.e'_6
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
⊢ ↑x = ↑x ^ (2 - 1)

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_9
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y => 1 + y ^ 2) (2 * ↑x) ↑x
z : ℂ
hz : 0 < z.re
⊢ z ^ t * (2 * (t + 1)) = (t + 1) * z ^ t * 2

Tactic:
ring

Result:
no goals

Proof state:
case hint.hu.h0
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ ∀ (a : ℝ), 1 + ↑a ^ 2 ∈ slitPlane

Tactic:
intro a

Result:
case hint.hu.h0
a✝ b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
a : ℝ
⊢ 1 + ↑a ^ 2 ∈ slitPlane

Proof state:
case hint.hu.hg
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ Continuous fun x => t

Tactic:
exact continuous_const

Result:
no goals

Proof state:
case hint
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ IntervalIntegrable (fun y => ↑y * (1 + ↑y ^ 2) ^ t) MeasureTheory.volume a b

Tactic:
apply Continuous.intervalIntegrable

Result:
case hint.hu
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ Continuous fun y => ↑y * (1 + ↑y ^ 2) ^ t

Proof state:
case hint.hu
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ Continuous fun y => (1 + ↑y ^ 2) ^ t

Tactic:
apply Continuous.cpow

Result:
case hint.hu.hf
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ Continuous fun x => 1 + ↑x ^ 2

case hint.hu.hg
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ Continuous fun x => t

case hint.hu.h0
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ ∀ (a : ℝ), 1 + ↑a ^ 2 ∈ slitPlane

Proof state:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
⊢ HasDerivAt (fun y => 1 + y ^ 2) (2 * ↑x) ↑x

Tactic:
convert (hasDerivAt_pow 2 (x : ℂ)).const_add 1

Result:
case h.e'_9.h.e'_6
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
⊢ ↑x = ↑x ^ (2 - 1)

Proof state:
case hderiv
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y => 1 + 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 + ↑b ^ 2) ^ (t + 1) / (2 * (t + 1))) (↑x * (1 + ↑x ^ 2) ^ t) x

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

Result:
case h.e'_9
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y => 1 + 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 + ↑x ^ 2) ^ t = (1 + ↑x ^ 2) ^ t / 2 * (2 * ↑x)

case hderiv
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y => 1 + 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 + ↑x ^ 2).re

Proof state:
case h.e'_9
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y => 1 + 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 + ↑x ^ 2) ^ t = (1 + ↑x ^ 2) ^ t / 2 * (2 * ↑x)

Tactic:
field_simp

Result:
case h.e'_9
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y => 1 + 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 + ↑x ^ 2) ^ t * 2 = (1 + ↑x ^ 2) ^ t * (2 * ↑x)

Proof state:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ ∫ (x : ℝ) in a..b, ↑x * (1 + ↑x ^ 2) ^ t =
    (1 + ↑b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + ↑a ^ 2) ^ (t + 1) / (2 * (t + 1))

Tactic:
apply integral_eq_sub_of_hasDerivAt

Result:
case hderiv
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ ∀ x ∈ [[a, b]], HasDerivAt (fun {b} => (1 + ↑b ^ 2) ^ (t + 1) / (2 * (t + 1))) (↑x * (1 + ↑x ^ 2) ^ t) x

case hint
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ IntervalIntegrable (fun y => ↑y * (1 + ↑y ^ 2) ^ t) MeasureTheory.volume a b