awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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
hm : Tendsto (logGammaSeq (x - 1)) atTop (𝓝 (f (x - 1) - f 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)

Tactic:
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
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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
hm : Tendsto (logGammaSeq (x - 1)) atTop (𝓝 (f (x - 1) - f 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)
⊢ 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)))

Tactic:
replace hm :=
      ((Tendsto.congr' this hm).add (tendsto_const_nhds : Tendsto (fun _ => log (x - 1)) _ _)).comp
        (tendsto_add_atTop_nat 1)
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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)))
h :
  ∀ (n : ℕ),
    ((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)
        n =
      logGammaSeq x n + x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
⊢ 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:
ext1 n
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 : ℝ))
h₁ h₂ :
  logGammaSeq x n + x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ)) =
    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 : ℝ))

Tactic:
rw [sub_add_cancel, Nat.add_sub_cancel]

Premises used: Nat.add_sub_cancel, sub_add_cancel
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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)))
⊢ 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]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 (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
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 : ℝ))
hm₁ :
  Tendsto (fun (n : ℕ) ↦ logGammaSeq x n + x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))) atTop
    (𝓝 (f (x - 1) - f 1 + log (x - 1)))
⊢ 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:
rw [this] at hm
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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
    (fun (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 : ℝ)))
    atTop (𝓝 (f (x - 1) - f 1 + log (x - 1) - x * 0))

Tactic:
hm.sub (tendsto_log_nat_add_one_sub_log.const_mul x)

Premises used: Filter.Tendsto.const_mul, Real.tendsto_log_nat_add_one_sub_log, Filter.Tendsto.sub
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 : ℝ))
h₁ : f x - f 1 = f (x - 1) - f 1 + log (x - 1) - x * 0
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Tactic:
convert! hm.sub (tendsto_log_nat_add_one_sub_log.const_mul x) using 2

Premises used: Filter.Tendsto.const_mul, Real.tendsto_log_nat_add_one_sub_log, Filter.Tendsto.sub
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 : ℝ))
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:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 - 1 + 1) = f (x - 1) + log (x - 1)

Tactic:
have := hf_feq ((Nat.cast_nonneg m).trans_lt hy)
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 (x - 1) + log (x - 1)

Tactic:
rw [sub_add_cancel] at this

Premises used: sub_add_cancel
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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)
h : f (x - 1) + log (x - 1) - f 1 = f (x - 1) - f 1 + log (x - 1) - x * 0
⊢ f x - f 1 = f (x - 1) - f 1 + log (x - 1) - x * 0

Tactic:
rw [this]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 - 1) + log (x - 1) - f 1 = f (x - 1) - f 1 + log (x - 1) - x * 0

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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))
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))
⊢ (↑m : ℝ) < x → x ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 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

Premises used: Nat.cast_succ, sub_le_iff_le_add, zero_add, Nat.cast_zero, lt_sub_iff_add_lt, sub_add_cancel, Real.BohrMollerup.tendsto_logGammaSeq_of_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : 0 < x
simp_rw : log (Γ x) = log (Γ x) - log (Γ 1)
simp_rw₁ : log (Γ x) = log (Γ x) - log 1
simp_rw₂ : log (Γ x) = log (Γ x) - 0
⊢ log (Γ x) = (log ∘ Γ) x - (log ∘ Γ) 1

Tactic:
simp_rw [Function.comp_apply, Gamma_one, log_one, sub_zero]

Premises used: sub_zero, Real.Gamma_one, Real.log_one, Function.comp_apply
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : 0 < x
⊢ 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]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : 0 < x
this : log (Γ x) = (log ∘ Γ) x - (log ∘ Γ) 1
rw : Tendsto (logGammaSeq x) atTop (𝓝 ((log ∘ Γ) x - (log ∘ Γ) 1))
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (log (Γ x)))

Tactic:
rw [this]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : 0 < x
this : log (Γ x) = (log ∘ Γ) x - (log ∘ Γ) 1
⊢ Tendsto (logGammaSeq x) atTop (𝓝 ((log ∘ Γ) x - (log ∘ Γ) 1))

Tactic:
BohrMollerup.tendsto_logGammaSeq convexOn_log_Gamma (fun {y} hy => ?_) hx

Premises used: Real.convexOn_log_Gamma, Real.BohrMollerup.tendsto_logGammaSeq
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : 0 < x
this : log (Γ x) = (log ∘ Γ) x - (log ∘ Γ) 1
refine : ∀ {y : ℝ} (hy : 0 < y), (log ∘ Γ) (y + 1) = (log ∘ Γ) y + log y
⊢ Tendsto (logGammaSeq x) atTop (𝓝 ((log ∘ Γ) x - (log ∘ Γ) 1))

Tactic:
refine BohrMollerup.tendsto_logGammaSeq convexOn_log_Gamma (fun {y} hy => ?_) hx

Premises used: Real.convexOn_log_Gamma, Real.BohrMollerup.tendsto_logGammaSeq
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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
rw₄ rw₅ : log (Γ y) + log y = log (Γ y) + log y
⊢ (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]

Premises used: Real.Gamma_pos_of_pos, Real.Gamma_add_one, add_comm, LT.lt.ne', Function.comp_apply, Real.log_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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
suffices : EqOn (log ∘ f) (log ∘ Γ) (Ioi 0)
⊢ EqOn f Γ (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)
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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
refine_1 : ∀ {y : ℝ}, 0 < y → (log ∘ f) (y + 1) = (log ∘ f) y + log y
⊢ (log ∘ f) x = (log ∘ Γ) x

Tactic:
have e1 := BohrMollerup.tendsto_logGammaSeq hf_conv ?_ hx
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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))
⊢ 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

Premises used: sub_zero, Real.log_one, Function.comp_apply