awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
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 : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) x →
      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
hF1 : F 1 = 0
rw :
  ∀
    (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 * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
hf :
  ∀
    (int_ev :
      Eq (α := ℂ)
        (∫ (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
hg :
  ∀
    (int_ev :
      Eq (α := ℂ)
        (∫ (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 : ℝ) ↦ v * ((↑y : ℂ) ^ u * (1 - (↑y : ℂ)) ^ (v - 1))) volume 0 1
⊢ u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v

Tactic:
rw [hF0, hF1, sub_zero, intervalIntegral.integral_sub, intervalIntegral.integral_const_mul,
    intervalIntegral.integral_const_mul] at int_ev

Premises used: sub_zero, intervalIntegral.integral_sub, intervalIntegral.integral_const_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
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 : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) x →
      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
rw :
  (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
⊢ u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v

Tactic:
rw [betaIntegral, betaIntegral, ← sub_eq_zero]

Premises used: sub_eq_zero, Complex.betaIntegral
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
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 : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) x →
      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) -
      v * ∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ (v - 1) =
    0

Tactic:
int_ev
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
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 : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) x →
      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
h : ∀ (x : ℝ), v + 1 - 1 = v
h₁ : ∀ (x : ℝ), u + 1 - 1 = u
⊢ (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
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
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 : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) x →
      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
x : ℝ
⊢ v + 1 - 1 = v

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
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 : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) x →
      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
x : ℝ
⊢ u + 1 - 1 = u

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
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 : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) x →
      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 :
  Eq (α := ℂ)
    (∫ (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
hf : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (u - 1) * (1 - (↑x : ℂ)) ^ v) volume 0 1
⊢ IntervalIntegrable (ε := ℂ) (fun (y : ℝ) ↦ u * ((↑y : ℂ) ^ (u - 1) * (1 - (↑y : ℂ)) ^ v)) volume 0 1

Tactic:
apply IntervalIntegrable.const_mul

Premises used: IntervalIntegrable.const_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
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 : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) x →
      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 :
  Eq (α := ℂ)
    (∫ (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 + 1 - 1)) volume 0 1

Tactic:
betaIntegral_convergent hu hv'

Premises used: Complex.betaIntegral_convergent
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
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 : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) x →
      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 :
  Eq (α := ℂ)
    (∫ (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
h : ∀ (x : ℝ), v = v + 1 - 1
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (u - 1) * (1 - (↑x : ℂ)) ^ v) volume 0 1

Tactic:
convert! betaIntegral_convergent hu hv'

Premises used: Complex.betaIntegral_convergent
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
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 : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) x →
      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 :
  Eq (α := ℂ)
    (∫ (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
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
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 : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) x →
      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 :
  Eq (α := ℂ)
    (∫ (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
hg : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ (v - 1)) volume 0 1
⊢ IntervalIntegrable (ε := ℂ) (fun (y : ℝ) ↦ v * ((↑y : ℂ) ^ u * (1 - (↑y : ℂ)) ^ (v - 1))) volume 0 1

Tactic:
apply IntervalIntegrable.const_mul

Premises used: IntervalIntegrable.const_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
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 : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) x →
      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 :
  Eq (α := ℂ)
    (∫ (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) * (1 - (↑x : ℂ)) ^ (v - 1)) volume 0 1

Tactic:
betaIntegral_convergent hu' hv

Premises used: Complex.betaIntegral_convergent
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
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 : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) x →
      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 :
  Eq (α := ℂ)
    (∫ (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
h : ∀ (x : ℝ), u = u + 1 - 1
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ (v - 1)) volume 0 1

Tactic:
convert! betaIntegral_convergent hu' hv

Premises used: Complex.betaIntegral_convergent
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
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 : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) x →
      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 :
  Eq (α := ℂ)
    (∫ (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 : ℝ
⊢ u = u + 1 - 1

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u : ℂ
hu : 0 < u.re
zero : 1 / u = HDiv.hDiv (α := ℂ) 1 (∏ j ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1), (u + (↑j : ℂ)))
⊢ u.betaIntegral (HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1) =
    HDiv.hDiv (α := ℂ) (↑0! : ℂ) (∏ j ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1), (u + (↑j : ℂ)))

Tactic:
rw [Nat.cast_zero, zero_add, betaIntegral_eval_one_right hu, Nat.factorial_zero, Nat.cast_one]

