awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
A : 0 < 3 / 2
y : ℝ
hy : 0 < y
⊢ (log ∘ Γ) (y + 1) = (log ∘ Γ) y + log y
have refine_1 : 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:
A : 0 < 3 / 2
y : ℝ
hy : 0 < y
refine_1 : log (Γ (y + 1)) = (log ∘ Γ) y + log y
⊢ (log ∘ Γ) (y + 1) = (log ∘ Γ) y + log y
have refine_1₁ : 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:
A : 0 < 3 / 2
y : ℝ
hy : 0 < y
refine_1 : log (Γ (y + 1)) = (log ∘ Γ) y + log y
refine_1₁ : log (y * Γ y) = (log ∘ Γ) y + log y
⊢ (log ∘ Γ) (y + 1) = (log ∘ Γ) y + log y
have refine_1₂ : 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:
A : 0 < 3 / 2
y : ℝ
hy : 0 < y
refine_1 : log (Γ (y + 1)) = (log ∘ Γ) y + log y
refine_1₁ : log (y * Γ y) = (log ∘ Γ) y + log y
refine_1₂ : log y + log (Γ y) = (log ∘ Γ) y + log y
⊢ (log ∘ Γ) (y + 1) = (log ∘ Γ) y + log y
have refine_1₃ : 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:
A : 0 < 3 / 2
y : ℝ
hy : 0 < y
refine_1 : log (Γ (y + 1)) = (log ∘ Γ) y + log y
refine_1₁ : log (y * Γ y) = (log ∘ Γ) y + log y
refine_1₂ : log y + log (Γ y) = (log ∘ Γ) y + log y
refine_1₃ : log (Γ y) + log y = (log ∘ Γ) y + log y
⊢ (log ∘ Γ) (y + 1) = (log ∘ Γ) y + log y
have refine_1₄ : 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 (hypothesis)
Goal:
A : 0 < 3 / 2
this : (log ∘ Γ) ((↑2 : ℝ) + 1 / 2) ≤ (log ∘ Γ) (↑2 : ℝ) + 1 / 2 * log (↑2 : ℝ)
⊢ Γ (3 / 2) < 1
have this₁ : Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
A : 0 < 3 / 2
this : Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ Γ (3 / 2) < 1
have refine_2 : 1 / 2 * log 2 - log (3 / 2) < 0
Tactic: refine this.trans_lt (exp_lt_one_iff.mpr ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
A : 0 < 3 / 2
this : Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ 1 / 2 * log 2 - log (3 / 2) < 0
have refine_2 : (log 2 * 1 - 2 * log (3 / 2)) / 2 < 0
Tactic: rw [mul_comm, ← mul_div_assoc, div_sub' two_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
A : 0 < 3 / 2
this : Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ (log 2 * 1 - 2 * log (3 / 2)) / 2 < 0
have refine_2 : log 2 * 1 - 2 * log (3 / 2) < 0
Tactic: refine div_neg_of_neg_of_pos ?_ two_pos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
A : 0 < 3 / 2
this : Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ log 2 * 1 - 2 * log (3 / 2) < 0
have refine_2 : 2 < HPow.hPow (β := ℕ) (3 / 2) 2
Tactic: rw [sub_neg, mul_one, ← Nat.cast_two, ← log_pow, ← exp_lt_exp, Nat.cast_two, exp_log two_pos,
      exp_log]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
A : 0 < 3 / 2
this : Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
refine_2 : 2 < HPow.hPow (β := ℕ) (3 / 2) 2
⊢ log 2 * 1 - 2 * log (3 / 2) < 0
have refine_2₁ : 0 < HPow.hPow (β := ℕ) (3 / 2) 2
Tactic: rw [sub_neg, mul_one, ← Nat.cast_two, ← log_pow, ← exp_lt_exp, Nat.cast_two, exp_log two_pos,
      exp_log]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
⊢ StrictMonoOn Γ (Ici 2)
have h : Eq (α := Set ℝ) (Ici 2) (Ioi 0 ∩ Ici 2)
Tactic: convert!
    convexOn_Gamma.strictMonoOn (by simp : (0 : ℝ) < 3 / 2) (by norm_num : (3 / 2 : ℝ) < 2)
      (Gamma_two.symm ▸ Gamma_three_div_two_lt_one)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
⊢ Eq (α := Set ℝ) (Ici 2) (Ioi 0 ∩ Ici 2)
have h : Eq (α := Set ℝ) (Ioi 0 ∩ Ici 2) (Ici 2)
Tactic: symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
⊢ Eq (α := Set ℝ) (Ioi 0 ∩ Ici 2) (Ici 2)
have h : Subset (α := Set ℝ) (Ici 2) (Ioi 0)
Tactic: rw [inter_eq_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
⊢ ∃ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioo 1 2) x ∧ IsMinOn Γ (Ioi 0) x
have have : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Icc 1 2) x) (hmin : IsMinOn Γ (Icc 1 2) x),
  ∃ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioo 1 2) x ∧ IsMinOn Γ (Ioi 0) x
