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)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
U : HasDerivAt (fun (y : ℂ) ↦ y ^ u) (u * (↑x : ℂ) ^ (u - 1)) (↑x : ℂ)
⊢ 0 < (id (1 - (↑x : ℂ))).re
have refine_1 : x < 1
Tactic: rw [id, sub_re, one_re, ofReal_re, sub_pos]
-- 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)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
U : HasDerivAt (fun (y : ℂ) ↦ y ^ u) (u * (↑x : ℂ) ^ (u - 1)) (↑x : ℂ)
A : HasDerivAt (fun (x : ℂ) ↦ x ^ v) (v * (1 - (↑x : ℂ)) ^ (v - 1) * 1) (1 - (↑x : ℂ))
⊢ HasDerivAt (F := ℂ) (fun (y : ℂ) ↦ 1 - y) (-1) (↑x : ℂ)
have hf : HasDerivAt (F := ℂ) (fun (x : ℂ) ↦ x) 1 (↑x : ℂ)
Tactic: apply HasDerivAt.const_sub
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
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)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
U : HasDerivAt (fun (y : ℂ) ↦ y ^ u) (u * (↑x : ℂ) ^ (u - 1)) (↑x : ℂ)
A : HasDerivAt (fun (x : ℂ) ↦ x ^ v) (v * (1 - (↑x : ℂ)) ^ (v - 1) * 1) (1 - (↑x : ℂ))
⊢ HasDerivAt (fun (y : ℂ) ↦ (1 - y) ^ v) (-v * (1 - (↑x : ℂ)) ^ (v - 1)) (↑x : ℂ)
have B : HasDerivAt (F := ℂ) (fun (y : ℂ) ↦ 1 - y) (-1) (↑x : ℂ)
Tactic: have B : HasDerivAt (fun y : ℂ => 1 - y) (-1) ↑x := by
        apply HasDerivAt.const_sub; apply hasDerivAt_id
