-- 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
𝕜 : 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}

Tactic:
intro w hw

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'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
⊢ w ∈ {x | ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen t ∧ ↑x ∈ t}

Proof state:
case left.inr.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
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'
⊢ ∃ t ⊆ {u | ⋯.order = ⊤}ᶜ, IsOpen t ∧ z ∈ t

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

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
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
⊢ w ∈ (fun ⦃w⦄ => t' ↑w) \ fun ⦃w⦄ => {↑z} ↑w

Tactic:
exact ⟨hw, mem_singleton_iff.not.1 (Subtype.coe_ne_coe.2 h₁w)⟩

Result:
no goals

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
⊢ ∀ x ∈ {u | ⋯.order = ⊤}ᶜ, ∃ t ⊆ {u | ⋯.order = ⊤}ᶜ, IsOpen t ∧ x ∈ t

Tactic:
intro z hz

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
z : ↑U
hz : z ∈ {u | ⋯.order = ⊤}ᶜ
⊢ ∃ t ⊆ {u | ⋯.order = ⊤}ᶜ, IsOpen t ∧ z ∈ t

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
t' : Set 𝕜
h₁t' : ∀ y ∈ t', f y = 0
h₂t' : IsOpen t'
h₃t' : ↑z ∈ t'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
⊢ w ∈ {x | ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen t ∧ ↑x ∈ t}

Tactic:
simp only [mem_setOf_eq]

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'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
⊢ ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen t ∧ ↑w ∈ t

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

Tactic:
constructor

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
⊢ IsClosed {u | ⋯.order = ⊤}

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
⊢ IsOpen {u | ⋯.order = ⊤}

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

Tactic:
simp only [mem_compl_iff, mem_singleton_iff, isOpen_induced h₂t', mem_preimage,
  h₃t', and_self, and_true]

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}

Proof state:
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'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
⊢ ¬⋯.order = ⊤

Tactic:
by_cases h₁w : w = z

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
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'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
h₁w : w = z
⊢ ¬⋯.order = ⊤

case neg
𝕜 : 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'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
h₁w : ¬w = z
⊢ ¬⋯.order = ⊤

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 : ∀ᶠ (z : 𝕜) in 𝓝 ↑z, f z = 0
⊢ ∃ t ⊆ {u | ⋯.order = ⊤}ᶜ, IsOpen t ∧ z ∈ t

Tactic:
rw [← (h₁f z.1 z.2).order_eq_top_iff] at 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 : ⋯.order = ⊤
⊢ ∃ t ⊆ {u | ⋯.order = ⊤}ᶜ, IsOpen t ∧ z ∈ t

Proof state:
case neg
𝕜 : 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'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
h₁w : ¬w = z
⊢ ¬⋯.order = ⊤

Tactic:
rw [(h₁f _ w.2).order_eq_zero_iff.2 ((h₁t' w hw) (Subtype.coe_ne_coe.mpr h₁w))]

Result:
case neg
𝕜 : 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'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
h₁w : ¬w = z
⊢ ¬0 = ⊤