Tactic: have ⟨x, hx, hmin⟩ := isCompact_Icc.exists_isMinOn (nonempty_Icc.mpr one_le_two) <|
    differentiableOn_Gamma_Ioi.continuousOn.mono <| by grind
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 1 2) x
hmin : IsMinOn Γ (Icc 1 2) x
⊢ ∃ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioo 1 2) x ∧ IsMinOn Γ (Ioi 0) x
have h1 : Γ (3 / 2) < Γ 1
Tactic: have ⟨h1, h2, h3half⟩ : Γ (3 / 2) < Γ 1 ∧ Γ (3 / 2) < Γ 2 ∧ Γ x ≤ Γ (3 / 2) := by
    simpa [Gamma_three_div_two_lt_one] using hmin <| by norm_num
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 1 2) x
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
⊢ ∃ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioo 1 2) x ∧ IsMinOn Γ (Ioi 0) x
have h2 : Γ (3 / 2) < Γ 2
Tactic: have ⟨h1, h2, h3half⟩ : Γ (3 / 2) < Γ 1 ∧ Γ (3 / 2) < Γ 2 ∧ Γ x ≤ Γ (3 / 2) := by
    simpa [Gamma_three_div_two_lt_one] using hmin <| by norm_num
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 1 2) x
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
⊢ ∃ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioo 1 2) x ∧ IsMinOn Γ (Ioi 0) x
have h3half : Γ x ≤ Γ (3 / 2)
Tactic: have ⟨h1, h2, h3half⟩ : Γ (3 / 2) < Γ 1 ∧ Γ (3 / 2) < Γ 2 ∧ Γ x ≤ Γ (3 / 2) := by
    simpa [Gamma_three_div_two_lt_one] using hmin <| by norm_num
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 1 2) x
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
h3half : Γ x ≤ Γ (3 / 2)
⊢ ∃ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioo 1 2) x ∧ IsMinOn Γ (Ioi 0) x
have refine : ∀ (y : ℝ),
  Membership.mem (γ := Set ℝ) (Ioi 0) y → Membership.mem (γ := Set ℝ) {x_2 : ℝ | (fun (x_3 : ℝ) ↦ Γ x ≤ Γ x_3) x_2} y
Tactic: refine ⟨x, by grind, fun y _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 1 2) x
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
h3half : Γ x ≤ Γ (3 / 2)
y : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) y
⊢ Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ Γ x ≤ Γ x_2) x_1} y
have inl : ∀ (hy : Membership.mem (γ := Set ℝ) (Ioc 0 1) y),
  Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ Γ x ≤ Γ x_2) x_1} y
Tactic: obtain hy | hy | hy : y ∈ Ioc 0 1 ∨ y ∈ Icc 1 2 ∨ y ∈ Ici 2 := by grind
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 1 2) x
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
h3half : Γ x ≤ Γ (3 / 2)
y : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) y
inl :
  ∀ (hy : Membership.mem (γ := Set ℝ) (Ioc 0 1) y),
    Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ Γ x ≤ Γ x_2) x_1} y
⊢ Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ Γ x ≤ Γ x_2) x_1} y
have inr : ∀ (hy : Membership.mem (γ := Set ℝ) (Icc 1 2) y),
  Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ Γ x ≤ Γ x_2) x_1} y
Tactic: obtain hy | hy | hy : y ∈ Ioc 0 1 ∨ y ∈ Icc 1 2 ∨ y ∈ Ici 2 := by grind
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 1 2) x
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
h3half : Γ x ≤ Γ (3 / 2)
y : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) y
inl :
  ∀ (hy : Membership.mem (γ := Set ℝ) (Ioc 0 1) y),
    Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ Γ x ≤ Γ x_2) x_1} y
