-- Mathlib/Analysis/Complex/Hadamard.lean
/-- The function `scale f l u` is `diffContOnCl`. -/
lemma scale_diffContOnCl {f : ℂ → E} {l u : ℝ} (hul : l < u)
    (hd : DiffContOnCl ℂ f (verticalStrip l u)) :
    DiffContOnCl ℂ (scale f l u) (verticalStrip 0 1)

Proof state:
case hg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
⊢ DiffContOnCl ℂ (fun z => ↑l + z • (↑u - ↑l)) (verticalStrip 0 1)

Tactic:
apply DiffContOnCl.const_add

Result:
case hg.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
⊢ DiffContOnCl ℂ (fun x => x • (↑u - ↑l)) (verticalStrip 0 1)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
⊢ DiffContOnCl ℂ (scale f l u) (verticalStrip 0 1)

Tactic:
unfold scale

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
⊢ DiffContOnCl ℂ (fun z => f (↑l + z • (↑u - ↑l))) (verticalStrip 0 1)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
⊢ DiffContOnCl ℂ (fun z => f (↑l + z • (↑u - ↑l))) (verticalStrip 0 1)

Tactic:
apply DiffContOnCl.comp (s := verticalStrip l u) hd

Result:
case hg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
⊢ DiffContOnCl ℂ (fun z => ↑l + z • (↑u - ↑l)) (verticalStrip 0 1)

case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
⊢ MapsTo (fun z => ↑l + z • (↑u - ↑l)) (verticalStrip 0 1) (verticalStrip l u)

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
⊢ MapsTo (fun z => ↑l + z • (↑u - ↑l)) (verticalStrip 0 1) (verticalStrip l u)

Tactic:
rw [MapsTo]

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
⊢ ∀ ⦃x : ℂ⦄, x ∈ verticalStrip 0 1 → ↑l + x • (↑u - ↑l) ∈ verticalStrip l u

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
⊢ ∀ ⦃x : ℂ⦄, x ∈ verticalStrip 0 1 → ↑l + x • (↑u - ↑l) ∈ verticalStrip l u

Tactic:
intro z hz

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
z : ℂ
hz : z ∈ verticalStrip 0 1
⊢ ↑l + z • (↑u - ↑l) ∈ verticalStrip l u

Proof state:
case hg.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
⊢ DiffContOnCl ℂ (fun x => x • (↑u - ↑l)) (verticalStrip 0 1)

Tactic:
apply DiffContOnCl.smul_const

Result:
case hg.hf.hc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
⊢ DiffContOnCl ℂ (fun x => x) (verticalStrip 0 1)

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
z : ℂ
hz : z ∈ verticalStrip 0 1
⊢ ↑l + z • (↑u - ↑l) ∈ verticalStrip l u

Tactic:
exact scale_id_mem_verticalStrip_of_mem_verticalStrip hul hz

Result:
no goals

Proof state:
case hg.hf.hc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
⊢ DiffContOnCl ℂ (fun x => x) (verticalStrip 0 1)

Tactic:
exact Differentiable.diffContOnCl differentiable_id'

Result:
no goals