awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
f_tends :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
h :
  ∀ (hxn : (↑n : ℝ) < x),
    Norm.norm (E := ℂ)
        (indicator (Ioc 0 (↑n : ℝ)) (fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) x) ≤
      rexp (-x) * x ^ (s.re - 1)
h₁ :
  ∀ (hxn : x ≤ (↑n : ℝ)),
    Norm.norm (E := ℂ)
        (indicator (Ioc 0 (↑n : ℝ)) (fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) x) ≤
      rexp (-x) * x ^ (s.re - 1)
⊢ Norm.norm (E := ℂ)
      (indicator (Ioc 0 (↑n : ℝ)) (fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) x) ≤
    rexp (-x) * x ^ (s.re - 1)

Tactic:
rcases lt_or_ge (n : ℝ) x with (hxn | hxn)

Premises used: Nat.cast, lt_or_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
f_tends :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
hxn : (↑n : ℝ) < x
h : 0 ≤ x ^ (s.re - 1)
⊢ Norm.norm (E := ℂ)
      (indicator (Ioc 0 (↑n : ℝ)) (fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) x) ≤
    rexp (-x) * x ^ (s.re - 1)

Tactic:
rw [indicator_of_notMem (notMem_Ioc_of_gt hxn), norm_zero,
        mul_nonneg_iff_right_nonneg_of_pos (exp_pos _)]

Premises used: norm_zero, Set.notMem_Ioc_of_gt, Set.indicator_of_notMem, mul_nonneg_iff_right_nonneg_of_pos, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
f_tends :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
hxn : (↑n : ℝ) < x
⊢ 0 ≤ x ^ (s.re - 1)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
f_tends :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
hxn : x ≤ (↑n : ℝ)
⊢ LE.le (α := ℝ) 0 (↑n : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
f_tends :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
hxn : x ≤ (↑n : ℝ)
h : (1 - x / (↑n : ℝ)) ^ n * x ^ (s.re - 1) ≤ rexp (-x) * x ^ (s.re - 1)
⊢ Norm.norm (E := ℂ)
      (indicator (Ioc 0 (↑n : ℝ)) (fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) x) ≤
    rexp (-x) * x ^ (s.re - 1)

Tactic:
rw [indicator_of_mem (mem_Ioc.mpr ⟨mem_Ioi.mp hx, hxn⟩), norm_mul, Complex.norm_of_nonneg
          (pow_nonneg (sub_nonneg.mpr <| div_le_one_of_le₀ hxn <| by positivity) _),
          norm_cpow_eq_rpow_re_of_pos hx, sub_re, one_re]

Premises used: div_le_one_of_le₀, Iff.mpr, pow_nonneg, Complex.sub_re, Set.mem_Ioi, norm_mul, Complex.norm_of_nonneg, Set.indicator_of_mem, And.intro, Iff.mp, Set.mem_Ioc, Complex.one_re, sub_nonneg, Complex.norm_cpow_eq_rpow_re_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
f_tends :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
hxn : x ≤ (↑n : ℝ)
h : (1 - x / (↑n : ℝ)) ^ n ≤ rexp (-x)
⊢ (1 - x / (↑n : ℝ)) ^ n * x ^ (s.re - 1) ≤ rexp (-x) * x ^ (s.re - 1)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
f_tends :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
hxn : x ≤ (↑n : ℝ)
⊢ (1 - x / (↑n : ℝ)) ^ n ≤ rexp (-x)

Tactic:
one_sub_div_pow_le_exp_neg hxn

Premises used: Real.one_sub_div_pow_le_exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
f_tends :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
hxn : x ≤ (↑n : ℝ)
⊢ (1 - x / (↑n : ℝ)) ^ n ≤ rexp (-x)

Tactic:
exact one_sub_div_pow_le_exp_neg hxn

Premises used: Real.one_sub_div_pow_le_exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
this : ∀ (m : ℕ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ : ∀ ⦃U : Set ℂ⦄, U ∈ 𝓝 (Gamma s) → U ∈ map s.GammaSeq atTop
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))

