-- Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
theorem betaIntegral_convergent_left {u : ℂ} (hu : 0 < re u) (v : ℂ) :
    IntervalIntegrable (fun x =>
      (x : ℂ) ^ (u - 1) * (1 - (x : ℂ)) ^ (v - 1) : ℝ → ℂ) volume 0 (1 / 2)

Proof state:
case hg.hcont.hg
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
⊢ ContinuousAt (fun x => v - 1) x

Tactic:
exact continuousAt_const

Result:
no goals

Proof state:
case hf
u : ℂ
hu : 0 < u.re
v : ℂ
⊢ IntervalIntegrable (fun x => ↑x ^ (u - 1)) volume 0 (1 / 2)

Tactic:
refine intervalIntegral.intervalIntegrable_cpow' ?_

Result:
case hf
u : ℂ
hu : 0 < u.re
v : ℂ
⊢ -1 < (u - 1).re

Proof state:
case hg.hcont.h0
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
⊢ 1 - ↑x ∈ slitPlane

Tactic:
norm_cast

Result:
case hg.hcont.h0
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
⊢ ↑(1 - x) ∈ slitPlane

Proof state:
case hg.hcont
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
⊢ ContinuousAt (fun x => (1 - ↑x) ^ (v - 1)) x

Tactic:
apply ContinuousAt.cpow

Result:
case hg.hcont.hf
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
⊢ ContinuousAt (fun x => 1 - ↑x) x

case hg.hcont.hg
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
⊢ ContinuousAt (fun x => v - 1) x

case hg.hcont.h0
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
⊢ 1 - ↑x ∈ slitPlane

Proof state:
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ uIcc 0 (1 / 2)
⊢ 0 ≤ 1 / 2

Tactic:
positivity

Result:
no goals

Proof state:
case hg
u : ℂ
hu : 0 < u.re
v : ℂ
⊢ ContinuousOn (fun x => (1 - ↑x) ^ (v - 1)) (uIcc 0 (1 / 2))

Tactic:
apply continuousOn_of_forall_continuousAt

Result:
case hg.hcont
u : ℂ
hu : 0 < u.re
v : ℂ
⊢ ∀ x ∈ uIcc 0 (1 / 2), ContinuousAt (fun x => (1 - ↑x) ^ (v - 1)) x

Proof state:
case hg.hcont
u : ℂ
hu : 0 < u.re
v : ℂ
⊢ ∀ x ∈ uIcc 0 (1 / 2), ContinuousAt (fun x => (1 - ↑x) ^ (v - 1)) x

Tactic:
intro x hx

Result:
case hg.hcont
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ uIcc 0 (1 / 2)
⊢ ContinuousAt (fun x => (1 - ↑x) ^ (v - 1)) x

Proof state:
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
⊢ 0 < 1 - x

Tactic:
linarith only [hx.2]

Result:
no goals

Proof state:
case hg.hcont
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ uIcc 0 (1 / 2)
⊢ ContinuousAt (fun x => (1 - ↑x) ^ (v - 1)) x

Tactic:
rw [uIcc_of_le (by positivity : (0 : ℝ) ≤ 1 / 2)] at hx

Result:
case hg.hcont
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
⊢ ContinuousAt (fun x => (1 - ↑x) ^ (v - 1)) x

Proof state:
case hf
u : ℂ
hu : 0 < u.re
v : ℂ
⊢ -1 < (u - 1).re

Tactic:
rwa [sub_re, one_re, ← zero_sub, sub_lt_sub_iff_right]

Result:
no goals

Proof state:
case hg.hcont.hf
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
⊢ ContinuousAt (fun x => 1 - ↑x) x

Tactic:
exact (continuous_const.sub continuous_ofReal).continuousAt

Result:
no goals

Proof state:
case hg.hcont.h0
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
⊢ ↑(1 - x) ∈ slitPlane

Tactic:
exact ofReal_mem_slitPlane.2 <| by linarith only [hx.2]

Result:
no goals

Proof state:
u : ℂ
hu : 0 < u.re
v : ℂ
⊢ IntervalIntegrable (fun x => ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)) volume 0 (1 / 2)

Tactic:
apply IntervalIntegrable.mul_continuousOn

Result:
case hf
u : ℂ
hu : 0 < u.re
v : ℂ
⊢ IntervalIntegrable (fun x => ↑x ^ (u - 1)) volume 0 (1 / 2)

case hg
u : ℂ
hu : 0 < u.re
v : ℂ
⊢ ContinuousOn (fun x => (1 - ↑x) ^ (v - 1)) (uIcc 0 (1 / 2))