awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
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
⊢ Gamma s ≠ 0
have succ₁ : s ≠ 0
Tactic: rw [Gamma_add_one, mul_ne_zero_iff] at this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
n : ℕ
⊢ -(↑n : ℝ) < s → Gamma s ≠ 0
have zero : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑0 : ℝ) < 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
Cleared hypotheses: s, hs, n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
n : ℕ
zero : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑0 : ℝ) < s → Gamma s ≠ 0
⊢ -(↑n : ℝ) < s → Gamma s ≠ 0
have 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
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
Cleared hypotheses: s, hs, n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
⊢ Gamma s = 0 → ∃ (m : ℕ), s = -(↑m : ℝ)
have contrapose! : (∀ (m : ℕ), s ≠ -(↑m : ℝ)) → Gamma s ≠ 0
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u : ℂ
hu : 0 < u.re
v : ℂ
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (u - 1) * (1 - (↑x : ℂ)) ^ (v - 1)) volume 0 (1 / 2)
have hf : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (u - 1)) volume 0 (1 / 2)
Tactic: apply IntervalIntegrable.mul_continuousOn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u : ℂ
hu : 0 < u.re
v : ℂ
hf : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (u - 1)) volume 0 (1 / 2)
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (u - 1) * (1 - (↑x : ℂ)) ^ (v - 1)) volume 0 (1 / 2)
have hg : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (1 - (↑x : ℂ)) ^ (v - 1)) (uIcc 0 (1 / 2))
Tactic: apply IntervalIntegrable.mul_continuousOn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u : ℂ
hu : 0 < u.re
v : ℂ
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (u - 1)) volume 0 (1 / 2)
have hf : -1 < (u - 1).re
Tactic: refine intervalIntegral.intervalIntegrable_cpow' ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u : ℂ
hu : 0 < u.re
v : ℂ
⊢ -1 < (u - 1).re
have hf : -1 < u.re - re 1
Tactic: rwa [sub_re, one_re, ← zero_sub, sub_lt_sub_iff_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u : ℂ
hu : 0 < u.re
v : ℂ
hf : -1 < u.re - re 1
⊢ -1 < (u - 1).re
have hf₁ : -1 < u.re - 1
Tactic: rwa [sub_re, one_re, ← zero_sub, sub_lt_sub_iff_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u : ℂ
hu : 0 < u.re
v : ℂ
hf : -1 < u.re - re 1
hf₁ : -1 < u.re - 1
⊢ -1 < (u - 1).re
have hf₂ : HSub.hSub (α := ℝ) 0 1 < u.re - 1
Tactic: rwa [sub_re, one_re, ← zero_sub, sub_lt_sub_iff_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u : ℂ
hu : 0 < u.re
v : ℂ
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (1 - (↑x : ℂ)) ^ (v - 1)) (uIcc 0 (1 / 2))
have hg : ∀ x ∈ uIcc 0 (1 / 2), ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (1 - (↑x : ℂ)) ^ (v - 1)) x
Tactic: apply continuousOn_of_forall_continuousAt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ uIcc 0 (1 / 2)
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (1 - (↑x : ℂ)) ^ (v - 1)) x
have hx₁ : x ∈ Icc 0 (1 / 2)
Tactic: rw [uIcc_of_le (by positivity : (0 : ℝ) ≤ 1 / 2)] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (1 - (↑x : ℂ)) ^ (v - 1)) x
have hg : 1 - (↑x : ℂ) ∈ slitPlane
Tactic: apply ContinuousAt.cpow (by fun_prop) (by fun_prop)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
⊢ 1 - (↑x : ℂ) ∈ slitPlane
have hg : (↑(1 - x) : ℂ) ∈ slitPlane
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
⊢ 0 < 1 - x
have linarith : 1 - x ≤ 0 → 2 / 2 = 1
Tactic: linarith only [hx.2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
linarith : 1 - x ≤ 0 → 2 / 2 = 1
⊢ 0 < 1 - x
have linarith₁ : 1 - x ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith only [hx.2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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
⊢ 0 < 1 - x
have linarith₂ : 1 - x ≤ 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith only [hx.2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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
⊢ 0 < 1 - x
have linarith₃ : 1 - x ≤ 0 → -1 + 2 * (1 - x - 0) + (2 * x - HMul.hMul (α := ℝ) 1 1) = 0
Tactic: linarith only [hx.2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (u - 1) * (1 - (↑x : ℂ)) ^ (v - 1)) volume 0 1
have refine : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (u - 1) * (1 - (↑x : ℂ)) ^ (v - 1)) volume (1 / 2) 1
Tactic: refine (betaIntegral_convergent_left hu v).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (u - 1) * (1 - (↑x : ℂ)) ^ (v - 1)) volume (1 / 2) 1
have rw : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑(-x) : ℂ) ^ (u - 1) * (1 - (↑(-x) : ℂ)) ^ (v - 1)) volume (-(1 / 2)) (-1)
Tactic: rw [IntervalIntegrable.iff_comp_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑(-x) : ℂ) ^ (u - 1) * (1 - (↑(-x) : ℂ)) ^ (v - 1)) volume (-(1 / 2)) (-1)
have h : Eq (α := ℝ → ℂ) (fun (x : ℝ) ↦ (↑(-x) : ℂ) ^ (u - 1) * (1 - (↑(-x) : ℂ)) ^ (v - 1)) fun (x : ℝ) ↦
  (↑(x + 1) : ℂ) ^ (v - 1) * (1 - (↑(x + 1) : ℂ)) ^ (u - 1)