inr :
  ∀ (hy : Membership.mem (γ := Set ℝ) (Icc 1 2) y),
    Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ Γ x ≤ Γ x_2) x_1} y
⊢ Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ Γ x ≤ Γ x_2) x_1} y
have inr₁ : ∀ (hy : Membership.mem (γ := Set ℝ) (Ici 2) y),
  Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ Γ x ≤ Γ x_2) x_1} y
Tactic: obtain hy | hy | hy : y ∈ Ioc 0 1 ∨ y ∈ Icc 1 2 ∨ y ∈ Ici 2 := by grind
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
s : ℝ
hs : s ≠ 0
⊢ (s + 1).doublingGamma = s * s.doublingGamma
have rw : Γ (s / 2 + 1 / 2) * (s / 2 * Γ (s / 2)) * (HPow.hPow (α := ℝ) 2 (s - 1) * 2) / √π =
  s * (Γ (s / 2) * Γ (s / 2 + 1 / 2) * HPow.hPow (α := ℝ) 2 (s - 1) / √π)
Tactic: rw [doublingGamma, doublingGamma, (by abel : s + 1 - 1 = s - 1 + 1), add_div, add_assoc,
    add_halves (1 : ℝ), Gamma_add_one (div_ne_zero hs two_ne_zero), rpow_add two_pos, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
⊢ doublingGamma 1 = 1
have simp_rw : Γ (1 / 2) * Γ (1 / 2 + 1 / 2) * HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℝ) 1 1) / √π = 1
Tactic: simp_rw [doublingGamma, Gamma_one_half_eq, add_halves (1 : ℝ), sub_self, Gamma_one, mul_one,
    rpow_zero, mul_one, div_self (sqrt_ne_zero'.mpr pi_pos)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
simp_rw : Γ (1 / 2) * Γ (1 / 2 + 1 / 2) * HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℝ) 1 1) / √π = 1
⊢ doublingGamma 1 = 1
have simp_rw₁ : √π * Γ (1 / 2 + 1 / 2) * HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℝ) 1 1) / √π = 1
Tactic: simp_rw [doublingGamma, Gamma_one_half_eq, add_halves (1 : ℝ), sub_self, Gamma_one, mul_one,
    rpow_zero, mul_one, div_self (sqrt_ne_zero'.mpr pi_pos)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
simp_rw : Γ (1 / 2) * Γ (1 / 2 + 1 / 2) * HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℝ) 1 1) / √π = 1
simp_rw₁ : √π * Γ (1 / 2 + 1 / 2) * HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℝ) 1 1) / √π = 1
⊢ doublingGamma 1 = 1
have simp_rw₂ : √π * Γ 1 * HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℝ) 1 1) / √π = 1
Tactic: simp_rw [doublingGamma, Gamma_one_half_eq, add_halves (1 : ℝ), sub_self, Gamma_one, mul_one,
    rpow_zero, mul_one, div_self (sqrt_ne_zero'.mpr pi_pos)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
simp_rw : Γ (1 / 2) * Γ (1 / 2 + 1 / 2) * HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℝ) 1 1) / √π = 1
simp_rw₁ : √π * Γ (1 / 2 + 1 / 2) * HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℝ) 1 1) / √π = 1
simp_rw₂ : √π * Γ 1 * HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℝ) 1 1) / √π = 1
⊢ doublingGamma 1 = 1
have simp_rw₃ : √π * Γ 1 * HPow.hPow (α := ℝ) (β := ℝ) 2 0 / √π = 1
Tactic: simp_rw [doublingGamma, Gamma_one_half_eq, add_halves (1 : ℝ), sub_self, Gamma_one, mul_one,
    rpow_zero, mul_one, div_self (sqrt_ne_zero'.mpr pi_pos)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
simp_rw : Γ (1 / 2) * Γ (1 / 2 + 1 / 2) * HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℝ) 1 1) / √π = 1
simp_rw₁ : √π * Γ (1 / 2 + 1 / 2) * HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℝ) 1 1) / √π = 1
simp_rw₂ : √π * Γ 1 * HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℝ) 1 1) / √π = 1
simp_rw₃ : √π * Γ 1 * HPow.hPow (α := ℝ) (β := ℝ) 2 0 / √π = 1
⊢ doublingGamma 1 = 1
have simp_rw₄ : √π * 1 * HPow.hPow (α := ℝ) (β := ℝ) 2 0 / √π = 1
Tactic: simp_rw [doublingGamma, Gamma_one_half_eq, add_halves (1 : ℝ), sub_self, Gamma_one, mul_one,
    rpow_zero, mul_one, div_self (sqrt_ne_zero'.mpr pi_pos)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
simp_rw : Γ (1 / 2) * Γ (1 / 2 + 1 / 2) * HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℝ) 1 1) / √π = 1
simp_rw₁ : √π * Γ (1 / 2 + 1 / 2) * HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℝ) 1 1) / √π = 1
simp_rw₂ : √π * Γ 1 * HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℝ) 1 1) / √π = 1
simp_rw₃ : √π * Γ 1 * HPow.hPow (α := ℝ) (β := ℝ) 2 0 / √π = 1
simp_rw₄ : √π * 1 * HPow.hPow (α := ℝ) (β := ℝ) 2 0 / √π = 1
⊢ doublingGamma 1 = 1
have simp_rw₅ : √π * HPow.hPow (α := ℝ) (β := ℝ) 2 0 / √π = 1
Tactic: simp_rw [doublingGamma, Gamma_one_half_eq, add_halves (1 : ℝ), sub_self, Gamma_one, mul_one,
    rpow_zero, mul_one, div_self (sqrt_ne_zero'.mpr pi_pos)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
simp_rw : Γ (1 / 2) * Γ (1 / 2 + 1 / 2) * HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℝ) 1 1) / √π = 1
simp_rw₁ : √π * Γ (1 / 2 + 1 / 2) * HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℝ) 1 1) / √π = 1
simp_rw₂ : √π * Γ 1 * HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℝ) 1 1) / √π = 1
simp_rw₃ : √π * Γ 1 * HPow.hPow (α := ℝ) (β := ℝ) 2 0 / √π = 1
simp_rw₄ : √π * 1 * HPow.hPow (α := ℝ) (β := ℝ) 2 0 / √π = 1
simp_rw₅ : √π * HPow.hPow (α := ℝ) (β := ℝ) 2 0 / √π = 1
⊢ doublingGamma 1 = 1
have simp_rw₆ : √π * 1 / √π = 1
Tactic: simp_rw [doublingGamma, Gamma_one_half_eq, add_halves (1 : ℝ), sub_self, Gamma_one, mul_one,
    rpow_zero, mul_one, div_self (sqrt_ne_zero'.mpr pi_pos)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
simp_rw : Γ (1 / 2) * Γ (1 / 2 + 1 / 2) * HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℝ) 1 1) / √π = 1
simp_rw₁ : √π * Γ (1 / 2 + 1 / 2) * HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℝ) 1 1) / √π = 1
simp_rw₂ : √π * Γ 1 * HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℝ) 1 1) / √π = 1
simp_rw₃ : √π * Γ 1 * HPow.hPow (α := ℝ) (β := ℝ) 2 0 / √π = 1
simp_rw₄ : √π * 1 * HPow.hPow (α := ℝ) (β := ℝ) 2 0 / √π = 1
simp_rw₅ : √π * HPow.hPow (α := ℝ) (β := ℝ) 2 0 / √π = 1
simp_rw₆ : √π * 1 / √π = 1
⊢ doublingGamma 1 = 1
have simp_rw₇ : √π / √π = 1
Tactic: simp_rw [doublingGamma, Gamma_one_half_eq, add_halves (1 : ℝ), sub_self, Gamma_one, mul_one,
    rpow_zero, mul_one, div_self (sqrt_ne_zero'.mpr pi_pos)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
s : ℝ
hs : Membership.mem (γ := Set ℝ) (Ioi 0) s
⊢ (log ∘ doublingGamma) s = (fun (s : ℝ) ↦ log (Γ (s / 2)) + log (Γ (s / 2 + 1 / 2)) + s * log 2 - log (2 * √π)) s
have h1 : √π ≠ 0
Tactic: have h1 : √π ≠ 0 := sqrt_ne_zero'.mpr pi_pos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
s : ℝ
hs : Membership.mem (γ := Set ℝ) (Ioi 0) s
h1 : √π ≠ 0
⊢ (log ∘ doublingGamma) s = (fun (s : ℝ) ↦ log (Γ (s / 2)) + log (Γ (s / 2 + 1 / 2)) + s * log 2 - log (2 * √π)) s
have h2 : Γ (s / 2) ≠ 0
Tactic: have h2 : Gamma (s / 2) ≠ 0 := (Gamma_pos_of_pos <| div_pos hs two_pos).ne'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
s : ℝ
hs : Membership.mem (γ := Set ℝ) (Ioi 0) s
h1 : √π ≠ 0
h2 : Γ (s / 2) ≠ 0
⊢ (log ∘ doublingGamma) s = (fun (s : ℝ) ↦ log (Γ (s / 2)) + log (Γ (s / 2 + 1 / 2)) + s * log 2 - log (2 * √π)) s
have h3 : Γ (s / 2 + 1 / 2) ≠ 0
Tactic: have h3 : Gamma (s / 2 + 1 / 2) ≠ 0 :=
    (Gamma_pos_of_pos <| add_pos (div_pos hs two_pos) one_half_pos).ne'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
s : ℝ
hs : Membership.mem (γ := Set ℝ) (Ioi 0) s
h1 : √π ≠ 0
h2 : Γ (s / 2) ≠ 0
h3 : Γ (s / 2 + 1 / 2) ≠ 0
⊢ (log ∘ doublingGamma) s = (fun (s : ℝ) ↦ log (Γ (s / 2)) + log (Γ (s / 2 + 1 / 2)) + s * log 2 - log (2 * √π)) s
have h4 : HPow.hPow (α := ℝ) 2 (s - 1) ≠ 0
Tactic: have h4 : (2 : ℝ) ^ (s - 1) ≠ 0 := (rpow_pos_of_pos two_pos _).ne'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
s : ℝ
hs : Membership.mem (γ := Set ℝ) (Ioi 0) s
h1 : √π ≠ 0
h2 : Γ (s / 2) ≠ 0
h3 : Γ (s / 2 + 1 / 2) ≠ 0
h4 : HPow.hPow (α := ℝ) 2 (s - 1) ≠ 0
⊢ (log ∘ doublingGamma) s = (fun (s : ℝ) ↦ log (Γ (s / 2)) + log (Γ (s / 2 + 1 / 2)) + s * log 2 - log (2 * √π)) s
have rw : log (Γ (s / 2)) + log (Γ (s / 2 + 1 / 2)) + (s - 1) * log 2 - log √π =
  (fun (s : ℝ) ↦ log (Γ (s / 2)) + log (Γ (s / 2 + 1 / 2)) + s * log 2 - (log 2 + log √π)) s
Tactic: rw [Function.comp_apply, doublingGamma, log_div (mul_ne_zero (mul_ne_zero h2 h3) h4) h1,
    log_mul (mul_ne_zero h2 h3) h4, log_mul h2 h3, log_rpow two_pos, log_mul two_ne_zero h1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
⊢ ConvexOn ℝ (Ioi 0) (log ∘ doublingGamma)
have refine_1 : ConvexOn ℝ (β := ℝ) (Ioi 0) fun (s : ℝ) ↦ log (Γ (s / 2))
Tactic: refine (((ConvexOn.add ?_ ?_).add ?_).add_const _).congr log_doublingGamma_eq.symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
refine_1 : ConvexOn ℝ (β := ℝ) (Ioi 0) fun (s : ℝ) ↦ log (Γ (s / 2))
⊢ ConvexOn ℝ (Ioi 0) (log ∘ doublingGamma)
have refine_2 : ConvexOn ℝ (β := ℝ) (Ioi 0) fun (s : ℝ) ↦ log (Γ (s / 2 + 1 / 2))
Tactic: refine (((ConvexOn.add ?_ ?_).add ?_).add_const _).congr log_doublingGamma_eq.symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
refine_1 : ConvexOn ℝ (β := ℝ) (Ioi 0) fun (s : ℝ) ↦ log (Γ (s / 2))
refine_2 : ConvexOn ℝ (β := ℝ) (Ioi 0) fun (s : ℝ) ↦ log (Γ (s / 2 + 1 / 2))
⊢ ConvexOn ℝ (Ioi 0) (log ∘ doublingGamma)
have refine_3 : ConvexOn ℝ (β := ℝ) (Ioi 0) fun (s : ℝ) ↦ s * log 2
Tactic: refine (((ConvexOn.add ?_ ?_).add ?_).add_const _).congr log_doublingGamma_eq.symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
⊢ ConvexOn ℝ (β := ℝ) (Ioi 0) fun (s : ℝ) ↦ log (Γ (s / 2))
have h : Eq (α := Set ℝ) (Ioi 0)
  (preimage (β := ℝ) (⇑(LinearMap.toAffineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2))) : (a : ℝ) → ℝ) (Ioi 0))
Tactic: convert!
    convexOn_log_Gamma.comp_affineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2 : ℝ)).toAffineMap using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
