awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
inst_3 : ConnectedSpace 𝕜
hf : AnalyticOnNhd 𝕜 f univ
hg : AnalyticOnNhd 𝕜 g univ
hfg : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = g z
⊢ f = g

Tactic:
funext fun x =>
    eqOn_of_preconnected_of_frequently_eq hf hg isPreconnected_univ (mem_univ z₀) hfg (mem_univ x)

Premises used: AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq, funext, Set.mem_univ, PreconnectedSpace.isPreconnected_univ
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst_1 : NormedRing A
inst_2 : IsDomain A
inst_3 : NormedAlgebra 𝕜 A
B : Type u_4
inst_4 : NormedAddCommGroup B
inst_5 : NormedSpace 𝕜 B
inst_6 : Module A B
inst_7 : IsTorsionFree A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
pos : ∀ (hU' : U = ∅), (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0
neg : ∀ (hU' : ¬U = ∅), (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

Tactic:
by_cases hU' : U = ∅
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst_1 : NormedRing A
inst_2 : IsDomain A
inst_3 : NormedAlgebra 𝕜 A
B : Type u_4
inst_4 : NormedAddCommGroup B
inst_5 : NormedSpace 𝕜 B
inst_6 : Module A B
inst_7 : IsTorsionFree A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : U = ∅
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

Tactic:
simp [hU']
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst_1 : NormedRing A
inst_2 : IsDomain A
inst_3 : NormedAlgebra 𝕜 A
B : Type u_4
inst_4 : NormedAddCommGroup B
inst_5 : NormedSpace 𝕜 B
inst_6 : Module A B
inst_7 : IsTorsionFree A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : ¬U = ∅
⊢ ∃ (z : 𝕜), z ∈ U

Tactic:
nonempty_iff_ne_empty.mpr hU'

Premises used: Iff.mpr, Set.Nonempty, Set.nonempty_iff_ne_empty
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst_1 : NormedRing A
inst_2 : IsDomain A
inst_3 : NormedAlgebra 𝕜 A
B : Type u_4
inst_4 : NormedAddCommGroup B
inst_5 : NormedSpace 𝕜 B
inst_6 : Module A B
inst_7 : IsTorsionFree A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : ¬U = ∅
neg : ∀ (z : 𝕜) (hz : z ∈ U), (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

Tactic:
obtain ⟨z, hz⟩ : ∃ z, z ∈ U := nonempty_iff_ne_empty.mpr hU'

Premises used: Iff.mpr, Set.nonempty_iff_ne_empty
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst_1 : NormedRing A
inst_2 : IsDomain A
inst_3 : NormedAlgebra 𝕜 A
B : Type u_4
inst_4 : NormedAddCommGroup B
inst_5 : NormedSpace 𝕜 B
inst_6 : Module A B
inst_7 : IsTorsionFree A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : ¬U = ∅
z : 𝕜
hz : z ∈ U
pos : ∀ (hU'' : U = {z}), (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0
neg : ∀ (hU'' : ¬U = {z}), (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

Tactic:
by_cases hU'' : U = {z}
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst_1 : NormedRing A
inst_2 : IsDomain A
inst_3 : NormedAlgebra 𝕜 A
B : Type u_4
inst_4 : NormedAddCommGroup B
inst_5 : NormedSpace 𝕜 B
inst_6 : Module A B
inst_7 : IsTorsionFree A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : ¬U = ∅
z : 𝕜
hz : z ∈ U
hU'' : U = {z}
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

Tactic:
simpa [hU''] using hfg z hz
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst_1 : NormedRing A
inst_2 : IsDomain A
inst_3 : NormedAlgebra 𝕜 A
B : Type u_4
inst_4 : NormedAddCommGroup B
inst_5 : NormedSpace 𝕜 B
inst_6 : Module A B
inst_7 : IsTorsionFree A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : ¬U = ∅
z : 𝕜
hz : z ∈ U
hU'' : ¬U = {z}
⊢ U.Nontrivial

Tactic:
apply (nontrivial_iff_ne_singleton hz).mpr at hU''

Premises used: Iff.mpr, Set.nontrivial_iff_ne_singleton
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst_1 : NormedRing A
inst_2 : IsDomain A
inst_3 : NormedAlgebra 𝕜 A
B : Type u_4
inst_4 : NormedAddCommGroup B
inst_5 : NormedSpace 𝕜 B
inst_6 : Module A B
inst_7 : IsTorsionFree A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : ¬U = ∅
z : 𝕜
hz : z ∈ U
hU'' : U.Nontrivial
⊢ ∃ᶠ (w : 𝕜) in 𝓝[≠] z, w ∈ U

Tactic:
have : ∃ᶠ w in 𝓝[≠] z, w ∈ U :=
    frequently_mem_iff_neBot.mpr <| hU.preperfect_of_nontrivial hU'' z hz
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst_1 : NormedRing A
inst_2 : IsDomain A
inst_3 : NormedAlgebra 𝕜 A
B : Type u_4
inst_4 : NormedAddCommGroup B
inst_5 : NormedSpace 𝕜 B
inst_6 : Module A B
inst_7 : IsTorsionFree A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : ¬U = ∅
z : 𝕜
hz : z ∈ U
hU'' : U.Nontrivial
this : ∃ᶠ (w : 𝕜) in 𝓝[≠] z, w ∈ U
w : 𝕜
hw : w ∈ U
⊢ f w = 0 ∨ g w = 0

Tactic:
smul_eq_zero.mp (hfg w hw)

Premises used: Iff.mp, smul_eq_zero
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst_1 : NormedRing A
inst_2 : IsDomain A
inst_3 : NormedAlgebra 𝕜 A
B : Type u_4
inst_4 : NormedAddCommGroup B
inst_5 : NormedSpace 𝕜 B
inst_6 : Module A B
inst_7 : IsTorsionFree A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : ¬U = ∅
z : 𝕜
hz : z ∈ U
hU'' : U.Nontrivial
this : ∃ᶠ (w : 𝕜) in 𝓝[≠] z, w ∈ U
h : ∀ (a : 𝕜), Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (x : 𝕜) ↦ x ∈ U → f x = 0 ∨ g x = 0) x} a
h₁ h₂ : ∀ (w : 𝕜) (hw : w ∈ U), f w = 0 ∨ g w = 0
⊢ ∀ᶠ (x : 𝕜) in 𝓝[≠] z, x ∈ U → f x = 0 ∨ g x = 0

Tactic:
filter_upwards with w hw using smul_eq_zero.mp (hfg w hw)
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst_1 : NormedRing A
inst_2 : IsDomain A
inst_3 : NormedAlgebra 𝕜 A
B : Type u_4
inst_4 : NormedAddCommGroup B
inst_5 : NormedSpace 𝕜 B
inst_6 : Module A B
inst_7 : IsTorsionFree A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : ¬U = ∅
z : 𝕜
hz : z ∈ U
hU'' : U.Nontrivial
this : ∃ᶠ (w : 𝕜) in 𝓝[≠] z, w ∈ U
⊢ ∃ᶠ (w : 𝕜) in 𝓝[≠] z, f w = 0 ∨ g w = 0

Tactic:
have : ∃ᶠ w in 𝓝[≠] z, f w = 0 ∨ g w = 0 :=
    this.mp <| by filter_upwards with w hw using smul_eq_zero.mp (hfg w hw)
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst_1 : NormedRing A
inst_2 : IsDomain A
inst_3 : NormedAlgebra 𝕜 A
B : Type u_4
inst_4 : NormedAddCommGroup B
inst_5 : NormedSpace 𝕜 B
inst_6 : Module A B
inst_7 : IsTorsionFree A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : ¬U = ∅
z : 𝕜
hz : z ∈ U
hU'' : U.Nontrivial
this_1 : ∃ᶠ (w : 𝕜) in 𝓝[≠] z, w ∈ U
this : ∃ᶠ (w : 𝕜) in 𝓝[≠] z, f w = 0 ∨ g w = 0
h : ∃ᶠ (x : 𝕜) in 𝓝[≠] z, f x = 0
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

Tactic:
Or.inl <| hf.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hz h

Premises used: AnalyticOnNhd.eqOn_zero_of_preconnected_of_frequently_eq_zero, Or.inl
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst_1 : NormedRing A
inst_2 : IsDomain A
inst_3 : NormedAlgebra 𝕜 A
B : Type u_4
inst_4 : NormedAddCommGroup B
inst_5 : NormedSpace 𝕜 B
inst_6 : Module A B
inst_7 : IsTorsionFree A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : ¬U = ∅
z : 𝕜
hz : z ∈ U
hU'' : U.Nontrivial
this_1 : ∃ᶠ (w : 𝕜) in 𝓝[≠] z, w ∈ U
this : ∃ᶠ (w : 𝕜) in 𝓝[≠] z, f w = 0 ∨ g w = 0
h : ∃ᶠ (x : 𝕜) in 𝓝[≠] z, f x = 0
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

Tactic:
exact Or.inl <| hf.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hz h

Premises used: AnalyticOnNhd.eqOn_zero_of_preconnected_of_frequently_eq_zero, Or.inl
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst_1 : NormedRing A
inst_2 : IsDomain A
inst_3 : NormedAlgebra 𝕜 A
B : Type u_4
inst_4 : NormedAddCommGroup B
inst_5 : NormedSpace 𝕜 B
inst_6 : Module A B
inst_7 : IsTorsionFree A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : ¬U = ∅
z : 𝕜
hz : z ∈ U
hU'' : U.Nontrivial
this_1 : ∃ᶠ (w : 𝕜) in 𝓝[≠] z, w ∈ U
this : ∃ᶠ (w : 𝕜) in 𝓝[≠] z, f w = 0 ∨ g w = 0
h : ∃ᶠ (x : 𝕜) in 𝓝[≠] z, g x = 0
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

Tactic:
Or.inr <| hg.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hz h

Premises used: AnalyticOnNhd.eqOn_zero_of_preconnected_of_frequently_eq_zero, Or.inr
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst_1 : NormedRing A
inst_2 : IsDomain A
inst_3 : NormedAlgebra 𝕜 A
B : Type u_4
inst_4 : NormedAddCommGroup B
inst_5 : NormedSpace 𝕜 B
inst_6 : Module A B
inst_7 : IsTorsionFree A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : ¬U = ∅
z : 𝕜
hz : z ∈ U
hU'' : U.Nontrivial
this_1 : ∃ᶠ (w : 𝕜) in 𝓝[≠] z, w ∈ U
this : ∃ᶠ (w : 𝕜) in 𝓝[≠] z, f w = 0 ∨ g w = 0
h : ∃ᶠ (x : 𝕜) in 𝓝[≠] z, g x = 0
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

Tactic:
exact Or.inr <| hg.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hz h

Premises used: AnalyticOnNhd.eqOn_zero_of_preconnected_of_frequently_eq_zero, Or.inr
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst_1 : NormedRing A
inst_2 : IsDomain A
inst_3 : NormedAlgebra 𝕜 A
B : Type u_4
inst_4 : NormedAddCommGroup B
inst_5 : NormedSpace 𝕜 B
inst_6 : Module A B
inst_7 : IsTorsionFree A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : ¬U = ∅
z : 𝕜
hz : z ∈ U
hU'' : U.Nontrivial
this_1 : ∃ᶠ (w : 𝕜) in 𝓝[≠] z, w ∈ U
this : ∃ᶠ (w : 𝕜) in 𝓝[≠] z, f w = 0 ∨ g w = 0
⊢ (∃ᶠ (x : 𝕜) in 𝓝[≠] z, f x = 0) ∨ ∃ᶠ (x : 𝕜) in 𝓝[≠] z, g x = 0

Tactic:
cases frequently_or_distrib.mp this with
  | inl h => exact Or.inl <| hf.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hz h
  | inr h => exact Or.inr <| hg.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hz h

Premises used: Iff.mp, Or.inl, Or.inr, Filter.frequently_or_distrib
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst_1 : NormedRing A
inst_2 : IsDomain A
inst_3 : NormedAlgebra 𝕜 A
f g : 𝕜 → A
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z * g z = 0
hU : IsPreconnected U
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

Tactic:
eq_zero_or_eq_zero_of_smul_eq_zero hf hg hfg hU

Premises used: AnalyticOnNhd.eq_zero_or_eq_zero_of_smul_eq_zero
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
s : Set E
hfx : AnalyticAt 𝕜 f x
h₂f : ¬EventuallyConst f (𝓝 x)
hs : s ∈ 𝓝[≠] f x
h : ∀ a ∈ f ⁻¹' insert (f x) s, f a ∈ insert (f x) s
⊢ ∀ᶠ (z : 𝕜) in 𝓝 x, f z ∈ insert (f x) s

Tactic:
filter_upwards [hfx.continuousAt.preimage_mem_nhds (insert_mem_nhds_iff.2 hs)]

Premises used: Iff.mpr, ContinuousAt.preimage_mem_nhds, AnalyticAt.continuousAt, insert_mem_nhds_iff
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
s : Set E
hfx : AnalyticAt 𝕜 f x
h₂f : ¬EventuallyConst f (𝓝 x)
hs : s ∈ 𝓝[≠] f x
h h₁ h₂ : ∀ a ∈ f ⁻¹' insert (f x) s, f a ∈ insert (f x) s
⊢ ∀ a ∈ f ⁻¹' insert (f x) s, f a ∈ insert (f x) s

Tactic:
tauto
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
s : Set E
hfx : AnalyticAt 𝕜 f x
h₂f : ¬EventuallyConst f (𝓝 x)
hs : s ∈ 𝓝[≠] f x
⊢ ∀ᶠ (z : 𝕜) in 𝓝 x, f z ∈ insert (f x) s

Tactic:
have : ∀ᶠ (z : 𝕜) in 𝓝 x, f z ∈ insert (f x) s := by
    filter_upwards [hfx.continuousAt.preimage_mem_nhds (insert_mem_nhds_iff.2 hs)]
    tauto
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
s : Set E
hfx : AnalyticAt 𝕜 f x
h₂f : ¬EventuallyConst f (𝓝 x)
hs : s ∈ 𝓝[≠] f x
this : ∀ᶠ (z : 𝕜) in 𝓝 x, f z ∈ insert (f x) s
contrapose : ∀ (h : ¬f ⁻¹' s ∈ 𝓝[≠] x), EventuallyConst f (𝓝 x)
⊢ f ⁻¹' s ∈ 𝓝[≠] x

Tactic:
contrapose h₂f with h
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
s : Set E
hfx : AnalyticAt 𝕜 f x
hs : s ∈ 𝓝[≠] f x
this : ∀ᶠ (z : 𝕜) in 𝓝 x, f z ∈ insert (f x) s
h : ¬f ⁻¹' s ∈ 𝓝[≠] x
rw : ∃ (c : E), f =ᶠ[𝓝 x] fun (x : 𝕜) ↦ c
⊢ EventuallyConst f (𝓝 x)

Tactic:
rw [eventuallyConst_iff_exists_eventuallyEq]

Premises used: Filter.eventuallyConst_iff_exists_eventuallyEq
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
s : Set E
hfx : AnalyticAt 𝕜 f x
hs : s ∈ 𝓝[≠] f x
this : ∀ᶠ (z : 𝕜) in 𝓝 x, f z ∈ insert (f x) s
h : ¬f ⁻¹' s ∈ 𝓝[≠] x
h₁ : f =ᶠ[𝓝 x] fun (x_1 : 𝕜) ↦ f x
⊢ ∃ (c : E), f =ᶠ[𝓝 x] fun (x : 𝕜) ↦ c

Tactic:
use f x
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
s : Set E
hfx : AnalyticAt 𝕜 f x
hs : s ∈ 𝓝[≠] f x
this : ∀ᶠ (z : 𝕜) in 𝓝 x, f z ∈ insert (f x) s
h : ¬f ⁻¹' s ∈ 𝓝[≠] x
h₁ : ∃ᶠ (z : 𝕜) in 𝓝[≠] x, f z = f x
⊢ f =ᶠ[𝓝 x] fun (x_1 : 𝕜) ↦ f x

Tactic:
rw [EventuallyEq, ← hfx.frequently_eq_iff_eventually_eq analyticAt_const]

Premises used: Filter.EventuallyEq, analyticAt_const, AnalyticAt.frequently_eq_iff_eventually_eq
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
s : Set E
hfx : AnalyticAt 𝕜 f x
hs : s ∈ 𝓝[≠] f x
this : ∀ᶠ (z : 𝕜) in 𝓝 x, f z ∈ insert (f x) s
h : ¬f ⁻¹' s ∈ 𝓝[≠] x
h₁ : ∀ (x_1 : 𝕜), (f x_1 ∈ s → False) ∧ f x_1 ∈ insert (f x) s → f x_1 = f x
⊢ ∃ᶠ (z : 𝕜) in 𝓝[≠] x, f z = f x

Tactic:
apply ((frequently_imp_distrib_right.2 h).and_eventually
    (eventually_nhdsWithin_of_eventually_nhds this)).mono

Premises used: Iff.mpr, eventually_nhdsWithin_of_eventually_nhds, Filter.Frequently.mono, Filter.Frequently.and_eventually, Filter.frequently_imp_distrib_right
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
s : Set E
hfx : AnalyticAt 𝕜 f x
hs : s ∈ 𝓝[≠] f x
this : ∀ᶠ (z : 𝕜) in 𝓝 x, f z ∈ insert (f x) s
h : ¬f ⁻¹' s ∈ 𝓝[≠] x
z : 𝕜
h₁ : ∀ (h₁z : f z ∈ s → False) (h₂z : f z ∈ insert (f x) s), f z = f x
⊢ (f z ∈ s → False) ∧ f z ∈ insert (f x) s → f z = f x

Tactic:
⟨h₁z, h₂z⟩
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
s : Set E
hfx : AnalyticAt 𝕜 f x
hs : s ∈ 𝓝[≠] f x
this : ∀ᶠ (z : 𝕜) in 𝓝 x, f z ∈ insert (f x) s
h : ¬f ⁻¹' s ∈ 𝓝[≠] x
z : 𝕜
h₁z : f z ∈ s → False
h₂z : f z ∈ insert (f x) s
⊢ f z = f x ∨ f z ∈ s

Tactic:
rw [Set.mem_insert_iff] at h₂z

Premises used: Set.mem_insert_iff
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
s : Set E
hfx : AnalyticAt 𝕜 f x
hs : s ∈ 𝓝[≠] f x
this : ∀ᶠ (z : 𝕜) in 𝓝 x, f z ∈ insert (f x) s
h : ¬f ⁻¹' s ∈ 𝓝[≠] x
z : 𝕜
h₁z : f z ∈ s → False
h₂z : f z = f x ∨ f z ∈ s
h₁ : ∀ (h₂z : f z = f x), f z = f x
h₂ : ∀ (h₂z : f z ∈ s), f z = f x
h₃ h₄ : ∀ (h₂z : f z = f x), f z = f x
⊢ f z = f x

Tactic:
tauto
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
hfx : AnalyticAt 𝕜 f x
h₂f : ¬EventuallyConst f (𝓝 x)
⊢ map f (𝓝[≠] x) ≤ 𝓝[≠] f x

Tactic:
fun _ hs ↦ mem_map.1 (preimage_of_nhdsNE hfx h₂f hs)

Premises used: Set.Mem, setOf, AnalyticAt.preimage_of_nhdsNE, Set.preimage, Iff.mp, Filter.mem_map
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
s : Set E
f : 𝕜 → E
hfU : AnalyticOnNhd 𝕜 f U
h₂f : ∀ x ∈ U, ¬EventuallyConst f (𝓝 x)
hs : s ∈ codiscreteWithin (f '' U)
simp_rw : ∀ (hs : ∀ x ∈ f '' U, s ∪ (f '' U)ᶜ ∈ 𝓝[≠] x), ∀ x ∈ U, f ⁻¹' s ∪ Uᶜ ∈ 𝓝[≠] x
⊢ f ⁻¹' s ∈ codiscreteWithin U

Tactic:
simp_rw [mem_codiscreteWithin, disjoint_principal_right, Set.compl_diff] at *

Premises used: mem_codiscreteWithin, Set.compl_diff, Filter.disjoint_principal_right
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
s : Set E
f : 𝕜 → E
hfU : AnalyticOnNhd 𝕜 f U
h₂f : ∀ x ∈ U, ¬EventuallyConst f (𝓝 x)
hs : ∀ x ∈ f '' U, s ∪ (f '' U)ᶜ ∈ 𝓝[≠] x
x : 𝕜
hx : x ∈ U
⊢ f x ∈ f '' U

Tactic:
tauto
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
s : Set E
f : 𝕜 → E
hfU : AnalyticOnNhd 𝕜 f U
h₂f : ∀ x ∈ U, ¬EventuallyConst f (𝓝 x)
hs : ∀ x ∈ f '' U, s ∪ (f '' U)ᶜ ∈ 𝓝[≠] x
x : 𝕜
hx : x ∈ U
apply : f ⁻¹' (s ∪ (f '' U)ᶜ) ⊆ f ⁻¹' s ∪ Uᶜ
⊢ f ⁻¹' s ∪ Uᶜ ∈ 𝓝[≠] x

Tactic:
apply mem_of_superset ((hfU x hx).preimage_of_nhdsNE (h₂f x hx) (hs (f x) (by tauto)))

Premises used: AnalyticAt.preimage_of_nhdsNE, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
s : Set E
f : 𝕜 → E
hfU : AnalyticOnNhd 𝕜 f U
h₂f : ∀ x ∈ U, ¬EventuallyConst f (𝓝 x)
hs : ∀ x ∈ f '' U, s ∪ (f '' U)ᶜ ∈ 𝓝[≠] x
x : 𝕜
hx : x ∈ U
rw : f ⁻¹' s ∪ (f ⁻¹' f '' U)ᶜ ⊆ f ⁻¹' s ∪ Uᶜ
⊢ f ⁻¹' (s ∪ (f '' U)ᶜ) ⊆ f ⁻¹' s ∪ Uᶜ

Tactic:
rw [preimage_union, preimage_compl]

Premises used: Set.preimage_union, Set.preimage_compl
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
s : Set E
f : 𝕜 → E
hfU : AnalyticOnNhd 𝕜 f U
h₂f : ∀ x ∈ U, ¬EventuallyConst f (𝓝 x)
hs : ∀ x ∈ f '' U, s ∪ (f '' U)ᶜ ∈ 𝓝[≠] x
x : 𝕜
hx : x ∈ U
apply : (f ⁻¹' f '' U)ᶜ ⊆ Uᶜ
⊢ f ⁻¹' s ∪ (f ⁻¹' f '' U)ᶜ ⊆ f ⁻¹' s ∪ Uᶜ

Tactic:
apply union_subset_union_right (f ⁻¹' s)

Premises used: Set.union_subset_union_right, Set.preimage
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
s : Set E
f : 𝕜 → E
hfU : AnalyticOnNhd 𝕜 f U
h₂f : ∀ x ∈ U, ¬EventuallyConst f (𝓝 x)
hs : ∀ x ∈ f '' U, s ∪ (f '' U)ᶜ ∈ 𝓝[≠] x
x_1 : 𝕜
hx_1 : x_1 ∈ U
x : 𝕜
hx : x ∈ (f ⁻¹' f '' U)ᶜ
⊢ ¬∃ x_2 ∈ U, f x_2 = f x

Tactic:
push _ ∈ _ at hx ⊢
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
s : Set E
f : 𝕜 → E
hfU : AnalyticOnNhd 𝕜 f U
h₂f : ∀ x ∈ U, ¬EventuallyConst f (𝓝 x)
hs : ∀ x ∈ f '' U, s ∪ (f '' U)ᶜ ∈ 𝓝[≠] x
x_1 : 𝕜
hx_1 : x_1 ∈ U
x : 𝕜
hx : ¬∃ x_2 ∈ U, f x_2 = f x
⊢ ∀ (x_2 : 𝕜) (_ : x_2 ∈ U), f x_2 ≠ f x

Tactic:
push Not at hx

Premises used: Not
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
s : Set E
f : 𝕜 → E
hfU : AnalyticOnNhd 𝕜 f U
h₂f : ∀ x ∈ U, ¬EventuallyConst f (𝓝 x)
hs : ∀ x ∈ f '' U, s ∪ (f '' U)ᶜ ∈ 𝓝[≠] x
x_1 : 𝕜
hx_1 : x_1 ∈ U
x : 𝕜
hx : ∀ (x_2 : 𝕜) (_ : x_2 ∈ U), f x_2 ≠ f x
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ : x ∈ U → False
⊢ x ∉ U

Tactic:
tauto
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hfU : AnalyticOnNhd 𝕜 f U
h₂f : ∀ x ∈ U, ¬EventuallyConst f (𝓝 x)
⊢ map f (codiscreteWithin U) ≤ codiscreteWithin (f '' U)

Tactic:
fun _ hs ↦ mem_map.1 (preimage_mem_codiscreteWithin hfU h₂f hs)

Premises used: Set.Mem, setOf, Set.preimage, AnalyticOnNhd.preimage_mem_codiscreteWithin, Iff.mp, Filter.mem_map
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (iteratedFDerivWithin 𝕜 0 f s) (p.iteratedFDerivSeries 0) s x r

Tactic:
(continuousMultilinearCurryFin0 𝕜 E F).symm
      |>.toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall h

Premises used: LinearIsometryEquiv.symm, continuousMultilinearCurryFin0, iteratedFDerivWithin, ContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall, ContinuousMultilinearMap.constOfIsEmpty, LinearIsometryEquiv.toContinuousLinearEquiv, ContinuousMultilinearMap.uncurry0, FormalMultilinearSeries.iteratedFDerivSeries, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (iteratedFDerivWithin 𝕜 0 f s) (p.iteratedFDerivSeries 0) s x r

Tactic:
exact (continuousMultilinearCurryFin0 𝕜 E F).symm
      |>.toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall h

Premises used: LinearIsometryEquiv.symm, continuousMultilinearCurryFin0, ContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall, LinearIsometryEquiv.toContinuousLinearEquiv, ContinuousLinearEquiv.toContinuousLinearMap