-- 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:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
⊢ 0 < (v + 1).re

Tactic:
rw [add_re, one_re]

Result:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
⊢ 0 < v.re + 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)
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 y => u * (↑y ^ (u - 1) * (1 - ↑y) ^ v)) volume 0 1

Tactic:
apply IntervalIntegrable.const_mul

Result:
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

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)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x
⊢ HasDerivAt (fun y => (1 - y) ^ v) (-v * (1 - ↑x) ^ (v - 1)) ↑x

Tactic:
have A := @HasDerivAt.cpow_const _ _ _ v (hasDerivAt_id (1 - (x : ℂ))) (Or.inl ?_)

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 => 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

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
⊢ u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v

Tactic:
have hF0 : F 0 = 0 := by
  simp only [F, mul_eq_zero, ofReal_zero, cpow_eq_zero_iff, eq_self_iff_true, Ne,
    true_and, sub_zero, one_cpow, one_ne_zero, or_false]
  contrapose! hu; rw [hu, zero_re]

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
⊢ 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
⊢ u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v

Tactic:
have hu' : 0 < re (u + 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
⊢ u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v

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)
B : HasDerivAt (fun y => 1 - y) (-1) ↑x
⊢ HasDerivAt (fun y => (1 - y) ^ v) (-v * (1 - ↑x) ^ (v - 1)) ↑x

Tactic:
convert HasDerivAt.comp (↑x) A B using 1

Result:
case h.e'_9
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
⊢ -v * (1 - ↑x) ^ (v - 1) = v * (1 - ↑x) ^ (v - 1) * 1 * -1

Proof state:
case h.e'_9
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
⊢ -v * (1 - ↑x) ^ (v - 1) = v * (1 - ↑x) ^ (v - 1) * 1 * -1

Tactic:
ring

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
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
⊢ u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v

Tactic:
have int_ev := intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le zero_le_one hc hder h_int

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
⊢ u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v

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 => id x ^ u) (u * id ↑x ^ (u - 1) * 1) ↑x
⊢ HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x

Tactic:
simp only [id_eq, mul_one] at this

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
this : HasDerivAt (fun x => x ^ u) (u * ↑x ^ (u - 1)) ↑x
⊢ HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x