h :
  Eq (α := Set ℝ) (Ioi 0)
    (preimage (β := ℝ) (⇑(LinearMap.toAffineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2))) : (a : ℝ) → ℝ) (Ioi 0))
⊢ ConvexOn ℝ (β := ℝ) (Ioi 0) fun (s : ℝ) ↦ log (Γ (s / 2))
have h₁ : Eq (α := ℝ → ℝ) (fun (s : ℝ) ↦ log (Γ (s / 2)))
  ((log ∘ Γ) ∘ (⇑(LinearMap.toAffineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2))) : (a : ℝ) → ℝ))
Tactic: convert!
    convexOn_log_Gamma.comp_affineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2 : ℝ)).toAffineMap using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
⊢ Eq (α := ℝ → ℝ) (fun (s : ℝ) ↦ log (Γ (s / 2)))
    ((log ∘ Γ) ∘ (⇑(LinearMap.toAffineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2))) : (a : ℝ) → ℝ))
have h : ∀ (x : ℝ),
  log (Γ (x / 2)) = ((log ∘ Γ) ∘ (⇑(LinearMap.toAffineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2))) : (a : ℝ) → ℝ)) x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
⊢ log (Γ (x / 2)) = log (Γ ((1 / 2) • x))
have h : log (Γ (x / 2)) = log (Γ (1 / 2 * x))
Tactic: rw [smul_eq_mul, mul_comm, mul_one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
h : log (Γ (x / 2)) = log (Γ (1 / 2 * x))
⊢ log (Γ (x / 2)) = log (Γ ((1 / 2) • x))
have h₁ : log (Γ (x / 2)) = log (Γ (x * (1 / 2)))
Tactic: rw [smul_eq_mul, mul_comm, mul_one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
h : log (Γ (x / 2)) = log (Γ (1 / 2 * x))
h₁ : log (Γ (x / 2)) = log (Γ (x * (1 / 2)))
⊢ log (Γ (x / 2)) = log (Γ ((1 / 2) • x))
have h₂ : log (Γ (x / 2)) = log (Γ (x / 2))
Tactic: rw [smul_eq_mul, mul_comm, mul_one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
⊢ ConvexOn ℝ (β := ℝ) (Ioi 0) fun (s : ℝ) ↦ log (Γ (s / 2 + 1 / 2))
have refine_2 : ConvexOn ℝ (β := ℝ) (Ioi (-1)) fun (s : ℝ) ↦ log (Γ (s / 2 + 1 / 2))
Tactic: refine ConvexOn.subset ?_ (Ioi_subset_Ioi <| neg_one_lt_zero.le) (convex_Ioi _)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
⊢ ConvexOn ℝ (β := ℝ) (Ioi (-1)) fun (s : ℝ) ↦ log (Γ (s / 2 + 1 / 2))
have h : Eq (α := Set ℝ) (Ioi (-1))
  (preimage (β := ℝ)
    (⇑(HAdd.hAdd (α := ℝ →ᵃ[ℝ] ℝ) (LinearMap.toAffineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2)))
          (AffineMap.const ℝ ℝ (1 / 2))) :
      (a : ℝ) → ℝ)
    (Ioi 0))
Tactic: convert!
      convexOn_log_Gamma.comp_affineMap
        ((DistribSMul.toLinearMap ℝ ℝ (1 / 2 : ℝ)).toAffineMap +
          AffineMap.const ℝ ℝ (1 / 2 : ℝ)) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
h :
  Eq (α := Set ℝ) (Ioi (-1))
    (preimage (β := ℝ)
      (⇑(HAdd.hAdd (α := ℝ →ᵃ[ℝ] ℝ) (LinearMap.toAffineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2)))
            (AffineMap.const ℝ ℝ (1 / 2))) :
        (a : ℝ) → ℝ)
      (Ioi 0))
