awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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
neg₁ : 1 - s.re ≤ 0
⊢ ⌊1 - s.re⌋₊ ≤ n

Tactic:
rw [Nat.floor_of_nonpos]

Premises used: Nat.floor_of_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
h : ¬0 ≤ 1 - s.re
⊢ 0 ≤ n

Tactic:
lia
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
h : ¬0 ≤ 1 - s.re
linarith : 0 < 1 - s.re → 1 - s.re - 0 + (0 - (1 - s.re)) = 0
⊢ 1 - s.re ≤ 0

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
⊢ -s.re < (↑n : ℝ)

Tactic:
simpa only [sub_sub_cancel_left] using Nat.sub_one_lt_floor (1 - s.re)

Premises used: HSub.hSub, sub_sub_cancel_left, Complex.re, Nat.sub_one_lt_floor, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
⊢ -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)
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
t1 : -s.re < (↑n : ℝ)
linarith : (↑n : ℝ) ≤ -(s.re + 1) → -1 + (-s.re - (↑n : ℝ)) + ((↑n : ℝ) - -(s.re + 1)) = 0
⊢ -(s.re + 1) < (↑n : ℝ)

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
t1 : -s.re < (↑n : ℝ)
⊢ -(s + 1).re < (↑n : ℝ)

Tactic:
have t2 : -(s + 1).re < n := by rw [add_re, one_re]; linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
t1 : -s.re < (↑n : ℝ)
t2 : -(s + 1).re < (↑n : ℝ)
rw : GammaAux n (s + 1) = s * (GammaAux n (s + 1) / s)
⊢ Gamma (s + 1) = s * Gamma s

Tactic:
rw [Gamma_eq_GammaAux s n t1, Gamma_eq_GammaAux (s + 1) n t2, GammaAux_recurrence1 s n t1]

