a b : ℝ
n : ℕ
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))
a b : ℝ
n : ℕ
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))
have : t + 1 ≠ 0 := by contrapose! ht; rwa [add_eq_zero_iff_eq_neg] at ht
case hderiv
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun {b} => (1 + ↑b ^ 2) ^ (t + 1) / (↑2 * (t + 1))) (↑x * (1 + ↑x ^ 2) ^ t) x

case hint
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ IntervalIntegrable (fun y => ↑y * (1 + ↑y ^ 2) ^ t) MeasureTheory.volume a b
a b : ℝ
n : ℕ
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))
apply integral_eq_sub_of_hasDerivAt
a b : ℝ
n : ℕ
t : ℂ
ht : t + 1 = 0
⊢ t = -1
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
⊢ t + 1 ≠ 0
contrapose! ht
no goals
a b : ℝ
n : ℕ
t : ℂ
ht : t + 1 = 0
⊢ t = -1
rwa [add_eq_zero_iff_eq_neg] at ht
case hderiv
a b : ℝ
n : ℕ
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
case hderiv
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun {b} => (1 + ↑b ^ 2) ^ (t + 1) / (↑2 * (t + 1))) (↑x * (1 + ↑x ^ 2) ^ t) x
intro x _
case hderiv
a b : ℝ
n : ℕ
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
case hderiv
a b : ℝ
n : ℕ
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
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
  field_simp
  ring
case h.e'_6
a b : ℝ
n : ℕ
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
⊢ (fun {b} => (1 + ↑b ^ 2) ^ (t + 1) / (↑2 * (t + 1))) = fun y =>
    ((fun z => z ^ (t + 1) / (2 * (t + 1))) ∘ fun y => ↑1 + y ^ 2) ↑y

case h.e'_7
a b : ℝ
n : ℕ
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 : ℝ
n : ℕ
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
case hderiv
a b : ℝ
n : ℕ
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
convert (HasDerivAt.comp (↑x) (g _) f).comp_ofReal using 1
case h.e'_6.h.h.e'_5
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
x✝ : ℂ
⊢ ↑1 = 1

case h.e'_7.h.e'_6
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
⊢ ↑x = ↑x ^ (2 - 1)
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
⊢ HasDerivAt (fun y => ↑1 + y ^ 2) (2 * ↑x) ↑x
convert (hasDerivAt_pow 2 (x : ℂ)).const_add 1
no goals
case h.e'_6.h.h.e'_5
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
x✝ : ℂ
⊢ ↑1 = 1
norm_cast
no goals
case h.e'_7.h.e'_6
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
⊢ ↑x = ↑x ^ (2 - 1)
simp
a b : ℝ
n : ℕ
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
a b : ℝ
n : ℕ
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
intro z hz
case h.e'_7
a b : ℝ
n : ℕ
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))
a b : ℝ
n : ℕ
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
convert (HasDerivAt.cpow_const (c := t + 1) (hasDerivAt_id _)
  (Or.inl hz)).div_const (2 * (t + 1)) using 1
case h.e'_7
a b : ℝ
n : ℕ
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
case h.e'_7
a b : ℝ
n : ℕ
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))
field_simp
no goals
case h.e'_7
a b : ℝ
n : ℕ
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
ring
no goals
case h.e'_6
a b : ℝ
n : ℕ
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
⊢ (fun {b} => (1 + ↑b ^ 2) ^ (t + 1) / (↑2 * (t + 1))) = fun y =>
    ((fun z => z ^ (t + 1) / (2 * (t + 1))) ∘ fun y => ↑1 + y ^ 2) ↑y
simp
case h.e'_7
a b : ℝ
n : ℕ
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)
case h.e'_7
a b : ℝ
n : ℕ
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)
field_simp
no goals
case h.e'_7
a b : ℝ
n : ℕ
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)
ring
no goals
case hderiv
a b : ℝ
n : ℕ
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
exact_mod_cast add_pos_of_pos_of_nonneg zero_lt_one (sq_nonneg x)
case hint.hu
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ Continuous fun y => ↑y * (1 + ↑y ^ 2) ^ t
case hint
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ IntervalIntegrable (fun y => ↑y * (1 + ↑y ^ 2) ^ t) MeasureTheory.volume a b
apply Continuous.intervalIntegrable
case hint.hu
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ Continuous fun y => (1 + ↑y ^ 2) ^ t
case hint.hu
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ Continuous fun y => ↑y * (1 + ↑y ^ 2) ^ t
refine' continuous_ofReal.mul _
case hint.hu.hf
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ Continuous fun x => 1 + ↑x ^ 2

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

case hint.hu.h0
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ ∀ (a : ℝ), 0 < (1 + ↑a ^ 2).re ∨ (1 + ↑a ^ 2).im ≠ 0
case hint.hu
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ Continuous fun y => (1 + ↑y ^ 2) ^ t
apply Continuous.cpow
no goals
case hint.hu.hf
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ Continuous fun x => 1 + ↑x ^ 2
exact continuous_const.add (continuous_ofReal.pow 2)
no goals
case hint.hu.hg
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ Continuous fun x => t
exact continuous_const
case hint.hu.h0
a✝ b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
a : ℝ
⊢ 0 < (1 + ↑a ^ 2).re ∨ (1 + ↑a ^ 2).im ≠ 0
case hint.hu.h0
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ ∀ (a : ℝ), 0 < (1 + ↑a ^ 2).re ∨ (1 + ↑a ^ 2).im ≠ 0
intro a
case hint.hu.h0
a✝ b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
a : ℝ
⊢ 0 < 1 + a ^ 2 ∨ (1 + ↑(a ^ 2)).im ≠ 0
case hint.hu.h0
a✝ b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
a : ℝ
⊢ 0 < (1 + ↑a ^ 2).re ∨ (1 + ↑a ^ 2).im ≠ 0
rw [add_re, one_re, ← ofReal_pow, ofReal_re]
no goals
case hint.hu.h0
a✝ b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
a : ℝ
⊢ 0 < 1 + a ^ 2 ∨ (1 + ↑(a ^ 2)).im ≠ 0
exact Or.inl (add_pos_of_pos_of_nonneg zero_lt_one (sq_nonneg a))