Tactic:
tauto
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
suffices : ∀ (m : ℕ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))

Tactic:
suffices ∀ m : ℕ, ⌊1 - s.re⌋₊ = m → Tendsto (GammaSeq s) atTop (𝓝 <| Gamma s) by tauto
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : ⌊1 - s.re⌋₊ = 0
⊢ 0 < s.re

Tactic:
rw [Nat.floor_eq_zero, sub_lt_self_iff] at hs

Premises used: sub_lt_self_iff, Nat.floor_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
zero :
  (fun (n : ℕ) ↦ ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) =ᶠ[atTop] s.GammaSeq
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))

Tactic:
apply (approx_Gamma_integral_tendsto_Gamma_integral hs).congr'

Premises used: Filter.Tendsto.congr', Complex.approx_Gamma_integral_tendsto_Gamma_integral
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
⊢ ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1) = s.GammaSeq n

Tactic:
(GammaSeq_eq_approx_Gamma_integral hs hn).symm

Premises used: Complex.GammaSeq_eq_approx_Gamma_integral, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
h :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ x ≠ 0) x} x →
          Membership.mem (γ := Set ℕ)
            {x : ℕ |
              (fun (x : ℕ) ↦
                  (fun (n : ℕ) ↦ (∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1) : ℂ))
                      x =
                    s.GammaSeq x)
                x}
            x}
      a
h₁ h₂ :
  ∀ (n : ℕ) (hn : n ≠ 0), ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1) = s.GammaSeq n
⊢ (fun (n : ℕ) ↦ ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) =ᶠ[atTop] s.GammaSeq

Tactic:
filter_upwards [eventually_ne_atTop 0] with n hn using
      (GammaSeq_eq_approx_Gamma_integral hs hn).symm

Premises used: Filter.eventually_ne_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
m : ℕ
IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
succ : ∀ (hs : ⌊1 - re 0⌋₊ = m + 1), Tendsto (GammaSeq 0) atTop (𝓝 (Gamma 0))
succ₁ : ∀ (hsne : s ≠ 0), Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))

Tactic:
rcases eq_or_ne s 0 with rfl | hsne

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
m : ℕ
IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
hs : ⌊1 - re 0⌋₊ = m + 1
⊢ Tendsto
    (fun (n : ℕ) ↦
      HPow.hPow (α := ℂ) (β := ℂ) (↑n : ℂ) 0 * (↑n ! : ℂ) / ∏ j ∈ Finset.range (n + 1), HAdd.hAdd (α := ℂ) 0 (↑j : ℂ))
    atTop (𝓝 (Gamma 0))

Tactic:
simp [Finset.prod_range_succ']

Premises used: Finset.prod_range_succ'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
m : ℕ
IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
hsne : s ≠ 0
succ : ⌊1 - (s + 1).re⌋₊ = m
succ₁ : ∀ (IH : Tendsto (s + 1).GammaSeq atTop (𝓝 (Gamma (s + 1)))), Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))

Tactic:
specialize IH (s + 1) ?_

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
m : ℕ
IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
hsne : s ≠ 0
⊢ m + 1 ≠ 0

Tactic:
lia
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
m : ℕ
IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
hsne : s ≠ 0
⊢ (↑(m + 1) : ℝ) ≤ 1 - s.re ∧ 1 - s.re < HAdd.hAdd (α := ℝ) (↑(m + 1) : ℝ) 1

