-- Mathlib/Analysis/Complex/Liouville.lean
theorem liouville_theorem_aux {f : ℂ → F} (hf : Differentiable ℂ f) (hb : IsBounded (range f))
    (z w : ℂ) : f z = f w

Proof state:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
z w : ℂ
⊢ ∀ (c : ℂ), deriv f c = 0

Tactic:
clear z w

Result:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
⊢ ∀ (c : ℂ), deriv f c = 0

Proof state:
case intro.intro
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
c : ℂ
C : ℝ
C₀ : C > 0
hC : ∀ (z : ℂ), ‖f z‖ ≤ C
ε : ℝ
ε₀ : 0 < ε
⊢ ‖deriv f c‖ ≤ ε

Tactic:
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'

Result:
no goals

Proof state:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
z w : ℂ
⊢ f z = f w

Tactic:
suffices ∀ c, deriv f c = 0 from is_const_of_deriv_eq_zero hf this z w

Result:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
z w : ℂ
⊢ ∀ (c : ℂ), deriv f c = 0

Proof state:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
⊢ ∀ (c : ℂ), deriv f c = 0

Tactic:
intro c

Result:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
c : ℂ
⊢ deriv f c = 0

Proof state:
case intro.intro
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
c : ℂ
C : ℝ
C₀ : C > 0
hC : ∀ (z : ℂ), ‖f z‖ ≤ C
⊢ deriv f c = 0

Tactic:
refine norm_le_zero_iff.1 (le_of_forall_gt_imp_ge_of_dense fun ε ε₀ => ?_)

Result:
case intro.intro
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
c : ℂ
C : ℝ
C₀ : C > 0
hC : ∀ (z : ℂ), ‖f z‖ ≤ C
ε : ℝ
ε₀ : 0 < ε
⊢ ‖deriv f c‖ ≤ ε

Proof state:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
c : ℂ
⊢ deriv f c = 0

Tactic:
obtain ⟨C, C₀, hC⟩ : ∃ C > (0 : ℝ), ∀ z, ‖f z‖ ≤ C := by
  rcases isBounded_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 _ _)⟩

Result:
case intro.intro
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
c : ℂ
C : ℝ
C₀ : C > 0
hC : ∀ (z : ℂ), ‖f z‖ ≤ C
⊢ deriv f c = 0

Proof state:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
c : ℂ
⊢ ∃ C > 0, ∀ (z : ℂ), ‖f z‖ ≤ C

Tactic:
rcases isBounded_iff_forall_norm_le.1 hb with ⟨C, hC⟩

Result:
case intro
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
c : ℂ
C : ℝ
hC : ∀ x ∈ range f, ‖x‖ ≤ C
⊢ ∃ C > 0, ∀ (z : ℂ), ‖f z‖ ≤ C

Proof state:
case intro
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
c : ℂ
C : ℝ
hC : ∀ x ∈ range f, ‖x‖ ≤ C
⊢ ∃ C > 0, ∀ (z : ℂ), ‖f z‖ ≤ C

Tactic:
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 _ _)⟩

Result:
no goals