awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : (↑m : ℝ) < x - 1
hy' : x - 1 ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
this :
  ∀ᶠ (n : ℕ) in atTop,
    logGammaSeq (x - 1) n =
      logGammaSeq x (n - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) - log (x - 1)
hm :
  Tendsto (α := ℕ)
    ((fun (x_1 : ℕ) ↦
        logGammaSeq x (x_1 - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(x_1 - 1) : ℝ) 1) - log (↑(x_1 - 1) : ℝ)) -
            log (x - 1) +
          log (x - 1)) ∘
      fun (a : ℕ) ↦ a + 1)
    atTop (𝓝 (f (x - 1) - f 1 + log (x - 1)))
n : ℕ
⊢ logGammaSeq x (n + 1 - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n + 1 - 1) : ℝ) 1) - log (↑(n + 1 - 1) : ℝ)) -
        log (x - 1) +
      log (x - 1) =
    logGammaSeq x n + x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
have h : logGammaSeq x (n + 1 - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n + 1 - 1) : ℝ) 1) - log (↑(n + 1 - 1) : ℝ)) =
  logGammaSeq x n + x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
Tactic: rw [sub_add_cancel, Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : (↑m : ℝ) < x - 1
hy' : x - 1 ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
this :
  ∀ᶠ (n : ℕ) in atTop,
    logGammaSeq (x - 1) n =
      logGammaSeq x (n - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) - log (x - 1)
hm :
  Tendsto (α := ℕ)
    ((fun (x_1 : ℕ) ↦
        logGammaSeq x (x_1 - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(x_1 - 1) : ℝ) 1) - log (↑(x_1 - 1) : ℝ)) -
            log (x - 1) +
          log (x - 1)) ∘
      fun (a : ℕ) ↦ a + 1)
    atTop (𝓝 (f (x - 1) - f 1 + log (x - 1)))
n : ℕ
h :
  logGammaSeq x (n + 1 - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n + 1 - 1) : ℝ) 1) - log (↑(n + 1 - 1) : ℝ)) =
    logGammaSeq x n + x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
⊢ logGammaSeq x (n + 1 - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n + 1 - 1) : ℝ) 1) - log (↑(n + 1 - 1) : ℝ)) -
        log (x - 1) +
      log (x - 1) =
    logGammaSeq x n + x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
have h₁ : logGammaSeq x n + x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ)) =
  logGammaSeq x n + x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
Tactic: rw [sub_add_cancel, Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : (↑m : ℝ) < x - 1
hy' : x - 1 ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
this :
  ∀ᶠ (n : ℕ) in atTop,
    logGammaSeq (x - 1) n =
      logGammaSeq x (n - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) - log (x - 1)
hm :
  Tendsto (α := ℕ)
    ((fun (x_1 : ℕ) ↦
        logGammaSeq x (x_1 - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(x_1 - 1) : ℝ) 1) - log (↑(x_1 - 1) : ℝ)) -
            log (x - 1) +
          log (x - 1)) ∘
      fun (a : ℕ) ↦ a + 1)
    atTop (𝓝 (f (x - 1) - f 1 + log (x - 1)))
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
have this₁ : Eq (α := ℕ → ℝ)
  ((fun (x_1 : ℕ) ↦
      HAdd.hAdd (α := ℝ)
        ((fun (n : ℕ) ↦
            logGammaSeq x (n - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) - log (x - 1))
          x_1)
        ((fun (b : ℕ) ↦ log (x - 1)) x_1)) ∘
    fun (a : ℕ) ↦ a + 1)
  fun (n : ℕ) ↦ logGammaSeq x n + x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
Tactic: have :
      ((fun x_1 : ℕ =>
            (fun n : ℕ =>
                  logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1))
                x_1 +
              (fun b : ℕ => log (x - 1)) x_1) ∘
          fun a : ℕ => a + 1) =
        fun n => logGammaSeq x n + x * (log (↑n + 1) - log ↑n) := by
      ext1 n
      dsimp only [Function.comp_apply]
      rw [sub_add_cancel, Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : (↑m : ℝ) < x - 1
hy' : x - 1 ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
this_1 :
  ∀ᶠ (n : ℕ) in atTop,
    logGammaSeq (x - 1) n =
      logGammaSeq x (n - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) - log (x - 1)
hm :
  Tendsto (α := ℕ)
    ((fun (x_1 : ℕ) ↦
        logGammaSeq x (x_1 - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(x_1 - 1) : ℝ) 1) - log (↑(x_1 - 1) : ℝ)) -
            log (x - 1) +
          log (x - 1)) ∘
      fun (a : ℕ) ↦ a + 1)
    atTop (𝓝 (f (x - 1) - f 1 + log (x - 1)))
