awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
n_ih : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑n : ℝ) < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
hs' : -(↑(n + 1) : ℝ) < s
⊢ HAdd.hAdd (α := ℝ) (-(↑n : ℝ)) (-1) < s

Tactic:
rw [Nat.cast_add, Nat.cast_one, neg_add] at hs'

Premises used: neg_add, Nat.cast_add, Nat.cast_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
n_ih : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑n : ℝ) < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
hs' : HAdd.hAdd (α := ℝ) (-(↑n : ℝ)) (-1) < s
linarith : s + 1 ≤ -(↑n : ℝ) → HAdd.hAdd (α := ℝ) (-(↑n : ℝ)) (-1) - s + (s + 1 - -(↑n : ℝ)) = 0
⊢ -(↑n : ℝ) < s + 1

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
n_ih : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑n : ℝ) < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
hs' : -(↑(n + 1) : ℝ) < s
⊢ Gamma (s + 1) ≠ 0

Tactic:
have : Gamma (s + 1) ≠ 0 := by
      apply n_ih
      · intro m
        specialize hs (1 + m)
        contrapose hs
        rw [← eq_sub_iff_add_eq] at hs
        rw [hs]
        push_cast
        ring
      · rw [Nat.cast_add, Nat.cast_one, neg_add] at hs'
        linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
n_ih : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑n : ℝ) < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
hs' : -(↑(n + 1) : ℝ) < s
this : Gamma (s + 1) ≠ 0
succ : ∀ (this : s ≠ 0 ∧ Gamma s ≠ 0), Gamma s ≠ 0
succ₁ : s ≠ 0
⊢ Gamma s ≠ 0

Tactic:
rw [Gamma_add_one, mul_ne_zero_iff] at this

Premises used: Real.Gamma_add_one, mul_ne_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
n_ih : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑n : ℝ) < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
hs' : -(↑(n + 1) : ℝ) < s
this : s ≠ 0 ∧ Gamma s ≠ 0
⊢ Gamma s ≠ 0

Tactic:
this.2

Premises used: And.right
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
n_ih : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑n : ℝ) < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
hs' : -(↑(n + 1) : ℝ) < s
this : s ≠ 0 ∧ Gamma s ≠ 0
⊢ Gamma s ≠ 0

Tactic:
exact this.2

Premises used: And.right
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
n_ih : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑n : ℝ) < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
hs' : -(↑(n + 1) : ℝ) < s
this : Gamma (s + 1) ≠ 0
⊢ s ≠ 0

Tactic:
simpa using hs 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
n : ℕ
zero : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑0 : ℝ) < s → Gamma s ≠ 0
succ :
  ∀ (n : ℕ) (n_ih : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑n : ℝ) < s → Gamma s ≠ 0) {s : ℝ}
    (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑(n + 1) : ℝ) < s → Gamma s ≠ 0
⊢ -(↑n : ℝ) < s → Gamma s ≠ 0

Tactic:
induction n generalizing s with
  | zero =>
    intro hs
    refine (Gamma_pos_of_pos ?_).ne'
    rwa [Nat.cast_zero, neg_zero] at hs
  | succ _ n_ih =>
    intro hs'
    have : Gamma (s + 1) ≠ 0 := by
      apply n_ih
      · intro m
        specialize hs (1 + m)
        contrapose hs
        rw [← eq_sub_iff_add_eq] at hs
        rw [hs]
        push_cast
        ring
      · rw [Nat.cast_add, Nat.cast_one, neg_add] at hs'
        linarith
    rw [Gamma_add_one, mul_ne_zero_iff] at this
    · exact this.2
    · simpa using hs 0

Premises used: Real.Gamma_pos_of_pos, Real.Gamma_add_one, LT.lt.ne', Nat.cast_zero, OfNat.ofNat, neg_zero, mul_ne_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
contrapose! : (∀ (m : ℕ), s ≠ -(↑m : ℝ)) → Gamma s ≠ 0
⊢ Gamma s = 0 → ∃ (m : ℕ), s = -(↑m : ℝ)

