Theorem: hurwitz_1 (RMT4/hurwitz.lean)

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
⊢ EqOn f 0 U ∨ ∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
Tactic:
refine or_iff_not_imp_right.2 (λ h => ?_)
State after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
h : ¬∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
⊢ EqOn f 0 U

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
h : ¬∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
⊢ EqOn f 0 U
Tactic:
obtain ⟨z₀, h1, h2⟩ : ∃ z₀ ∈ U, ∃ᶠ z in 𝓝[≠] z₀, f z = 0 := by simpa [not_forall] using h
State after:
case intro.intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀✝ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
h : ¬∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
z₀ : ℂ
h1 : z₀ ∈ U
h2 : ∃ᶠ (z : ℂ) in 𝓝[≠] z₀, f z = 0
⊢ EqOn f 0 U

State before:
case intro.intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀✝ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
h : ¬∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
z₀ : ℂ
h1 : z₀ ∈ U
h2 : ∃ᶠ (z : ℂ) in 𝓝[≠] z₀, f z = 0
⊢ EqOn f 0 U
Tactic:
exact (hf.analyticOn hU).eqOn_zero_of_preconnected_of_frequently_eq_zero hU' h1 h2
State after:
no goals

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
h : ¬∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
⊢ ∃ z₀ ∈ U, ∃ᶠ (z : ℂ) in 𝓝[≠] z₀, f z = 0
Tactic:
simpa [not_forall] using h
State after:
no goals