-- Mathlib/Analysis/Complex/Hadamard.lean
/-- The function `invInterpStrip` is `diffContOnCl`. -/
lemma diffContOnCl_invInterpStrip {ε : ℝ} (hε : ε > 0) :
    DiffContOnCl ℂ (fun z ↦ invInterpStrip f z ε) (verticalStrip 0 1)

Proof state:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ ↑ε + ↑(sSupNormIm f 0) ≠ 0

Tactic:
rw [← ofReal_add, ofReal_ne_zero]

Result:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ ε + sSupNormIm f 0 ≠ 0

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ ↑ε + ↑(sSupNormIm f 0) ≠ 0 ∨ ∀ (x : ℂ), x - 1 ≠ 0

Tactic:
left

Result:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ ↑ε + ↑(sSupNormIm f 0) ≠ 0

Proof state:
case h.hb
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ Differentiable ℂ fun y => (↑ε + ↑(sSupNormIm f 1)) ^ (-y)

Tactic:
apply Differentiable.const_cpow (Differentiable.neg differentiable_id')

Result:
case h.hb
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ ↑ε + ↑(sSupNormIm f 1) ≠ 0 ∨ ∀ (x : ℂ), -x ≠ 0

Proof state:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ ε + sSupNormIm f 0 ≠ 0

Tactic:
simp only [ne_eq, ne_of_gt (sSupNormIm_eps_pos f hε 0), not_false_eq_true]

Result:
no goals

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ DiffContOnCl ℂ (fun z => invInterpStrip f z ε) (verticalStrip 0 1)

Tactic:
apply Differentiable.diffContOnCl

Result:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ Differentiable ℂ fun z => invInterpStrip f z ε

Proof state:
case h.ha
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ Differentiable ℂ fun y => (↑ε + ↑(sSupNormIm f 0)) ^ (y - 1)

Tactic:
apply Differentiable.const_cpow (Differentiable.sub_const (differentiable_id') 1) _

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ ↑ε + ↑(sSupNormIm f 0) ≠ 0 ∨ ∀ (x : ℂ), x - 1 ≠ 0

Proof state:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ Differentiable ℂ fun z => invInterpStrip f z ε

Tactic:
apply Differentiable.mul

Result:
case h.ha
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ Differentiable ℂ fun y => (↑ε + ↑(sSupNormIm f 0)) ^ (y - 1)

case h.hb
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ Differentiable ℂ fun y => (↑ε + ↑(sSupNormIm f 1)) ^ (-y)

Proof state:
case h.hb
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ ↑ε + ↑(sSupNormIm f 1) ≠ 0 ∨ ∀ (x : ℂ), -x ≠ 0

Tactic:
apply Or.inl

Result:
case h.hb.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ ↑ε + ↑(sSupNormIm f 1) ≠ 0

Proof state:
case h.hb.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ ↑ε + ↑(sSupNormIm f 1) ≠ 0

Tactic:
rw [← ofReal_add, ofReal_ne_zero]

Result:
case h.hb.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ ε + sSupNormIm f 1 ≠ 0

Proof state:
case h.hb.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ ε + sSupNormIm f 1 ≠ 0

Tactic:
exact (ne_of_gt (sSupNormIm_eps_pos f hε 1))

Result:
no goals