Tactic:
contrapose!
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
⊢ (∀ (m : ℕ), s ≠ -(↑m : ℝ)) → Gamma s ≠ 0

Tactic:
Gamma_ne_zero

Premises used: Real.Gamma_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
⊢ (∀ (m : ℕ), s ≠ -(↑m : ℝ)) → Gamma s ≠ 0

Tactic:
exact Gamma_ne_zero

Premises used: Real.Gamma_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
m : ℕ
⊢ Gamma (-(↑m : ℝ)) = 0

Tactic:
Gamma_neg_nat_eq_zero m

Premises used: Real.Gamma_neg_nat_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
m : ℕ
⊢ Gamma (-(↑m : ℝ)) = 0

Tactic:
exact Gamma_neg_nat_eq_zero m

Premises used: Real.Gamma_neg_nat_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u : ℂ
hu : 0 < u.re
v : ℂ
hf : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (u - 1)) volume 0 (1 / 2)
hg : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (1 - (↑x : ℂ)) ^ (v - 1)) (uIcc 0 (1 / 2))
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (u - 1) * (1 - (↑x : ℂ)) ^ (v - 1)) volume 0 (1 / 2)

Tactic:
apply IntervalIntegrable.mul_continuousOn

Premises used: IntervalIntegrable.mul_continuousOn
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u : ℂ
hu : 0 < u.re
v : ℂ
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (u - 1)) volume 0 (1 / 2)

Tactic:
intervalIntegral.intervalIntegrable_cpow' ?_

Premises used: intervalIntegral.intervalIntegrable_cpow'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u : ℂ
hu : 0 < u.re
v : ℂ
hf : -1 < (u - 1).re
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (u - 1)) volume 0 (1 / 2)

Tactic:
refine intervalIntegral.intervalIntegrable_cpow' ?_

Premises used: intervalIntegral.intervalIntegrable_cpow'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u : ℂ
hu : 0 < u.re
v : ℂ
hf : -1 < u.re - re 1
hf₁ : -1 < u.re - 1
hf₂ : HSub.hSub (α := ℝ) 0 1 < u.re - 1
hf₃ hf₄ hf₅ hf₆ : 0 < u.re
⊢ -1 < (u - 1).re

Tactic:
rwa [sub_re, one_re, ← zero_sub, sub_lt_sub_iff_right]

Premises used: Complex.sub_re, sub_lt_sub_iff_right, Complex.one_re, zero_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u : ℂ
hu : 0 < u.re
v : ℂ
hg : ∀ x ∈ uIcc 0 (1 / 2), ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (1 - (↑x : ℂ)) ^ (v - 1)) x
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (1 - (↑x : ℂ)) ^ (v - 1)) (uIcc 0 (1 / 2))

Tactic:
apply continuousOn_of_forall_continuousAt

Premises used: continuousOn_of_forall_continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ uIcc 0 (1 / 2)
⊢ 0 ≤ 1 / 2

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ uIcc 0 (1 / 2)
⊢ x ∈ Icc 0 (1 / 2)

Tactic:
rw [uIcc_of_le (by positivity : (0 : ℝ) ≤ 1 / 2)] at hx

Premises used: Set.uIcc_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ 1 - (↑x : ℂ)) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ v - 1) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
hg : 1 - (↑x : ℂ) ∈ slitPlane
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (1 - (↑x : ℂ)) ^ (v - 1)) x

Tactic:
apply ContinuousAt.cpow (by fun_prop) (by fun_prop)

