-- Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
theorem betaIntegral_symm (u v : ℂ) : betaIntegral v u = betaIntegral u v

Proof state:
u v : ℂ
this : ∫ (x : ℝ) in 0 ..1, (-↑x + 1) ^ (u - 1) * ↑x ^ (v - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
⊢ ∫ (x : ℝ) in 0 ..1, ↑x ^ (v - 1) * (1 - ↑x) ^ (u - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)

Tactic:
conv_lhs at this => arg 1; intro x; rw [add_comm, ← sub_eq_add_neg, mul_comm]

Result:
u v : ℂ
this : ∫ (x : ℝ) in 0 ..1, ↑x ^ (v - 1) * (1 - ↑x) ^ (u - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
⊢ ∫ (x : ℝ) in 0 ..1, ↑x ^ (v - 1) * (1 - ↑x) ^ (u - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)

Proof state:
u v : ℂ
⊢ ∫ (x : ℝ) in 0 ..1, ↑x ^ (v - 1) * (1 - ↑x) ^ (u - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)

Tactic:
have := intervalIntegral.integral_comp_mul_add (a := 0) (b := 1) (c := -1)
  (fun x : ℝ => (x : ℂ) ^ (u - 1) * (1 - (x : ℂ)) ^ (v - 1)) neg_one_lt_zero.ne 1

Result:
u v : ℂ
this :
  ∫ (x : ℝ) in 0 ..1, ↑(-1 * x + 1) ^ (u - 1) * (1 - ↑(-1 * x + 1)) ^ (v - 1) =
    (-1)⁻¹ • ∫ (x : ℝ) in -1 * 0 + 1 ..-1 * 1 + 1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
⊢ ∫ (x : ℝ) in 0 ..1, ↑x ^ (v - 1) * (1 - ↑x) ^ (u - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)

Proof state:
u v : ℂ
this :
  ∫ (x : ℝ) in 0 ..1, ↑(-1 * x + 1) ^ (u - 1) * (1 - ↑(-1 * x + 1)) ^ (v - 1) =
    ∫ (x : ℝ) in -1 * 1 + 1 ..-1 * 0 + 1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
⊢ ∫ (x : ℝ) in 0 ..1, ↑x ^ (v - 1) * (1 - ↑x) ^ (u - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)

Tactic:
simp only [neg_mul, one_mul, ofReal_add, ofReal_neg, ofReal_one, sub_add_cancel_right, neg_neg,
  mul_one, neg_add_cancel, mul_zero, zero_add] at this

Result:
u v : ℂ
this : ∫ (x : ℝ) in 0 ..1, (-↑x + 1) ^ (u - 1) * ↑x ^ (v - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
⊢ ∫ (x : ℝ) in 0 ..1, ↑x ^ (v - 1) * (1 - ↑x) ^ (u - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)

Proof state:
u v : ℂ
this :
  ∫ (x : ℝ) in 0 ..1, ↑(-1 * x + 1) ^ (u - 1) * (1 - ↑(-1 * x + 1)) ^ (v - 1) =
    ∫ (x : ℝ) in -1 * 1 + 1 ..-1 * 0 + 1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
⊢ ∫ (x : ℝ) in 0 ..1, ↑x ^ (v - 1) * (1 - ↑x) ^ (u - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)

Tactic:
simp? at this says
  simp only [neg_mul, one_mul, ofReal_add, ofReal_neg, ofReal_one, sub_add_cancel_right, neg_neg,
    mul_one, neg_add_cancel, mul_zero, zero_add] at this

Result:
u v : ℂ
this : ∫ (x : ℝ) in 0 ..1, (-↑x + 1) ^ (u - 1) * ↑x ^ (v - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
⊢ ∫ (x : ℝ) in 0 ..1, ↑x ^ (v - 1) * (1 - ↑x) ^ (u - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)

Proof state:
u v : ℂ
this : ∫ (x : ℝ) in 0 ..1, ↑x ^ (v - 1) * (1 - ↑x) ^ (u - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
⊢ ∫ (x : ℝ) in 0 ..1, ↑x ^ (v - 1) * (1 - ↑x) ^ (u - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)

Tactic:
exact this

Result:
no goals

Proof state:
u v : ℂ
⊢ v.betaIntegral u = u.betaIntegral v

Tactic:
rw [betaIntegral, betaIntegral]

Result:
u v : ℂ
⊢ ∫ (x : ℝ) in 0 ..1, ↑x ^ (v - 1) * (1 - ↑x) ^ (u - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)

Proof state:
u v : ℂ
this :
  ∫ (x : ℝ) in 0 ..1, ↑(-1 * x + 1) ^ (u - 1) * (1 - ↑(-1 * x + 1)) ^ (v - 1) =
    (-1)⁻¹ • ∫ (x : ℝ) in -1 * 0 + 1 ..-1 * 1 + 1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
⊢ ∫ (x : ℝ) in 0 ..1, ↑x ^ (v - 1) * (1 - ↑x) ^ (u - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)

Tactic:
rw [inv_neg, inv_one, neg_one_smul, ← intervalIntegral.integral_symm] at this

Result:
u v : ℂ
this :
  ∫ (x : ℝ) in 0 ..1, ↑(-1 * x + 1) ^ (u - 1) * (1 - ↑(-1 * x + 1)) ^ (v - 1) =
    ∫ (x : ℝ) in -1 * 1 + 1 ..-1 * 0 + 1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
⊢ ∫ (x : ℝ) in 0 ..1, ↑x ^ (v - 1) * (1 - ↑x) ^ (u - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)