awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
refine : Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1)
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ

Tactic:
refine (Differentiable.mul ?_ (differentiable_const _)).differentiableOn

Premises used: differentiable_const, Differentiable.differentiableOn, Differentiable.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
ha : Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹
hb : Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ HPow.hPow (α := ℂ) 2 (2 * z - 1)
⊢ Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1)

Tactic:
apply Differentiable.mul

Premises used: Differentiable.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹

Tactic:
differentiable_one_div_Gamma.comp (differentiable_id.const_mul _)

Premises used: Differentiable.const_mul, Complex.differentiable_one_div_Gamma, Differentiable.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹

Tactic:
exact differentiable_one_div_Gamma.comp (differentiable_id.const_mul _)

Premises used: Differentiable.const_mul, Complex.differentiable_one_div_Gamma, Differentiable.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ HPow.hPow (α := ℂ) 2 (2 * z - 1)

Tactic:
fun t => DifferentiableAt.const_cpow ?_ (Or.inl two_ne_zero)

Premises used: Differentiable, DifferentiableAt.const_cpow, two_ne_zero, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
hb : ∀ (t : ℂ), DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ 2 * z - 1) t
⊢ Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ HPow.hPow (α := ℂ) 2 (2 * z - 1)

Tactic:
refine fun t => DifferentiableAt.const_cpow ?_ (Or.inl two_ne_zero)

Premises used: DifferentiableAt.const_cpow, two_ne_zero, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
t : ℂ
⊢ DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ 2 * z - 1) t

Tactic:
DifferentiableAt.sub_const (differentiableAt_id.const_mul _) _

Premises used: DifferentiableAt.sub_const
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
t : ℂ
⊢ DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ 2 * z - 1) t

Tactic:
exact DifferentiableAt.sub_const (differentiableAt_id.const_mul _) _

Premises used: DifferentiableAt.sub_const
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ

Tactic:
have h2 : AnalyticOnNhd ℂ
      (fun z => (Gamma (2 * z))⁻¹ * (2 : ℂ) ^ (2 * z - 1) / ↑(√π)) univ := by
    refine DifferentiableOn.analyticOnNhd ?_ isOpen_univ
    refine (Differentiable.mul ?_ (differentiable_const _)).differentiableOn
    apply Differentiable.mul
    · exact differentiable_one_div_Gamma.comp (differentiable_id.const_mul _)
    · refine fun t => DifferentiableAt.const_cpow ?_ (Or.inl two_ne_zero)
      exact DifferentiableAt.sub_const (differentiableAt_id.const_mul _) _
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
rw : Tendsto ofReal (𝓝[≠] 1) (𝓝 1) ∧ ∀ᶠ (n : ℝ) in 𝓝[≠] 1, Membership.mem (γ := Set ℂ) {1}ᶜ (↑n : ℂ)
⊢ Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)

Tactic:
rw [tendsto_nhdsWithin_iff]

Premises used: tendsto_nhdsWithin_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
left : Tendsto ofReal (𝓝[≠] 1) (𝓝 1)
right : ∀ᶠ (n : ℝ) in 𝓝[≠] 1, Membership.mem (γ := Set ℂ) {1}ᶜ (↑n : ℂ)
⊢ Tendsto ofReal (𝓝[≠] 1) (𝓝 1) ∧ ∀ᶠ (n : ℝ) in 𝓝[≠] 1, Membership.mem (γ := Set ℂ) {1}ᶜ (↑n : ℂ)

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
⊢ Tendsto ofReal (𝓝[≠] 1) (𝓝 1)

Tactic:
tendsto_nhdsWithin_of_tendsto_nhds continuous_ofReal.continuousAt

Premises used: Continuous.continuousAt, tendsto_nhdsWithin_of_tendsto_nhds, Complex.continuous_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
⊢ Tendsto ofReal (𝓝[≠] 1) (𝓝 1)

Tactic:
exact tendsto_nhdsWithin_of_tendsto_nhds continuous_ofReal.continuousAt

