-- Mathlib/Analysis/Complex/Hadamard.lean
lemma diffContOnCl_interpStrip :
    DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)

Proof state:
case neg.intro.h.refine_2.refine_2.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ ↑(sSupNormIm f 1) ≠ 0

Tactic:
simp only [Ne, ofReal_eq_zero]

Result:
case neg.intro.h.refine_2.refine_2.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ ¬sSupNormIm f 1 = 0

Proof state:
case pos
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
⊢ DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)

Tactic:
eta_expand

Result:
case pos
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
⊢ DiffContOnCl ℂ (fun z => interpStrip (fun a => f a) z) fun a => verticalStrip 0 1 a

Proof state:
case neg.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : sSupNormIm f 0 ≠ 0
h1 : sSupNormIm f 1 ≠ 0
⊢ DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)

Tactic:
rw [ne_comm] at h0 h1

Result:
case neg.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
⊢ DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)

Proof state:
case neg.intro.h.refine_2.refine_2.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ ¬sSupNormIm f 1 = 0

Tactic:
rwa [eq_comm]

Result:
no goals

Proof state:
case neg.intro.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (fun z => interpStrip (fun a => f a) z) z

Tactic:
simp_rw [interpStrip_eq_of_pos f _ (lt_of_le_of_ne (sSupNormIm_nonneg f 0) h0)
  (lt_of_le_of_ne (sSupNormIm_nonneg f 1) h1)]

Result:
case neg.intro.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (fun z => ↑(sSupNormIm f 0) ^ (1 - z) * ↑(sSupNormIm f 1) ^ z) z

Proof state:
case neg.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
⊢ DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)

Tactic:
apply Differentiable.diffContOnCl

Result:
case neg.intro.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
⊢ Differentiable ℂ (interpStrip f)

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ ↑(sSupNormIm f 0) ≠ 0 ∨ 1 - z ≠ 0

Tactic:
left

Result:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ ↑(sSupNormIm f 0) ≠ 0

Proof state:
case pos
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
⊢ DiffContOnCl ℂ (fun z => interpStrip (fun a => f a) z) fun a => verticalStrip 0 1 a

Tactic:
simp_rw [interpStrip_eq_of_zero f _ h]

Result:
case pos
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
⊢ DiffContOnCl ℂ (fun z => 0) fun a => verticalStrip 0 1 a

Proof state:
case neg.intro.h.refine_2.refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (fun x => x) z

Tactic:
apply differentiableAt_id'

Result:
no goals

Proof state:
case neg.intro.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (interpStrip f) z

Tactic:
eta_expand

Result:
case neg.intro.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (fun z => interpStrip (fun a => f a) z) z

Proof state:
case neg.intro.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
⊢ Differentiable ℂ (interpStrip f)

Tactic:
intro z

Result:
case neg.intro.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (interpStrip f) z

Proof state:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ ↑(sSupNormIm f 0) ≠ 0

Tactic:
simp only [Ne, ofReal_eq_zero]

Result:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ ¬sSupNormIm f 0 = 0

Proof state:
case neg.intro.h.refine_2.refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ ↑(sSupNormIm f 1) ≠ 0 ∨ z ≠ 0

Tactic:
left

Result:
case neg.intro.h.refine_2.refine_2.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ ↑(sSupNormIm f 1) ≠ 0

Proof state:
case neg.intro.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (fun z => ↑(sSupNormIm f 0) ^ (1 - z) * ↑(sSupNormIm f 1) ^ z) z

Tactic:
refine DifferentiableAt.mul ?_ ?_

Result:
case neg.intro.h.refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (fun z => ↑(sSupNormIm f 0) ^ (1 - z)) z

case neg.intro.h.refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (HPow.hPow ↑(sSupNormIm f 1)) z

Proof state:
case pos
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
⊢ DiffContOnCl ℂ (fun z => 0) fun a => verticalStrip 0 1 a

Tactic:
exact diffContOnCl_const

Result:
no goals

Proof state:
case neg
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h : sSupNormIm f 0 ≠ 0 ∧ sSupNormIm f 1 ≠ 0
⊢ DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)

Tactic:
rcases h with ⟨h0, h1⟩

Result:
case neg.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : sSupNormIm f 0 ≠ 0
h1 : sSupNormIm f 1 ≠ 0
⊢ DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
⊢ DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)

Tactic:
by_cases h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0

Result:
case pos
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
⊢ DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)

case neg
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h : ¬(sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0)
⊢ DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)

Proof state:
case neg
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h : ¬(sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0)
⊢ DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)

Tactic:
push_neg at h

Result:
case neg
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h : sSupNormIm f 0 ≠ 0 ∧ sSupNormIm f 1 ≠ 0
⊢ DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)

Proof state:
case neg.intro.h.refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (fun z => ↑(sSupNormIm f 0) ^ (1 - z)) z

Tactic:
apply DifferentiableAt.const_cpow (DifferentiableAt.const_sub (differentiableAt_id') 1) _

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ ↑(sSupNormIm f 0) ≠ 0 ∨ 1 - z ≠ 0