Premises used: _private.0.Complex.Gamma_eq_GammaAux, _private.0.Complex.GammaAux_recurrence1, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
t1 : -s.re < (↑n : ℝ)
t2 : -(s + 1).re < (↑n : ℝ)
⊢ GammaAux n (s + 1) = s * (GammaAux n (s + 1) / s)

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
norm_cast : -s.re < 0
⊢ -s.re < (↑0 : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
linarith : 0 ≤ -s.re → 0 - s.re + (0 - -s.re) = 0
⊢ -s.re < 0

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
rw : GammaIntegral 1 = 1
rw₁ : 0 < re 1
⊢ Gamma 1 = 1

Tactic:
rw [Gamma_eq_integral]

Premises used: Complex.Gamma_eq_integral
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
⊢ GammaIntegral 1 = 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
⊢ 0 < re 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
⊢ Gamma (HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1) = (↑0! : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
hn : Gamma (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = (↑n ! : ℂ)
succ : (↑n.succ : ℂ) * Gamma (↑n.succ : ℂ) = (↑(n + 1)! : ℂ)
⊢ Gamma (HAdd.hAdd (α := ℂ) (↑(n + 1) : ℂ) 1) = (↑(n + 1)! : ℂ)

Tactic:
rw [Gamma_add_one n.succ <| Nat.cast_ne_zero.mpr <| Nat.succ_ne_zero n]

Premises used: Iff.mpr, Complex.Gamma_add_one, Nat.cast, Nat.succ_ne_zero, Nat.succ, Nat.cast_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
hn : Gamma (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = (↑n ! : ℂ)
succ :
  HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * Gamma (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (↑n ! : ℂ)
⊢ (↑n.succ : ℂ) * Gamma (↑n.succ : ℂ) = (↑(n + 1)! : ℂ)

Tactic:
simp only [Nat.cast_succ, Nat.factorial_succ, Nat.cast_mul]

Premises used: Nat.cast_succ, Nat.factorial_succ, Nat.cast_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
hn : Gamma (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = (↑n ! : ℂ)
⊢ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * Gamma (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (↑n ! : ℂ)

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
zero : Gamma (HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1) = (↑0! : ℂ)
succ :
  ∀ (n : ℕ) (hn : Gamma (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = (↑n ! : ℂ)),
    Gamma (HAdd.hAdd (α := ℂ) (↑(n + 1) : ℂ) 1) = (↑(n + 1)! : ℂ)
⊢ Gamma (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = (↑n ! : ℂ)

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

Premises used: Iff.mpr, Nat.cast_succ, Complex.Gamma_add_one, Nat.factorial_succ, Nat.cast, Nat.succ_ne_zero, Nat.cast_mul, Nat.succ, Nat.cast_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
inst : (n + 1).AtLeastTwo
⊢ Gamma (OfNat.ofNat (n + 1)) = (↑n ! : ℂ)

Tactic:
mod_cast Gamma_nat_eq_factorial (n : ℕ)

Premises used: Complex.Gamma_nat_eq_factorial, congrArg, Nat.cast_add._simp_1, cast, Complex.Gamma, Nat.cast, HAdd.hAdd, Nat.factorial, congrFun', OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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
simp_rw₄ : (HAdd.hAdd (α := ℂ) 0 1).GammaIntegral / 0 = 0
⊢ Gamma 0 = 0

Tactic:
simp_rw [Gamma, zero_re, sub_zero, Nat.floor_one, GammaAux, div_zero]

Premises used: sub_zero, Complex.Gamma, Complex.zero_re, Nat.floor_one, div_zero, _private.0.Complex.GammaAux
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
zero : Gamma (-0) = 0
zero₁ : Gamma 0 = 0
zero₂ zero₃ : Eq (α := ℂ) 0 0
⊢ Gamma (-(↑0 : ℂ)) = 0

Tactic:
rw [Nat.cast_zero, neg_zero, Gamma_zero]

Premises used: Nat.cast_zero, neg_zero, Complex.Gamma_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
IH : Gamma (-(↑n : ℂ)) = 0
rw : n.succ ≠ 0
⊢ Ne (α := ℂ) (-(↑n.succ : ℂ)) 0

Tactic:
rw [neg_ne_zero, Nat.cast_ne_zero]

Premises used: neg_ne_zero, Nat.cast_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
IH : Gamma (-(↑n : ℂ)) = 0
⊢ n.succ ≠ 0

Tactic:
apply Nat.succ_ne_zero

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
IH : Gamma (-(↑n : ℂ)) = 0
⊢ Ne (α := ℂ) (-(↑n.succ : ℂ)) 0

Tactic:
have A : -(n.succ : ℂ) ≠ 0 := by
      rw [neg_ne_zero, Nat.cast_ne_zero]
      apply Nat.succ_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
IH : Gamma (-(↑n : ℂ)) = 0
A : Ne (α := ℂ) (-(↑n.succ : ℂ)) 0
⊢ -(↑n : ℂ) = HAdd.hAdd (α := ℂ) (-(↑n.succ : ℂ)) 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
IH : Gamma (-(↑n : ℂ)) = 0
A : Ne (α := ℂ) (-(↑n.succ : ℂ)) 0
⊢ -(↑n : ℂ) = HAdd.hAdd (α := ℂ) (-(↑n.succ : ℂ)) 1

Tactic:
have : -(n : ℂ) = -↑n.succ + 1 := by simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
IH : Gamma (-(↑n : ℂ)) = 0
A : Ne (α := ℂ) (-(↑n.succ : ℂ)) 0
this : -(↑n : ℂ) = HAdd.hAdd (α := ℂ) (-(↑n.succ : ℂ)) 1
⊢ -(↑n.succ : ℂ) * Gamma (-(↑n.succ : ℂ)) = 0

Tactic:
rw [this, Gamma_add_one _ A] at IH

Premises used: Complex.Gamma_add_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
IH : Gamma (-(↑n : ℂ)) = 0
A : Ne (α := ℂ) (-(↑n.succ : ℂ)) 0
this : -(↑n : ℂ) = HAdd.hAdd (α := ℂ) (-(↑n.succ : ℂ)) 1
IH₁ : -(↑n.succ : ℂ) * Gamma (-(↑n.succ : ℂ)) = 0
⊢ Ne (α := ℂ) (-(↑n.succ : ℂ)) 0

Tactic:
rw [this, Gamma_add_one _ A] at IH

Premises used: Complex.Gamma_add_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
IH : Gamma (-(↑n : ℂ)) = 0
A : Ne (α := ℂ) (-(↑n.succ : ℂ)) 0
this : -(↑n : ℂ) = HAdd.hAdd (α := ℂ) (-(↑n.succ : ℂ)) 1
IH₁ : -(↑n.succ : ℂ) * Gamma (-(↑n.succ : ℂ)) = 0
A₁ : Ne (α := ℂ) (-(↑n.succ : ℂ)) 0
⊢ -(↑n : ℂ) = HAdd.hAdd (α := ℂ) (-(↑n.succ : ℂ)) 1

Tactic:
rw [this, Gamma_add_one _ A] at IH

Premises used: Complex.Gamma_add_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
IH : -(↑n.succ : ℂ) * Gamma (-(↑n.succ : ℂ)) = 0
A : Ne (α := ℂ) (-(↑n.succ : ℂ)) 0
this : -(↑n : ℂ) = HAdd.hAdd (α := ℂ) (-(↑n.succ : ℂ)) 1
succ : ∀ (IH : Gamma (-(↑(n + 1) : ℂ)) ≠ 0), -(↑n.succ : ℂ) * Gamma (-(↑n.succ : ℂ)) ≠ 0
⊢ Gamma (-(↑(n + 1) : ℂ)) = 0

Tactic:
contrapose! IH
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
A : Ne (α := ℂ) (-(↑n.succ : ℂ)) 0
this : -(↑n : ℂ) = HAdd.hAdd (α := ℂ) (-(↑n.succ : ℂ)) 1
IH : Gamma (-(↑(n + 1) : ℂ)) ≠ 0
⊢ -(↑n.succ : ℂ) * Gamma (-(↑n.succ : ℂ)) ≠ 0

Tactic:
mul_ne_zero A IH

Premises used: mul_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
A : Ne (α := ℂ) (-(↑n.succ : ℂ)) 0
this : -(↑n : ℂ) = HAdd.hAdd (α := ℂ) (-(↑n.succ : ℂ)) 1
IH : Gamma (-(↑(n + 1) : ℂ)) ≠ 0
⊢ -(↑n.succ : ℂ) * Gamma (-(↑n.succ : ℂ)) ≠ 0

Tactic:
exact mul_ne_zero A IH

Premises used: mul_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
zero : Gamma (-(↑0 : ℂ)) = 0
succ : ∀ (n : ℕ) (IH : Gamma (-(↑n : ℂ)) = 0), Gamma (-(↑(n + 1) : ℂ)) = 0
⊢ Gamma (-(↑n : ℂ)) = 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

Premises used: Nat.cast_zero, neg_zero, Complex.Gamma_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
this : ∀ (n : ℕ) (s : ℂ), GammaAux n ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n s)
⊢ Gamma ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) (Gamma s)

Tactic:
simp [Gamma, this]

Premises used: Complex.Gamma
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
suffices :
  ∀ (n : ℕ) (s : ℂ), GammaAux n ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n s)
⊢ Gamma ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) (Gamma s)

Tactic:
suffices ∀ (n : ℕ) (s : ℂ), GammaAux n (conj s) = conj (GammaAux n s) by
    simp [Gamma, this]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
⊢ ∀ (s : ℂ), GammaIntegral ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) s.GammaIntegral

Tactic:
GammaIntegral_conj

Premises used: Complex.GammaIntegral_conj
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
⊢ ∀ (s : ℂ), GammaIntegral ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) s.GammaIntegral

Tactic:
exact GammaIntegral_conj

Premises used: Complex.GammaIntegral_conj
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s_1 : ℂ
n : ℕ
IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n s)
s : ℂ
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 : ℂ)
⊢ HDiv.hDiv (β := ℂ) (GammaAux n (HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ)))
      ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n (s + 1) / s)