Premises used: ContinuousAt.cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
hg : (↑(1 - x) : ℂ) ∈ slitPlane
⊢ 1 - (↑x : ℂ) ∈ slitPlane

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
linarith : 1 - x ≤ 0 → 2 / 2 = 1
linarith₁ : 1 - x ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 - x ≤ 0 → GT.gt (α := ℝ) 2 0
linarith₃ : 1 - x ≤ 0 → -1 + 2 * (1 - x - 0) + (2 * x - HMul.hMul (α := ℝ) 1 1) = 0
linarith₄ : 1 - x ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < 1 - x

Tactic:
linarith only [hx.2]

Premises used: And.right
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
⊢ (↑(1 - x) : ℂ) ∈ slitPlane

Tactic:
exact ofReal_mem_slitPlane.2 <| by linarith only [hx.2]

Premises used: Iff.mpr, Complex.ofReal_mem_slitPlane
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (u - 1) * (1 - (↑x : ℂ)) ^ (v - 1)) volume 0 1

Tactic:
(betaIntegral_convergent_left hu v).trans ?_

Premises used: IntervalIntegrable.trans, Complex.betaIntegral_convergent_left
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
refine : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (u - 1) * (1 - (↑x : ℂ)) ^ (v - 1)) volume (1 / 2) 1
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (u - 1) * (1 - (↑x : ℂ)) ^ (v - 1)) volume 0 1

Tactic:
refine (betaIntegral_convergent_left hu v).trans ?_

Premises used: IntervalIntegrable.trans, Complex.betaIntegral_convergent_left
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
rw :
  IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑(-x) : ℂ) ^ (u - 1) * (1 - (↑(-x) : ℂ)) ^ (v - 1)) volume (-(1 / 2)) (-1)
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (u - 1) * (1 - (↑x : ℂ)) ^ (v - 1)) volume (1 / 2) 1

Tactic:
rw [IntervalIntegrable.iff_comp_neg]

Premises used: IntervalIntegrable.iff_comp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑(x + 1) : ℂ) ^ (v - 1) * (1 - (↑(x + 1) : ℂ)) ^ (u - 1)) volume
    (1 / 2 - 1) (HSub.hSub (α := ℝ) 0 1)

Tactic:
((betaIntegral_convergent_left hv u).comp_add_right 1).symm

Premises used: IntervalIntegrable.comp_add_right, IntervalIntegrable.symm, Complex.betaIntegral_convergent_left, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
h :
  Eq (α := ℝ → ℂ) (fun (x : ℝ) ↦ (↑(-x) : ℂ) ^ (u - 1) * (1 - (↑(-x) : ℂ)) ^ (v - 1)) fun (x : ℝ) ↦
    (↑(x + 1) : ℂ) ^ (v - 1) * (1 - (↑(x + 1) : ℂ)) ^ (u - 1)
h₁ : -(1 / 2) = 1 / 2 - 1
h₂ : -1 = HSub.hSub (α := ℝ) 0 1
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑(-x) : ℂ) ^ (u - 1) * (1 - (↑(-x) : ℂ)) ^ (v - 1)) volume (-(1 / 2)) (-1)

Tactic:
convert! ((betaIntegral_convergent_left hv u).comp_add_right 1).symm using 1

Premises used: IntervalIntegrable.comp_add_right, IntervalIntegrable.symm, Complex.betaIntegral_convergent_left, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
h :
  ∀ (x : ℝ),
    (↑(-x) : ℂ) ^ (u - 1) * (1 - (↑(-x) : ℂ)) ^ (v - 1) = (↑(x + 1) : ℂ) ^ (v - 1) * (1 - (↑(x + 1) : ℂ)) ^ (u - 1)
⊢ Eq (α := ℝ → ℂ) (fun (x : ℝ) ↦ (↑(-x) : ℂ) ^ (u - 1) * (1 - (↑(-x) : ℂ)) ^ (v - 1)) fun (x : ℝ) ↦
    (↑(x + 1) : ℂ) ^ (v - 1) * (1 - (↑(x + 1) : ℂ)) ^ (u - 1)