⊢ ConvexOn ℝ (β := ℝ) (Ioi (-1)) fun (s : ℝ) ↦ log (Γ (s / 2 + 1 / 2))
have h₁ : Eq (α := ℝ → ℝ) (fun (s : ℝ) ↦ log (Γ (s / 2 + 1 / 2)))
  ((log ∘ Γ) ∘
    (⇑(HAdd.hAdd (α := ℝ →ᵃ[ℝ] ℝ) (LinearMap.toAffineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2)))
          (AffineMap.const ℝ ℝ (1 / 2))) :
      (a : ℝ) → ℝ))
Tactic: convert!
      convexOn_log_Gamma.comp_affineMap
        ((DistribSMul.toLinearMap ℝ ℝ (1 / 2 : ℝ)).toAffineMap +
          AffineMap.const ℝ ℝ (1 / 2 : ℝ)) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
⊢ Eq (α := Set ℝ) (Ioi (-1)) (preimage (β := ℝ) ((fun (x : ℝ) ↦ x + 1 / 2) ∘ fun (x : ℝ) ↦ 1 / 2 * x) (Ioi 0))
have h : Eq (α := Set ℝ) (Ioi (-1))
  (preimage (β := ℝ) (fun (x : ℝ) ↦ 1 / 2 * x) (preimage (β := ℝ) (fun (x : ℝ) ↦ x + 1 / 2) (Ioi 0)))
