awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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
⊢ (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
have h₁ : ∀ (x : ℝ), u + 1 - 1 = u
Tactic: convert! int_ev
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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 (y : ℝ) ↦ u * ((↑y : ℂ) ^ (u - 1) * (1 - (↑y : ℂ)) ^ v)) volume 0 1
have hf : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (u - 1) * (1 - (↑x : ℂ)) ^ v) volume 0 1
Tactic: apply IntervalIntegrable.const_mul
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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) volume 0 1
have h : ∀ (x : ℝ), v = v + 1 - 1
Tactic: convert! betaIntegral_convergent hu hv'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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 (y : ℝ) ↦ v * ((↑y : ℂ) ^ u * (1 - (↑y : ℂ)) ^ (v - 1))) volume 0 1
have hg : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ (v - 1)) volume 0 1
Tactic: apply IntervalIntegrable.const_mul
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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 - (↑x : ℂ)) ^ (v - 1)) volume 0 1
have h : ∀ (x : ℝ), u = u + 1 - 1
Tactic: convert! betaIntegral_convergent hu' hv
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u : ℂ
hu : 0 < u.re
⊢ u.betaIntegral (HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1) =
    HDiv.hDiv (α := ℂ) (↑0! : ℂ) (∏ j ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1), (u + (↑j : ℂ)))
have zero : 1 / u = HDiv.hDiv (α := ℂ) 1 (∏ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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
⊢ u.betaIntegral (HAdd.hAdd (α := ℂ) (↑(n + 1) : ℂ) 1) =
    HDiv.hDiv (α := ℂ) (↑(n + 1)! : ℂ) (∏ j ∈ Finset.range (n + 1 + 1), (u + (↑j : ℂ)))
have 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 : ℂ)))
Tactic: have := betaIntegral_recurrence hu (?_ : 0 < re n.succ)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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 : ℂ)))
⊢ u.betaIntegral (HAdd.hAdd (α := ℂ) (↑(n + 1) : ℂ) 1) =
    HDiv.hDiv (α := ℂ) (↑(n + 1)! : ℂ) (∏ j ∈ Finset.range (n + 1 + 1), (u + (↑j : ℂ)))
have succ₁ : 0 < re (↑n.succ : ℂ)
Tactic: have := betaIntegral_recurrence hu (?_ : 0 < re n.succ)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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 : ℂ)
⊢ u.betaIntegral (HAdd.hAdd (α := ℂ) (↑(n + 1) : ℂ) 1) =
    HDiv.hDiv (α := ℂ) (↑(n + 1)! : ℂ) (∏ j ∈ Finset.range (n + 1 + 1), (u + (↑j : ℂ)))
have 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 : ℂ)))
Tactic: rw [mul_comm u _, ← eq_div_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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 : ℂ)))
⊢ u.betaIntegral (HAdd.hAdd (α := ℂ) (↑(n + 1) : ℂ) 1) =
    HDiv.hDiv (α := ℂ) (↑(n + 1)! : ℂ) (∏ j ∈ Finset.range (n + 1 + 1), (u + (↑j : ℂ)))
have succ₁ : ∀ (this : u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n.succ : ℂ) 1) * u = (↑n.succ : ℂ) * (u + 1).betaIntegral (↑n.succ : ℂ)),
  u ≠ 0
Tactic: rw [mul_comm u _, ← eq_div_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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 : ℂ)
⊢ u ≠ 0
have succ : ∀ (hu : u = 0), u.re ≤ 0
Tactic: contrapose! hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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
⊢ u.re ≤ 0
have succ : re 0 ≤ 0
Tactic: rw [hu, zero_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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
⊢ u.re ≤ 0
have succ₁ : LE.le (α := ℝ) 0 0
Tactic: rw [hu, zero_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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
⊢ u.betaIntegral (HAdd.hAdd (α := ℂ) (↑(n + 1) : ℂ) 1) =
    HDiv.hDiv (α := ℂ) (↑(n + 1)! : ℂ) (∏ j ∈ Finset.range (n + 1 + 1), (u + (↑j : ℂ)))
have 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 : ℂ)))
Tactic: rw [this, Finset.prod_range_succ', Nat.cast_succ, IH]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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 : ℂ)))
⊢ u.betaIntegral (HAdd.hAdd (α := ℂ) (↑(n + 1) : ℂ) 1) =
    HDiv.hDiv (α := ℂ) (↑(n + 1)! : ℂ) (∏ j ∈ Finset.range (n + 1 + 1), (u + (↑j : ℂ)))
have succ₁ : 0 < (u + 1).re
Tactic: rw [this, Finset.prod_range_succ', Nat.cast_succ, IH]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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
⊢ 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 : ℂ)))
have 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
Tactic: rw [Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one, Nat.cast_zero, add_zero, ←
      mul_div_assoc, ← div_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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
⊢ (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
have succ : ∀ (j : ℕ), u + 1 + (↑j : ℂ) = u + (↑(j + 1) : ℂ)
Tactic: congr 3 with j : 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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 + (↑(j + 1) : ℂ)
have succ : u + 1 + (↑j : ℂ) = u + HAdd.hAdd (α := ℂ) (↑j : ℂ) 1
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u : ℂ
hu : 0 < u.re
n : ℕ
⊢ u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) =
    HDiv.hDiv (α := ℂ) (↑n ! : ℂ) (∏ j ∈ Finset.range (n + 1), (u + (↑j : ℂ)))
have zero : ∀ {u : ℂ} (hu : 0 < u.re),
  u.betaIntegral (HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1) =
    HDiv.hDiv (α := ℂ) (↑0! : ℂ) (∏ j ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 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
Cleared hypotheses: u, hu, n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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 : ℂ)))
⊢ u.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) =
    HDiv.hDiv (α := ℂ) (↑n ! : ℂ) (∏ j ∈ Finset.range (n + 1), (u + (↑j : ℂ)))