Tactic:
rw [Nat.floor_eq_iff' (by lia)] at hs

Premises used: Nat.floor_eq_iff'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
m : ℕ
IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
hsne : s ≠ 0
hs₁ : (↑(m + 1) : ℝ) ≤ 1 - s.re ∧ 1 - s.re < HAdd.hAdd (α := ℝ) (↑(m + 1) : ℝ) 1
⊢ s ≠ 0

Tactic:
rw [Nat.floor_eq_iff' (by lia)] at hs

Premises used: Nat.floor_eq_iff'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
m : ℕ
IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
s : ℂ
hs : (↑(m + 1) : ℝ) ≤ 1 - s.re ∧ 1 - s.re < HAdd.hAdd (α := ℝ) (↑(m + 1) : ℝ) 1
hsne : s ≠ 0
⊢ s.re ≤ -(↑m : ℝ)

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
m : ℕ
IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
s : ℂ
hs : (↑(m + 1) : ℝ) ≤ 1 - s.re ∧ 1 - s.re < HAdd.hAdd (α := ℝ) (↑(m + 1) : ℝ) 1
hsne : s ≠ 0
⊢ s.re ≤ -(↑m : ℝ)

Tactic:
have : s.re ≤ -m := by grind
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
m : ℕ
IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
s : ℂ
hs : (↑(m + 1) : ℝ) ≤ 1 - s.re ∧ 1 - s.re < HAdd.hAdd (α := ℝ) (↑(m + 1) : ℝ) 1
hsne : s ≠ 0
this : s.re ≤ -(↑m : ℝ)
⊢ s.re ≤ 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
m : ℕ
IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
s : ℂ
hs : (↑(m + 1) : ℝ) ≤ 1 - s.re ∧ 1 - s.re < HAdd.hAdd (α := ℝ) (↑(m + 1) : ℝ) 1
hsne : s ≠ 0
this : s.re ≤ -(↑m : ℝ)
⊢ 0 ≤ 1 - (s + 1).re

Tactic:
simpa using (show s.re ≤ 0 by grind)
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
m : ℕ
IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
s : ℂ
hs : (↑(m + 1) : ℝ) ≤ 1 - s.re ∧ 1 - s.re < HAdd.hAdd (α := ℝ) (↑(m + 1) : ℝ) 1
hsne : s ≠ 0
this : s.re ≤ -(↑m : ℝ)
succ : (↑m : ℝ) ≤ 1 - (s + 1).re ∧ 1 - (s + 1).re < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
⊢ ⌊1 - (s + 1).re⌋₊ = m

Tactic:
rw [Nat.floor_eq_iff <| by simpa using (show s.re ≤ 0 by grind)]

Premises used: Nat.floor_eq_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
m : ℕ
IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
s : ℂ
hs : (↑(m + 1) : ℝ) ≤ 1 - s.re ∧ 1 - s.re < HAdd.hAdd (α := ℝ) (↑(m + 1) : ℝ) 1
hsne : s ≠ 0
this : s.re ≤ -(↑m : ℝ)
⊢ (↑m : ℝ) ≤ 1 - (s + 1).re ∧ 1 - (s + 1).re < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1

Tactic:
grind [add_re, one_re]

Premises used: Complex.add_re, Complex.one_re
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
m : ℕ
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
hsne : s ≠ 0
IH : Tendsto (s + 1).GammaSeq atTop (𝓝 (Gamma (s + 1)))
⊢ Tendsto (s + 1).GammaSeq atTop (𝓝 (s * Gamma s))

Tactic:
rw [Gamma_add_one _ hsne] at IH

Premises used: Complex.Gamma_add_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
m : ℕ
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
hsne : s ≠ 0
IH : Tendsto (s + 1).GammaSeq atTop (𝓝 (s * Gamma s))
n : ℕ
⊢ n ≠ 0 → (s + 1).GammaSeq n / s = (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s) * s.GammaSeq n

Tactic:
GammaSeq_add_one_left s

Premises used: Complex.GammaSeq_add_one_left
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
m : ℕ
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
hsne : s ≠ 0
IH : Tendsto (s + 1).GammaSeq atTop (𝓝 (s * Gamma s))
h :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ x ≠ 0) x} x →
          Membership.mem (γ := Set ℕ)
            {x : ℕ |
              (fun (x : ℕ) ↦
                  (fun (a : ℕ) ↦ (s + 1).GammaSeq a / s) x =
                    (↑x : ℂ) / (HAdd.hAdd (α := ℂ) (↑x : ℂ) 1 + s) * s.GammaSeq x)
                x}
            x}
      a