Tactic: rw [preimage_comp, preimage_add_const_Ioi, zero_sub,
        preimage_const_mul_Ioi₀ (_ : ℝ) one_half_pos, neg_div, div_self (@one_half_pos ℝ _).ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
h :
  Eq (α := Set ℝ) (Ioi (-1))
    (preimage (β := ℝ) (fun (x : ℝ) ↦ 1 / 2 * x) (preimage (β := ℝ) (fun (x : ℝ) ↦ x + 1 / 2) (Ioi 0)))
⊢ Eq (α := Set ℝ) (Ioi (-1)) (preimage (β := ℝ) ((fun (x : ℝ) ↦ x + 1 / 2) ∘ fun (x : ℝ) ↦ 1 / 2 * x) (Ioi 0))
have h₁ : Eq (α := Set ℝ) (Ioi (-1)) ((fun (x : ℝ) ↦ 1 / 2 * x) ⁻¹' Ioi (0 - 1 / 2))
Tactic: rw [preimage_comp, preimage_add_const_Ioi, zero_sub,
        preimage_const_mul_Ioi₀ (_ : ℝ) one_half_pos, neg_div, div_self (@one_half_pos ℝ _).ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
h :
  Eq (α := Set ℝ) (Ioi (-1))
    (preimage (β := ℝ) (fun (x : ℝ) ↦ 1 / 2 * x) (preimage (β := ℝ) (fun (x : ℝ) ↦ x + 1 / 2) (Ioi 0)))
h₁ : Eq (α := Set ℝ) (Ioi (-1)) ((fun (x : ℝ) ↦ 1 / 2 * x) ⁻¹' Ioi (0 - 1 / 2))
⊢ Eq (α := Set ℝ) (Ioi (-1)) (preimage (β := ℝ) ((fun (x : ℝ) ↦ x + 1 / 2) ∘ fun (x : ℝ) ↦ 1 / 2 * x) (Ioi 0))
have h₂ : Eq (α := Set ℝ) (Ioi (-1)) ((fun (x : ℝ) ↦ 1 / 2 * x) ⁻¹' Ioi (-(1 / 2)))
Tactic: rw [preimage_comp, preimage_add_const_Ioi, zero_sub,
        preimage_const_mul_Ioi₀ (_ : ℝ) one_half_pos, neg_div, div_self (@one_half_pos ℝ _).ne']