-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem Gamma_ne_zero {s : ℝ} (hs : ∀ m : ℕ, s ≠ -m) : Gamma s ≠ 0

Proof state:
case a
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
hs' : -↑n✝ + -1 < s
⊢ -↑n✝ < s + 1

Tactic:
linarith

Result:
no goals

Proof state:
case hs
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs' : -↑(n✝ + 1) < s
m : ℕ
hs : s + 1 = -↑m
⊢ s = -↑(1 + m)

Tactic:
rw [← eq_sub_iff_add_eq] at hs

Result:
case hs
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs' : -↑(n✝ + 1) < s
m : ℕ
hs : s = -↑m - 1
⊢ s = -↑(1 + m)

Proof state:
case a
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
hs' : -↑(n✝ + 1) < s
⊢ -↑n✝ < s + 1

Tactic:
rw [Nat.cast_add, Nat.cast_one, neg_add] at hs'

Result:
case a
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
hs' : -↑n✝ + -1 < s
⊢ -↑n✝ < s + 1

Proof state:
case zero
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ -↑0 < s → Gamma s ≠ 0

Tactic:
intro hs

Result:
case zero
s : ℝ
hs✝ : ∀ (m : ℕ), s ≠ -↑m
hs : -↑0 < s
⊢ Gamma s ≠ 0

Proof state:
case hs
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs' : -↑(n✝ + 1) < s
m : ℕ
hs : s = -↑m - 1
⊢ -↑m - 1 = -(1 + ↑m)

Tactic:
ring

Result:
no goals

Proof state:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ ∀ {n : ℕ}, -↑n < s → Gamma s ≠ 0

Tactic:
intro n

Result:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ
⊢ -↑n < s → Gamma s ≠ 0

Proof state:
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
hs' : -↑(n✝ + 1) < s
⊢ Gamma (s + 1) ≠ 0

Tactic:
apply n_ih

Result:
case hs
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
hs' : -↑(n✝ + 1) < s
⊢ ∀ (m : ℕ), s + 1 ≠ -↑m

case a
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
hs' : -↑(n✝ + 1) < s
⊢ -↑n✝ < s + 1

Proof state:
case a
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
this : ∀ {n : ℕ}, -↑n < s → Gamma s ≠ 0
⊢ -↑?n < s

case n
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
this : ∀ {n : ℕ}, -↑n < s → Gamma s ≠ 0
⊢ ℕ

Tactic:
swap

Result:
case n
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
this : ∀ {n : ℕ}, -↑n < s → Gamma s ≠ 0
⊢ ℕ

case a
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
this : ∀ {n : ℕ}, -↑n < s → Gamma s ≠ 0
⊢ -↑?n < s

Proof state:
case hs
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs' : -↑(n✝ + 1) < s
m : ℕ
hs : s = -↑m - 1
⊢ -↑m - 1 = -↑(1 + m)

Tactic:
push_cast

Result:
case hs
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs' : -↑(n✝ + 1) < s
m : ℕ
hs : s = -↑m - 1
⊢ -↑m - 1 = -(1 + ↑m)

Proof state:
case succ
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
hs' : -↑(n✝ + 1) < s
this : Gamma (s + 1) ≠ 0
⊢ s ≠ 0

Tactic:
simpa using hs 0

Result:
no goals

Proof state:
case a
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
this : ∀ {n : ℕ}, -↑n < s → Gamma s ≠ 0
⊢ -↑(⌊-s⌋₊ + 1) < s

Tactic:
rw [neg_lt, Nat.cast_add, Nat.cast_one]

Result:
case a
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
this : ∀ {n : ℕ}, -↑n < s → Gamma s ≠ 0
⊢ -s < ↑⌊-s⌋₊ + 1

Proof state:
case hs
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs' : -↑(n✝ + 1) < s
m : ℕ
hs : s = -↑m - 1
⊢ s = -↑(1 + m)