Premises used: Complex.betaIntegral_eval_one_right, zero_add, Nat.factorial_zero, Nat.cast_zero, Nat.cast_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u : ℂ
hu : 0 < u.re
⊢ 1 / u = HDiv.hDiv (α := ℂ) 1 (∏ j ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1), (u + (↑j : ℂ)))

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
n : ℕ
IH :
  ∀ {u : ℂ} (hu : 0 < u.re),
    u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) =
      HDiv.hDiv (α := ℂ) (↑n ! : ℂ) (∏ j ∈ Finset.range (n + 1), (u + (↑j : ℂ)))
u : ℂ
hu : 0 < u.re
succ :
  ∀
    (this :
      u * u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n.succ : ℂ) 1) = (↑n.succ : ℂ) * (u + 1).betaIntegral (↑n.succ : ℂ)),
    u.betaIntegral (HAdd.hAdd (α := ℂ) (↑(n + 1) : ℂ) 1) =
      HDiv.hDiv (α := ℂ) (↑(n + 1)! : ℂ) (∏ j ∈ Finset.range (n + 1 + 1), (u + (↑j : ℂ)))
succ₁ : 0 < re (↑n.succ : ℂ)
⊢ u.betaIntegral (HAdd.hAdd (α := ℂ) (↑(n + 1) : ℂ) 1) =
    HDiv.hDiv (α := ℂ) (↑(n + 1)! : ℂ) (∏ j ∈ Finset.range (n + 1 + 1), (u + (↑j : ℂ)))

Tactic:
have := betaIntegral_recurrence hu (?_ : 0 < re n.succ)
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
n : ℕ
IH :
  ∀ {u : ℂ} (hu : 0 < u.re),
    u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) =
      HDiv.hDiv (α := ℂ) (↑n ! : ℂ) (∏ j ∈ Finset.range (n + 1), (u + (↑j : ℂ)))
u : ℂ
hu : 0 < u.re
⊢ LT.lt (α := ℝ) 0 (↑n.succ : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
n : ℕ
IH :
  ∀ {u : ℂ} (hu : 0 < u.re),
    u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) =
      HDiv.hDiv (α := ℂ) (↑n ! : ℂ) (∏ j ∈ Finset.range (n + 1), (u + (↑j : ℂ)))
u : ℂ
hu : 0 < u.re
this : u * u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n.succ : ℂ) 1) = (↑n.succ : ℂ) * (u + 1).betaIntegral (↑n.succ : ℂ)
succ :
  ∀
    (this :
      u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n.succ : ℂ) 1) = (↑n.succ : ℂ) * (u + 1).betaIntegral (↑n.succ : ℂ) / u),
    u.betaIntegral (HAdd.hAdd (α := ℂ) (↑(n + 1) : ℂ) 1) =
      HDiv.hDiv (α := ℂ) (↑(n + 1)! : ℂ) (∏ j ∈ Finset.range (n + 1 + 1), (u + (↑j : ℂ)))
succ₁ :
  ∀
    (this :
      u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n.succ : ℂ) 1) * u = (↑n.succ : ℂ) * (u + 1).betaIntegral (↑n.succ : ℂ)),
    u ≠ 0
⊢ u.betaIntegral (HAdd.hAdd (α := ℂ) (↑(n + 1) : ℂ) 1) =
    HDiv.hDiv (α := ℂ) (↑(n + 1)! : ℂ) (∏ j ∈ Finset.range (n + 1 + 1), (u + (↑j : ℂ)))

Tactic:
rw [mul_comm u _, ← eq_div_iff] at this

Premises used: mul_comm, eq_div_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
n : ℕ
IH :
  ∀ {u : ℂ} (hu : 0 < u.re),
    u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) =
      HDiv.hDiv (α := ℂ) (↑n ! : ℂ) (∏ j ∈ Finset.range (n + 1), (u + (↑j : ℂ)))
u : ℂ
hu : 0 < u.re
this : u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n.succ : ℂ) 1) * u = (↑n.succ : ℂ) * (u + 1).betaIntegral (↑n.succ : ℂ)
succ : ∀ (hu : u = 0), u.re ≤ 0
⊢ u ≠ 0