Tactic:
ext1 x
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
rw : (1 - (↑(-x) : ℂ)) ^ (v - 1) * (↑(-x) : ℂ) ^ (u - 1)
| (↑(-x) : ℂ) ^ (u - 1) * (1 - (↑(-x) : ℂ)) ^ (v - 1)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
h : (1 - (↑(-x) : ℂ)) ^ (v - 1) * (↑(-x) : ℂ) ^ (u - 1) = (↑(x + 1) : ℂ) ^ (v - 1) * (1 - (↑(x + 1) : ℂ)) ^ (u - 1)
⊢ (↑(-x) : ℂ) ^ (u - 1) * (1 - (↑(-x) : ℂ)) ^ (v - 1) = (↑(x + 1) : ℂ) ^ (v - 1) * (1 - (↑(x + 1) : ℂ)) ^ (u - 1)

Tactic:
conv_lhs => rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
h : 1 - (↑(-x) : ℂ) = (↑(x + 1) : ℂ)
h₁ : (↑(-x) : ℂ) = 1 - (↑(x + 1) : ℂ)
⊢ (1 - (↑(-x) : ℂ)) ^ (v - 1) * (↑(-x) : ℂ) ^ (u - 1) = (↑(x + 1) : ℂ) ^ (v - 1) * (1 - (↑(x + 1) : ℂ)) ^ (u - 1)