Tactic:
rw [div_eq_mul_inv _ s, map_mul, conj_inv, ← div_eq_mul_inv]

Premises used: Complex.conj_inv, div_eq_mul_inv, map_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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 : ℂ)
rw₁ rw₂ :
  HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n (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 : ℂ)

Tactic:
rw [this, IH]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s_1 : ℂ
n : ℕ
IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n s)
s : ℂ
succ : 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 : ℂ)

Tactic:
suffices conj s + 1 = conj (s + 1) by rw [this, IH]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s_1 : ℂ
n : ℕ
IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n s)
s : ℂ
succ :
  HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) =
    HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ)
succ₁ succ₂ :
  HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) =
    HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ)
⊢ HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) = (starRingEnd ℂ : (a : ℂ) → ℂ) (s + 1)

Tactic:
rw [map_add, map_one]

Premises used: map_add, map_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
zero : ∀ (s : ℂ), GammaAux 0 ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux 0 s)
succ :
  ∀ (n : ℕ)
    (IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n s))
    (s : ℂ), GammaAux (n + 1) ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux (n + 1) s)
⊢ ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n s)

Tactic:
induction n with
  | zero => rw [GammaAux]; exact GammaIntegral_conj
  | succ n IH =>
    intro s
    rw [GammaAux]
    dsimp only
    rw [div_eq_mul_inv _ s, map_mul, conj_inv, ← div_eq_mul_inv]
    suffices conj s + 1 = conj (s + 1) by rw [this, IH]
    rw [map_add, map_one]

Premises used: Complex.conj_inv, map_add, div_eq_mul_inv, map_mul, map_one, Complex.GammaIntegral_conj, _private.0.Complex.GammaAux
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
nth_rewrite : (1 / (↑r : ℂ)) ^ a = HPow.hPow (β := ℂ) (1 / (↑r : ℂ)) 1 * (1 / (↑r : ℂ)) ^ (a - 1)
⊢ (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)

