-- Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean
theorem differentiableAt_Gamma (s : ℂ) (hs : ∀ m : ℕ, s ≠ -m) : DifferentiableAt ℂ Gamma s

Proof state:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ DifferentiableAt ℂ Gamma s

Tactic:
let n := ⌊1 - s.re⌋₊ + 1

Result:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
⊢ DifferentiableAt ℂ Gamma s

Proof state:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
⊢ DifferentiableAt ℂ Gamma s

Tactic:
have hn : 1 - s.re < n := mod_cast Nat.lt_floor_add_one (1 - s.re)

Result:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
⊢ DifferentiableAt ℂ Gamma s

Proof state:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
this : S ∈ 𝓝 s
t : ℂ
ht : t ∈ S
⊢ Gamma t = GammaAux n t

Tactic:
rw [mem_setOf_eq] at ht

Result:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
this : S ∈ 𝓝 s
t : ℂ
ht : 1 - t.re < ↑n
⊢ Gamma t = GammaAux n t

Proof state:
case h
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
x✝ : ℂ
⊢ x✝ ∈ S ↔ x✝ ∈ re ⁻¹' Ioi (1 - ↑n)

Tactic:
rw [preimage, Ioi, mem_setOf_eq, mem_setOf_eq, mem_setOf_eq]

Result:
case h
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
x✝ : ℂ
⊢ 1 - x✝.re < ↑n ↔ 1 - ↑n < x✝.re

Proof state:
case h
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
this : S = re ⁻¹' Ioi (1 - ↑n)
⊢ IsOpen S

Tactic:
rw [this]

Result:
case h
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
this : S = re ⁻¹' Ioi (1 - ↑n)
⊢ IsOpen (re ⁻¹' Ioi (1 - ↑n))

Proof state:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
⊢ S = re ⁻¹' Ioi (1 - ↑n)

Tactic:
ext

Result:
case h
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
x✝ : ℂ
⊢ x✝ ∈ S ↔ x✝ ∈ re ⁻¹' Ioi (1 - ↑n)

Proof state:
case h
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
⊢ S ⊆ S ∧ IsOpen S ∧ s ∈ S

Tactic:
refine ⟨Subset.rfl, ?_, hn⟩

Result:
case h
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
⊢ IsOpen S

Proof state:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
this : S ∈ 𝓝 s
t : ℂ
ht : 1 - t.re < ↑n
⊢ Gamma t = GammaAux n t

Tactic:
apply Gamma_eq_GammaAux

Result:
case h1
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
this : S ∈ 𝓝 s
t : ℂ
ht : 1 - t.re < ↑n
⊢ -t.re < ↑n

Proof state:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
⊢ S ∈ 𝓝 s

Tactic:
rw [mem_nhds_iff]

Result:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
⊢ ∃ t ⊆ S, IsOpen t ∧ s ∈ t

Proof state:
case h
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
x✝ : ℂ
⊢ 1 - x✝.re < ↑n ↔ 1 - ↑n < x✝.re

Tactic:
exact sub_lt_comm

Result:
no goals

Proof state:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
⊢ DifferentiableAt ℂ Gamma s

Tactic:
apply (differentiableAt_GammaAux s n hn hs).congr_of_eventuallyEq

Result:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
⊢ Gamma =ᶠ[𝓝 s] GammaAux n

Proof state:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
⊢ ∃ t ⊆ S, IsOpen t ∧ s ∈ t

Tactic:
use S

Result:
case h
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
⊢ S ⊆ S ∧ IsOpen S ∧ s ∈ S

Proof state:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
this : S ∈ 𝓝 s
⊢ Gamma =ᶠ[𝓝 s] GammaAux n

Tactic:
apply eventuallyEq_of_mem this

Result:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
this : S ∈ 𝓝 s
⊢ EqOn Gamma (GammaAux n) S

Proof state:
case h
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
⊢ IsOpen S

Tactic:
have : S = re ⁻¹' Ioi (1 - n : ℝ) := by
  ext; rw [preimage, Ioi, mem_setOf_eq, mem_setOf_eq, mem_setOf_eq]; exact sub_lt_comm

Result:
case h
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
this : S = re ⁻¹' Ioi (1 - ↑n)
⊢ IsOpen S

Proof state:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
this : S ∈ 𝓝 s
⊢ EqOn Gamma (GammaAux n) S

Tactic:
intro t ht

Result:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
this : S ∈ 𝓝 s
t : ℂ
ht : t ∈ S
⊢ Gamma t = GammaAux n t

Proof state:
case h1
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
this : S ∈ 𝓝 s
t : ℂ
ht : 1 - t.re < ↑n
⊢ -t.re < ↑n

Tactic:
linarith

Result:
no goals

Proof state:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
⊢ Gamma =ᶠ[𝓝 s] GammaAux n

Tactic:
have : S ∈ 𝓝 s := by
  rw [mem_nhds_iff]; use S
  refine ⟨Subset.rfl, ?_, hn⟩
  have : S = re ⁻¹' Ioi (1 - n : ℝ) := by
    ext; rw [preimage, Ioi, mem_setOf_eq, mem_setOf_eq, mem_setOf_eq]; exact sub_lt_comm
  rw [this]
  exact Continuous.isOpen_preimage continuous_re _ isOpen_Ioi

Result:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
this : S ∈ 𝓝 s
⊢ Gamma =ᶠ[𝓝 s] GammaAux n

Proof state:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
⊢ Gamma =ᶠ[𝓝 s] GammaAux n

Tactic:
let S := {t : ℂ | 1 - t.re < n}

Result:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
⊢ Gamma =ᶠ[𝓝 s] GammaAux n

Proof state:
case h
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ := ⌊1 - s.re⌋₊ + 1
hn : 1 - s.re < ↑n
S : Set ℂ := {t | 1 - t.re < ↑n}
this : S = re ⁻¹' Ioi (1 - ↑n)
⊢ IsOpen (re ⁻¹' Ioi (1 - ↑n))

Tactic:
exact Continuous.isOpen_preimage continuous_re _ isOpen_Ioi

Result:
no goals