-- Mathlib/Analysis/Meromorphic/Order.lean
theorem exists_order_ne_top_iff_forall (hU : IsConnected U) :
    (∃ u : U, (hf u u.2).order ≠ ⊤) ↔ (∀ u : U, (hf u u.2).order ≠ ⊤)

Proof state:
case mp.inr.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU✝ : IsConnected U
this : PreconnectedSpace ↑U
h : {u | ⋯.order = ⊤} = univ
u : ↑U
hU : ⋯.order ≠ ⊤
⊢ ∀ (u : ↑U), ⋯.order ≠ ⊤

Tactic:
have : u ∈ univ := by trivial

Result:
case mp.inr.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU✝ : IsConnected U
this✝ : PreconnectedSpace ↑U
h : {u | ⋯.order = ⊤} = univ
u : ↑U
hU : ⋯.order ≠ ⊤
this : u ∈ univ
⊢ ∀ (u : ↑U), ⋯.order ≠ ⊤

Proof state:
case mp.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∃ u, ⋯.order ≠ ⊤
this : PreconnectedSpace ↑U
h : {u | ⋯.order = ⊤} = ∅
u : ↑U
⊢ ⋯.order ≠ ⊤

Tactic:
have : u ∉ (∅ : Set U) := by exact fun a => a

Result:
case mp.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∃ u, ⋯.order ≠ ⊤
this✝ : PreconnectedSpace ↑U
h : {u | ⋯.order = ⊤} = ∅
u : ↑U
this : u ∉ ∅
⊢ ⋯.order ≠ ⊤

Proof state:
case mp.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∃ u, ⋯.order ≠ ⊤
this : PreconnectedSpace ↑U
h : {u | ⋯.order = ⊤} = univ
⊢ ∀ (u : ↑U), ⋯.order ≠ ⊤

Tactic:
obtain ⟨u, hU⟩ := h₂f

Result:
case mp.inr.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU✝ : IsConnected U
this : PreconnectedSpace ↑U
h : {u | ⋯.order = ⊤} = univ
u : ↑U
hU : ⋯.order ≠ ⊤
⊢ ∀ (u : ↑U), ⋯.order ≠ ⊤

Proof state:
case mp.inr.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU✝ : IsConnected U
this✝ : PreconnectedSpace ↑U
h : {u | ⋯.order = ⊤} = univ
u : ↑U
hU : ⋯.order ≠ ⊤
this : u ∈ univ
⊢ ∀ (u : ↑U), ⋯.order ≠ ⊤

Tactic:
rw [← h] at this

Result:
case mp.inr.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU✝ : IsConnected U
this✝ : PreconnectedSpace ↑U
h : {u | ⋯.order = ⊤} = univ
u : ↑U
hU : ⋯.order ≠ ⊤
this : u ∈ {u | ⋯.order = ⊤}
⊢ ∀ (u : ↑U), ⋯.order ≠ ⊤

Proof state:
case mp.inr.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU✝ : IsConnected U
this✝ : PreconnectedSpace ↑U
h : {u | ⋯.order = ⊤} = univ
u : ↑U
hU : ⋯.order ≠ ⊤
this : u ∈ {u | ⋯.order = ⊤}
⊢ ∀ (u : ↑U), ⋯.order ≠ ⊤

Tactic:
tauto

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∃ u, ⋯.order ≠ ⊤
this : PreconnectedSpace ↑U
h : {u | ⋯.order = ⊤} = ∅
u : ↑U
⊢ u ∉ ∅

Tactic:
exact fun a => a

Result:
no goals

Proof state:
case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
⊢ (∀ (u : ↑U), ⋯.order ≠ ⊤) → ∃ u, ⋯.order ≠ ⊤

Tactic:
intro h₂f

Result:
case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∀ (u : ↑U), ⋯.order ≠ ⊤
⊢ ∃ u, ⋯.order ≠ ⊤

Proof state:
case mpr.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∀ (u : ↑U), ⋯.order ≠ ⊤
v : 𝕜
hv : v ∈ U
⊢ ∃ u, ⋯.order ≠ ⊤

Tactic:
use ⟨v, hv⟩, h₂f ⟨v, hv⟩

Result:
no goals

Proof state:
case mp.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∃ u, ⋯.order ≠ ⊤
this✝ : PreconnectedSpace ↑U
h : {u | ⋯.order = ⊤} = ∅
u : ↑U
this : u ∉ {u | ⋯.order = ⊤}
⊢ ⋯.order ≠ ⊤

Tactic:
tauto

Result:
no goals

Proof state:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∃ u, ⋯.order ≠ ⊤
⊢ ∀ (u : ↑U), ⋯.order ≠ ⊤

Tactic:
have := isPreconnected_iff_preconnectedSpace.1 hU.isPreconnected

Result:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∃ u, ⋯.order ≠ ⊤
this : PreconnectedSpace ↑U
⊢ ∀ (u : ↑U), ⋯.order ≠ ⊤

Proof state:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
⊢ (∃ u, ⋯.order ≠ ⊤) → ∀ (u : ↑U), ⋯.order ≠ ⊤

Tactic:
intro h₂f

Result:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∃ u, ⋯.order ≠ ⊤
⊢ ∀ (u : ↑U), ⋯.order ≠ ⊤

Proof state:
case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∀ (u : ↑U), ⋯.order ≠ ⊤
⊢ ∃ u, ⋯.order ≠ ⊤

Tactic:
obtain ⟨v, hv⟩ := hU.nonempty

Result:
case mpr.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∀ (u : ↑U), ⋯.order ≠ ⊤
v : 𝕜
hv : v ∈ U
⊢ ∃ u, ⋯.order ≠ ⊤

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU✝ : IsConnected U
this : PreconnectedSpace ↑U
h : {u | ⋯.order = ⊤} = univ
u : ↑U
hU : ⋯.order ≠ ⊤
⊢ u ∈ univ

Tactic:
trivial

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
⊢ (∃ u, ⋯.order ≠ ⊤) ↔ ∀ (u : ↑U), ⋯.order ≠ ⊤

Tactic:
constructor

Result:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
⊢ (∃ u, ⋯.order ≠ ⊤) → ∀ (u : ↑U), ⋯.order ≠ ⊤

case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
⊢ (∀ (u : ↑U), ⋯.order ≠ ⊤) → ∃ u, ⋯.order ≠ ⊤