this :
  Eq (α := ℕ → ℝ)
    ((fun (x_1 : ℕ) ↦
        HAdd.hAdd (α := ℝ)
          ((fun (n : ℕ) ↦
              logGammaSeq x (n - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) -
                log (x - 1))
            x_1)
          ((fun (b : ℕ) ↦ log (x - 1)) x_1)) ∘
      fun (a : ℕ) ↦ a + 1)
    fun (n : ℕ) ↦ logGammaSeq x n + x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
have hm₁ : Tendsto (fun (n : ℕ) ↦ logGammaSeq x n + x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))) atTop
  (𝓝 (f (x - 1) - f 1 + log (x - 1)))
Tactic: rw [this] at hm
Cleared hypotheses: hm, this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : (↑m : ℝ) < x - 1
hy' : x - 1 ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
this_1 :
  ∀ᶠ (n : ℕ) in atTop,
    logGammaSeq (x - 1) n =
      logGammaSeq x (n - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) - log (x - 1)
hm :
  Tendsto (fun (n : ℕ) ↦ logGammaSeq x n + x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))) atTop
    (𝓝 (f (x - 1) - f 1 + log (x - 1)))
this :
  Eq (α := ℕ → ℝ)
    ((fun (x_1 : ℕ) ↦
        HAdd.hAdd (α := ℝ)
          ((fun (n : ℕ) ↦
              logGammaSeq x (n - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) -
                log (x - 1))
            x_1)
          ((fun (b : ℕ) ↦ log (x - 1)) x_1)) ∘
      fun (a : ℕ) ↦ a + 1)
    fun (n : ℕ) ↦ logGammaSeq x n + x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
have h : ∀ (x_1 : ℕ),
  logGammaSeq x x_1 =
    logGammaSeq x x_1 + x * (log (HAdd.hAdd (α := ℝ) (↑x_1 : ℝ) 1) - log (↑x_1 : ℝ)) -
      x * (log (HAdd.hAdd (α := ℝ) (↑x_1 : ℝ) 1) - log (↑x_1 : ℝ))
Tactic: convert! hm.sub (tendsto_log_nat_add_one_sub_log.const_mul x) using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : (↑m : ℝ) < x - 1
hy' : x - 1 ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
this_1 :
  ∀ᶠ (n : ℕ) in atTop,
    logGammaSeq (x - 1) n =
      logGammaSeq x (n - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) - log (x - 1)
hm :
  Tendsto (fun (n : ℕ) ↦ logGammaSeq x n + x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))) atTop
    (𝓝 (f (x - 1) - f 1 + log (x - 1)))
this :
  Eq (α := ℕ → ℝ)
    ((fun (x_1 : ℕ) ↦
        HAdd.hAdd (α := ℝ)
          ((fun (n : ℕ) ↦
              logGammaSeq x (n - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) -
                log (x - 1))
            x_1)
          ((fun (b : ℕ) ↦ log (x - 1)) x_1)) ∘
      fun (a : ℕ) ↦ a + 1)
    fun (n : ℕ) ↦ logGammaSeq x n + x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
h :
  ∀ (x_1 : ℕ),
    logGammaSeq x x_1 =
      logGammaSeq x x_1 + x * (log (HAdd.hAdd (α := ℝ) (↑x_1 : ℝ) 1) - log (↑x_1 : ℝ)) -
        x * (log (HAdd.hAdd (α := ℝ) (↑x_1 : ℝ) 1) - log (↑x_1 : ℝ))
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
have h₁ : f x - f 1 = f (x - 1) - f 1 + log (x - 1) - x * 0
Tactic: convert! hm.sub (tendsto_log_nat_add_one_sub_log.const_mul x) using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : (↑m : ℝ) < x - 1
hy' : x - 1 ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
this_1 :
  ∀ᶠ (n : ℕ) in atTop,
    logGammaSeq (x - 1) n =
      logGammaSeq x (n - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) - log (x - 1)
hm :
  Tendsto (fun (n : ℕ) ↦ logGammaSeq x n + x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))) atTop
    (𝓝 (f (x - 1) - f 1 + log (x - 1)))
