-- Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean
theorem differentiableAt_Λ {s : ℂ} (hs : s ≠ 0 ∨ P.f₀ = 0) (hs' : s ≠ P.k ∨ P.g₀ = 0) :
    DifferentiableAt ℂ P.Λ s

Proof state:
case refine_2.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : P.g₀ = 0
⊢ DifferentiableAt ℂ (fun y => (P.ε / (↑P.k - y)) • P.g₀) s

Tactic:
simp [hs']

Result:
no goals

Proof state:
case refine_2.inl.hc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ ↑P.k
⊢ ↑P.k - s ≠ 0

Tactic:
simpa [sub_eq_zero, eq_comm]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
⊢ DifferentiableAt ℂ P.Λ s

Tactic:
refine ((P.differentiable_Λ₀ s).sub ?_).sub ?_

Result:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
⊢ DifferentiableAt ℂ (fun y => (1 / y) • P.f₀) s

case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
⊢ DifferentiableAt ℂ (fun y => (P.ε / (↑P.k - y)) • P.g₀) s

Proof state:
case refine_1.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
hs : P.f₀ = 0
⊢ DifferentiableAt ℂ (fun y => (1 / y) • P.f₀) s

Tactic:
simp [hs]

Result:
no goals

Proof state:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
⊢ DifferentiableAt ℂ (fun y => (P.ε / (↑P.k - y)) • P.g₀) s

Tactic:
rcases hs' with hs' | hs'

Result:
case refine_2.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ ↑P.k
⊢ DifferentiableAt ℂ (fun y => (P.ε / (↑P.k - y)) • P.g₀) s

case refine_2.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : P.g₀ = 0
⊢ DifferentiableAt ℂ (fun y => (P.ε / (↑P.k - y)) • P.g₀) s

Proof state:
case refine_1.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
hs : s ≠ 0
⊢ DifferentiableAt ℂ (fun y => (1 / y) • P.f₀) s

Tactic:
simpa using (differentiableAt_inv hs).smul_const _

Result:
no goals

Proof state:
case refine_2.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ ↑P.k
⊢ DifferentiableAt ℂ (fun y => (P.ε / (↑P.k - y)) • P.g₀) s

Tactic:
apply DifferentiableAt.smul_const

Result:
case refine_2.inl.hc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ ↑P.k
⊢ DifferentiableAt ℂ (fun y => P.ε / (↑P.k - y)) s

Proof state:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
⊢ DifferentiableAt ℂ (fun y => (1 / y) • P.f₀) s

Tactic:
rcases hs with hs | hs

Result:
case refine_1.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
hs : s ≠ 0
⊢ DifferentiableAt ℂ (fun y => (1 / y) • P.f₀) s

case refine_1.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
hs : P.f₀ = 0
⊢ DifferentiableAt ℂ (fun y => (1 / y) • P.f₀) s

Proof state:
case refine_2.inl.hc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ ↑P.k
⊢ DifferentiableAt ℂ (fun y => P.ε / (↑P.k - y)) s

Tactic:
apply (differentiableAt_const _).div ((differentiableAt_const _).sub (differentiable_id _))

Result:
case refine_2.inl.hc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ ↑P.k
⊢ ↑P.k - s ≠ 0