awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
n : ℕ
hn : ∀ (s : ℂ) (h1 : -s.re < (↑n : ℝ)), GammaAux n s = GammaAux n (s + 1) / s
s : ℂ
h1 : -s.re < (↑(n + 1) : ℝ)
hh1 : -(s + 1).re < (↑n : ℝ)
⊢ GammaAux n (s + 1) / s = GammaAux n (s + 1 + 1) / (s + 1) / s
have succ : GammaAux n (s + 1) / s = GammaAux n (s + 1) / s
Tactic: rw [← hn (s + 1) hh1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
⊢ GammaAux n s = GammaAux n (s + 1) / s
have zero : ∀ (s : ℂ) (h1 : -s.re < (↑0 : ℝ)), GammaAux 0 s = GammaAux 0 (s + 1) / s
Tactic: induction n generalizing s with
  | zero =>
    simp only [CharP.cast_eq_zero, Left.neg_neg_iff] at h1
    dsimp only [GammaAux]; rw [GammaIntegral_add_one h1]
    rw [mul_comm, mul_div_cancel_right₀]; contrapose! h1; rw [h1]
    simp
  | succ n hn =>
    dsimp only [GammaAux]
    have hh1 : -(s + 1).re < n := by
      rw [Nat.cast_add, Nat.cast_one] at h1
      rw [add_re, one_re]; linarith
    rw [← hn (s + 1) hh1]
Cleared hypotheses: s, n, h1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
zero : ∀ (s : ℂ) (h1 : -s.re < (↑0 : ℝ)), GammaAux 0 s = GammaAux 0 (s + 1) / s
⊢ GammaAux n s = GammaAux n (s + 1) / s
have succ : ∀ (n : ℕ) (hn : ∀ (s : ℂ) (h1 : -s.re < (↑n : ℝ)), GammaAux n s = GammaAux n (s + 1) / s) (s : ℂ)
  (h1 : -s.re < (↑(n + 1) : ℝ)), GammaAux (n + 1) s = GammaAux (n + 1) (s + 1) / s
Tactic: induction n generalizing s with
  | zero =>
    simp only [CharP.cast_eq_zero, Left.neg_neg_iff] at h1
    dsimp only [GammaAux]; rw [GammaIntegral_add_one h1]
    rw [mul_comm, mul_div_cancel_right₀]; contrapose! h1; rw [h1]
    simp
  | succ n hn =>
    dsimp only [GammaAux]
    have hh1 : -(s + 1).re < n := by
      rw [Nat.cast_add, Nat.cast_one] at h1
      rw [add_re, one_re]; linarith
    rw [← hn (s + 1) hh1]
Cleared hypotheses: s, n, h1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
⊢ GammaAux n s = GammaAux (n + 1) s
have zero : ∀ (h1 : -s.re < (↑0 : ℝ)), GammaAux 0 s = GammaAux (HAdd.hAdd (α := ℕ) 0 1) s
Tactic: rcases n with - | n
Cleared hypotheses: n, h1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
zero : ∀ (h1 : -s.re < (↑0 : ℝ)), GammaAux 0 s = GammaAux (HAdd.hAdd (α := ℕ) 0 1) s
⊢ GammaAux n s = GammaAux (n + 1) s
have succ : ∀ (n : ℕ) (h1 : -s.re < (↑(n + 1) : ℝ)), GammaAux (n + 1) s = GammaAux (n + 1 + 1) s
Tactic: rcases n with - | n
Cleared hypotheses: n, h1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
s : ℂ
h1 : -s.re < (↑0 : ℝ)
⊢ GammaAux 0 s = GammaAux (HAdd.hAdd (α := ℕ) 0 1) s
have h1₁ : 0 < s.re
Tactic: simp only [CharP.cast_eq_zero, Left.neg_neg_iff] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
h1 : 0 < s.re
⊢ s.GammaIntegral = (s + 1).GammaIntegral / s
have zero : s ≠ 0
Tactic: rw [GammaIntegral_add_one h1, mul_div_cancel_left₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
h1 : 0 < re 0
⊢ False
have h1₁ : LT.lt (α := ℝ) 0 0
Tactic: rw [zero_re] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑(n + 1) : ℝ)
⊢ -(s + 1).re < (↑n : ℝ)
have h1₁ : -s.re < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: rw [Nat.cast_add, Nat.cast_one] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ -(s.re + 1) < (↑n : ℝ)
have linarith : (↑n : ℝ) ≤ -(s.re + 1) → -s.re - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + ((↑n : ℝ) - -(s.re + 1)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑(n + 1) : ℝ)
⊢ GammaAux n (s + 1 + 1) / (s + 1) = GammaAux n (s + 1)
have hh1 : -(s + 1).re < (↑n : ℝ)
Tactic: have hh1 : -(s + 1).re < n := by
        rw [Nat.cast_add, Nat.cast_one] at h1
        rw [add_re, one_re]; linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑(n + 1) : ℝ)