this :
  Eq (α := ℕ → ℝ)
    ((fun (x_1 : ℕ) ↦
        HAdd.hAdd (α := ℝ)
          ((fun (n : ℕ) ↦
              logGammaSeq x (n - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) -
                log (x - 1))
            x_1)
          ((fun (b : ℕ) ↦ log (x - 1)) x_1)) ∘
      fun (a : ℕ) ↦ a + 1)
    fun (n : ℕ) ↦ logGammaSeq x n + x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
⊢ f x - f 1 = f (x - 1) - f 1 + log (x - 1) - x * 0
have this₁ : f (x - 1 + 1) = f (x - 1) + log (x - 1)
Tactic: have := hf_feq ((Nat.cast_nonneg m).trans_lt hy)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : (↑m : ℝ) < x - 1
hy' : x - 1 ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
this_1 :
  ∀ᶠ (n : ℕ) in atTop,
    logGammaSeq (x - 1) n =
      logGammaSeq x (n - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) - log (x - 1)
hm :
  Tendsto (fun (n : ℕ) ↦ logGammaSeq x n + x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))) atTop
    (𝓝 (f (x - 1) - f 1 + log (x - 1)))
this_2 :
  Eq (α := ℕ → ℝ)
    ((fun (x_1 : ℕ) ↦
        HAdd.hAdd (α := ℝ)
          ((fun (n : ℕ) ↦
              logGammaSeq x (n - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) -
                log (x - 1))
            x_1)
          ((fun (b : ℕ) ↦ log (x - 1)) x_1)) ∘
      fun (a : ℕ) ↦ a + 1)
    fun (n : ℕ) ↦ logGammaSeq x n + x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
this : f (x - 1 + 1) = f (x - 1) + log (x - 1)
⊢ f x - f 1 = f (x - 1) - f 1 + log (x - 1) - x * 0
have this₁ : f x = f (x - 1) + log (x - 1)
Tactic: rw [sub_add_cancel] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : (↑m : ℝ) < x - 1
hy' : x - 1 ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
this_1 :
  ∀ᶠ (n : ℕ) in atTop,
    logGammaSeq (x - 1) n =
      logGammaSeq x (n - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) - log (x - 1)
hm :
  Tendsto (fun (n : ℕ) ↦ logGammaSeq x n + x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))) atTop
    (𝓝 (f (x - 1) - f 1 + log (x - 1)))
this_2 :
  Eq (α := ℕ → ℝ)
    ((fun (x_1 : ℕ) ↦
        HAdd.hAdd (α := ℝ)
          ((fun (n : ℕ) ↦
              logGammaSeq x (n - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) -
                log (x - 1))
            x_1)
          ((fun (b : ℕ) ↦ log (x - 1)) x_1)) ∘
      fun (a : ℕ) ↦ a + 1)
    fun (n : ℕ) ↦ logGammaSeq x n + x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
