-- Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
theorem betaIntegral_recurrence {u v : ℂ} (hu : 0 < re u) (hv : 0 < re v) :
    u * betaIntegral u (v + 1) = v * betaIntegral (u + 1) v

Proof state:
case hf.hf
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ x ∈ Ioo 0 1, HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : ∫ (y : ℝ) in 0 ..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = 0
hF0 : F 0 = 0
hF1 : F 1 = 0
⊢ IntervalIntegrable (fun x => ↑x ^ (u - 1) * (1 - ↑x) ^ v) volume 0 1

Tactic:
convert betaIntegral_convergent hu hv'

Result:
case h.e'_3.h.h.e'_6.h.e'_6
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ x ∈ Ioo 0 1, HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : ∫ (y : ℝ) in 0 ..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = 0
hF0 : F 0 = 0
hF1 : F 1 = 0
x✝ : ℝ
⊢ v = v + 1 - 1

Proof state:
case hf
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x
A : HasDerivAt (fun x => x ^ v) (v * (1 - ↑x) ^ (v - 1) * 1) (1 - ↑x)
⊢ HasDerivAt (fun x => x) 1 ↑x

Tactic:
apply hasDerivAt_id

Result:
no goals

Proof state:
case refine_2
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x
A : HasDerivAt (fun x => x ^ v) (v * (1 - ↑x) ^ (v - 1) * 1) (1 - ↑x)
⊢ HasDerivAt (fun y => (1 - y) ^ v) (-v * (1 - ↑x) ^ (v - 1)) ↑x

Tactic:
have B : HasDerivAt (fun y : ℂ => 1 - y) (-1) ↑x := by
  apply HasDerivAt.const_sub; apply hasDerivAt_id

Result:
case refine_2
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x
A : HasDerivAt (fun x => x ^ v) (v * (1 - ↑x) ^ (v - 1) * 1) (1 - ↑x)
B : HasDerivAt (fun y => 1 - y) (-1) ↑x
⊢ HasDerivAt (fun y => (1 - y) ^ v) (-v * (1 - ↑x) ^ (v - 1)) ↑x

Proof state:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ x ∈ Ioo 0 1, HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : ∫ (y : ℝ) in 0 ..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = F 1 - F 0
hF0 : F 0 = 0
⊢ F 1 = 0

Tactic:
simp only [F, mul_eq_zero, ofReal_one, one_cpow, one_ne_zero, sub_self, cpow_eq_zero_iff,
  eq_self_iff_true, Ne, true_and, false_or]

Result:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ x ∈ Ioo 0 1, HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : ∫ (y : ℝ) in 0 ..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = F 1 - F 0
hF0 : F 0 = 0
⊢ ¬v = 0

Proof state:
case refine_2
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
this : HasDerivAt (fun x => x ^ u) (u * ↑x ^ (u - 1)) ↑x
⊢ HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x

Tactic:
exact this

Result:
no goals

Proof state:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
⊢ u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v

Tactic:
have hv' : 0 < re (v + 1) := by rw [add_re, one_re]; positivity

Result:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
⊢ u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v

Proof state:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ x ∈ Ioo 0 1, HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : (u * ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * ∫ (x : ℝ) in 0 ..1, ↑x ^ u * (1 - ↑x) ^ (v - 1) = 0
hF0 : F 0 = 0
hF1 : F 1 = 0
⊢ (u * ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v + 1 - 1)) -
      v * ∫ (x : ℝ) in 0 ..1, ↑x ^ (u + 1 - 1) * (1 - ↑x) ^ (v - 1) =
    0

Tactic:
convert int_ev <;> ring

Result:
no goals

Proof state:
case refine_2
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x
A : HasDerivAt (fun x => id x ^ v) (v * id (1 - ↑x) ^ (v - 1) * 1) (1 - ↑x)
⊢ HasDerivAt (fun y => (1 - y) ^ v) (-v * (1 - ↑x) ^ (v - 1)) ↑x

case refine_1
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x
⊢ 0 < (id (1 - ↑x)).re

Tactic:
swap

Result:
case refine_1
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x
⊢ 0 < (id (1 - ↑x)).re

case refine_2
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x
A : HasDerivAt (fun x => id x ^ v) (v * id (1 - ↑x) ^ (v - 1) * 1) (1 - ↑x)
⊢ HasDerivAt (fun y => (1 - y) ^ v) (-v * (1 - ↑x) ^ (v - 1)) ↑x

Proof state:
case h.e'_3.h.h.e'_6.h.e'_6
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ x ∈ Ioo 0 1, HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : ∫ (y : ℝ) in 0 ..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = 0
hF0 : F 0 = 0
hF1 : F 1 = 0
x✝ : ℝ
⊢ v = v + 1 - 1

Tactic:
ring

Result:
no goals

Proof state:
case refine_1
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
x : ℝ
hx : x ∈ Icc 0 1
⊢ 0 ≤ (↑x).re

Tactic:
rw [ofReal_re]

Result:
case refine_1
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
x : ℝ
hx : x ∈ Icc 0 1
⊢ 0 ≤ x