Tactic: convert! ((betaIntegral_convergent_left hv u).comp_add_right 1).symm using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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)
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑(-x) : ℂ) ^ (u - 1) * (1 - (↑(-x) : ℂ)) ^ (v - 1)) volume (-(1 / 2)) (-1)
have h₁ : -(1 / 2) = 1 / 2 - 1
Tactic: convert! ((betaIntegral_convergent_left hv u).comp_add_right 1).symm using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑(-x) : ℂ) ^ (u - 1) * (1 - (↑(-x) : ℂ)) ^ (v - 1)) volume (-(1 / 2)) (-1)
have h₂ : -1 = HSub.hSub (α := ℝ) 0 1
Tactic: convert! ((betaIntegral_convergent_left hv u).comp_add_right 1).symm using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ Eq (α := ℝ → ℂ) (fun (x : ℝ) ↦ (↑(-x) : ℂ) ^ (u - 1) * (1 - (↑(-x) : ℂ)) ^ (v - 1)) fun (x : ℝ) ↦
    (↑(x + 1) : ℂ) ^ (v - 1) * (1 - (↑(x + 1) : ℂ)) ^ (u - 1)
have h : ∀ (x : ℝ),
  (↑(-x) : ℂ) ^ (u - 1) * (1 - (↑(-x) : ℂ)) ^ (v - 1) = (↑(x + 1) : ℂ) ^ (v - 1) * (1 - (↑(x + 1) : ℂ)) ^ (u - 1)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
