awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
this : HasDerivAt (fun (x : ℂ) ↦ id x ^ u) (u * id (↑x : ℂ) ^ (u - 1) * 1) (↑x : ℂ)
⊢ HasDerivAt (fun (x : ℂ) ↦ x ^ u) (u * (↑x : ℂ) ^ (u - 1)) (↑x : ℂ)

Tactic:
simp only [id_eq, mul_one] at this

Premises used: mul_one, id_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
this : HasDerivAt (fun (x : ℂ) ↦ x ^ u) (u * (↑x : ℂ) ^ (u - 1)) (↑x : ℂ)
⊢ HasDerivAt (fun (y : ℂ) ↦ y ^ u) (u * (↑x : ℂ) ^ (u - 1)) (↑x : ℂ)

Tactic:
this
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
this : HasDerivAt (fun (x : ℂ) ↦ x ^ u) (u * (↑x : ℂ) ^ (u - 1)) (↑x : ℂ)
⊢ HasDerivAt (fun (y : ℂ) ↦ y ^ u) (u * (↑x : ℂ) ^ (u - 1)) (↑x : ℂ)

Tactic:
exact this
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
refine_1 : 0 < x
⊢ 0 < (id (↑x : ℂ)).re

Tactic:
rw [id_eq, ofReal_re]

Premises used: Complex.ofReal_re, id_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
⊢ 0 < x

Tactic:
hx.1

Premises used: And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
⊢ 0 < x

Tactic:
exact hx.1

Premises used: And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
⊢ HasDerivAt (fun (y : ℂ) ↦ y ^ u) (u * (↑x : ℂ) ^ (u - 1)) (↑x : ℂ)

Tactic:
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
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℂ)
refine_2 :
  ∀ (A : HasDerivAt (fun (x : ℂ) ↦ id x ^ v) (v * id (1 - (↑x : ℂ)) ^ (v - 1) * 1) (1 - (↑x : ℂ))),
    HasDerivAt (fun (y : ℂ) ↦ (1 - y) ^ v) (-v * (1 - (↑x : ℂ)) ^ (v - 1)) (↑x : ℂ)
refine_1 : 0 < (id (1 - (↑x : ℂ))).re
⊢ HasDerivAt (fun (y : ℂ) ↦ (1 - y) ^ v) (-v * (1 - (↑x : ℂ)) ^ (v - 1)) (↑x : ℂ)

Tactic:
have A := @HasDerivAt.cpow_const _ _ _ v (hasDerivAt_id (1 - (x : ℂ))) (Or.inl ?_)
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℂ)
refine_1 : x < 1
⊢ 0 < (id (1 - (↑x : ℂ))).re

Tactic:
rw [id, sub_re, one_re, ofReal_re, sub_pos]

Premises used: sub_pos, Complex.sub_re, id, Complex.ofReal_re, Complex.one_re
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℂ)
⊢ x < 1

Tactic:
hx.2

Premises used: And.right
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℂ)
⊢ x < 1

Tactic:
exact hx.2

Premises used: And.right
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℂ))
hf : HasDerivAt (F := ℂ) (fun (x : ℂ) ↦ x) 1 (↑x : ℂ)
⊢ HasDerivAt (F := ℂ) (fun (y : ℂ) ↦ 1 - y) (-1) (↑x : ℂ)

Tactic:
apply HasDerivAt.const_sub

Premises used: HasDerivAt.const_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 (x : ℂ) ↦ x) 1 (↑x : ℂ)

Tactic:
apply hasDerivAt_id

Premises used: hasDerivAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℂ)

Tactic:
have B : HasDerivAt (fun y : ℂ => 1 - y) (-1) ↑x := by
        apply HasDerivAt.const_sub; apply hasDerivAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 (x : ℂ) ↦ x ^ v) ∘ HSub.hSub (α := ℂ) 1) (v * (1 - (↑x : ℂ)) ^ (v - 1) * 1 * -1) (↑x : ℂ)

Tactic:
HasDerivAt.comp (↑x) A B

Premises used: HasDerivAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℂ)
h : -v * (1 - (↑x : ℂ)) ^ (v - 1) = v * (1 - (↑x : ℂ)) ^ (v - 1) * 1 * -1
⊢ HasDerivAt (fun (y : ℂ) ↦ (1 - y) ^ v) (-v * (1 - (↑x : ℂ)) ^ (v - 1)) (↑x : ℂ)

Tactic:
convert! HasDerivAt.comp (↑x) A B using 1

Premises used: HasDerivAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℂ)
⊢ -v * (1 - (↑x : ℂ)) ^ (v - 1) = v * (1 - (↑x : ℂ)) ^ (v - 1) * 1 * -1

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 (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
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
    (fun (y : ℝ) ↦ HMul.hMul (α := ℂ → ℂ) (β := ℂ → ℂ) (fun (y : ℂ) ↦ y ^ u) (fun (y : ℂ) ↦ (1 - y) ^ v) (↑y : ℂ))
    (u * (↑x : ℂ) ^ (u - 1) * (1 - (↑x : ℂ)) ^ v + (↑x : ℂ) ^ u * (-v * (1 - (↑x : ℂ)) ^ (v - 1))) x

Tactic:
(U.mul V).comp_ofReal

Premises used: HasDerivAt.comp_ofReal, HasDerivAt.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℂ)
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))
⊢ HasDerivAt F (u * ((↑x : ℂ) ^ (u - 1) * (1 - (↑x : ℂ)) ^ v) - v * ((↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ (v - 1))) x

Tactic:
convert! (U.mul V).comp_ofReal using 1

Premises used: HasDerivAt.comp_ofReal, HasDerivAt.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℂ)
⊢ 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:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℝ),
    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
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
⊢ 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)
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
⊢ 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

Premises used: add_sub_cancel_right
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
⊢ ∫ (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
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
simp : ¬u = 0
⊢ F 0 = 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]

Premises used: sub_zero, Complex.cpow_eq_zero_iff, Ne, mul_eq_zero, Complex.ofReal_zero, Complex.one_cpow, or_false, one_ne_zero, true_and
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
contrapose! : ∀ (hu : u = 0), u.re ≤ 0
⊢ ¬u = 0

Tactic:
contrapose! hu
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
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 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

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]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
simp : ¬v = 0
⊢ F 1 = 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]

Premises used: sub_self, Complex.cpow_eq_zero_iff, Complex.ofReal_one, Ne, false_or, mul_eq_zero, Complex.one_cpow, one_ne_zero, true_and
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
contrapose! : ∀ (hv : v = 0), v.re ≤ 0
⊢ ¬v = 0

Tactic:
contrapose! hv
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
rw₁ rw₂ : LE.le (α := ℝ) 0 0
⊢ v.re ≤ 0

Tactic:
rw [hv, zero_re]

Premises used: Complex.zero_re
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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

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]