a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ (∫ (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 : ∀ 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)
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ ↑(∫ (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
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ (∫ (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))
rw [← ofReal_inj]
case h.e'_2
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ ↑(∫ (x : ℝ) in a..b, x * (1 + x ^ 2) ^ t) = ∫ (x : ℝ) in ?convert_1..?convert_2, ↑x * (1 + ↑x ^ 2) ^ ↑t

case h.e'_3
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ ↑((1 + b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + a ^ 2) ^ (t + 1) / (2 * (t + 1))) =
    (1 + ↑?convert_2 ^ 2) ^ (↑t + 1) / (↑2 * (↑t + 1)) - (1 + ↑?convert_1 ^ 2) ^ (↑t + 1) / (2 * (↑t + 1))

case convert_1
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ ℝ

case convert_2
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ ℝ

case convert_3
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ ↑t ≠ -1
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ ↑(∫ (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)))
convert integral_mul_cpow_one_add_sq (_ : (t : ℂ) ≠ -1)
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
x s : ℝ
⊢ ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
⊢ ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
intro x s
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
x s : ℝ
⊢ ↑((1 + x ^ 2) ^ s) = ↑(1 + x ^ 2) ^ ↑s
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
x s : ℝ
⊢ ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
norm_cast
case hx
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
x s : ℝ
⊢ 0 ≤ 1 + x ^ 2
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
x s : ℝ
⊢ ↑((1 + x ^ 2) ^ s) = ↑(1 + x ^ 2) ^ ↑s
rw [ofReal_cpow, ofReal_add, ofReal_pow, ofReal_one]
no goals
case hx
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
x s : ℝ
⊢ 0 ≤ 1 + x ^ 2
exact add_nonneg zero_le_one (sq_nonneg x)
case h.e'_2
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ (∫ (x : ℝ) in a..b, ↑(x * (1 + x ^ 2) ^ t)) = ∫ (x : ℝ) in ?convert_1..?convert_2, ↑x * (1 + ↑x ^ 2) ^ ↑t

case convert_1
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ ℝ

case convert_2
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ ℝ
case h.e'_2
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ ↑(∫ (x : ℝ) in a..b, x * (1 + x ^ 2) ^ t) = ∫ (x : ℝ) in ?convert_1..?convert_2, ↑x * (1 + ↑x ^ 2) ^ ↑t
rw [← intervalIntegral.integral_ofReal]
case h.e'_2.e_f.h
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
x : ℝ
⊢ ↑(x * (1 + x ^ 2) ^ t) = ↑x * (1 + ↑x ^ 2) ^ ↑t
case h.e'_2
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ (∫ (x : ℝ) in a..b, ↑(x * (1 + x ^ 2) ^ t)) = ∫ (x : ℝ) in ?convert_1..?convert_2, ↑x * (1 + ↑x ^ 2) ^ ↑t

case convert_1
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ ℝ

case convert_2
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ ℝ
congr with x : 1
case h.e'_2.e_f.h
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
x : ℝ
⊢ ↑x * (↑1 + ↑x ^ 2) ^ ↑t = ↑x * (1 + ↑x ^ 2) ^ ↑t
case h.e'_2.e_f.h
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
x : ℝ
⊢ ↑(x * (1 + x ^ 2) ^ t) = ↑x * (1 + ↑x ^ 2) ^ ↑t
rw [ofReal_mul, this x t]
no goals
case h.e'_2.e_f.h
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
x : ℝ
⊢ ↑x * (↑1 + ↑x ^ 2) ^ ↑t = ↑x * (1 + ↑x ^ 2) ^ ↑t
norm_cast
case h.e'_3
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ (↑1 + ↑b ^ 2) ^ ↑(t + 1) / ↑(2 * (t + 1)) - (↑1 + ↑a ^ 2) ^ ↑(t + 1) / ↑(2 * (t + 1)) =
    (1 + ↑b ^ 2) ^ (↑t + 1) / (↑2 * (↑t + 1)) - (1 + ↑a ^ 2) ^ (↑t + 1) / (2 * (↑t + 1))
case h.e'_3
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ ↑((1 + b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + a ^ 2) ^ (t + 1) / (2 * (t + 1))) =
    (1 + ↑b ^ 2) ^ (↑t + 1) / (↑2 * (↑t + 1)) - (1 + ↑a ^ 2) ^ (↑t + 1) / (2 * (↑t + 1))
simp_rw [ofReal_sub, ofReal_div, this a (t + 1), this b (t + 1)]
case h.e'_3
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ (1 + ↑b ^ 2) ^ (↑t + 1) / (2 * (↑t + 1)) - (1 + ↑a ^ 2) ^ (↑t + 1) / (2 * (↑t + 1)) =
    (1 + ↑b ^ 2) ^ (↑t + 1) / (2 * (↑t + 1)) - (1 + ↑a ^ 2) ^ (↑t + 1) / (2 * (↑t + 1))
case h.e'_3
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ (↑1 + ↑b ^ 2) ^ ↑(t + 1) / ↑(2 * (t + 1)) - (↑1 + ↑a ^ 2) ^ ↑(t + 1) / ↑(2 * (t + 1)) =
    (1 + ↑b ^ 2) ^ (↑t + 1) / (↑2 * (↑t + 1)) - (1 + ↑a ^ 2) ^ (↑t + 1) / (2 * (↑t + 1))
push_cast
no goals
case h.e'_3
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ (1 + ↑b ^ 2) ^ (↑t + 1) / (2 * (↑t + 1)) - (1 + ↑a ^ 2) ^ (↑t + 1) / (2 * (↑t + 1)) =
    (1 + ↑b ^ 2) ^ (↑t + 1) / (2 * (↑t + 1)) - (1 + ↑a ^ 2) ^ (↑t + 1) / (2 * (↑t + 1))
rfl
case convert_3
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ ¬t = -1
case convert_3
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ ↑t ≠ -1
rw [← ofReal_one, ← ofReal_neg, Ne.def, ofReal_inj]
no goals
case convert_3
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ ¬t = -1
exact ht