| (↑(-x) : ℂ) ^ (u - 1) * (1 - (↑(-x) : ℂ)) ^ (v - 1)
have rw : (1 - (↑(-x) : ℂ)) ^ (v - 1) * (↑(-x) : ℂ) ^ (u - 1)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
⊢ (↑(-x) : ℂ) ^ (u - 1) * (1 - (↑(-x) : ℂ)) ^ (v - 1) = (↑(x + 1) : ℂ) ^ (v - 1) * (1 - (↑(x + 1) : ℂ)) ^ (u - 1)
have h : (1 - (↑(-x) : ℂ)) ^ (v - 1) * (↑(-x) : ℂ) ^ (u - 1) = (↑(x + 1) : ℂ) ^ (v - 1) * (1 - (↑(x + 1) : ℂ)) ^ (u - 1)
Tactic: conv_lhs => rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
⊢ (1 - (↑(-x) : ℂ)) ^ (v - 1) * (↑(-x) : ℂ) ^ (u - 1) = (↑(x + 1) : ℂ) ^ (v - 1) * (1 - (↑(x + 1) : ℂ)) ^ (u - 1)
have h : 1 - (↑(-x) : ℂ) = (↑(x + 1) : ℂ)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
h : 1 - (↑(-x) : ℂ) = (↑(x + 1) : ℂ)
⊢ (1 - (↑(-x) : ℂ)) ^ (v - 1) * (↑(-x) : ℂ) ^ (u - 1) = (↑(x + 1) : ℂ) ^ (v - 1) * (1 - (↑(x + 1) : ℂ)) ^ (u - 1)
have h₁ : (↑(-x) : ℂ) = 1 - (↑(x + 1) : ℂ)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
⊢ 1 - (↑(-x) : ℂ) = (↑(x + 1) : ℂ)
have h : 1 - -(↑x : ℂ) = (↑x : ℂ) + 1
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
⊢ (↑(-x) : ℂ) = 1 - (↑(x + 1) : ℂ)
have h : -(↑x : ℂ) = 1 - ((↑x : ℂ) + 1)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u : ℂ
hu : 0 < u.re
⊢ u.betaIntegral 1 = 1 / u
have simp_rw : ∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (u - 1) = 1 / u
Tactic: simp_rw [betaIntegral, sub_self, cpow_zero, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u : ℂ
hu : 0 < u.re
⊢ ∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (u - 1) = 1 / u
have rw : ((↑1 : ℂ) ^ (u - 1 + 1) - (↑0 : ℂ) ^ (u - 1 + 1)) / (u - 1 + 1) = 1 / u
Tactic: rw [integral_cpow (Or.inl _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u : ℂ
hu : 0 < u.re
rw : ((↑1 : ℂ) ^ (u - 1 + 1) - (↑0 : ℂ) ^ (u - 1 + 1)) / (u - 1 + 1) = 1 / u
⊢ ∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (u - 1) = 1 / u
have rw₁ : -1 < (u - 1).re
Tactic: rw [integral_cpow (Or.inl _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u : ℂ
hu : 0 < u.re
⊢ ((↑1 : ℂ) ^ (u - 1 + 1) - (↑0 : ℂ) ^ (u - 1 + 1)) / (u - 1 + 1) = 1 / u
have rw : u - 1 + 1 ≠ 0
Tactic: rw [ofReal_zero, ofReal_one, one_cpow, zero_cpow, sub_zero, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u : ℂ
hu : 0 < u.re
⊢ u - 1 + 1 ≠ 0
have rw : u ≠ 0
Tactic: rw [sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u : ℂ
hu : 0 < u.re
⊢ u ≠ 0
have contrapose! : ∀ (hu : u = 0), u.re ≤ 0
Tactic: contrapose! hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u : ℂ
hu : u = 0
⊢ u.re ≤ 0
have rw : re 0 ≤ 0
Tactic: rw [hu, zero_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u : ℂ
hu : u = 0
rw : re 0 ≤ 0
⊢ u.re ≤ 0
have rw₁ : LE.le (α := ℝ) 0 0
Tactic: rw [hu, zero_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u : ℂ
hu : 0 < u.re
⊢ -1 < (u - 1).re
have rwa : -1 < u.re - re 1
Tactic: rwa [sub_re, one_re, ← sub_pos, sub_neg_eq_add, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u : ℂ
hu : 0 < u.re
rwa : -1 < u.re - re 1
⊢ -1 < (u - 1).re
have rwa₁ : -1 < u.re - 1
Tactic: rwa [sub_re, one_re, ← sub_pos, sub_neg_eq_add, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u : ℂ
hu : 0 < u.re
rwa : -1 < u.re - re 1
rwa₁ : -1 < u.re - 1
⊢ -1 < (u - 1).re
have rwa₂ : 0 < u.re - 1 - -1
Tactic: rwa [sub_re, one_re, ← sub_pos, sub_neg_eq_add, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u : ℂ
hu : 0 < u.re
rwa : -1 < u.re - re 1
rwa₁ : -1 < u.re - 1
rwa₂ : 0 < u.re - 1 - -1
⊢ -1 < (u - 1).re
have rwa₃ : 0 < u.re - 1 + 1
Tactic: rwa [sub_re, one_re, ← sub_pos, sub_neg_eq_add, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
s t : ℂ
a : ℝ
ha : 0 < a
⊢ ∫ (x : ℝ) in 0..a, (↑x : ℂ) ^ (s - 1) * ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) = (↑a : ℂ) ^ (s + t - 1) * s.betaIntegral t
have ha' : (↑a : ℂ) ≠ 0
Tactic: have ha' : (a : ℂ) ≠ 0 := ofReal_ne_zero.mpr ha.ne'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : (↑a : ℂ) ≠ 0
⊢ (↑a : ℂ) ^ (s + t - 1) = (↑a : ℂ) * ((↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1))
have rw : s + t - 1 = 1 + (s - 1) + (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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : (↑a : ℂ) ≠ 0
rw : s + t - 1 = 1 + (s - 1) + (t - 1)
⊢ (↑a : ℂ) ^ (s + t - 1) = (↑a : ℂ) * ((↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1))
have rw₁ : (↑a : ℂ) ^ (1 + (s - 1) + (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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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))
⊢ (↑a : ℂ) ^ (s + t - 1) = (↑a : ℂ) * ((↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1))
have rw₂ : (↑a : ℂ) ^ (1 + (s - 1)) * (↑a : ℂ) ^ (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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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))
⊢ (↑a : ℂ) ^ (s + t - 1) = (↑a : ℂ) * ((↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1))
have rw₃ : HPow.hPow (β := ℂ) (↑a : ℂ) 1 * (↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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))
⊢ (↑a : ℂ) ^ (s + t - 1) = (↑a : ℂ) * ((↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1))
have rw₄ : (↑a : ℂ) * (↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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))
⊢ (↑a : ℂ) ^ (s + t - 1) = (↑a : ℂ) * ((↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1))
have rw₅ : (↑a : ℂ) * ((↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
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)
have A : (↑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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
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)
have 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)))
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : (↑a : ℂ) ≠ 0
A : (↑a : ℂ) ^ (s + t - 1) = (↑a : ℂ) * ((↑a : ℂ) ^ (s - 1) * (↑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)))
have 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)))
Tactic: simp_rw [intervalIntegral.integral_of_le ha.le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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)))
have 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))
Tactic: refine setIntegral_congr_fun measurableSet_Ioc fun x hx => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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
⊢ (↑x : ℂ) ^ (s - 1) * ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) =
    (↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1) * ((↑(x / a) : ℂ) ^ (s - 1) * (1 - (↑(x / a) : ℂ)) ^ (t - 1))