hh1 : -(s + 1).re < (↑n : ℝ)
⊢ GammaAux n (s + 1 + 1) / (s + 1) = GammaAux n (s + 1)
have rw : GammaAux n (s + 1 + 1) / (s + 1) = GammaAux n (s + 1 + 1) / (s + 1)
Tactic: rw [GammaAux_recurrence1 (s + 1) n hh1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑(n + 1) : ℝ)
⊢ GammaAux n (s + 1) / s = GammaAux n (s + 1 + 1) / (s + 1) / s
have this : GammaAux n (s + 1 + 1) / (s + 1) = GammaAux n (s + 1)
Tactic: have : GammaAux n (s + 1 + 1) / (s + 1) = GammaAux n (s + 1) := by
      have hh1 : -(s + 1).re < n := by
        rw [Nat.cast_add, Nat.cast_one] at h1
        rw [add_re, one_re]; linarith
      rw [GammaAux_recurrence1 (s + 1) n hh1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑(n + 1) : ℝ)
this : GammaAux n (s + 1 + 1) / (s + 1) = GammaAux n (s + 1)
⊢ GammaAux n (s + 1) / s = GammaAux n (s + 1 + 1) / (s + 1) / s
have succ : GammaAux n (s + 1) / s = GammaAux n (s + 1) / s
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
⊢ GammaAux (⌊1 - s.re⌋₊ + (k + 1)) s = Gamma s
have succ : GammaAux (⌊1 - s.re⌋₊ + k + 1) s = GammaAux (⌊1 - s.re⌋₊ + k) s
Tactic: rw [← hk, ← add_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
⊢ GammaAux (⌊1 - s.re⌋₊ + k + 1) s = GammaAux (⌊1 - s.re⌋₊ + k) s
have succ : -s.re < (↑(⌊1 - s.re⌋₊ + k) : ℝ)
Tactic: refine (GammaAux_recurrence2 s (⌊1 - s.re⌋₊ + k) ?_).symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
⊢ -s.re < (↑(⌊1 - s.re⌋₊ + k) : ℝ)
have succ : -s.re < HAdd.hAdd (α := ℝ) (↑⌊1 - s.re⌋₊ : ℝ) (↑k : ℝ)
Tactic: rw [Nat.cast_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
⊢ -s.re < HAdd.hAdd (α := ℝ) (↑⌊1 - s.re⌋₊ : ℝ) (↑k : ℝ)
have i0 : 1 - s.re - 1 < (↑⌊1 - s.re⌋₊ : ℝ)
Tactic: have i0 := Nat.sub_one_lt_floor (1 - s.re)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
i0 : 1 - s.re - 1 < (↑⌊1 - s.re⌋₊ : ℝ)
⊢ -s.re < HAdd.hAdd (α := ℝ) (↑⌊1 - s.re⌋₊ : ℝ) (↑k : ℝ)
have i0₁ : -s.re < (↑⌊1 - s.re⌋₊ : ℝ)
Tactic: simp only [sub_sub_cancel_left] at i0
Cleared hypotheses: i0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
i0 : -s.re < (↑⌊1 - s.re⌋₊ : ℝ)
⊢ -s.re < HAdd.hAdd (α := ℝ) (↑⌊1 - s.re⌋₊ : ℝ) (↑k : ℝ)
have succ : LE.le (α := ℝ) 0 (↑k : ℝ)
Tactic: refine lt_add_of_lt_of_nonneg i0 ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
i0 : -s.re < (↑⌊1 - s.re⌋₊ : ℝ)
⊢ LE.le (α := ℝ) 0 (↑k : ℝ)
have succ : 0 ≤ k
Tactic: rw [← Nat.cast_zero, Nat.cast_le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
k : ℕ
⊢ GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
have zero : GammaAux (⌊1 - s.re⌋₊ + 0) s = Gamma s
Tactic: induction k with
    | zero => simp [Gamma]
    | succ k hk =>
      rw [← hk, ← add_assoc]
      refine (GammaAux_recurrence2 s (⌊1 - s.re⌋₊ + k) ?_).symm
      rw [Nat.cast_add]
      have i0 := Nat.sub_one_lt_floor (1 - s.re)
      simp only [sub_sub_cancel_left] at i0
      refine lt_add_of_lt_of_nonneg i0 ?_
      rw [← Nat.cast_zero, Nat.cast_le]; exact Nat.zero_le k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
k : ℕ
zero : GammaAux (⌊1 - s.re⌋₊ + 0) s = Gamma s
⊢ GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
have succ : ∀ (k : ℕ) (hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s), GammaAux (⌊1 - s.re⌋₊ + (k + 1)) s = Gamma s
Tactic: induction k with
    | zero => simp [Gamma]
    | succ k hk =>
      rw [← hk, ← add_assoc]
      refine (GammaAux_recurrence2 s (⌊1 - s.re⌋₊ + k) ?_).symm
      rw [Nat.cast_add]
      have i0 := Nat.sub_one_lt_floor (1 - s.re)
      simp only [sub_sub_cancel_left] at i0
      refine lt_add_of_lt_of_nonneg i0 ?_
      rw [← Nat.cast_zero, Nat.cast_le]; exact Nat.zero_le k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
⊢ Gamma s = GammaAux n s
have u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
Tactic: have u : ∀ k : ℕ, GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s := fun k ↦ by
    induction k with
    | zero => simp [Gamma]
    | succ k hk =>
      rw [← hk, ← add_assoc]
      refine (GammaAux_recurrence2 s (⌊1 - s.re⌋₊ + k) ?_).symm
      rw [Nat.cast_add]
      have i0 := Nat.sub_one_lt_floor (1 - s.re)
      simp only [sub_sub_cancel_left] at i0
      refine lt_add_of_lt_of_nonneg i0 ?_
      rw [← Nat.cast_zero, Nat.cast_le]; exact Nat.zero_le k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
⊢ Gamma s = GammaAux n s
have h : n = ⌊1 - s.re⌋₊ + (n - ⌊1 - s.re⌋₊)
Tactic: convert! (u <| n - ⌊1 - s.re⌋₊).symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
⊢ n = ⌊1 - s.re⌋₊ + (n - ⌊1 - s.re⌋₊)
have h : ⌊1 - s.re⌋₊ ≤ n
Tactic: rw [Nat.add_sub_of_le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
⊢ ⌊1 - s.re⌋₊ ≤ n
have pos : ∀ (h : 0 ≤ 1 - s.re), ⌊1 - s.re⌋₊ ≤ n
Tactic: by_cases h : 0 ≤ 1 - s.re
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
pos : ∀ (h : 0 ≤ 1 - s.re), ⌊1 - s.re⌋₊ ≤ n
⊢ ⌊1 - s.re⌋₊ ≤ n
have neg : ∀ (h : ¬0 ≤ 1 - s.re), ⌊1 - s.re⌋₊ ≤ n
Tactic: by_cases h : 0 ≤ 1 - s.re
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
h : 0 ≤ 1 - s.re
⊢ ⌊1 - s.re⌋₊ ≤ n
have pos : ⌊1 - s.re⌋₊ < n.succ
Tactic: apply Nat.le_of_lt_succ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
h : 0 ≤ 1 - s.re
⊢ 1 - s.re < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have linarith : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ 1 - s.re → -s.re - (↑n : ℝ) + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - (1 - s.re)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
h : ¬0 ≤ 1 - s.re
⊢ ⌊1 - s.re⌋₊ ≤ n
have neg : 0 ≤ n
Tactic: rw [Nat.floor_of_nonpos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
h : ¬0 ≤ 1 - s.re
neg : 0 ≤ n
⊢ ⌊1 - s.re⌋₊ ≤ n
have neg₁ : 1 - s.re ≤ 0
Tactic: rw [Nat.floor_of_nonpos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
h : ¬0 ≤ 1 - s.re
⊢ 1 - s.re ≤ 0
have linarith : 0 < 1 - s.re → 1 - s.re - 0 + (0 - (1 - s.re)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
⊢ Gamma (s + 1) = s * Gamma s
have t1 : -s.re < (↑n : ℝ)
Tactic: have t1 : -s.re < n := by simpa only [sub_sub_cancel_left] using Nat.sub_one_lt_floor (1 - s.re)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
t1 : -s.re < (↑n : ℝ)
⊢ -(s.re + 1) < (↑n : ℝ)
have linarith : (↑n : ℝ) ≤ -(s.re + 1) → -1 + (-s.re - (↑n : ℝ)) + ((↑n : ℝ) - -(s.re + 1)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
t1 : -s.re < (↑n : ℝ)
⊢ Gamma (s + 1) = s * Gamma s
have t2 : -(s + 1).re < (↑n : ℝ)
Tactic: have t2 : -(s + 1).re < n := by rw [add_re, one_re]; linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
t1 : -s.re < (↑n : ℝ)
t2 : -(s + 1).re < (↑n : ℝ)
⊢ Gamma (s + 1) = s * Gamma s
have rw : GammaAux n (s + 1) = s * (GammaAux n (s + 1) / s)
Tactic: rw [Gamma_eq_GammaAux s n t1, Gamma_eq_GammaAux (s + 1) n t2, GammaAux_recurrence1 s n t1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
⊢ -s.re < (↑0 : ℝ)
have norm_cast : -s.re < 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
⊢ -s.re < 0
have linarith : 0 ≤ -s.re → 0 - s.re + (0 - -s.re) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
⊢ Gamma 1 = 1
have rw : GammaIntegral 1 = 1
Tactic: rw [Gamma_eq_integral]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
rw : GammaIntegral 1 = 1
⊢ Gamma 1 = 1
have rw₁ : 0 < re 1
Tactic: rw [Gamma_eq_integral]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
n : ℕ
hn : Gamma (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = (↑n ! : ℂ)
⊢ Gamma (HAdd.hAdd (α := ℂ) (↑(n + 1) : ℂ) 1) = (↑(n + 1)! : ℂ)
have succ : (↑n.succ : ℂ) * Gamma (↑n.succ : ℂ) = (↑(n + 1)! : ℂ)
Tactic: rw [Gamma_add_one n.succ <| Nat.cast_ne_zero.mpr <| Nat.succ_ne_zero n]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
n : ℕ
hn : Gamma (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = (↑n ! : ℂ)
⊢ (↑n.succ : ℂ) * Gamma (↑n.succ : ℂ) = (↑(n + 1)! : ℂ)
have succ : HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * Gamma (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (↑n ! : ℂ)
Tactic: simp only [Nat.cast_succ, Nat.factorial_succ, Nat.cast_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
n : ℕ
⊢ Gamma (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = (↑n ! : ℂ)
have zero : Gamma (HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1) = (↑0! : ℂ)
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    rw [Gamma_add_one n.succ <| Nat.cast_ne_zero.mpr <| Nat.succ_ne_zero n]
    simp only [Nat.cast_succ, Nat.factorial_succ, Nat.cast_mul]
    congr
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
n : ℕ
zero : Gamma (HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1) = (↑0! : ℂ)
⊢ Gamma (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = (↑n ! : ℂ)
have succ : ∀ (n : ℕ) (hn : Gamma (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = (↑n ! : ℂ)),
  Gamma (HAdd.hAdd (α := ℂ) (↑(n + 1) : ℂ) 1) = (↑(n + 1)! : ℂ)
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    rw [Gamma_add_one n.succ <| Nat.cast_ne_zero.mpr <| Nat.succ_ne_zero n]
    simp only [Nat.cast_succ, Nat.factorial_succ, Nat.cast_mul]
    congr
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
⊢ Gamma 0 = 0
have simp_rw : GammaAux ⌊1 - re 0⌋₊ 0 = 0
Tactic: simp_rw [Gamma, zero_re, sub_zero, Nat.floor_one, GammaAux, div_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
simp_rw : GammaAux ⌊1 - re 0⌋₊ 0 = 0
⊢ Gamma 0 = 0
have simp_rw₁ : GammaAux ⌊HSub.hSub (α := ℝ) 1 0⌋₊ 0 = 0
Tactic: simp_rw [Gamma, zero_re, sub_zero, Nat.floor_one, GammaAux, div_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
simp_rw : GammaAux ⌊1 - re 0⌋₊ 0 = 0
simp_rw₁ : GammaAux ⌊HSub.hSub (α := ℝ) 1 0⌋₊ 0 = 0
⊢ Gamma 0 = 0
have simp_rw₂ : GammaAux (Nat.floor (α := ℝ) 1) 0 = 0
Tactic: simp_rw [Gamma, zero_re, sub_zero, Nat.floor_one, GammaAux, div_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
simp_rw : GammaAux ⌊1 - re 0⌋₊ 0 = 0
simp_rw₁ : GammaAux ⌊HSub.hSub (α := ℝ) 1 0⌋₊ 0 = 0
simp_rw₂ : GammaAux (Nat.floor (α := ℝ) 1) 0 = 0
⊢ Gamma 0 = 0
have simp_rw₃ : GammaAux 1 0 = 0
Tactic: simp_rw [Gamma, zero_re, sub_zero, Nat.floor_one, GammaAux, div_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
simp_rw : GammaAux ⌊1 - re 0⌋₊ 0 = 0
simp_rw₁ : GammaAux ⌊HSub.hSub (α := ℝ) 1 0⌋₊ 0 = 0
simp_rw₂ : GammaAux (Nat.floor (α := ℝ) 1) 0 = 0
simp_rw₃ : GammaAux 1 0 = 0
⊢ Gamma 0 = 0
have simp_rw₄ : (HAdd.hAdd (α := ℂ) 0 1).GammaIntegral / 0 = 0
Tactic: simp_rw [Gamma, zero_re, sub_zero, Nat.floor_one, GammaAux, div_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
⊢ Gamma (-(↑0 : ℂ)) = 0
have zero : Gamma (-0) = 0
Tactic: rw [Nat.cast_zero, neg_zero, Gamma_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
zero : Gamma (-0) = 0
⊢ Gamma (-(↑0 : ℂ)) = 0
have zero₁ : Gamma 0 = 0
Tactic: rw [Nat.cast_zero, neg_zero, Gamma_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
zero : Gamma (-0) = 0
zero₁ : Gamma 0 = 0
⊢ Gamma (-(↑0 : ℂ)) = 0
have zero₂ : Eq (α := ℂ) 0 0
Tactic: rw [Nat.cast_zero, neg_zero, Gamma_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
n : ℕ
IH : Gamma (-(↑n : ℂ)) = 0
⊢ Ne (α := ℂ) (-(↑n.succ : ℂ)) 0
have rw : n.succ ≠ 0
Tactic: rw [neg_ne_zero, Nat.cast_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
n : ℕ
IH : Gamma (-(↑n : ℂ)) = 0
⊢ Gamma (-(↑(n + 1) : ℂ)) = 0
have A : Ne (α := ℂ) (-(↑n.succ : ℂ)) 0
Tactic: have A : -(n.succ : ℂ) ≠ 0 := by
      rw [neg_ne_zero, Nat.cast_ne_zero]
      apply Nat.succ_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
n : ℕ
IH : Gamma (-(↑n : ℂ)) = 0
A : Ne (α := ℂ) (-(↑n.succ : ℂ)) 0
⊢ Gamma (-(↑(n + 1) : ℂ)) = 0
have this : -(↑n : ℂ) = HAdd.hAdd (α := ℂ) (-(↑n.succ : ℂ)) 1
Tactic: have : -(n : ℂ) = -↑n.succ + 1 := by simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
n : ℕ
IH : Gamma (-(↑n : ℂ)) = 0
A : Ne (α := ℂ) (-(↑n.succ : ℂ)) 0
this : -(↑n : ℂ) = HAdd.hAdd (α := ℂ) (-(↑n.succ : ℂ)) 1
⊢ Gamma (-(↑(n + 1) : ℂ)) = 0
have IH₁ : -(↑n.succ : ℂ) * Gamma (-(↑n.succ : ℂ)) = 0
Tactic: rw [this, Gamma_add_one _ A] at IH
Cleared hypotheses: IH, A, this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
n : ℕ
IH : -(↑n.succ : ℂ) * Gamma (-(↑n.succ : ℂ)) = 0
A : Ne (α := ℂ) (-(↑n.succ : ℂ)) 0
this : -(↑n : ℂ) = HAdd.hAdd (α := ℂ) (-(↑n.succ : ℂ)) 1
⊢ Gamma (-(↑(n + 1) : ℂ)) = 0
have succ : ∀ (IH : Gamma (-(↑(n + 1) : ℂ)) ≠ 0), -(↑n.succ : ℂ) * Gamma (-(↑n.succ : ℂ)) ≠ 0
Tactic: contrapose! IH
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
n : ℕ
⊢ Gamma (-(↑n : ℂ)) = 0
have zero : Gamma (-(↑0 : ℂ)) = 0
Tactic: induction n with
  | zero => rw [Nat.cast_zero, neg_zero, Gamma_zero]
  | succ n IH =>
    have A : -(n.succ : ℂ) ≠ 0 := by
      rw [neg_ne_zero, Nat.cast_ne_zero]
      apply Nat.succ_ne_zero
    have : -(n : ℂ) = -↑n.succ + 1 := by simp
    rw [this, Gamma_add_one _ A] at IH
    contrapose! IH
    exact mul_ne_zero A IH
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
n : ℕ
zero : Gamma (-(↑0 : ℂ)) = 0
⊢ Gamma (-(↑n : ℂ)) = 0
have succ : ∀ (n : ℕ) (IH : Gamma (-(↑n : ℂ)) = 0), Gamma (-(↑(n + 1) : ℂ)) = 0
Tactic: induction n with
  | zero => rw [Nat.cast_zero, neg_zero, Gamma_zero]
  | succ n IH =>
    have A : -(n.succ : ℂ) ≠ 0 := by
      rw [neg_ne_zero, Nat.cast_ne_zero]
      apply Nat.succ_ne_zero
    have : -(n : ℂ) = -↑n.succ + 1 := by simp
    rw [this, Gamma_add_one _ A] at IH
    contrapose! IH
    exact mul_ne_zero A IH
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
⊢ Gamma ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) (Gamma s)
have suffices : ∀ (n : ℕ) (s : ℂ), GammaAux n ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n s)
Tactic: suffices ∀ (n : ℕ) (s : ℂ), GammaAux n (conj s) = conj (GammaAux n s) by
    simp [Gamma, this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s_1 : ℂ
n : ℕ
IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n s)
s : ℂ
⊢ HDiv.hDiv (β := ℂ) (GammaAux n (HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ)))
      ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n (s + 1) / s)
have succ : HDiv.hDiv (β := ℂ) (GammaAux n (HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ)))
    ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) =
  HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n (s + 1)) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ)
Tactic: rw [div_eq_mul_inv _ s, map_mul, conj_inv, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s_1 : ℂ
n : ℕ
IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n s)
s : ℂ
this : HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) = (starRingEnd ℂ : (a : ℂ) → ℂ) (s + 1)
⊢ HDiv.hDiv (β := ℂ) (GammaAux n (HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ)))
      ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) =
    HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n (s + 1)) : ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ)
have rw : HDiv.hDiv (β := ℂ) (GammaAux n ((starRingEnd ℂ : (a : ℂ) → ℂ) (s + 1))) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) =
  HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n (s + 1)) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ)
Tactic: rw [this, IH]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s_1 : ℂ
n : ℕ
IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n s)
s : ℂ
this : HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) = (starRingEnd ℂ : (a : ℂ) → ℂ) (s + 1)
rw :
  HDiv.hDiv (β := ℂ) (GammaAux n ((starRingEnd ℂ : (a : ℂ) → ℂ) (s + 1))) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) =
    HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n (s + 1)) : ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ)
⊢ HDiv.hDiv (β := ℂ) (GammaAux n (HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ)))
      ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) =
    HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n (s + 1)) : ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ)
have rw₁ : HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n (s + 1)) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) =
  HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n (s + 1)) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ)
Tactic: rw [this, IH]