this : f x = f (x - 1) + log (x - 1)
⊢ f x - f 1 = f (x - 1) - f 1 + log (x - 1) - x * 0
have h : f (x - 1) + log (x - 1) - f 1 = f (x - 1) - f 1 + log (x - 1) - x * 0
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
m : ℕ
⊢ (↑m : ℝ) < x → x ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
have zero : ∀ {x : ℝ} (hx : 0 < x), (↑0 : ℝ) < x → x ≤ HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
Tactic: induction m generalizing x with
  | zero =>
    rw [Nat.cast_zero, zero_add]
    exact fun _ hx' => tendsto_logGammaSeq_of_le_one hf_conv (@hf_feq) hx hx'
  | succ m hm =>
    intro hy hy'
    rw [Nat.cast_succ, ← sub_le_iff_le_add] at hy'
    rw [Nat.cast_succ, ← lt_sub_iff_add_lt] at hy
    specialize hm ((Nat.cast_nonneg _).trans_lt hy) hy hy'
    -- now massage gauss_product n (x - 1) into gauss_product (n - 1) x
    have :
      ∀ᶠ n : ℕ in atTop,
        logGammaSeq (x - 1) n =
          logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1) := by
      refine Eventually.mp (eventually_ge_atTop 1) (Eventually.of_forall fun n hn => ?_)
      have := logGammaSeq_add_one (x - 1) (n - 1)
      rw [sub_add_cancel, Nat.sub_add_cancel hn] at this
      rw [this]
      ring
    replace hm :=
      ((Tendsto.congr' this hm).add (tendsto_const_nhds : Tendsto (fun _ => log (x - 1)) _ _)).comp
        (tendsto_add_atTop_nat 1)
    have :
      ((fun x_1 : ℕ =>
            (fun n : ℕ =>
                  logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1))
                x_1 +
              (fun b : ℕ => log (x - 1)) x_1) ∘
          fun a : ℕ => a + 1) =
        fun n => logGammaSeq x n + x * (log (↑n + 1) - log ↑n) := by
      ext1 n
      dsimp only [Function.comp_apply]
      rw [sub_add_cancel, Nat.add_sub_cancel]
    rw [this] at hm
    convert! hm.sub (tendsto_log_nat_add_one_sub_log.const_mul x) using 2
    · ring
    · have := hf_feq ((Nat.cast_nonneg m).trans_lt hy)
      rw [sub_add_cancel] at this
      rw [this]
      ring
Cleared hypotheses: x, hx, m
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
m : ℕ
zero :
  ∀ {x : ℝ} (hx : 0 < x),
    (↑0 : ℝ) < x → x ≤ HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
⊢ (↑m : ℝ) < x → x ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
have succ : ∀ (m : ℕ)
  (hm :
    ∀ {x : ℝ} (hx : 0 < x),
      (↑m : ℝ) < x → x ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1)))
  {x : ℝ} (hx : 0 < x),
  (↑(m + 1) : ℝ) < x → x ≤ HAdd.hAdd (α := ℝ) (↑(m + 1) : ℝ) 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
