-- Mathlib/Analysis/Analytic/Order.lean
theorem isClopen_setOf_order_eq_top (h₁f : AnalyticOnNhd 𝕜 f U) :
    IsClopen { u : U | (h₁f u.1 u.2).order = ⊤ }

Proof state:
case h.right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | ⋯.order = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen t'
h₃t' : ↑z ∈ t'
⊢ IsOpen (Subtype.val ⁻¹' t') ∧ z ∈ Subtype.val ⁻¹' t'

Tactic:
exact ⟨isOpen_induced h₂t', h₃t'⟩

Result:
no goals

Proof state:
case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : ⋯.order = ⊤
⊢ ∃ x ⊆ {x | ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen t ∧ ↑x ∈ t}, IsOpen x ∧ z ∈ x

Tactic:
rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff] at hz

Result:
case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen t ∧ ↑z ∈ t
⊢ ∃ x ⊆ {x | ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen t ∧ ↑x ∈ t}, IsOpen x ∧ z ∈ x

Proof state:
case left
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
⊢ IsClosed {u | ⋯.order = ⊤}

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_forall_mem_open]

Result:
case left
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
⊢ ∀ x ∈ {u | ⋯.order = ⊤}ᶜ, ∃ t ⊆ {u | ⋯.order = ⊤}ᶜ, IsOpen t ∧ x ∈ t

Proof state:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
z : ↑U
t' : Set 𝕜
h₁t' : ∀ y ∈ t', f y = 0
h₂t' : IsOpen t'
h₃t' : ↑z ∈ t'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
h₁w : w = z
⊢ ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen t ∧ ↑w ∈ t

Tactic:
rw [h₁w]

Result:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
z : ↑U
t' : Set 𝕜
h₁t' : ∀ y ∈ t', f y = 0
h₂t' : IsOpen t'
h₃t' : ↑z ∈ t'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
h₁w : w = z
⊢ ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen t ∧ ↑z ∈ t

Proof state:
case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | ⋯.order = ⊤}
⊢ ∃ x ⊆ {x | ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen t ∧ ↑x ∈ t}, IsOpen x ∧ z ∈ x

Tactic:
simp only [mem_setOf_eq] at hz

Result:
case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : ⋯.order = ⊤
⊢ ∃ x ⊆ {x | ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen t ∧ ↑x ∈ t}, IsOpen x ∧ z ∈ x

Proof state:
case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
⊢ ∀ x ∈ {u | ⋯.order = ⊤}, ∃ t ⊆ {u | ⋯.order = ⊤}, IsOpen t ∧ x ∈ t

Tactic:
intro z hz

Result:
case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | ⋯.order = ⊤}
⊢ ∃ t ⊆ {u | ⋯.order = ⊤}, IsOpen t ∧ z ∈ t

Proof state:
case left
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | ⋯.order = ⊤}ᶜ
⊢ ∃ t ⊆ {u | ⋯.order = ⊤}ᶜ, IsOpen t ∧ z ∈ t

Tactic:
rcases (h₁f z.1 z.2).eventually_eq_zero_or_eventually_ne_zero with h | h

Result:
case left.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | ⋯.order = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝 ↑z, f z = 0
⊢ ∃ t ⊆ {u | ⋯.order = ⊤}ᶜ, IsOpen t ∧ z ∈ t

case left.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | ⋯.order = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
⊢ ∃ t ⊆ {u | ⋯.order = ⊤}ᶜ, IsOpen t ∧ z ∈ t

Proof state:
case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | ⋯.order = ⊤}
⊢ ∃ t ⊆ {u | ⋯.order = ⊤}, IsOpen t ∧ z ∈ t

Tactic:
conv =>
  arg 1; intro; left; right; arg 1; intro
  rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff]

Result:
case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | ⋯.order = ⊤}
⊢ ∃ x ⊆ {x | ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen t ∧ ↑x ∈ t}, IsOpen x ∧ z ∈ x

Proof state:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | ⋯.order = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen t'
h₃t' : ↑z ∈ t'
⊢ Subtype.val ⁻¹' t' ⊆ {u | ⋯.order = ⊤}ᶜ ∧ IsOpen (Subtype.val ⁻¹' t') ∧ z ∈ Subtype.val ⁻¹' t'

Tactic:
constructor

Result:
case h.left
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | ⋯.order = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen t'
h₃t' : ↑z ∈ t'
⊢ Subtype.val ⁻¹' t' ⊆ {u | ⋯.order = ⊤}ᶜ

case h.right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | ⋯.order = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen t'
h₃t' : ↑z ∈ t'
⊢ IsOpen (Subtype.val ⁻¹' t') ∧ z ∈ Subtype.val ⁻¹' t'

Proof state:
case right.intro.intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
z : ↑U
t' : Set 𝕜
h₁t' : ∀ y ∈ t', f y = 0
h₂t' : IsOpen t'
h₃t' : ↑z ∈ t'
⊢ ∃ x ⊆ {x | ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen t ∧ ↑x ∈ t}, IsOpen x ∧ z ∈ x

Tactic:
use Subtype.val ⁻¹' t'

Result:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
z : ↑U
t' : Set 𝕜
h₁t' : ∀ y ∈ t', f y = 0
h₂t' : IsOpen t'
h₃t' : ↑z ∈ t'
⊢ Subtype.val ⁻¹' t' ⊆ {x | ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen t ∧ ↑x ∈ t} ∧
    IsOpen (Subtype.val ⁻¹' t') ∧ z ∈ Subtype.val ⁻¹' t'

Proof state:
case left.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | ⋯.order = ⊤}ᶜ
h : ⋯.order = ⊤
⊢ ∃ t ⊆ {u | ⋯.order = ⊤}ᶜ, IsOpen t ∧ z ∈ t

Tactic:
tauto

Result:
no goals