h₁ h₂ : ∀ (n : ℕ), n ≠ 0 → (s + 1).GammaSeq n / s = (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s) * s.GammaSeq n
⊢ EventuallyEq (β := ℂ) atTop (fun (a : ℕ) ↦ (s + 1).GammaSeq a / s) fun (n : ℕ) ↦
    (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s) * s.GammaSeq n

Tactic:
filter_upwards [eventually_ne_atTop 0] with n using GammaSeq_add_one_left s

Premises used: Filter.eventually_ne_atTop, Complex.GammaSeq_add_one_left, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
m : ℕ
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
hsne : s ≠ 0
IH : Tendsto (s + 1).GammaSeq atTop (𝓝 (s * Gamma s))
⊢ Tendsto (fun (n : ℕ) ↦ (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s) * s.GammaSeq n) atTop (𝓝 (s * Gamma s / s))

Tactic:
have := (IH.div_const s).congr' <| by
      filter_upwards [eventually_ne_atTop 0] with n using GammaSeq_add_one_left s
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
m : ℕ
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
hsne : s ≠ 0
IH : Tendsto (s + 1).GammaSeq atTop (𝓝 (s * Gamma s))
this : Tendsto (fun (n : ℕ) ↦ (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s) * s.GammaSeq n) atTop (𝓝 (s * Gamma s / s))
⊢ Tendsto (fun (n : ℕ) ↦ s.GammaSeq n * ((↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s))) atTop (𝓝 (s * Gamma s / s))

Tactic:
simp only [mul_comm _ (s.GammaSeq _)] at this

Premises used: mul_comm, Complex.GammaSeq
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
m : ℕ
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
hsne : s ≠ 0
IH : Tendsto (s + 1).GammaSeq atTop (𝓝 (s * Gamma s))
this :
  Tendsto (fun (n : ℕ) ↦ s.GammaSeq n * ((↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s))) atTop (𝓝 (s * Gamma s / s))
rwa :
  ∀
    (this :
      Tendsto (fun (n : ℕ) ↦ s.GammaSeq n * ((↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s))) atTop (𝓝 (Gamma s * 1))),
    Tendsto (β := ℂ) (fun (n : ℕ) ↦ (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s)) atTop (𝓝 1)
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))

