-- Mathlib/Analysis/Analytic/IsolatedZeros.lean
theorem eqOn_zero_or_eventually_ne_zero_of_preconnected (hf : AnalyticOnNhd 𝕜 f U)
    (hU : IsPreconnected U) : EqOn f 0 U ∨ ∀ᶠ x in codiscreteWithin U, f x ≠ 0

Proof state:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
x : 𝕜
hx : x ∈ U
hx2 : (U \ {x | ¬f x = 0})ᶜ ∉ 𝓝[≠] x
nh : ∀ᶠ (x : 𝕜) in 𝓝[≠] x, ¬(fun z => f z = 0) x
a : 𝕜
ha : ¬f a = 0
⊢ a ∈ (U \ {x | ¬f x = 0})ᶜ

Tactic:
simp_all

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 : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
⊢ EqOn f 0 U ∨ ∀ᶠ (x : 𝕜) in codiscreteWithin U, f x ≠ 0

Tactic:
simp only [or_iff_not_imp_right, ne_eq, eventually_iff, mem_codiscreteWithin,
  disjoint_principal_right, not_forall]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
⊢ (∃ x, ∃ (_ : x ∈ U), (U \ {x | ¬f x = 0})ᶜ ∉ 𝓝[≠] x) → EqOn f 0 U

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
x : 𝕜
hx : x ∈ U
hx2 : (U \ {x | ¬f x = 0})ᶜ ∉ 𝓝[≠] x
⊢ EqOn f 0 U

Tactic:
refine hf.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hx fun nh ↦ hx2 ?_

Result:
case intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
x : 𝕜
hx : x ∈ U
hx2 : (U \ {x | ¬f x = 0})ᶜ ∉ 𝓝[≠] x
nh : ∀ᶠ (x : 𝕜) in 𝓝[≠] x, ¬(fun z => f z = 0) x
⊢ (U \ {x | ¬f x = 0})ᶜ ∈ 𝓝[≠] x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
⊢ (∃ x, ∃ (_ : x ∈ U), (U \ {x | ¬f x = 0})ᶜ ∉ 𝓝[≠] x) → EqOn f 0 U

Tactic:
rintro ⟨x, hx, hx2⟩

Result:
case intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
x : 𝕜
hx : x ∈ U
hx2 : (U \ {x | ¬f x = 0})ᶜ ∉ 𝓝[≠] x
⊢ EqOn f 0 U

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
x : 𝕜
hx : x ∈ U
hx2 : (U \ {x | ¬f x = 0})ᶜ ∉ 𝓝[≠] x
nh : ∀ᶠ (x : 𝕜) in 𝓝[≠] x, ¬(fun z => f z = 0) x
⊢ (U \ {x | ¬f x = 0})ᶜ ∈ 𝓝[≠] x

Tactic:
filter_upwards [nh] with a ha

Result:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
x : 𝕜
hx : x ∈ U
hx2 : (U \ {x | ¬f x = 0})ᶜ ∉ 𝓝[≠] x
nh : ∀ᶠ (x : 𝕜) in 𝓝[≠] x, ¬(fun z => f z = 0) x
a : 𝕜
ha : ¬f a = 0
⊢ a ∈ (U \ {x | ¬f x = 0})ᶜ