have 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 : ℂ)))
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
Cleared hypotheses: u, hu, n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
⊢ s.GammaSeq n = HPow.hPow (α := ℂ) (↑n : ℂ) s * s.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
have rw : HPow.hPow (α := ℂ) (↑n : ℂ) s * (↑n ! : ℂ) / ∏ j ∈ Finset.range (n + 1), (s + (↑j : ℂ)) =
  HPow.hPow (α := ℂ) (↑n : ℂ) s * s.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
Tactic: rw [GammaSeq, betaIntegral_eval_nat_add_one_right hs n, ← mul_div_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
rw :
  HPow.hPow (α := ℂ) (↑n : ℂ) s * (↑n ! : ℂ) / ∏ j ∈ Finset.range (n + 1), (s + (↑j : ℂ)) =
    HPow.hPow (α := ℂ) (↑n : ℂ) s * s.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
⊢ s.GammaSeq n = HPow.hPow (α := ℂ) (↑n : ℂ) s * s.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
have rw₁ : HPow.hPow (α := ℂ) (↑n : ℂ) s * (↑n ! : ℂ) / ∏ j ∈ Finset.range (n + 1), (s + (↑j : ℂ)) =
  HPow.hPow (α := ℂ) (↑n : ℂ) s * HDiv.hDiv (α := ℂ) (↑n ! : ℂ) (∏ j ∈ Finset.range (n + 1), (s + (↑j : ℂ)))
Tactic: rw [GammaSeq, betaIntegral_eval_nat_add_one_right hs n, ← mul_div_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
rw :
  HPow.hPow (α := ℂ) (↑n : ℂ) s * (↑n ! : ℂ) / ∏ j ∈ Finset.range (n + 1), (s + (↑j : ℂ)) =
    HPow.hPow (α := ℂ) (↑n : ℂ) s * s.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
rw₁ :
  HPow.hPow (α := ℂ) (↑n : ℂ) s * (↑n ! : ℂ) / ∏ j ∈ Finset.range (n + 1), (s + (↑j : ℂ)) =
    HPow.hPow (α := ℂ) (↑n : ℂ) s * HDiv.hDiv (α := ℂ) (↑n ! : ℂ) (∏ j ∈ Finset.range (n + 1), (s + (↑j : ℂ)))
⊢ s.GammaSeq n = HPow.hPow (α := ℂ) (↑n : ℂ) s * s.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
have rw₂ : HPow.hPow (α := ℂ) (↑n : ℂ) s * (↑n ! : ℂ) / ∏ j ∈ Finset.range (n + 1), (s + (↑j : ℂ)) =
  HPow.hPow (α := ℂ) (↑n : ℂ) s * (↑n ! : ℂ) / ∏ j ∈ Finset.range (n + 1), (s + (↑j : ℂ))
Tactic: rw [GammaSeq, betaIntegral_eval_nat_add_one_right hs n, ← mul_div_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
| (s + 1).GammaSeq n / s
have rw : HPow.hPow (α := ℂ) (↑n : ℂ) (s + 1) * (↑n ! : ℂ) / ((∏ x ∈ Finset.range n, (s + 1 + (↑x : ℂ))) * (s + 1 + (↑n : ℂ)) * s)
Tactic: rw [GammaSeq, Finset.prod_range_succ, div_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ (s + 1).GammaSeq n / s = (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s) * s.GammaSeq n
have conv_lhs : HPow.hPow (α := ℂ) (↑n : ℂ) (s + 1) * (↑n ! : ℂ) /
    ((∏ x ∈ Finset.range n, (s + 1 + (↑x : ℂ))) * (s + 1 + (↑n : ℂ)) * s) =
  (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s) * s.GammaSeq n
Tactic: conv_lhs => rw [GammaSeq, Finset.prod_range_succ, div_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
| (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s) * s.GammaSeq n
have rw : (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) s * (↑n ! : ℂ) /
  ((∏ k ∈ Finset.range n, (s + (↑(k + 1) : ℂ))) * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s) * s)
Tactic: rw [GammaSeq, Finset.prod_range_succ', Nat.cast_zero, add_zero, div_mul_div_comm, ← mul_assoc,
      ← mul_assoc, mul_comm _ (Finset.prod _ _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) (s + 1) * (↑n ! : ℂ) /
      ((∏ x ∈ Finset.range n, (s + 1 + (↑x : ℂ))) * (s + 1 + (↑n : ℂ)) * s) =
    (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s) * s.GammaSeq n
have conv_rhs : HPow.hPow (α := ℂ) (↑n : ℂ) (s + 1) * (↑n ! : ℂ) /
    ((∏ x ∈ Finset.range n, (s + 1 + (↑x : ℂ))) * (s + 1 + (↑n : ℂ)) * s) =
  (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) s * (↑n ! : ℂ) /
    ((∏ k ∈ Finset.range n, (s + (↑(k + 1) : ℂ))) * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s) * s)
Tactic: conv_rhs =>
    rw [GammaSeq, Finset.prod_range_succ', Nat.cast_zero, add_zero, div_mul_div_comm, ← mul_assoc,
      ← mul_assoc, mul_comm _ (Finset.prod _ _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) (s + 1) * (↑n ! : ℂ) /
      ((∏ x ∈ Finset.range n, (s + 1 + (↑x : ℂ))) * (s + 1 + (↑n : ℂ)) * s) =
    (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) s * (↑n ! : ℂ) /
      ((∏ k ∈ Finset.range n, (s + (↑(k + 1) : ℂ))) * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s) * s)
have e_a : HPow.hPow (α := ℂ) (↑n : ℂ) (s + 1) = (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) s
Tactic: congr 3
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
e_a : HPow.hPow (α := ℂ) (↑n : ℂ) (s + 1) = (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) s
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) (s + 1) * (↑n ! : ℂ) /
      ((∏ x ∈ Finset.range n, (s + 1 + (↑x : ℂ))) * (s + 1 + (↑n : ℂ)) * s) =
    (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) s * (↑n ! : ℂ) /
      ((∏ k ∈ Finset.range n, (s + (↑(k + 1) : ℂ))) * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s) * s)
have e_a₁ : Eq (α := ℂ) (∏ x ∈ Finset.range n, (s + 1 + (↑x : ℂ))) (∏ k ∈ Finset.range n, (s + (↑(k + 1) : ℂ)))
Tactic: congr 3
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
e_a : HPow.hPow (α := ℂ) (↑n : ℂ) (s + 1) = (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) s
e_a₁ : Eq (α := ℂ) (∏ x ∈ Finset.range n, (s + 1 + (↑x : ℂ))) (∏ k ∈ Finset.range n, (s + (↑(k + 1) : ℂ)))
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) (s + 1) * (↑n ! : ℂ) /
      ((∏ x ∈ Finset.range n, (s + 1 + (↑x : ℂ))) * (s + 1 + (↑n : ℂ)) * s) =
    (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) s * (↑n ! : ℂ) /
      ((∏ k ∈ Finset.range n, (s + (↑(k + 1) : ℂ))) * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s) * s)