Tactic:
congr 2
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
h : 1 - -(↑x : ℂ) = (↑x : ℂ) + 1
⊢ 1 - (↑(-x) : ℂ) = (↑(x + 1) : ℂ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
⊢ 1 - -(↑x : ℂ) = (↑x : ℂ) + 1

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
h : -(↑x : ℂ) = 1 - ((↑x : ℂ) + 1)
⊢ (↑(-x) : ℂ) = 1 - (↑(x + 1) : ℂ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
⊢ -(↑x : ℂ) = 1 - ((↑x : ℂ) + 1)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ -(1 / 2) = 1 / 2 - 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ -1 = HSub.hSub (α := ℝ) 0 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u v : ℂ
⊢ v.betaIntegral u = u.betaIntegral v

Tactic:
simpa [betaIntegral, ← intervalIntegral.integral_symm, add_comm, mul_comm, sub_eq_add_neg]
    using 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

Premises used: HMul.hMul, sub_eq_add_neg, HSub.hSub, intervalIntegral.integral_symm, Complex.ofReal, add_comm, HPow.hPow, Complex.betaIntegral, mul_comm, neg_one_lt_zero, intervalIntegral.integral_comp_mul_add, OfNat.ofNat, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u : ℂ
hu : 0 < u.re
simp_rw : ∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (u - 1) = 1 / u
⊢ u.betaIntegral 1 = 1 / u

Tactic:
simp_rw [betaIntegral, sub_self, cpow_zero, mul_one]

Premises used: sub_self, Complex.betaIntegral, mul_one, Complex.cpow_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u : ℂ
hu : 0 < u.re
rw : ((↑1 : ℂ) ^ (u - 1 + 1) - (↑0 : ℂ) ^ (u - 1 + 1)) / (u - 1 + 1) = 1 / u
rw₁ : -1 < (u - 1).re
⊢ ∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (u - 1) = 1 / u

Tactic:
rw [integral_cpow (Or.inl _)]

Premises used: integral_cpow, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u : ℂ
hu : 0 < u.re
rw : u - 1 + 1 ≠ 0
⊢ ((↑1 : ℂ) ^ (u - 1 + 1) - (↑0 : ℂ) ^ (u - 1 + 1)) / (u - 1 + 1) = 1 / u

Tactic:
rw [ofReal_zero, ofReal_one, one_cpow, zero_cpow, sub_zero, sub_add_cancel]

Premises used: sub_zero, Complex.ofReal_one, Complex.zero_cpow, Complex.ofReal_zero, Complex.one_cpow, sub_add_cancel
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u : ℂ
hu : 0 < u.re
rw : u ≠ 0
⊢ u - 1 + 1 ≠ 0

Tactic:
rw [sub_add_cancel]

Premises used: sub_add_cancel
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u : ℂ
hu : 0 < u.re
contrapose! : ∀ (hu : u = 0), u.re ≤ 0
⊢ u ≠ 0

Tactic:
contrapose! hu
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u : ℂ
hu : u = 0
rw : re 0 ≤ 0
rw₁ rw₂ : LE.le (α := ℝ) 0 0
⊢ u.re ≤ 0

Tactic:
rw [hu, zero_re]

Premises used: Complex.zero_re
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u : ℂ
hu : 0 < u.re
rwa : -1 < u.re - re 1
rwa₁ : -1 < u.re - 1
rwa₂ : 0 < u.re - 1 - -1
rwa₃ : 0 < u.re - 1 + 1
rwa₄ rwa₅ rwa₆ rwa₇ : 0 < u.re
⊢ -1 < (u - 1).re

Tactic:
rwa [sub_re, one_re, ← sub_pos, sub_neg_eq_add, sub_add_cancel]

Premises used: sub_pos, Complex.sub_re, Complex.one_re, sub_add_cancel, sub_neg_eq_add
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s t : ℂ
a : ℝ
ha : 0 < a
⊢ (↑a : ℂ) ≠ 0

Tactic:
have ha' : (a : ℂ) ≠ 0 := ofReal_ne_zero.mpr ha.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : (↑a : ℂ) ≠ 0
⊢ s + t - 1 = 1 + (s - 1) + (t - 1)

Tactic:
abel
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : (↑a : ℂ) ≠ 0
rw : s + t - 1 = 1 + (s - 1) + (t - 1)
rw₁ : (↑a : ℂ) ^ (1 + (s - 1) + (t - 1)) = (↑a : ℂ) * ((↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1))
rw₂ : (↑a : ℂ) ^ (1 + (s - 1)) * (↑a : ℂ) ^ (t - 1) = (↑a : ℂ) * ((↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1))
rw₃ :
  HPow.hPow (β := ℂ) (↑a : ℂ) 1 * (↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1) =
    (↑a : ℂ) * ((↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1))
rw₄ : (↑a : ℂ) * (↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1) = (↑a : ℂ) * ((↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1))
rw₅ rw₆ : (↑a : ℂ) * ((↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1)) = (↑a : ℂ) * ((↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1))
⊢ (↑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]

Premises used: mul_assoc, Complex.cpow_one, Complex.cpow_add, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : (↑a : ℂ) ≠ 0
⊢ (↑a : ℂ) ^ (s + t - 1) = (↑a : ℂ) * ((↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (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]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : (↑a : ℂ) ≠ 0
A : (↑a : ℂ) ^ (s + t - 1) = (↑a : ℂ) * ((↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1))
rw :
  Eq (α := ℂ) (∫ (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)))
⊢ ∫ (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]

Premises used: Complex.real_smul, mul_assoc, zero_div, intervalIntegral.integral_comp_div, LT.lt.ne', div_self, intervalIntegral.integral_const_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : (↑a : ℂ) ≠ 0
A : (↑a : ℂ) ^ (s + t - 1) = (↑a : ℂ) * ((↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1))
simp_rw :
  Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 a)) fun (x : ℝ) ↦
      (↑x : ℂ) ^ (s - 1) * ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 a)) fun (x : ℝ) ↦
      (↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1) * ((↑(x / a) : ℂ) ^ (s - 1) * (1 - (↑(x / a) : ℂ)) ^ (t - 1)))