Premises used: Continuous.continuousAt, tendsto_nhdsWithin_of_tendsto_nhds, Complex.continuous_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
⊢ ∀ᶠ (n : ℝ) in 𝓝[≠] 1, Membership.mem (γ := Set ℂ) {1}ᶜ (↑n : ℂ)

Tactic:
eventually_nhdsWithin_iff.mpr (Eventually.of_forall fun t ht => ofReal_ne_one.mpr ht)

Premises used: Iff.mpr, Complex.ofReal_ne_one, Filter.Eventually.of_forall, eventually_nhdsWithin_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
⊢ ∀ᶠ (n : ℝ) in 𝓝[≠] 1, Membership.mem (γ := Set ℂ) {1}ᶜ (↑n : ℂ)

Tactic:
exact eventually_nhdsWithin_iff.mpr (Eventually.of_forall fun t ht => ofReal_ne_one.mpr ht)

Premises used: Iff.mpr, Complex.ofReal_ne_one, Filter.Eventually.of_forall, eventually_nhdsWithin_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
⊢ Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)

Tactic:
have h3 : Tendsto ((↑) : ℝ → ℂ) (𝓝[≠] 1) (𝓝[≠] 1) := by
    rw [tendsto_nhdsWithin_iff]; constructor
    · exact tendsto_nhdsWithin_of_tendsto_nhds continuous_ofReal.continuousAt
    · exact eventually_nhdsWithin_iff.mpr (Eventually.of_forall fun t ht => ofReal_ne_one.mpr ht)
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
⊢ Eq (α := (z : ℂ) → ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) fun (z : ℂ) ↦
    (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)

Tactic:
AnalyticOnNhd.eq_of_frequently_eq h1 h2 (h3.frequently ?_)

