-- Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
theorem Gamma_three_div_two_lt_one : Gamma (3 / 2) < 1

Proof state:
A : 0 < 3 / 2
⊢ Gamma (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 : ℝ))

Result:
case refine_2
A : 0 < 3 / 2
this : (log ∘ Gamma) (↑2 + 1 / 2) ≤ (log ∘ Gamma) ↑2 + 1 / 2 * log ↑2
⊢ Gamma (3 / 2) < 1

case refine_1
A : 0 < 3 / 2
y : ℝ
hy : 0 < y
⊢ (log ∘ Gamma) (y + 1) = (log ∘ Gamma) y + log y

Proof state:
case refine_2
A : 0 < 3 / 2
this : Gamma (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ Gamma (3 / 2) < 1

Tactic:
refine this.trans_lt (exp_lt_one_iff.mpr ?_)

Result:
case refine_2
A : 0 < 3 / 2
this : Gamma (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ 1 / 2 * log 2 - log (3 / 2) < 0

Proof state:
case refine_2
A : 0 < 3 / 2
this : (log ∘ Gamma) (↑2 + 1 / 2) ≤ (log ∘ Gamma) ↑2 + 1 / 2 * log ↑2
⊢ Gamma (3 / 2) < 1

case refine_1
A : 0 < 3 / 2
y : ℝ
hy : 0 < y
⊢ (log ∘ Gamma) (y + 1) = (log ∘ Gamma) y + log y

Tactic:
swap

Result:
case refine_1
A : 0 < 3 / 2
y : ℝ
hy : 0 < y
⊢ (log ∘ Gamma) (y + 1) = (log ∘ Gamma) y + log y

case refine_2
A : 0 < 3 / 2
this : (log ∘ Gamma) (↑2 + 1 / 2) ≤ (log ∘ Gamma) ↑2 + 1 / 2 * log ↑2
⊢ Gamma (3 / 2) < 1

Proof state:
A : 0 < 3 / 2
this : log (Gamma (2 + 1 / 2)) ≤ 1 / 2 * log 2
⊢ 2 + 1 / 2 = 3 / 2 + 1

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ Gamma (3 / 2) < 1

Tactic:
have A : (0 : ℝ) < 3 / 2 := by norm_num

Result:
A : 0 < 3 / 2
⊢ Gamma (3 / 2) < 1

Proof state:
case refine_2
A : 0 < 3 / 2
this : (log ∘ Gamma) (↑2 + 1 / 2) ≤ (log ∘ Gamma) ↑2 + 1 / 2 * log ↑2
⊢ Gamma (3 / 2) < 1

Tactic:
rw [Function.comp_apply, Function.comp_apply, Nat.cast_two, Gamma_two, log_one, zero_add,
  (by norm_num : (2 : ℝ) + 1 / 2 = 3 / 2 + 1), Gamma_add_one A.ne',
  log_mul A.ne' (Gamma_pos_of_pos A).ne', ← le_sub_iff_add_le',
  log_le_iff_le_exp (Gamma_pos_of_pos A)] at this

Result:
case refine_2
A : 0 < 3 / 2
this : Gamma (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ Gamma (3 / 2) < 1

Proof state:
case refine_2
A : 0 < 3 / 2
this : Gamma (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ (log 2 * 1 - 2 * log (3 / 2)) / 2 < 0

Tactic:
refine div_neg_of_neg_of_pos ?_ two_pos

Result:
case refine_2
A : 0 < 3 / 2
this : Gamma (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ log 2 * 1 - 2 * log (3 / 2) < 0

Proof state:
case refine_2
A : 0 < 3 / 2
this : Gamma (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ log 2 * 1 - 2 * log (3 / 2) < 0

Tactic:
rw [sub_neg, mul_one, ← Nat.cast_two, ← log_pow, ← exp_lt_exp, Nat.cast_two, exp_log two_pos,
    exp_log] <;>
  norm_num

Result:
no goals

Proof state:
⊢ 0 < 3 / 2

Tactic:
norm_num

Result:
no goals

Proof state:
case refine_2
A : 0 < 3 / 2
this : Gamma (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ 1 / 2 * log 2 - log (3 / 2) < 0

Tactic:
rw [mul_comm, ← mul_div_assoc, div_sub' two_ne_zero]

Result:
case refine_2
A : 0 < 3 / 2
this : Gamma (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ (log 2 * 1 - 2 * log (3 / 2)) / 2 < 0

Proof state:
case refine_1
A : 0 < 3 / 2
y : ℝ
hy : 0 < y
⊢ (log ∘ Gamma) (y + 1) = (log ∘ Gamma) 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]

Result:
no goals

Proof state:
A : 0 < 3 / 2
⊢ 1 / 2 ≤ 1

Tactic:
norm_num

Result:
no goals