Tactic:
nth_rewrite 2 [← cpow_one (1 / r : ℂ)]

Premises used: HDiv.hDiv, Complex.ofReal, Complex.cpow_one, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
rw : (1 / (↑r : ℂ)) ^ a = (1 / (↑r : ℂ)) ^ (1 + (a - 1))
rw₁ rw₂ : (1 / (↑r : ℂ)) ^ a = (1 / (↑r : ℂ)) ^ a
⊢ (1 / (↑r : ℂ)) ^ a = HPow.hPow (β := ℂ) (1 / (↑r : ℂ)) 1 * (1 / (↑r : ℂ)) ^ (a - 1)

Tactic:
rw [← cpow_add _ _ (one_div_ne_zero <| ofReal_ne_zero.mpr hr.ne'), add_sub_cancel]

Premises used: Iff.mpr, Complex.ofReal_ne_zero, LT.lt.ne', add_sub_cancel, Complex.cpow_add, one_div_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
⊢ (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)

Tactic:
have aux : (1 / r : ℂ) ^ a = 1 / r * (1 / r) ^ (a - 1) := by
    nth_rewrite 2 [← cpow_one (1 / r : ℂ)]
    rw [← cpow_add _ _ (one_div_ne_zero <| ofReal_ne_zero.mpr hr.ne'), add_sub_cancel]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ))))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) * (↑t : ℂ)) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ))))

Tactic:
MeasureTheory.setIntegral_congr_fun measurableSet_Ioi (fun x hx ↦ ?_)

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
refine :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
    (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
      (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) * (↑x : ℂ)) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ))))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) * (↑t : ℂ)) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ))))

Tactic:
refine MeasureTheory.setIntegral_congr_fun measurableSet_Ioi (fun x hx ↦ ?_)

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ 0 < x

Tactic:
rw [mem_Ioi] at hx

Premises used: Set.mem_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
x : ℝ
hx : 0 < x
rw :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1)) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₁ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * (↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₂ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (↑r : ℂ)⁻¹ ^ (a - 1) * (↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₃ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (↑r⁻¹ : ℂ) ^ (a - 1) * (↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₄ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    ((↑r⁻¹ : ℂ) * (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₅ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (↑(r⁻¹ * r) : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₆ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (↑1 : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₇ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    HPow.hPow (α := ℂ) 1 (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₈ : (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) = 1 * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₉ rw₁₀ : (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) = (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
⊢ (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) * (↑x : ℂ)) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))

Tactic:
rw [mul_cpow_ofReal_nonneg hr.le hx.le, ← mul_assoc, one_div, ← ofReal_inv,
        ← mul_cpow_ofReal_nonneg (inv_pos.mpr hr).le hr.le, ← ofReal_mul r⁻¹,
        inv_mul_cancel₀ hr.ne', ofReal_one, one_cpow, one_mul]

Premises used: Iff.mpr, mul_assoc, inv_pos, LT.lt.le, Complex.ofReal_one, Complex.mul_cpow_ofReal_nonneg, LT.lt.ne', Inv.inv, one_div, Complex.one_cpow, inv_mul_cancel₀, Complex.ofReal_inv, one_mul, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (1 / (↑r : ℂ)) ^ (a - 1) * (↑(r * t) : ℂ) ^ (a - 1) * cexp (-(↑(r * t) : ℂ))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) * (↑t : ℂ)) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ)))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))

Tactic:
simp_rw [← ofReal_mul]

Premises used: Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
simp_rw :
  Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      1 / (↑r : ℂ) * ((1 / (↑r : ℂ)) ^ (a - 1) * (↑a_1 : ℂ) ^ (a - 1) * cexp (-(↑a_1 : ℂ))))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1) * ((↑a_1 : ℂ) ^ (a - 1) * cexp (-(↑a_1 : ℂ))))
⊢ (1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))) =
    1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))

Tactic:
simp_rw [← MeasureTheory.integral_const_mul, mul_assoc]

Premises used: MeasureTheory.integral_const_mul, mul_assoc
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
rw :
  (1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))) =
    1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1) * a.GammaIntegral
⊢ (1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))) =
    (1 / (↑r : ℂ)) ^ a * Gamma a

Tactic:
rw [aux, Gamma_eq_integral ha]

Premises used: Complex.Gamma_eq_integral
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
e_a : ∀ (x : ℝ), (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ)) = (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (a - 1)
⊢ (1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))) =
    1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1) * a.GammaIntegral

Tactic:
congr 2 with x