Premises used: Filter.Tendsto.frequently, AnalyticOnNhd.eq_of_frequently_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
refine :
  ∃ᶠ (x : ℝ) in 𝓝[≠] 1,
    (Gamma (↑x : ℂ))⁻¹ * (Gamma ((↑x : ℂ) + 1 / 2))⁻¹ =
      (Gamma (2 * (↑x : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑x : ℂ) - 1) / (↑√π : ℂ)
⊢ Eq (α := (z : ℂ) → ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) fun (z : ℂ) ↦
    (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)

Tactic:
refine AnalyticOnNhd.eq_of_frequently_eq h1 h2 (h3.frequently ?_)

Premises used: Filter.Tendsto.frequently, AnalyticOnNhd.eq_of_frequently_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
⊢ ∃ᶠ (x : ℝ) in 𝓝[≠] 1,
    (Gamma (↑x : ℂ))⁻¹ * (Gamma ((↑x : ℂ) + 1 / 2))⁻¹ =
      (Gamma (2 * (↑x : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑x : ℂ) - 1) / (↑√π : ℂ)

Tactic:
((Eventually.filter_mono nhdsWithin_le_nhds) ?_).frequently

Premises used: Filter.Eventually.filter_mono, nhdsWithin_le_nhds, Filter.Eventually.frequently
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
refine :
  ∀ᶠ (x : ℝ) in 𝓝 1,
    (Gamma (↑x : ℂ))⁻¹ * (Gamma ((↑x : ℂ) + 1 / 2))⁻¹ =
      (Gamma (2 * (↑x : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑x : ℂ) - 1) / (↑√π : ℂ)
⊢ ∃ᶠ (x : ℝ) in 𝓝[≠] 1,
    (Gamma (↑x : ℂ))⁻¹ * (Gamma ((↑x : ℂ) + 1 / 2))⁻¹ =
      (Gamma (2 * (↑x : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑x : ℂ) - 1) / (↑√π : ℂ)

Tactic:
refine ((Eventually.filter_mono nhdsWithin_le_nhds) ?_).frequently

Premises used: Filter.Eventually.filter_mono, nhdsWithin_le_nhds, Filter.Eventually.frequently
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
⊢ ∀ᶠ (x : ℝ) in 𝓝 1,
    (Gamma (↑x : ℂ))⁻¹ * (Gamma ((↑x : ℂ) + 1 / 2))⁻¹ =
      (Gamma (2 * (↑x : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑x : ℂ) - 1) / (↑√π : ℂ)

Tactic:
(eventually_gt_nhds zero_lt_one).mp (Eventually.of_forall fun t ht => ?_)

Premises used: Filter.Eventually.of_forall, eventually_gt_nhds, zero_lt_one, Filter.Eventually.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
refine :
  ∀ (t : ℝ) (ht : 0 < t),
    (Gamma (↑t : ℂ))⁻¹ * (Gamma ((↑t : ℂ) + 1 / 2))⁻¹ =
      (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
⊢ ∀ᶠ (x : ℝ) in 𝓝 1,
    (Gamma (↑x : ℂ))⁻¹ * (Gamma ((↑x : ℂ) + 1 / 2))⁻¹ =
      (Gamma (2 * (↑x : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑x : ℂ) - 1) / (↑√π : ℂ)

Tactic:
refine (eventually_gt_nhds zero_lt_one).mp (Eventually.of_forall fun t ht => ?_)

Premises used: Filter.Eventually.of_forall, eventually_gt_nhds, zero_lt_one, Filter.Eventually.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
t : ℝ
ht : 0 < t
⊢ (↑t : ℂ) + 1 / 2 = (↑(t + 1 / 2) : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
t : ℝ
ht : 0 < t
⊢ 2 * (↑t : ℂ) = (↑(2 * t) : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
t : ℝ
ht : 0 < t
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ℕ) 2 2
⊢ (↑2 : ℂ) = 2

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℝ
rw : (↑(Gamma s * Gamma (s + 1 / 2)) : ℂ) = (↑(Gamma (2 * s) * HPow.hPow (α := ℝ) 2 (1 - 2 * s) * √π) : ℂ)
⊢ Gamma s * Gamma (s + 1 / 2) = Gamma (2 * s) * HPow.hPow (α := ℝ) 2 (1 - 2 * s) * √π

Tactic:
rw [← ofReal_inj]

Premises used: Complex.ofReal_inj
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℝ
⊢ (↑(Gamma s * Gamma (s + 1 / 2)) : ℂ) = (↑(Gamma (2 * s) * HPow.hPow (α := ℝ) 2 (1 - 2 * s) * √π) : ℂ)

Tactic:
simpa only [← Gamma_ofReal, ofReal_cpow zero_le_two, ofReal_mul, ofReal_add, ofReal_div,
    ofReal_sub] using Complex.Gamma_mul_Gamma_add_half ↑s

Premises used: Complex.ofReal_cpow, Complex.ofReal_add, Complex.ofReal, Complex.ofReal_div, Complex.ofReal_sub, zero_le_two, Complex.Gamma_mul_Gamma_add_half, Complex.Gamma_ofReal, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
⊢ (1 / a).HolderConjugate (1 / b)

Tactic:
have e : HolderConjugate (1 / a) (1 / b) := Real.holderConjugate_one_div ha hb hab
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
linarith : b < 1 - a → -(a + b - 1) + (b - (1 - a)) = 0
linarith₁ : 1 - a < b → a + b - 1 + (1 - a - b) = 0
⊢ b = 1 - a

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
⊢ b = 1 - a

Tactic:
have hab' : b = 1 - a := by linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
⊢ 0 < a * s + b * t

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
⊢ 0 < a * s + b * t

Tactic:
have hst : 0 < a * s + b * t := by positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
⊢ ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x

Tactic:
have posf : ∀ c u x : ℝ, x ∈ Ioi (0 : ℝ) → 0 ≤ f c u x := fun c u x hx =>
    mul_nonneg (exp_pos _).le (rpow_pos_of_pos hx _).le
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
⊢ ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x

Tactic:
have posf' : ∀ c u : ℝ, ∀ᵐ x : ℝ ∂volume.restrict (Ioi 0), 0 ≤ f c u x := fun c u =>
    (ae_restrict_iff' measurableSet_Ioi).mpr (ae_of_all _ (posf c u))
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
c x : ℝ
hc : 0 < c
u : ℝ
hx : 0 < x
dsimp : rexp (-x) * x ^ (u - 1) = (rexp (-c * x) * x ^ (c * (u - 1))) ^ (1 / c)
⊢ rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)

Tactic:
dsimp only [f]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
c x : ℝ
hc : 0 < c
u : ℝ
hx : 0 < x
rw : rexp (-x) * x ^ (u - 1) = rexp (-c * x * (1 / c)) * x ^ (c * (u - 1) * (1 / c))
⊢ rexp (-x) * x ^ (u - 1) = (rexp (-c * x) * x ^ (c * (u - 1))) ^ (1 / c)

Tactic:
rw [mul_rpow (exp_pos _).le ((rpow_nonneg hx.le) _), ← exp_mul, ← rpow_mul hx.le]

Premises used: Real.exp_mul, Real.mul_rpow, LT.lt.le, Real.rpow_nonneg, Real.rpow_mul, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
c x : ℝ
hc : 0 < c
u : ℝ
hx : 0 < x
e_a : -x = -c * x * (1 / c)
e_a₁ : u - 1 = c * (u - 1) * (1 / c)
⊢ rexp (-x) * x ^ (u - 1) = rexp (-c * x * (1 / c)) * x ^ (c * (u - 1) * (1 / c))

Tactic:
congr 2
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
c x : ℝ
hc : 0 < c
u : ℝ
hx : 0 < x
⊢ -x = -c * x * (1 / c)

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
c x : ℝ
hc : 0 < c
u : ℝ
hx : 0 < x
⊢ u - 1 = c * (u - 1) * (1 / c)

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
⊢ ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)

Tactic:
have fpow :
    ∀ {c x : ℝ} (_ : 0 < c) (u : ℝ) (_ : 0 < x), exp (-x) * x ^ (u - 1) = f c u x ^ (1 / c) := by
    intro c x hc u hx
    dsimp only [f]
    rw [mul_rpow (exp_pos _).le ((rpow_nonneg hx.le) _), ← exp_mul, ← rpow_mul hx.le]
    congr 2 <;> field
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
rwa : ¬ENNReal.ofReal (1 / c) = 0
rwa₁ : ¬1 / c ≤ 0
rwa₂ : 0 < 1 / c
rwa₃ rwa₄ rwa₅ rwa₆ : 0 < c
⊢ ENNReal.ofReal (1 / c) ≠ 0

Tactic:
rwa [Ne, ENNReal.ofReal_eq_zero, not_le, one_div_pos]

Premises used: not_le, ENNReal.ofReal_eq_zero, Ne, one_div_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
⊢ ENNReal.ofReal (1 / c) ≠ 0

Tactic:
have A : ENNReal.ofReal (1 / c) ≠ 0 := by
      rwa [Ne, ENNReal.ofReal_eq_zero, not_le, one_div_pos]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
⊢ ENNReal.ofReal (1 / c) ≠ ∞

Tactic:
have B : ENNReal.ofReal (1 / c) ≠ ∞ := ENNReal.ofReal_ne_top
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
B : ENNReal.ofReal (1 / c) ≠ ∞
rw :
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ ‖f c u x‖ ^ (1 / c))
    (Measure.restrict volume (Ioi 0))
rw₁ : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (f c u) (Measure.restrict volume (Ioi 0))
⊢ MemLp (m0 := MeasureSpace.toMeasurableSpace) (f c u) (ENNReal.ofReal (1 / c)) (Measure.restrict volume (Ioi 0))

Tactic:
rw [← memLp_norm_rpow_iff _ A B, ENNReal.toReal_ofReal (one_div_nonneg.mpr hc.le),
      ENNReal.div_self A B, memLp_one_iff_integrable]

Premises used: Iff.mpr, one_div_nonneg, LT.lt.le, ENNReal.toReal_ofReal, ENNReal.div_self, MeasureTheory.memLp_norm_rpow_iff, MeasureTheory.memLp_one_iff_integrable