-- Mathlib/Analysis/Complex/Liouville.lean
theorem eq_const_of_tendsto_cocompact [Nontrivial E] {f : E → F} (hf : Differentiable ℂ f) {c : F}
    (hb : Tendsto f (cocompact E) (𝓝 c)) : f = Function.const E c

Proof state:
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
h_bdd : Bornology.IsBounded (range f)
⊢ f = const E c

Tactic:
obtain ⟨c', hc'⟩ := hf.exists_eq_const_of_bounded h_bdd

Result:
case intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
h_bdd : Bornology.IsBounded (range f)
c' : F
hc' : f = const E c'
⊢ f = const E c

Proof state:
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
⊢ f = const E c

Tactic:
have h_bdd : Bornology.IsBounded (Set.range f) := by
  obtain ⟨s, hs, hs_bdd⟩ := Metric.exists_isBounded_image_of_tendsto hb
  obtain ⟨t, ht, hts⟩ := mem_cocompact.mp hs
  apply ht.image hf.continuous |>.isBounded.union hs_bdd |>.subset
  simpa [Set.image_union, Set.image_univ] using Set.image_subset _ <| calc
    Set.univ = t ∪ tᶜ := t.union_compl_self.symm
    _        ⊆ t ∪ s  := by gcongr

Result:
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
h_bdd : Bornology.IsBounded (range f)
⊢ f = const E c

Proof state:
case h.e'_3.h.e'_3
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
h_bdd : Bornology.IsBounded (range f)
c' : F
hc' : f = const E c'
⊢ c = c'

Tactic:
exact tendsto_nhds_unique hb (by simpa [hc'] using tendsto_const_nhds)

Result:
no goals

Proof state:
case intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
h_bdd : Bornology.IsBounded (range f)
c' : F
hc' : f = const E c'
⊢ f = const E c

Tactic:
convert hc'

Result:
case h.e'_3.h.e'_3
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
h_bdd : Bornology.IsBounded (range f)
c' : F
hc' : f = const E c'
⊢ c = c'

Proof state:
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
h_bdd : Bornology.IsBounded (range f)
c' : F
hc' : f = const E c'
⊢ Tendsto f (cocompact E) (𝓝 c')

Tactic:
simpa [hc'] using tendsto_const_nhds

Result:
no goals

Proof state:
case intro.intro.intro.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
s : Set E
hs : s ∈ cocompact E
hs_bdd : Bornology.IsBounded (f '' s)
t : Set E
ht : IsCompact t
hts : tᶜ ⊆ s
⊢ Bornology.IsBounded (range f)

Tactic:
apply ht.image hf.continuous |>.isBounded.union hs_bdd |>.subset

Result:
case intro.intro.intro.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
s : Set E
hs : s ∈ cocompact E
hs_bdd : Bornology.IsBounded (f '' s)
t : Set E
ht : IsCompact t
hts : tᶜ ⊆ s
⊢ range f ⊆ f '' t ∪ f '' s

Proof state:
case intro.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
s : Set E
hs : s ∈ cocompact E
hs_bdd : Bornology.IsBounded (f '' s)
⊢ Bornology.IsBounded (range f)

Tactic:
obtain ⟨t, ht, hts⟩ := mem_cocompact.mp hs

Result:
case intro.intro.intro.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
s : Set E
hs : s ∈ cocompact E
hs_bdd : Bornology.IsBounded (f '' s)
t : Set E
ht : IsCompact t
hts : tᶜ ⊆ s
⊢ Bornology.IsBounded (range f)

Proof state:
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
⊢ Bornology.IsBounded (range f)

Tactic:
obtain ⟨s, hs, hs_bdd⟩ := Metric.exists_isBounded_image_of_tendsto hb

Result:
case intro.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
s : Set E
hs : s ∈ cocompact E
hs_bdd : Bornology.IsBounded (f '' s)
⊢ Bornology.IsBounded (range f)

Proof state:
case intro.intro.intro.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
s : Set E
hs : s ∈ cocompact E
hs_bdd : Bornology.IsBounded (f '' s)
t : Set E
ht : IsCompact t
hts : tᶜ ⊆ s
⊢ range f ⊆ f '' t ∪ f '' s

Tactic:
simpa [Set.image_union, Set.image_univ] using Set.image_subset _ <| calc
  Set.univ = t ∪ tᶜ := t.union_compl_self.symm
  _        ⊆ t ∪ s  := by gcongr

Result:
no goals

Proof state:
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
s : Set E
hs : s ∈ cocompact E
hs_bdd : Bornology.IsBounded (f '' s)
t : Set E
ht : IsCompact t
hts : tᶜ ⊆ s
⊢ t ∪ tᶜ ⊆ t ∪ s

Tactic:
gcongr

Result:
no goals