Tactic:
rwa [mul_div_cancel_left₀ _ hsne, ← mul_one (Gamma s),
      tendsto_mul_iff_of_ne_zero _ (one_ne_zero' ℂ)] at this

Premises used: Filter.tendsto_mul_iff_of_ne_zero, one_ne_zero', mul_div_cancel_left₀, Complex.Gamma, mul_one, Complex
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
m : ℕ
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
hsne : s ≠ 0
IH : Tendsto (s + 1).GammaSeq atTop (𝓝 (s * Gamma s))
this : Tendsto (fun (n : ℕ) ↦ s.GammaSeq n * ((↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s))) atTop (𝓝 (Gamma s * 1))
simp_rw : Tendsto (β := ℂ) (fun (n : ℕ) ↦ (↑n : ℂ) / ((↑n : ℂ) + (1 + s))) atTop (𝓝 1)
⊢ Tendsto (β := ℂ) (fun (n : ℕ) ↦ (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s)) atTop (𝓝 1)

Tactic:
simp_rw [add_assoc]

Premises used: add_assoc
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
m : ℕ
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
hsne : s ≠ 0
IH : Tendsto (s + 1).GammaSeq atTop (𝓝 (s * Gamma s))
this : Tendsto (fun (n : ℕ) ↦ s.GammaSeq n * ((↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s))) atTop (𝓝 (Gamma s * 1))
⊢ Tendsto (β := ℂ) (fun (n : ℕ) ↦ (↑n : ℂ) / ((↑n : ℂ) + (1 + s))) atTop (𝓝 1)

Tactic:
tendsto_natCast_div_add_atTop (1 + s)

Premises used: tendsto_natCast_div_add_atTop, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
m : ℕ
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
hsne : s ≠ 0
IH : Tendsto (s + 1).GammaSeq atTop (𝓝 (s * Gamma s))
this : Tendsto (fun (n : ℕ) ↦ s.GammaSeq n * ((↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s))) atTop (𝓝 (Gamma s * 1))
⊢ Tendsto (β := ℂ) (fun (n : ℕ) ↦ (↑n : ℂ) / ((↑n : ℂ) + (1 + s))) atTop (𝓝 1)

Tactic:
exact tendsto_natCast_div_add_atTop (1 + s)

Premises used: tendsto_natCast_div_add_atTop, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
m : ℕ
zero zero₁ : ∀ (s : ℂ) (hs : ⌊1 - s.re⌋₊ = 0), Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
succ succ₁ :
  ∀ (m : ℕ) (IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))) (s : ℂ)
    (hs : ⌊1 - s.re⌋₊ = m + 1), Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
⊢ ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))

Tactic:
induction m generalizing s with intro hs
  | zero => -- Base case: `0 < re s`, so Gamma is given by the integral formula
    rw [Nat.floor_eq_zero, sub_lt_self_iff] at hs
    apply (approx_Gamma_integral_tendsto_Gamma_integral hs).congr'
    filter_upwards [eventually_ne_atTop 0] with n hn using
      (GammaSeq_eq_approx_Gamma_integral hs hn).symm
  | succ m IH => -- Induction step: use recurrence formulae in `s` for Gamma and GammaSeq
    -- Silly case `s = 0`: both sides are zero
    rcases eq_or_ne s 0 with rfl | hsne
    · unfold GammaSeq
      simp [Finset.prod_range_succ']
    specialize IH (s + 1) ?_
    · rw [Nat.floor_eq_iff' (by lia)] at hs
      have : s.re ≤ -m := by grind
      rw [Nat.floor_eq_iff <| by simpa using (show s.re ≤ 0 by grind)]
      grind [add_re, one_re]
    rw [Gamma_add_one _ hsne] at IH
    have := (IH.div_const s).congr' <| by
      filter_upwards [eventually_ne_atTop 0] with n using GammaSeq_add_one_left s
    simp only [mul_comm _ (s.GammaSeq _)] at this
    rwa [mul_div_cancel_left₀ _ hsne, ← mul_one (Gamma s),
      tendsto_mul_iff_of_ne_zero _ (one_ne_zero' ℂ)] at this
    simp_rw [add_assoc]
    exact tendsto_natCast_div_add_atTop (1 + s)

Premises used: Finset.prod_range_succ', Nat.floor_eq_iff, Filter.tendsto_mul_iff_of_ne_zero, one_ne_zero', add_assoc, Complex.add_re, tendsto_natCast_div_add_atTop, Complex.Gamma, Filter.eventually_ne_atTop, HAdd.hAdd, mul_comm, sub_lt_self_iff, eq_or_ne, Nat.floor_eq_zero, Complex.GammaSeq, mul_one, Complex, Nat.floor_eq_iff', OfNat.ofNat, Complex.one_re, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
n : ℕ
hn : n ≠ 0
a b c d : ℂ
⊢ a * b * (c * d) = a * c * (b * d)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
n : ℕ
hn : n ≠ 0
⊢ ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)

Tactic:
have aux : ∀ a b c d : ℂ, a * b * (c * d) = a * c * (b * d) := by intros; ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
rw :
  HPow.hPow (α := ℂ) (↑n : ℂ) z * HPow.hPow (α := ℂ) (↑n : ℂ) (1 - z) * HPow.hPow (α := ℂ) (β := ℕ) (↑n ! : ℂ) 2 /
      HMul.hMul (α := ℂ) (∏ j ∈ Finset.range (n + 1), (z + (↑j : ℂ))) (∏ j ∈ Finset.range (n + 1), (1 - z + (↑j : ℂ))) =
    (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z) *
      (1 /
        (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)))
⊢ z.GammaSeq n * (1 - z).GammaSeq n =
    (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z) *
      (1 /
        (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)))

Tactic:
rw [GammaSeq, GammaSeq, div_mul_div_comm, aux, ← pow_two]

Premises used: pow_two, div_mul_div_comm, Complex.GammaSeq
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
rw : HPow.hPow (α := ℂ) (↑n : ℂ) (z + (1 - z)) = (↑n : ℂ)
rw₁ : HPow.hPow (α := ℂ) (β := ℂ) (↑n : ℂ) 1 = (↑n : ℂ)
rw₂ rw₃ : Eq (α := ℂ) (↑n : ℂ) (↑n : ℂ)
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) z * HPow.hPow (α := ℂ) (↑n : ℂ) (1 - z) = (↑n : ℂ)

