-- Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
theorem f_nat_eq (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y) (hn : n ≠ 0) :
    f n = f 1 + log (n - 1)!

Proof state:
f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
⊢ f ↑1 = f 1 + log ↑(1 - 1)!

Tactic:
simp

Result:
no goals

Proof state:
f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
m : ℕ
hm : 1 ≤ m
IH : f ↑m = f 1 + log ↑(m - 1)!
A : 0 < ↑m
⊢ f ↑m + log ↑m = f 1 + log ↑m !

Tactic:
rw [IH, add_assoc, ← log_mul (Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero _)) A.ne', ←
  Nat.cast_mul]

Result:
f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
m : ℕ
hm : 1 ≤ m
IH : f ↑m = f 1 + log ↑(m - 1)!
A : 0 < ↑m
⊢ f 1 + log ↑((m - 1)! * m) = f 1 + log ↑m !

Proof state:
f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
⊢ f ↑n = f 1 + log ↑(n - 1)!

Tactic:
refine Nat.le_induction (by simp) (fun m hm IH => ?_) n (Nat.one_le_iff_ne_zero.2 hn)

Result:
f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
m : ℕ
hm : 1 ≤ m
IH : f ↑m = f 1 + log ↑(m - 1)!
⊢ f ↑(m + 1) = f 1 + log ↑(m + 1 - 1)!

Proof state:
f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
m : ℕ
hm : 1 ≤ m
IH : f ↑m = f 1 + log ↑(m - 1)!
A : 0 < ↑m
⊢ f ↑(m + 1) = f 1 + log ↑(m + 1 - 1)!

Tactic:
simp only [hf_feq A, Nat.cast_add, Nat.cast_one, Nat.add_succ_sub_one, add_zero]

Result:
f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
m : ℕ
hm : 1 ≤ m
IH : f ↑m = f 1 + log ↑(m - 1)!
A : 0 < ↑m
⊢ f ↑m + log ↑m = f 1 + log ↑m !

Proof state:
f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
m : ℕ
hm : 1 ≤ m
IH : f ↑m = f 1 + log ↑(m - 1)!
⊢ f ↑(m + 1) = f 1 + log ↑(m + 1 - 1)!

Tactic:
have A : 0 < (m : ℝ) := Nat.cast_pos.2 hm

Result:
f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
m : ℕ
hm : 1 ≤ m
IH : f ↑m = f 1 + log ↑(m - 1)!
A : 0 < ↑m
⊢ f ↑(m + 1) = f 1 + log ↑(m + 1 - 1)!

Proof state:
f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
m : ℕ
hm : 1 ≤ m
IH : f ↑m = f 1 + log ↑(m - 1)!
A : 0 < ↑m
⊢ f 1 + log ↑((m - 1)! * m) = f 1 + log ↑(m.pred ! * (m.pred + 1))

Tactic:
congr

Result:
case e_a.e_x.e_a.e_a
f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
m : ℕ
hm : 1 ≤ m
IH : f ↑m = f 1 + log ↑(m - 1)!
A : 0 < ↑m
⊢ m = m.pred + 1

Proof state:
case e_a.e_x.e_a.e_a
f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
m : ℕ
hm : 1 ≤ m
IH : f ↑m = f 1 + log ↑(m - 1)!
A : 0 < ↑m
⊢ m = m.pred + 1

Tactic:
exact (Nat.succ_pred_eq_of_pos hm).symm

Result:
no goals

Proof state:
f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
m : ℕ
hm : 1 ≤ m
IH : f ↑m = f 1 + log ↑(m - 1)!
A : 0 < ↑m
⊢ f 1 + log ↑((m - 1)! * m) = f 1 + log ↑m !

Tactic:
conv_rhs => rw [← Nat.succ_pred_eq_of_pos hm, Nat.factorial_succ, mul_comm]

Result:
f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
m : ℕ
hm : 1 ≤ m
IH : f ↑m = f 1 + log ↑(m - 1)!
A : 0 < ↑m
⊢ f 1 + log ↑((m - 1)! * m) = f 1 + log ↑(m.pred ! * (m.pred + 1))