have e_a₂ : s + 1 + (↑n : ℂ) = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s
Tactic: congr 3
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) (s + 1) = (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) s
have e_a : HPow.hPow (α := ℂ) (↑n : ℂ) s * HPow.hPow (α := ℂ) (β := ℂ) (↑n : ℂ) 1 = (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) s
Tactic: rw [cpow_add _ _ (Nat.cast_ne_zero.mpr hn), cpow_one, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
e_a : HPow.hPow (α := ℂ) (↑n : ℂ) s * HPow.hPow (α := ℂ) (β := ℂ) (↑n : ℂ) 1 = (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) s
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) (s + 1) = (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) s
have e_a₁ : HPow.hPow (α := ℂ) (↑n : ℂ) s * (↑n : ℂ) = (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) s
Tactic: rw [cpow_add _ _ (Nat.cast_ne_zero.mpr hn), cpow_one, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
e_a : HPow.hPow (α := ℂ) (↑n : ℂ) s * HPow.hPow (α := ℂ) (β := ℂ) (↑n : ℂ) 1 = (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) s
e_a₁ : HPow.hPow (α := ℂ) (↑n : ℂ) s * (↑n : ℂ) = (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) s
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) (s + 1) = (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) s
have e_a₂ : (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) s = (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) s
Tactic: rw [cpow_add _ _ (Nat.cast_ne_zero.mpr hn), cpow_one, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ Eq (α := ℂ) (∏ x ∈ Finset.range n, (s + 1 + (↑x : ℂ))) (∏ k ∈ Finset.range n, (s + (↑(k + 1) : ℂ)))
have e_a : ∀ x ∈ Finset.range n, s + 1 + (↑x : ℂ) = s + (↑(x + 1) : ℂ)
Tactic: refine Finset.prod_congr (by rfl) fun x _ => ?_