Tactic:
rw [hs]

Result:
case hs
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs' : -↑(n✝ + 1) < s
m : ℕ
hs : s = -↑m - 1
⊢ -↑m - 1 = -↑(1 + m)

Proof state:
case hs
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs' : -↑(n✝ + 1) < s
m : ℕ
hs : s ≠ -↑(1 + m)
⊢ s + 1 ≠ -↑m

Tactic:
contrapose! hs

Result:
case hs
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs' : -↑(n✝ + 1) < s
m : ℕ
hs : s + 1 = -↑m
⊢ s = -↑(1 + m)

Proof state:
case hs
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
hs' : -↑(n✝ + 1) < s
⊢ ∀ (m : ℕ), s + 1 ≠ -↑m

Tactic:
intro m

Result:
case hs
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
hs' : -↑(n✝ + 1) < s
m : ℕ
⊢ s + 1 ≠ -↑m

Proof state:
case zero
s : ℝ
hs✝ : ∀ (m : ℕ), s ≠ -↑m
hs : -↑0 < s
⊢ Gamma s ≠ 0

Tactic:
refine (Gamma_pos_of_pos ?_).ne'

Result:
case zero
s : ℝ
hs✝ : ∀ (m : ℕ), s ≠ -↑m
hs : -↑0 < s
⊢ 0 < s

Proof state:
case a
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
this : ∀ {n : ℕ}, -↑n < s → Gamma s ≠ 0
⊢ -s < ↑⌊-s⌋₊ + 1

Tactic:
exact Nat.lt_floor_add_one _

Result:
no goals

Proof state:
case hs
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
hs' : -↑(n✝ + 1) < s
m : ℕ
⊢ s + 1 ≠ -↑m

Tactic:
specialize hs (1 + m)

Result:
case hs
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs' : -↑(n✝ + 1) < s
m : ℕ
hs : s ≠ -↑(1 + m)
⊢ s + 1 ≠ -↑m

Proof state:
case succ
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
hs' : -↑(n✝ + 1) < s
this : Gamma (s + 1) ≠ 0
⊢ Gamma s ≠ 0

Tactic:
rw [Gamma_add_one, mul_ne_zero_iff] at this

Result:
case succ
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
hs' : -↑(n✝ + 1) < s
this : s ≠ 0 ∧ Gamma s ≠ 0
⊢ Gamma s ≠ 0

case succ
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
hs' : -↑(n✝ + 1) < s
this : Gamma (s + 1) ≠ 0
⊢ s ≠ 0

Proof state:
case n
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
this : ∀ {n : ℕ}, -↑n < s → Gamma s ≠ 0
⊢ ℕ

Tactic:
exact ⌊-s⌋₊ + 1

Result:
no goals

Proof state:
case succ
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ -↑(n✝ + 1) < s → Gamma s ≠ 0

Tactic:
intro hs'

Result:
case succ
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
hs' : -↑(n✝ + 1) < s
⊢ Gamma s ≠ 0

Proof state:
case succ
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
hs' : -↑(n✝ + 1) < s
this : s ≠ 0 ∧ Gamma s ≠ 0
⊢ Gamma s ≠ 0

Tactic:
exact this.2

Result:
no goals

Proof state:
case zero
s : ℝ
hs✝ : ∀ (m : ℕ), s ≠ -↑m
hs : -↑0 < s
⊢ 0 < s

Tactic:
rwa [Nat.cast_zero, neg_zero] at hs

Result:
no goals

Proof state:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
this : ∀ {n : ℕ}, -↑n < s → Gamma s ≠ 0
⊢ Gamma s ≠ 0

Tactic:
apply this

Result:
case a
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
this : ∀ {n : ℕ}, -↑n < s → Gamma s ≠ 0
⊢ -↑?n < s

case n
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
this : ∀ {n : ℕ}, -↑n < s → Gamma s ≠ 0
⊢ ℕ