have rw : (↑x : ℂ) ^ (s - 1) * ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) =
  (↑a : ℂ) ^ (s - 1) * (↑(x / a) : ℂ) ^ (s - 1) * ((↑a : ℂ) ^ (t - 1) * (1 - (↑(x / a) : ℂ)) ^ (t - 1))
Tactic: rw [mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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
⊢ (↑x : ℂ) ^ (s - 1) * ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) =
    (↑a : ℂ) ^ (s - 1) * (↑(x / a) : ℂ) ^ (s - 1) * ((↑a : ℂ) ^ (t - 1) * (1 - (↑(x / a) : ℂ)) ^ (t - 1))
have e_a : (↑x : ℂ) ^ (s - 1) = (↑a : ℂ) ^ (s - 1) * (↑(x / a) : ℂ) ^ (s - 1)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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)
⊢ (↑x : ℂ) ^ (s - 1) * ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) =
    (↑a : ℂ) ^ (s - 1) * (↑(x / a) : ℂ) ^ (s - 1) * ((↑a : ℂ) ^ (t - 1) * (1 - (↑(x / a) : ℂ)) ^ (t - 1))
have e_a₁ : ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) = (↑a : ℂ) ^ (t - 1) * (1 - (↑(x / a) : ℂ)) ^ (t - 1)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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
⊢ (↑x : ℂ) ^ (s - 1) = (↑a : ℂ) ^ (s - 1) * (↑(x / a) : ℂ) ^ (s - 1)
have e_a : (↑x : ℂ) ^ (s - 1) = ((↑a : ℂ) * (↑(x / a) : ℂ)) ^ (s - 1)
Tactic: rw [← mul_cpow_ofReal_nonneg ha.le (div_pos hx.1 ha).le, ofReal_div, mul_div_cancel₀ _ ha']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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)
⊢ (↑x : ℂ) ^ (s - 1) = (↑a : ℂ) ^ (s - 1) * (↑(x / a) : ℂ) ^ (s - 1)
have e_a₁ : (↑x : ℂ) ^ (s - 1) = ((↑a : ℂ) * ((↑x : ℂ) / (↑a : ℂ))) ^ (s - 1)
Tactic: rw [← mul_cpow_ofReal_nonneg ha.le (div_pos hx.1 ha).le, ofReal_div, mul_div_cancel₀ _ ha']