⊢ Eq (α := ℂ) (∫ (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]

Premises used: LT.lt.le, intervalIntegral.integral_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : (↑a : ℂ) ≠ 0
A : (↑a : ℂ) ^ (s + t - 1) = (↑a : ℂ) * ((↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1))
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 a)) fun (x : ℝ) ↦
      (↑x : ℂ) ^ (s - 1) * ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 a)) fun (x : ℝ) ↦
      (↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1) * ((↑(x / a) : ℂ) ^ (s - 1) * (1 - (↑(x / a) : ℂ)) ^ (t - 1)))

Tactic:
setIntegral_congr_fun measurableSet_Ioc fun x hx => ?_

Premises used: MeasureTheory.setIntegral_congr_fun, measurableSet_Ioc
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : (↑a : ℂ) ≠ 0
A : (↑a : ℂ) ^ (s + t - 1) = (↑a : ℂ) * ((↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1))
refine :
  ∀ (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))
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 a)) fun (x : ℝ) ↦
      (↑x : ℂ) ^ (s - 1) * ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 a)) fun (x : ℝ) ↦
      (↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1) * ((↑(x / a) : ℂ) ^ (s - 1) * (1 - (↑(x / a) : ℂ)) ^ (t - 1)))

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

Premises used: MeasureTheory.setIntegral_congr_fun, measurableSet_Ioc
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
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
rw :
  (↑x : ℂ) ^ (s - 1) * ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) =
    (↑a : ℂ) ^ (s - 1) * (↑(x / a) : ℂ) ^ (s - 1) * ((↑a : ℂ) ^ (t - 1) * (1 - (↑(x / a) : ℂ)) ^ (t - 1))
⊢ (↑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]

Premises used: mul_mul_mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
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
e_a : (↑x : ℂ) ^ (s - 1) = (↑a : ℂ) ^ (s - 1) * (↑(x / a) : ℂ) ^ (s - 1)
e_a₁ : ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) = (↑a : ℂ) ^ (t - 1) * (1 - (↑(x / a) : ℂ)) ^ (t - 1)
⊢ (↑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
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
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
e_a : (↑x : ℂ) ^ (s - 1) = ((↑a : ℂ) * (↑(x / a) : ℂ)) ^ (s - 1)
e_a₁ : (↑x : ℂ) ^ (s - 1) = ((↑a : ℂ) * ((↑x : ℂ) / (↑a : ℂ))) ^ (s - 1)
e_a₂ e_a₃ : (↑x : ℂ) ^ (s - 1) = (↑x : ℂ) ^ (s - 1)
⊢ (↑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']

Premises used: LT.lt.le, Complex.mul_cpow_ofReal_nonneg, mul_div_cancel₀, And.left, Complex.ofReal_div, div_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
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
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 1 - x / a = 1 - x / a
⊢ 1 - (↑(x / a) : ℂ) = (↑(1 - x / a) : ℂ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
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
e_a : ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) = ((↑a : ℂ) * (↑(1 - x / a) : ℂ)) ^ (t - 1)
⊢ ((↑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)]

Premises used: Iff.mpr, LT.lt.le, Complex.mul_cpow_ofReal_nonneg, div_le_one, And.right, sub_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
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
e_a : ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) = ((↑a : ℂ) * (1 - (↑x : ℂ) / (↑a : ℂ))) ^ (t - 1)
⊢ ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) = ((↑a : ℂ) * (↑(1 - x / a) : ℂ)) ^ (t - 1)

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
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
e_a : ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) = ((↑a : ℂ) * 1 - (↑a : ℂ) * ((↑x : ℂ) / (↑a : ℂ))) ^ (t - 1)
e_a₁ : ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) = ((↑a : ℂ) - (↑a : ℂ) * ((↑x : ℂ) / (↑a : ℂ))) ^ (t - 1)
e_a₂ e_a₃ : ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) = ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1)
⊢ ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) = ((↑a : ℂ) * (1 - (↑x : ℂ) / (↑a : ℂ))) ^ (t - 1)

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

Premises used: mul_sub, mul_div_cancel₀, mul_one