Tactic:
contrapose! hu
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
n : ℕ
IH :
  ∀ {u : ℂ} (hu : 0 < u.re),
    u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) =
      HDiv.hDiv (α := ℂ) (↑n ! : ℂ) (∏ j ∈ Finset.range (n + 1), (u + (↑j : ℂ)))
u : ℂ
this : u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n.succ : ℂ) 1) * u = (↑n.succ : ℂ) * (u + 1).betaIntegral (↑n.succ : ℂ)
hu : u = 0
succ : re 0 ≤ 0
succ₁ succ₂ : LE.le (α := ℝ) 0 0
⊢ u.re ≤ 0

Tactic:
rw [hu, zero_re]

Premises used: Complex.zero_re
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
n : ℕ
IH :
  ∀ {u : ℂ} (hu : 0 < u.re),
    u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) =
      HDiv.hDiv (α := ℂ) (↑n ! : ℂ) (∏ j ∈ Finset.range (n + 1), (u + (↑j : ℂ)))
u : ℂ
hu : 0 < u.re
this : u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n.succ : ℂ) 1) = (↑n.succ : ℂ) * (u + 1).betaIntegral (↑n.succ : ℂ) / u
succ :
  HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * HDiv.hDiv (α := ℂ) (↑n ! : ℂ) (∏ j ∈ Finset.range (n + 1), (u + 1 + (↑j : ℂ))) / u =
    (↑(n + 1)! : ℂ) / ((∏ k ∈ Finset.range (n + 1), (u + (↑(k + 1) : ℂ))) * (u + (↑0 : ℂ)))
succ₁ : 0 < (u + 1).re
⊢ u.betaIntegral (HAdd.hAdd (α := ℂ) (↑(n + 1) : ℂ) 1) =
    HDiv.hDiv (α := ℂ) (↑(n + 1)! : ℂ) (∏ j ∈ Finset.range (n + 1 + 1), (u + (↑j : ℂ)))

Tactic:
rw [this, Finset.prod_range_succ', Nat.cast_succ, IH]

Premises used: Nat.cast_succ, Finset.prod_range_succ'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
n : ℕ
IH :
  ∀ {u : ℂ} (hu : 0 < u.re),
    u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) =
      HDiv.hDiv (α := ℂ) (↑n ! : ℂ) (∏ j ∈ Finset.range (n + 1), (u + (↑j : ℂ)))
u : ℂ
hu : 0 < u.re
this : u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n.succ : ℂ) 1) = (↑n.succ : ℂ) * (u + 1).betaIntegral (↑n.succ : ℂ) / u
⊢ 0 < u.re + 1

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
n : ℕ
IH :
  ∀ {u : ℂ} (hu : 0 < u.re),
    u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) =
      HDiv.hDiv (α := ℂ) (↑n ! : ℂ) (∏ j ∈ Finset.range (n + 1), (u + (↑j : ℂ)))
u : ℂ
hu : 0 < u.re
this : u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n.succ : ℂ) 1) = (↑n.succ : ℂ) * (u + 1).betaIntegral (↑n.succ : ℂ) / u
succ :
  (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (↑n ! : ℂ) / ∏ j ∈ Finset.range (n + 1), (u + 1 + (↑j : ℂ))) / u =
    (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (↑n ! : ℂ) / ∏ k ∈ Finset.range (n + 1), (u + (↑(k + 1) : ℂ))) / u
⊢ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * HDiv.hDiv (α := ℂ) (↑n ! : ℂ) (∏ j ∈ Finset.range (n + 1), (u + 1 + (↑j : ℂ))) / u =
    (↑(n + 1)! : ℂ) / ((∏ k ∈ Finset.range (n + 1), (u + (↑(k + 1) : ℂ))) * (u + (↑0 : ℂ)))

Tactic:
rw [Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one, Nat.cast_zero, add_zero, ←
      mul_div_assoc, ← div_div]

Premises used: Nat.factorial_succ, mul_div_assoc, Nat.cast_add, Nat.cast_mul, Nat.cast_zero, div_div, add_zero, Nat.cast_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
n : ℕ
IH :
  ∀ {u : ℂ} (hu : 0 < u.re),
    u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) =
      HDiv.hDiv (α := ℂ) (↑n ! : ℂ) (∏ j ∈ Finset.range (n + 1), (u + (↑j : ℂ)))