Tactic: induction m generalizing x with
  | zero =>
    rw [Nat.cast_zero, zero_add]
    exact fun _ hx' => tendsto_logGammaSeq_of_le_one hf_conv (@hf_feq) hx hx'
  | succ m hm =>
    intro hy hy'
    rw [Nat.cast_succ, ← sub_le_iff_le_add] at hy'
    rw [Nat.cast_succ, ← lt_sub_iff_add_lt] at hy
    specialize hm ((Nat.cast_nonneg _).trans_lt hy) hy hy'
    -- now massage gauss_product n (x - 1) into gauss_product (n - 1) x
    have :
      ∀ᶠ n : ℕ in atTop,
        logGammaSeq (x - 1) n =
          logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1) := by
      refine Eventually.mp (eventually_ge_atTop 1) (Eventually.of_forall fun n hn => ?_)
      have := logGammaSeq_add_one (x - 1) (n - 1)
      rw [sub_add_cancel, Nat.sub_add_cancel hn] at this
      rw [this]
      ring
    replace hm :=
      ((Tendsto.congr' this hm).add (tendsto_const_nhds : Tendsto (fun _ => log (x - 1)) _ _)).comp
        (tendsto_add_atTop_nat 1)
    have :
      ((fun x_1 : ℕ =>
            (fun n : ℕ =>
                  logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1))
                x_1 +
              (fun b : ℕ => log (x - 1)) x_1) ∘
          fun a : ℕ => a + 1) =
        fun n => logGammaSeq x n + x * (log (↑n + 1) - log ↑n) := by
      ext1 n
      dsimp only [Function.comp_apply]
      rw [sub_add_cancel, Nat.add_sub_cancel]
    rw [this] at hm
    convert! hm.sub (tendsto_log_nat_add_one_sub_log.const_mul x) using 2
    · ring
    · have := hf_feq ((Nat.cast_nonneg m).trans_lt hy)
      rw [sub_add_cancel] at this
      rw [this]
      ring
Cleared hypotheses: x, hx, m
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
hx : 0 < x
⊢ log (Γ x) = (log ∘ Γ) x - (log ∘ Γ) 1
have simp_rw : log (Γ x) = log (Γ x) - log (Γ 1)
Tactic: simp_rw [Function.comp_apply, Gamma_one, log_one, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
hx : 0 < x
simp_rw : log (Γ x) = log (Γ x) - log (Γ 1)
⊢ log (Γ x) = (log ∘ Γ) x - (log ∘ Γ) 1
have simp_rw₁ : log (Γ x) = log (Γ x) - log 1
Tactic: simp_rw [Function.comp_apply, Gamma_one, log_one, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
hx : 0 < x
simp_rw : log (Γ x) = log (Γ x) - log (Γ 1)
simp_rw₁ : log (Γ x) = log (Γ x) - log 1
⊢ log (Γ x) = (log ∘ Γ) x - (log ∘ Γ) 1
have simp_rw₂ : log (Γ x) = log (Γ x) - 0
Tactic: simp_rw [Function.comp_apply, Gamma_one, log_one, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
x : ℝ
hx : 0 < x
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (log (Γ x)))
have this : log (Γ x) = (log ∘ Γ) x - (log ∘ Γ) 1
Tactic: have : log (Gamma x) = (log ∘ Gamma) x - (log ∘ Gamma) 1 := by
    simp_rw [Function.comp_apply, Gamma_one, log_one, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
hx : 0 < x
this : log (Γ x) = (log ∘ Γ) x - (log ∘ Γ) 1
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (log (Γ x)))
have rw : Tendsto (logGammaSeq x) atTop (𝓝 ((log ∘ Γ) x - (log ∘ Γ) 1))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
hx : 0 < x
this : log (Γ x) = (log ∘ Γ) x - (log ∘ Γ) 1
⊢ Tendsto (logGammaSeq x) atTop (𝓝 ((log ∘ Γ) x - (log ∘ Γ) 1))
have refine : ∀ {y : ℝ} (hy : 0 < y), (log ∘ Γ) (y + 1) = (log ∘ Γ) y + log y
Tactic: refine BohrMollerup.tendsto_logGammaSeq convexOn_log_Gamma (fun {y} hy => ?_) hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
hx : 0 < x
this : log (Γ x) = (log ∘ Γ) x - (log ∘ Γ) 1
y : ℝ
hy : 0 < y
⊢ (log ∘ Γ) (y + 1) = (log ∘ Γ) y + log y
have rw : log (Γ (y + 1)) = (log ∘ Γ) y + log y
Tactic: rw [Function.comp_apply, Gamma_add_one hy.ne', log_mul hy.ne' (Gamma_pos_of_pos hy).ne', add_comm,
    Function.comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
hx : 0 < x
this : log (Γ x) = (log ∘ Γ) x - (log ∘ Γ) 1
y : ℝ
hy : 0 < y
rw : log (Γ (y + 1)) = (log ∘ Γ) y + log y
⊢ (log ∘ Γ) (y + 1) = (log ∘ Γ) y + log y
have rw₁ : log (y * Γ y) = (log ∘ Γ) y + log y
Tactic: rw [Function.comp_apply, Gamma_add_one hy.ne', log_mul hy.ne' (Gamma_pos_of_pos hy).ne', add_comm,
    Function.comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
hx : 0 < x
this : log (Γ x) = (log ∘ Γ) x - (log ∘ Γ) 1
y : ℝ
hy : 0 < y
rw : log (Γ (y + 1)) = (log ∘ Γ) y + log y
rw₁ : log (y * Γ y) = (log ∘ Γ) y + log y
⊢ (log ∘ Γ) (y + 1) = (log ∘ Γ) y + log y
have rw₂ : log y + log (Γ y) = (log ∘ Γ) y + log y
Tactic: rw [Function.comp_apply, Gamma_add_one hy.ne', log_mul hy.ne' (Gamma_pos_of_pos hy).ne', add_comm,
    Function.comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
hx : 0 < x
this : log (Γ x) = (log ∘ Γ) x - (log ∘ Γ) 1
y : ℝ
hy : 0 < y
rw : log (Γ (y + 1)) = (log ∘ Γ) y + log y
rw₁ : log (y * Γ y) = (log ∘ Γ) y + log y
rw₂ : log y + log (Γ y) = (log ∘ Γ) y + log y
⊢ (log ∘ Γ) (y + 1) = (log ∘ Γ) y + log y
have rw₃ : log (Γ y) + log y = (log ∘ Γ) y + log y
Tactic: rw [Function.comp_apply, Gamma_add_one hy.ne', log_mul hy.ne' (Gamma_pos_of_pos hy).ne', add_comm,
    Function.comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
hx : 0 < x
this : log (Γ x) = (log ∘ Γ) x - (log ∘ Γ) 1
y : ℝ
hy : 0 < y
rw : log (Γ (y + 1)) = (log ∘ Γ) y + log y
rw₁ : log (y * Γ y) = (log ∘ Γ) y + log y
rw₂ : log y + log (Γ y) = (log ∘ Γ) y + log y
rw₃ : log (Γ y) + log y = (log ∘ Γ) y + log y
⊢ (log ∘ Γ) (y + 1) = (log ∘ Γ) y + log y
have rw₄ : log (Γ y) + log y = log (Γ y) + log y
Tactic: rw [Function.comp_apply, Gamma_add_one hy.ne', log_mul hy.ne' (Gamma_pos_of_pos hy).ne', add_comm,
    Function.comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y
hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y
hf_one : f 1 = 1
⊢ EqOn f Γ (Ioi 0)
have suffices : EqOn (log ∘ f) (log ∘ Γ) (Ioi 0)
Tactic: suffices EqOn (log ∘ f) (log ∘ Gamma) (Ioi (0 : ℝ)) from
    fun x hx ↦ log_injOn_pos (hf_pos hx) (Gamma_pos_of_pos hx) (this hx)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y
hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y
hf_one : f 1 = 1
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ (log ∘ f) x = (log ∘ Γ) x
have refine_2 : ∀ (e1 : Tendsto (BohrMollerup.logGammaSeq x) atTop (𝓝 ((log ∘ f) x - (log ∘ f) 1))), (log ∘ f) x = (log ∘ Γ) x
Tactic: have e1 := BohrMollerup.tendsto_logGammaSeq hf_conv ?_ hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y
hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y
hf_one : f 1 = 1
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
refine_2 :
  ∀ (e1 : Tendsto (BohrMollerup.logGammaSeq x) atTop (𝓝 ((log ∘ f) x - (log ∘ f) 1))), (log ∘ f) x = (log ∘ Γ) x
⊢ (log ∘ f) x = (log ∘ Γ) x
have refine_1 : ∀ {y : ℝ}, 0 < y → (log ∘ f) (y + 1) = (log ∘ f) y + log y
Tactic: have e1 := BohrMollerup.tendsto_logGammaSeq hf_conv ?_ hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y
hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y
hf_one : f 1 = 1
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
e1 : Tendsto (BohrMollerup.logGammaSeq x) atTop (𝓝 ((log ∘ f) x - (log ∘ f) 1))
⊢ (log ∘ f) x = (log ∘ Γ) x
have e1₁ : Tendsto (BohrMollerup.logGammaSeq x) atTop (𝓝 ((log ∘ f) x))
Tactic: rw [Function.comp_apply (f := log) (g := f) (x := 1), hf_one, log_one, sub_zero] at e1
Cleared hypotheses: e1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y
hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y
hf_one : f 1 = 1
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
y : ℝ
hy : 0 < y
⊢ (log ∘ f) (y + 1) = (log ∘ f) y + log y
have refine_1 : log y + log (f y) = log (f y) + log y
Tactic: rw [Function.comp_apply, Function.comp_apply, hf_feq hy, log_mul hy.ne' (hf_pos hy).ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
⊢ Γ (3 / 2) < 1
have A : 0 < 3 / 2
Tactic: have A : (0 : ℝ) < 3 / 2 := by simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
A : 0 < 3 / 2
⊢ Γ (3 / 2) < 1
have refine_2 : ∀ (this : (log ∘ Γ) ((↑2 : ℝ) + 1 / 2) ≤ (log ∘ Γ) (↑2 : ℝ) + 1 / 2 * log (↑2 : ℝ)), Γ (3 / 2) < 1
Tactic: have :=
    BohrMollerup.f_add_nat_le convexOn_log_Gamma (fun {y} hy => ?_) two_ne_zero one_half_pos
      (by norm_num : 1 / 2 ≤ (1 : ℝ))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
A : 0 < 3 / 2
refine_2 : ∀ (this : (log ∘ Γ) ((↑2 : ℝ) + 1 / 2) ≤ (log ∘ Γ) (↑2 : ℝ) + 1 / 2 * log (↑2 : ℝ)), Γ (3 / 2) < 1
⊢ Γ (3 / 2) < 1
have refine_1 : ∀ {y : ℝ} (hy : 0 < y), (log ∘ Γ) (y + 1) = (log ∘ Γ) y + log y
Tactic: have :=
    BohrMollerup.f_add_nat_le convexOn_log_Gamma (fun {y} hy => ?_) two_ne_zero one_half_pos
      (by norm_num : 1 / 2 ≤ (1 : ℝ))