-- 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)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
U : HasDerivAt (fun (y : ℂ) ↦ y ^ u) (u * (↑x : ℂ) ^ (u - 1)) (↑x : ℂ)
A : HasDerivAt (fun (x : ℂ) ↦ x ^ v) (v * (1 - (↑x : ℂ)) ^ (v - 1) * 1) (1 - (↑x : ℂ))
B : HasDerivAt (F := ℂ) (fun (y : ℂ) ↦ 1 - y) (-1) (↑x : ℂ)
⊢ HasDerivAt (fun (y : ℂ) ↦ (1 - y) ^ v) (-v * (1 - (↑x : ℂ)) ^ (v - 1)) (↑x : ℂ)
have h : -v * (1 - (↑x : ℂ)) ^ (v - 1) = v * (1 - (↑x : ℂ)) ^ (v - 1) * 1 * -1
Tactic: convert! HasDerivAt.comp (↑x) A B using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
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)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
U : HasDerivAt (fun (y : ℂ) ↦ y ^ u) (u * (↑x : ℂ) ^ (u - 1)) (↑x : ℂ)
⊢ HasDerivAt F (u * ((↑x : ℂ) ^ (u - 1) * (1 - (↑x : ℂ)) ^ v) - v * ((↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ (v - 1))) x
have V : HasDerivAt (fun (y : ℂ) ↦ (1 - y) ^ v) (-v * (1 - (↑x : ℂ)) ^ (v - 1)) (↑x : ℂ)
Tactic: have V : HasDerivAt (fun y : ℂ => (1 - y) ^ v) (-v * (1 - (x : ℂ)) ^ (v - 1)) ↑x := by
      have A := @HasDerivAt.cpow_const _ _ _ v (hasDerivAt_id (1 - (x : ℂ))) (Or.inl ?_)
      swap; · rw [id, sub_re, one_re, ofReal_re, sub_pos]; exact hx.2
      simp_rw [id] at A
      have B : HasDerivAt (fun y : ℂ => 1 - y) (-1) ↑x := by
        apply HasDerivAt.const_sub; apply hasDerivAt_id
      convert! HasDerivAt.comp (↑x) A B using 1
      ring
-- 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)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
U : HasDerivAt (fun (y : ℂ) ↦ y ^ u) (u * (↑x : ℂ) ^ (u - 1)) (↑x : ℂ)
V : HasDerivAt (fun (y : ℂ) ↦ (1 - y) ^ v) (-v * (1 - (↑x : ℂ)) ^ (v - 1)) (↑x : ℂ)
⊢ HasDerivAt F (u * ((↑x : ℂ) ^ (u - 1) * (1 - (↑x : ℂ)) ^ v) - v * ((↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ (v - 1))) x
have h : u * ((↑x : ℂ) ^ (u - 1) * (1 - (↑x : ℂ)) ^ v) - v * ((↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ (v - 1)) =
  u * (↑x : ℂ) ^ (u - 1) * (1 - (↑x : ℂ)) ^ v + (↑x : ℂ) ^ u * (-v * (1 - (↑x : ℂ)) ^ (v - 1))
Tactic: convert! (U.mul V).comp_ofReal using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
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)
⊢ u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
have 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
Tactic: have hder : ∀ x : ℝ, x ∈ Ioo (0 : ℝ) 1 →
      HasDerivAt F (u * ((x : ℂ) ^ (u - 1) * (1 - (x : ℂ)) ^ v) -
        v * ((x : ℂ) ^ u * (1 - (x : ℂ)) ^ (v - 1))) x := by
    intro x hx
    have U : HasDerivAt (fun y : ℂ => y ^ u) (u * (x : ℂ) ^ (u - 1)) ↑x := by
      have := @HasDerivAt.cpow_const _ _ _ u (hasDerivAt_id (x : ℂ)) (Or.inl ?_)
      · simp only [id_eq, mul_one] at this
        exact this
      · rw [id_eq, ofReal_re]; exact hx.1
    have V : HasDerivAt (fun y : ℂ => (1 - y) ^ v) (-v * (1 - (x : ℂ)) ^ (v - 1)) ↑x := by
      have A := @HasDerivAt.cpow_const _ _ _ v (hasDerivAt_id (1 - (x : ℂ))) (Or.inl ?_)
      swap; · rw [id, sub_re, one_re, ofReal_re, sub_pos]; exact hx.2
      simp_rw [id] at A
      have B : HasDerivAt (fun y : ℂ => 1 - y) (-1) ↑x := by
        apply HasDerivAt.const_sub; apply hasDerivAt_id
      convert! HasDerivAt.comp (↑x) A B using 1
      ring
    convert! (U.mul V).comp_ofReal using 1
    ring
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
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
⊢ u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
have h_int : IntervalIntegrable (ε := ℂ)
  (fun (x : ℝ) ↦
    u * ((↑x : ℂ) ^ (u - 1) * (1 - (↑x : ℂ)) ^ (v + 1 - 1)) - v * ((↑x : ℂ) ^ (u + 1 - 1) * (1 - (↑x : ℂ)) ^ (v - 1)))
  volume 0 1
Tactic: have h_int := ((betaIntegral_convergent hu hv').const_mul u).sub
    ((betaIntegral_convergent hu' hv).const_mul v)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
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 + 1 - 1)) - v * ((↑x : ℂ) ^ (u + 1 - 1) * (1 - (↑x : ℂ)) ^ (v - 1)))
    volume 0 1
⊢ u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
have h_int₁ : IntervalIntegrable (ε := ℂ)
  (fun (x : ℝ) ↦ u * ((↑x : ℂ) ^ (u - 1) * (1 - (↑x : ℂ)) ^ v) - v * ((↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ (v - 1))) volume 0
  1
Tactic: rw [add_sub_cancel_right, add_sub_cancel_right] at h_int
Cleared hypotheses: h_int
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
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
⊢ u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
have int_ev : ∫ (y : ℝ) in 0..1, u * ((↑y : ℂ) ^ (u - 1) * (1 - (↑y : ℂ)) ^ v) - v * ((↑y : ℂ) ^ u * (1 - (↑y : ℂ)) ^ (v - 1)) =
  F 1 - F 0
Tactic: have int_ev := intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le zero_le_one hc hder h_int
-- 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 :
  ∫ (y : ℝ) in 0..1, u * ((↑y : ℂ) ^ (u - 1) * (1 - (↑y : ℂ)) ^ v) - v * ((↑y : ℂ) ^ u * (1 - (↑y : ℂ)) ^ (v - 1)) =
    F 1 - F 0
⊢ F 0 = 0
have simp : ¬u = 0
Tactic: simp only [F, mul_eq_zero, ofReal_zero, cpow_eq_zero_iff, Ne,
      true_and, sub_zero, one_cpow, one_ne_zero, or_false]
-- 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 :
  ∫ (y : ℝ) in 0..1, u * ((↑y : ℂ) ^ (u - 1) * (1 - (↑y : ℂ)) ^ v) - v * ((↑y : ℂ) ^ u * (1 - (↑y : ℂ)) ^ (v - 1)) =
    F 1 - F 0
⊢ ¬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 v : ℂ
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 :
  ∫ (y : ℝ) in 0..1, u * ((↑y : ℂ) ^ (u - 1) * (1 - (↑y : ℂ)) ^ v) - v * ((↑y : ℂ) ^ u * (1 - (↑y : ℂ)) ^ (v - 1)) =
    F 1 - F 0
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 v : ℂ
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 :
  ∫ (y : ℝ) in 0..1, u * ((↑y : ℂ) ^ (u - 1) * (1 - (↑y : ℂ)) ^ v) - v * ((↑y : ℂ) ^ u * (1 - (↑y : ℂ)) ^ (v - 1)) =
    F 1 - F 0
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 (hypothesis)
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 :
  ∫ (y : ℝ) in 0..1, u * ((↑y : ℂ) ^ (u - 1) * (1 - (↑y : ℂ)) ^ v) - v * ((↑y : ℂ) ^ u * (1 - (↑y : ℂ)) ^ (v - 1)) =
    F 1 - F 0
⊢ u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
have hF0 : F 0 = 0
Tactic: have hF0 : F 0 = 0 := by
    simp only [F, mul_eq_zero, ofReal_zero, cpow_eq_zero_iff, Ne,
      true_and, sub_zero, one_cpow, one_ne_zero, or_false]
    contrapose! hu; rw [hu, zero_re]
-- 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 :
  ∫ (y : ℝ) in 0..1, u * ((↑y : ℂ) ^ (u - 1) * (1 - (↑y : ℂ)) ^ v) - v * ((↑y : ℂ) ^ u * (1 - (↑y : ℂ)) ^ (v - 1)) =
    F 1 - F 0
hF0 : F 0 = 0
⊢ F 1 = 0
have simp : ¬v = 0
Tactic: simp only [F, mul_eq_zero, ofReal_one, one_cpow, one_ne_zero, sub_self, cpow_eq_zero_iff,
      Ne, true_and, false_or]
-- 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 :
  ∫ (y : ℝ) in 0..1, u * ((↑y : ℂ) ^ (u - 1) * (1 - (↑y : ℂ)) ^ v) - v * ((↑y : ℂ) ^ u * (1 - (↑y : ℂ)) ^ (v - 1)) =
    F 1 - F 0
hF0 : F 0 = 0
⊢ ¬v = 0
have contrapose! : ∀ (hv : v = 0), v.re ≤ 0
Tactic: contrapose! hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u v : ℂ
hu : 0 < u.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 :
  ∫ (y : ℝ) in 0..1, u * ((↑y : ℂ) ^ (u - 1) * (1 - (↑y : ℂ)) ^ v) - v * ((↑y : ℂ) ^ u * (1 - (↑y : ℂ)) ^ (v - 1)) =
    F 1 - F 0
hF0 : F 0 = 0
hv : v = 0
⊢ v.re ≤ 0
have rw : re 0 ≤ 0
Tactic: rw [hv, zero_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u v : ℂ
hu : 0 < u.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 :
  ∫ (y : ℝ) in 0..1, u * ((↑y : ℂ) ^ (u - 1) * (1 - (↑y : ℂ)) ^ v) - v * ((↑y : ℂ) ^ u * (1 - (↑y : ℂ)) ^ (v - 1)) =
    F 1 - F 0
hF0 : F 0 = 0
hv : v = 0
rw : re 0 ≤ 0
⊢ v.re ≤ 0
have rw₁ : LE.le (α := ℝ) 0 0
Tactic: rw [hv, zero_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
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 :
  ∫ (y : ℝ) in 0..1, u * ((↑y : ℂ) ^ (u - 1) * (1 - (↑y : ℂ)) ^ v) - v * ((↑y : ℂ) ^ u * (1 - (↑y : ℂ)) ^ (v - 1)) =
    F 1 - F 0
hF0 : F 0 = 0
⊢ u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
have hF1 : F 1 = 0
Tactic: have hF1 : F 1 = 0 := by
    simp only [F, mul_eq_zero, ofReal_one, one_cpow, one_ne_zero, sub_self, cpow_eq_zero_iff,
      Ne, true_and, false_or]
    contrapose! hv; rw [hv, zero_re]
-- 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 :
  ∫ (y : ℝ) in 0..1, u * ((↑y : ℂ) ^ (u - 1) * (1 - (↑y : ℂ)) ^ v) - v * ((↑y : ℂ) ^ u * (1 - (↑y : ℂ)) ^ (v - 1)) =
    F 1 - F 0
hF0 : F 0 = 0
hF1 : F 1 = 0
⊢ u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
have rw : ∀
  (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), u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
Tactic: rw [hF0, hF1, sub_zero, intervalIntegral.integral_sub, intervalIntegral.integral_const_mul,
    intervalIntegral.integral_const_mul] at int_ev
Cleared hypotheses: int_ev, hF0, hF1
-- 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 :
  ∫ (y : ℝ) in 0..1, u * ((↑y : ℂ) ^ (u - 1) * (1 - (↑y : ℂ)) ^ v) - v * ((↑y : ℂ) ^ u * (1 - (↑y : ℂ)) ^ (v - 1)) =
    F 1 - F 0
hF0 : F 0 = 0
hF1 : F 1 = 0
rw :
  ∀
    (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), u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
⊢ u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
have hf : ∀
  (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
Tactic: rw [hF0, hF1, sub_zero, intervalIntegral.integral_sub, intervalIntegral.integral_const_mul,
    intervalIntegral.integral_const_mul] at int_ev
Cleared hypotheses: int_ev, hF0, hF1
-- 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 :
  ∫ (y : ℝ) in 0..1, u * ((↑y : ℂ) ^ (u - 1) * (1 - (↑y : ℂ)) ^ v) - v * ((↑y : ℂ) ^ u * (1 - (↑y : ℂ)) ^ (v - 1)) =
    F 1 - F 0
hF0 : F 0 = 0
hF1 : F 1 = 0
rw :
  ∀
    (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), u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
hf :
  ∀
    (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
⊢ u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
have hg : ∀
  (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
Tactic: rw [hF0, hF1, sub_zero, intervalIntegral.integral_sub, intervalIntegral.integral_const_mul,
    intervalIntegral.integral_const_mul] at int_ev
Cleared hypotheses: int_ev, hF0, hF1
-- 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
⊢ u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
have rw : (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
Tactic: rw [betaIntegral, betaIntegral, ← sub_eq_zero]
-- 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
⊢ (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 : ℝ), v + 1 - 1 = v
Tactic: convert! int_ev