u : ℂ
hu : 0 < u.re
this : u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n.succ : ℂ) 1) = (↑n.succ : ℂ) * (u + 1).betaIntegral (↑n.succ : ℂ) / u
succ : ∀ (j : ℕ), u + 1 + (↑j : ℂ) = u + (↑(j + 1) : ℂ)
⊢ (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (↑n ! : ℂ) / ∏ j ∈ Finset.range (n + 1), (u + 1 + (↑j : ℂ))) / u =
    (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (↑n ! : ℂ) / ∏ k ∈ Finset.range (n + 1), (u + (↑(k + 1) : ℂ))) / u

Tactic:
congr 3 with j : 1
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
n : ℕ
IH :
  ∀ {u : ℂ} (hu : 0 < u.re),
    u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) =
      HDiv.hDiv (α := ℂ) (↑n ! : ℂ) (∏ j ∈ Finset.range (n + 1), (u + (↑j : ℂ)))
u : ℂ
hu : 0 < u.re
this : u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n.succ : ℂ) 1) = (↑n.succ : ℂ) * (u + 1).betaIntegral (↑n.succ : ℂ) / u
j : ℕ
succ : u + 1 + (↑j : ℂ) = u + HAdd.hAdd (α := ℂ) (↑j : ℂ) 1
⊢ u + 1 + (↑j : ℂ) = u + (↑(j + 1) : ℂ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
n : ℕ
IH :
  ∀ {u : ℂ} (hu : 0 < u.re),
    u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) =
      HDiv.hDiv (α := ℂ) (↑n ! : ℂ) (∏ j ∈ Finset.range (n + 1), (u + (↑j : ℂ)))
u : ℂ
hu : 0 < u.re
this : u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n.succ : ℂ) 1) = (↑n.succ : ℂ) * (u + 1).betaIntegral (↑n.succ : ℂ) / u
j : ℕ
⊢ u + 1 + (↑j : ℂ) = u + HAdd.hAdd (α := ℂ) (↑j : ℂ) 1

Tactic:
abel
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u : ℂ
hu : 0 < u.re
n : ℕ
zero :
  ∀ {u : ℂ} (hu : 0 < u.re),
    u.betaIntegral (HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1) =
      HDiv.hDiv (α := ℂ) (↑0! : ℂ) (∏ j ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1), (u + (↑j : ℂ)))
succ :
  ∀ (n : ℕ)
    (IH :
      ∀ {u : ℂ} (hu : 0 < u.re),
        u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) =
          HDiv.hDiv (α := ℂ) (↑n ! : ℂ) (∏ j ∈ Finset.range (n + 1), (u + (↑j : ℂ))))
    {u : ℂ} (hu : 0 < u.re),
    u.betaIntegral (HAdd.hAdd (α := ℂ) (↑(n + 1) : ℂ) 1) =
      HDiv.hDiv (α := ℂ) (↑(n + 1)! : ℂ) (∏ j ∈ Finset.range (n + 1 + 1), (u + (↑j : ℂ)))
⊢ u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) =
    HDiv.hDiv (α := ℂ) (↑n ! : ℂ) (∏ j ∈ Finset.range (n + 1), (u + (↑j : ℂ)))

Tactic:
induction n generalizing u with
  | zero =>
    rw [Nat.cast_zero, zero_add, betaIntegral_eval_one_right hu, Nat.factorial_zero, Nat.cast_one]
    simp
  | succ n IH =>
    have := betaIntegral_recurrence hu (?_ : 0 < re n.succ)
    swap; · rw [← ofReal_natCast, ofReal_re]; positivity
    rw [mul_comm u _, ← eq_div_iff] at this
    swap; · contrapose! hu; rw [hu, zero_re]
    rw [this, Finset.prod_range_succ', Nat.cast_succ, IH]
    swap; · rw [add_re, one_re]; positivity
    rw [Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one, Nat.cast_zero, add_zero, ←
      mul_div_assoc, ← div_div]
    congr 3 with j : 1
    push_cast; abel

Premises used: Nat.cast_succ, Finset.prod_range_succ', Nat.factorial_succ, Complex.betaIntegral_eval_one_right, mul_div_assoc, Complex.add_re, zero_add, Nat.cast_add, Nat.cast_mul, Complex.ofReal_natCast, mul_comm, Complex.zero_re, Complex.ofReal_re, Nat.factorial_zero, Nat.cast_zero, div_div, add_zero, eq_div_iff, Complex.one_re, Nat.cast_one