Tactic:
rw [← cpow_add _ _ (Nat.cast_ne_zero.mpr hn), add_sub_cancel, cpow_one]

Premises used: Iff.mpr, Complex.cpow_one, add_sub_cancel, Complex.cpow_add, Nat.cast_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) z * HPow.hPow (α := ℂ) (↑n : ℂ) (1 - z) = (↑n : ℂ)

Tactic:
have : (n : ℂ) ^ z * (n : ℂ) ^ (1 - z) = n := by
    rw [← cpow_add _ _ (Nat.cast_ne_zero.mpr hn), add_sub_cancel, cpow_one]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this : HPow.hPow (α := ℂ) (↑n : ℂ) z * HPow.hPow (α := ℂ) (↑n : ℂ) (1 - z) = (↑n : ℂ)
rw :
  (↑n : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n ! : ℂ) 2 /
      ((∏ x ∈ Finset.range n, (z + (↑(x + 1) : ℂ)) * (1 - z + (↑x : ℂ))) * (z * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z))) =
    (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z) *
      (1 /
        (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)))
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) z * HPow.hPow (α := ℂ) (↑n : ℂ) (1 - z) * HPow.hPow (α := ℂ) (β := ℕ) (↑n ! : ℂ) 2 /
      HMul.hMul (α := ℂ) (∏ j ∈ Finset.range (n + 1), (z + (↑j : ℂ))) (∏ j ∈ Finset.range (n + 1), (1 - z + (↑j : ℂ))) =
    (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z) *
      (1 /
        (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)))

Tactic:
rw [this, Finset.prod_range_succ', Finset.prod_range_succ, aux, ← Finset.prod_mul_distrib,
    Nat.cast_zero, add_zero, add_comm (1 - z) n, ← add_sub_assoc]

Premises used: add_sub_assoc, Finset.prod_range_succ', Finset.prod_mul_distrib, HSub.hSub, Nat.cast, add_comm, Finset.prod_range_succ, Nat.cast_zero, add_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this : HPow.hPow (α := ℂ) (↑n : ℂ) z * HPow.hPow (α := ℂ) (↑n : ℂ) (1 - z) = (↑n : ℂ)
j : ℕ
push_cast :
  (z + HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) * (1 - z + (↑j : ℂ)) =
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2 *
      (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
⊢ (z + (↑(j + 1) : ℂ)) * (1 - z + (↑j : ℂ)) =
    (↑(HPow.hPow (β := ℕ) (j + 1) 2) : ℂ) *
      (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)

Tactic:
push_cast