E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
z w : ℂ
this : ∀ (c : ℂ), deriv f c = 0
⊢ f z = f w

case this
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
z w : ℂ
⊢ ∀ (c : ℂ), deriv f c = 0
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
z w : ℂ
⊢ f z = f w
suffices : ∀ c, deriv f c = 0
case this
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
z w : ℂ
⊢ ∀ (c : ℂ), deriv f c = 0
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
z w : ℂ
this : ∀ (c : ℂ), deriv f c = 0
⊢ f z = f w

case this
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
z w : ℂ
⊢ ∀ (c : ℂ), deriv f c = 0
exact is_const_of_deriv_eq_zero hf this z w
case this
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
⊢ ∀ (c : ℂ), deriv f c = 0
case this
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
z w : ℂ
⊢ ∀ (c : ℂ), deriv f c = 0
clear z w
case this
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
c : ℂ
⊢ deriv f c = 0
case this
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
⊢ ∀ (c : ℂ), deriv f c = 0
intro c
case this.intro.intro
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
c : ℂ
C : ℝ
C₀ : C > 0
hC : ∀ (z : ℂ), ‖f z‖ ≤ C
⊢ deriv f c = 0
case this
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
c : ℂ
⊢ deriv f c = 0
obtain ⟨C, C₀, hC⟩ : ∃ C > (0 : ℝ), ∀ z, ‖f z‖ ≤ C := by
  rcases bounded_iff_forall_norm_le.1 hb with ⟨C, hC⟩
  exact
    ⟨max C 1, lt_max_iff.2 (Or.inr zero_lt_one), fun z =>
      (hC (f z) (mem_range_self _)).trans (le_max_left _ _)⟩
case this.intro.intro
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
c : ℂ
C : ℝ
C₀ : C > 0
hC : ∀ (z : ℂ), ‖f z‖ ≤ C
ε : ℝ
ε₀ : 0 < ε
⊢ ‖deriv f c‖ ≤ ε
case this.intro.intro
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
c : ℂ
C : ℝ
C₀ : C > 0
hC : ∀ (z : ℂ), ‖f z‖ ≤ C
⊢ deriv f c = 0
refine' norm_le_zero_iff.1 (le_of_forall_le_of_dense fun ε ε₀ => _)
no goals
case this.intro.intro
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
c : ℂ
C : ℝ
C₀ : C > 0
hC : ∀ (z : ℂ), ‖f z‖ ≤ C
ε : ℝ
ε₀ : 0 < ε
⊢ ‖deriv f c‖ ≤ ε
calc
  ‖deriv f c‖ ≤ C / (C / ε) :=
    norm_deriv_le_of_forall_mem_sphere_norm_le (div_pos C₀ ε₀) hf.diffContOnCl fun z _ => hC z
  _ = ε := div_div_cancel' C₀.lt.ne'
case intro
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
c : ℂ
C : ℝ
hC : ∀ (x : F), x ∈ range f → ‖x‖ ≤ C
⊢ ∃ C, C > 0 ∧ ∀ (z : ℂ), ‖f z‖ ≤ C
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
c : ℂ
⊢ ∃ C, C > 0 ∧ ∀ (z : ℂ), ‖f z‖ ≤ C
rcases bounded_iff_forall_norm_le.1 hb with ⟨C, hC⟩
no goals
case intro
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
c : ℂ
C : ℝ
hC : ∀ (x : F), x ∈ range f → ‖x‖ ≤ C
⊢ ∃ C, C > 0 ∧ ∀ (z : ℂ), ‖f z‖ ≤ C
exact
  ⟨max C 1, lt_max_iff.2 (Or.inr zero_lt_one), fun z =>
    (hC (f z) (mem_range_self _)).trans (le_max_left _ _)⟩