-- Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
theorem betaIntegral_scaled (s t : ℂ) {a : ℝ} (ha : 0 < a) :
    ∫ x in (0)..a, (x : ℂ) ^ (s - 1) * ((a : ℂ) - x) ^ (t - 1) =
    (a : ℂ) ^ (s + t - 1) * betaIntegral s t

Proof state:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
⊢ ∫ (x : ℝ) in 0 ..a, ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) =
    ↑a ^ (s + t - 1) * ∫ (x : ℝ) in 0 ..1, ↑x ^ (s - 1) * (1 - ↑x) ^ (t - 1)

Tactic:
rw [A, mul_assoc, ← intervalIntegral.integral_const_mul, ← real_smul, ← zero_div a, ←
  div_self ha.ne', ← intervalIntegral.integral_comp_div _ ha.ne', zero_div]

Result:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
⊢ ∫ (x : ℝ) in 0 ..a, ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) =
    ∫ (x : ℝ) in 0 ..a, ↑a ^ (s - 1) * ↑a ^ (t - 1) * (↑(x / a) ^ (s - 1) * (1 - ↑(x / a)) ^ (t - 1))

Proof state:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
⊢ s + t - 1 = 1 + (s - 1) + (t - 1)

Tactic:
abel

Result:
no goals

Proof state:
case e_a
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ (↑a - ↑x) ^ (t - 1) = (↑a * ↑(1 - x / a)) ^ (t - 1)

Tactic:
push_cast

Result:
case e_a
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ (↑a - ↑x) ^ (t - 1) = (↑a * (1 - ↑x / ↑a)) ^ (t - 1)

Proof state:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
⊢ ∫ (x : ℝ) in 0 ..a, ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) = ↑a ^ (s + t - 1) * s.betaIntegral t

Tactic:
rw [betaIntegral]

Result:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
⊢ ∫ (x : ℝ) in 0 ..a, ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) =
    ↑a ^ (s + t - 1) * ∫ (x : ℝ) in 0 ..1, ↑x ^ (s - 1) * (1 - ↑x) ^ (t - 1)

Proof state:
case e_a
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ (↑a - ↑x) ^ (t - 1) = (↑a * (1 - ↑x / ↑a)) ^ (t - 1)

Tactic:
rw [mul_sub, mul_one, mul_div_cancel₀ _ ha']

Result:
no goals

Proof state:
case e_a
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ ↑x ^ (s - 1) = ↑a ^ (s - 1) * ↑(x / a) ^ (s - 1)

Tactic:
rw [← mul_cpow_ofReal_nonneg ha.le (div_pos hx.1 ha).le, ofReal_div, mul_div_cancel₀ _ ha']

Result:
no goals

Proof state:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) = ↑a ^ (s - 1) * ↑(x / a) ^ (s - 1) * (↑a ^ (t - 1) * (1 - ↑(x / a)) ^ (t - 1))

Tactic:
congr 1

Result:
case e_a
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ ↑x ^ (s - 1) = ↑a ^ (s - 1) * ↑(x / a) ^ (s - 1)

case e_a
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ (↑a - ↑x) ^ (t - 1) = ↑a ^ (t - 1) * (1 - ↑(x / a)) ^ (t - 1)

Proof state:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
⊢ ∫ (x : ℝ) in 0 ..a, ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) =
    ↑a ^ (s + t - 1) * ∫ (x : ℝ) in 0 ..1, ↑x ^ (s - 1) * (1 - ↑x) ^ (t - 1)

Tactic:
have A : (a : ℂ) ^ (s + t - 1) = a * ((a : ℂ) ^ (s - 1) * (a : ℂ) ^ (t - 1)) := by
  rw [(by abel : s + t - 1 = 1 + (s - 1) + (t - 1)), cpow_add _ _ ha', cpow_add 1 _ ha', cpow_one,
    mul_assoc]

Result:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
⊢ ∫ (x : ℝ) in 0 ..a, ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) =
    ↑a ^ (s + t - 1) * ∫ (x : ℝ) in 0 ..1, ↑x ^ (s - 1) * (1 - ↑x) ^ (t - 1)

Proof state:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
⊢ ∫ (x : ℝ) in 0 ..a, ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) =
    ∫ (x : ℝ) in 0 ..a, ↑a ^ (s - 1) * ↑a ^ (t - 1) * (↑(x / a) ^ (s - 1) * (1 - ↑(x / a)) ^ (t - 1))

Tactic:
simp_rw [intervalIntegral.integral_of_le ha.le]

Result:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
⊢ ∫ (x : ℝ) in Ioc 0 a, ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) ∂volume =
    ∫ (x : ℝ) in Ioc 0 a, ↑a ^ (s - 1) * ↑a ^ (t - 1) * (↑(x / a) ^ (s - 1) * (1 - ↑(x / a)) ^ (t - 1)) ∂volume

Proof state:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) = ↑a ^ (s - 1) * ↑a ^ (t - 1) * (↑(x / a) ^ (s - 1) * (1 - ↑(x / a)) ^ (t - 1))

Tactic:
rw [mul_mul_mul_comm]

Result:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) = ↑a ^ (s - 1) * ↑(x / a) ^ (s - 1) * (↑a ^ (t - 1) * (1 - ↑(x / a)) ^ (t - 1))

Proof state:
case e_a
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ (↑a - ↑x) ^ (t - 1) = ↑a ^ (t - 1) * (1 - ↑(x / a)) ^ (t - 1)

Tactic:
rw [(by norm_cast : (1 : ℂ) - ↑(x / a) = ↑(1 - x / a)), ←
  mul_cpow_ofReal_nonneg ha.le (sub_nonneg.mpr <| (div_le_one ha).mpr hx.2)]

Result:
case e_a
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ (↑a - ↑x) ^ (t - 1) = (↑a * ↑(1 - x / a)) ^ (t - 1)

Proof state:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ 1 - ↑(x / a) = ↑(1 - x / a)

Tactic:
norm_cast

Result:
no goals

Proof state:
s t : ℂ
a : ℝ
ha : 0 < a
⊢ ∫ (x : ℝ) in 0 ..a, ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) = ↑a ^ (s + t - 1) * s.betaIntegral t

Tactic:
have ha' : (a : ℂ) ≠ 0 := ofReal_ne_zero.mpr ha.ne'

Result:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
⊢ ∫ (x : ℝ) in 0 ..a, ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) = ↑a ^ (s + t - 1) * s.betaIntegral t

Proof state:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
⊢ ∫ (x : ℝ) in Ioc 0 a, ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) ∂volume =
    ∫ (x : ℝ) in Ioc 0 a, ↑a ^ (s - 1) * ↑a ^ (t - 1) * (↑(x / a) ^ (s - 1) * (1 - ↑(x / a)) ^ (t - 1)) ∂volume

Tactic:
refine setIntegral_congr_fun measurableSet_Ioc fun x hx => ?_

Result:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) = ↑a ^ (s - 1) * ↑a ^ (t - 1) * (↑(x / a) ^ (s - 1) * (1 - ↑(x / a)) ^ (t - 1))

Proof state:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
⊢ ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))

Tactic:
rw [(by abel : s + t - 1 = 1 + (s - 1) + (t - 1)), cpow_add _ _ ha', cpow_add 1 _ ha', cpow_one,
  mul_assoc]

Result:
no goals