awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
hg_ne : g z₀ ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
⊢ ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
have mp : ∀ (hg_ne : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0), g z₀ = 0
Tactic: contrapose hg_ne
Cleared hypotheses: hg_ne
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
hg_ne : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ g z₀ = 0
have mp : g =ᶠ[𝓝 z₀] fun {z₀ : 𝕜} ↦ 0
Tactic: apply EventuallyEq.eq_of_nhds
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
hg_ne : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ g =ᶠ[𝓝 z₀] fun {z₀ : 𝕜} ↦ 0
have mp : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, g z = 0
Tactic: rw [EventuallyEq, ← AnalyticAt.frequently_eq_iff_eventually_eq hg_an analyticAt_const]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
hg_ne : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, g z = 0
have mp : ∀ᶠ (x : 𝕜) in 𝓝 z₀, Membership.mem (γ := Set 𝕜) {z₀}ᶜ x → g x = 0
Tactic: refine (eventually_nhdsWithin_iff.mpr ?_).frequently
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
hg_ne : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ ∀ᶠ (x : 𝕜) in 𝓝 z₀, Membership.mem (γ := Set 𝕜) {z₀}ᶜ x → g x = 0
have h : ∀ (z : 𝕜) (hf_eq : f z = (z - z₀) ^ n • g z) (hf0 : f z = 0) (hz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z), g z = 0
Tactic: filter_upwards [hg_eq, hg_ne] with z hf_eq hf0 hz
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
hg_ne : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
z : 𝕜
hf_eq : f z = (z - z₀) ^ n • g z
hf0 : f z = 0
hz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z
⊢ g z = 0
have h : ∀ (hf_eq : (z - z₀) ^ n • g z = 0) (hf0 : f z = 0) (hz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z), (z - z₀) ^ n ≠ 0
Tactic: rwa [hf0, eq_comm, smul_eq_zero_iff_right] at hf_eq
Cleared hypotheses: hf_eq, hf0, hz
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hf_ne : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ ∃ (n : ℕ) (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
have mpr : ∀ (p : FormalMultilinearSeries 𝕜 𝕜 E) (hp : HasFPowerSeriesAt f p z₀),
  ∃ (n : ℕ) (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
Tactic: rcases hf with ⟨p, hp⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
⊢ EqOn f 0 U ∨ ∀ᶠ (x : 𝕜) in codiscreteWithin U, f x ≠ 0
have simp : (∃ (x : 𝕜) (_ : x ∈ U), (U \ {x : 𝕜 | ¬f x = 0})ᶜ ∉ 𝓝[≠] x) → EqOn f 0 U
Tactic: simp only [or_iff_not_imp_right, ne_eq, eventually_iff, mem_codiscreteWithin,
    disjoint_principal_right, not_forall]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : 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
have refine : ∀ (nh : ∀ᶠ (x : 𝕜) in 𝓝[≠] x, ¬(fun (z : 𝕜) ↦ f z = 0) x), (U \ {x : 𝕜 | ¬f x = 0})ᶜ ∈ 𝓝[≠] x
Tactic: refine hf.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hx fun nh ↦ hx2 ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : 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
have h : ∀ (a : 𝕜) (ha : ¬f a = 0), a ∈ (U \ {x : 𝕜 | ¬f x = 0})ᶜ
Tactic: filter_upwards [nh] with a ha
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
h₀ : z₀ ∈ U
hfg : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = g z
z : 𝕜
h : f z = g z
⊢ (f - g) z = 0
have rw : f z - g z = 0
Tactic: rw [Pi.sub_apply, h, sub_self]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
h₀ : z₀ ∈ U
hfg : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = g z
z : 𝕜
h : f z = g z
rw : f z - g z = 0
⊢ (f - g) z = 0
have rw₁ : g z - g z = 0
Tactic: rw [Pi.sub_apply, h, sub_self]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
h₀ : z₀ ∈ U
hfg : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = g z
z : 𝕜
h : f z = g z
rw : f z - g z = 0
rw₁ : g z - g z = 0
⊢ (f - g) z = 0
have rw₂ : Eq.{u_2 + 1} (α := E) 0 0
Tactic: rw [Pi.sub_apply, h, sub_self]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
h₀ : z₀ ∈ U
hfg : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = g z
⊢ EqOn f g U
have hfg' : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, (f - g) z = 0
Tactic: have hfg' : ∃ᶠ z in 𝓝[≠] z₀, (f - g) z = 0 :=
    hfg.mono fun z h => by rw [Pi.sub_apply, h, sub_self]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0
have pos : ∀ (hU' : U = ∅), (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0
Tactic: by_cases hU' : U = ∅
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0
have neg : ∀ (hU' : ¬U = ∅), (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0
Tactic: by_cases hU' : U = ∅
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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
have neg : ∀ (z : 𝕜) (hz : z ∈ U), (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0
Tactic: obtain ⟨z, hz⟩ : ∃ z, z ∈ U := nonempty_iff_ne_empty.mpr hU'
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0
have pos : ∀ (hU'' : U = {z}), (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0
Tactic: by_cases hU'' : U = {z}
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0
have neg : ∀ (hU'' : ¬U = {z}), (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0
Tactic: by_cases hU'' : U = {z}
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (hypothesis)
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
have hU''₁ : U.Nontrivial
Tactic: apply (nontrivial_iff_ne_singleton hz).mpr at hU''
Cleared hypotheses: hU''
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (hypothesis)
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
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0
have this : ∃ᶠ (w : 𝕜) in 𝓝[≠] z, w ∈ U
Tactic: have : ∃ᶠ w in 𝓝[≠] z, w ∈ U :=
    frequently_mem_iff_neBot.mpr <| hU.preperfect_of_nontrivial hU'' z hz
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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
⊢ ∀ᶠ (x : 𝕜) in 𝓝[≠] z, x ∈ U → f x = 0 ∨ g x = 0
have h : ∀ (a : 𝕜), Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (x : 𝕜) ↦ x ∈ U → f x = 0 ∨ g x = 0) x} a
Tactic: filter_upwards with w hw using smul_eq_zero.mp (hfg w hw)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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
⊢ ∀ᶠ (x : 𝕜) in 𝓝[≠] z, x ∈ U → f x = 0 ∨ g x = 0
have h₁ : ∀ a ∈ U, f a = 0 ∨ g a = 0
Tactic: filter_upwards with w hw using smul_eq_zero.mp (hfg w hw)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (hypothesis)
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
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0
have this₁ : ∃ᶠ (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)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (hypothesis)
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
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0
have x : (∃ᶠ (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
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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
have h : ∀ a ∈ f ⁻¹' insert (f x) s, f a ∈ insert (f x) s
Tactic: filter_upwards [hfx.continuousAt.preimage_mem_nhds (insert_mem_nhds_iff.2 hs)]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (hypothesis)
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
⊢ f ⁻¹' s ∈ 𝓝[≠] x
have this : ∀ᶠ (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
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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
⊢ f ⁻¹' s ∈ 𝓝[≠] x
have contrapose : ∀ (h : ¬f ⁻¹' s ∈ 𝓝[≠] x), EventuallyConst f (𝓝 x)
Tactic: contrapose h₂f with h
Cleared hypotheses: h₂f
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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
⊢ EventuallyConst f (𝓝 x)
have rw : ∃ (c : E), f =ᶠ[𝓝 x] fun (x : 𝕜) ↦ c
Tactic: rw [eventuallyConst_iff_exists_eventuallyEq]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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
⊢ ∃ (c : E), f =ᶠ[𝓝 x] fun (x : 𝕜) ↦ c
have h₁ : f =ᶠ[𝓝 x] fun (x_1 : 𝕜) ↦ f x
Tactic: use f x
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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
⊢ f =ᶠ[𝓝 x] fun (x_1 : 𝕜) ↦ f x
have h₁ : ∃ᶠ (z : 𝕜) in 𝓝[≠] x, f z = f x
Tactic: rw [EventuallyEq, ← hfx.frequently_eq_iff_eventually_eq analyticAt_const]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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 : 𝕜) in 𝓝[≠] x, f z = f x
have h₁ : ∀ (x_1 : 𝕜), (f x_1 ∈ s → False) ∧ f x_1 ∈ insert (f x) s → f x_1 = f x
Tactic: apply ((frequently_imp_distrib_right.2 h).and_eventually
    (eventually_nhdsWithin_of_eventually_nhds this)).mono
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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 : 𝕜
⊢ (f z ∈ s → False) ∧ f z ∈ insert (f x) s → f z = f x
have h₁ : ∀ (h₁z : f z ∈ s → False) (h₂z : f z ∈ insert (f x) s), f z = f x
Tactic: ⟨h₁z, h₂z⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (hypothesis)
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
have h₂z₁ : f z = f x ∨ f z ∈ s
Tactic: rw [Set.mem_insert_iff] at h₂z
Cleared hypotheses: h₂z
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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
⊢ f z = f x
have h₁ : ∀ (h₂z : f z = f x), f z = f x
Tactic: tauto
Cleared hypotheses: h₂z
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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
⊢ f z = f x
have h₂ : ∀ (h₂z : f z ∈ s), f z = f x
Tactic: tauto
Cleared hypotheses: h₂z
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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)
⊢ f ⁻¹' s ∈ codiscreteWithin U
have simp_rw : ∀ (hs : ∀ x ∈ f '' U, s ∪ (f '' U)ᶜ ∈ 𝓝[≠] x), ∀ x ∈ U, f ⁻¹' s ∪ Uᶜ ∈ 𝓝[≠] x
Tactic: simp_rw [mem_codiscreteWithin, disjoint_principal_right, Set.compl_diff] at *
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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 ⁻¹' s ∪ Uᶜ ∈ 𝓝[≠] x
have apply : f ⁻¹' (s ∪ (f '' U)ᶜ) ⊆ f ⁻¹' s ∪ Uᶜ
Tactic: apply mem_of_superset ((hfU x hx).preimage_of_nhdsNE (h₂f x hx) (hs (f x) (by tauto)))
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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 ⁻¹' (s ∪ (f '' U)ᶜ) ⊆ f ⁻¹' s ∪ Uᶜ
have rw : f ⁻¹' s ∪ (f ⁻¹' f '' U)ᶜ ⊆ f ⁻¹' s ∪ Uᶜ
Tactic: rw [preimage_union, preimage_compl]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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 ⁻¹' s ∪ (f ⁻¹' f '' U)ᶜ ⊆ f ⁻¹' s ∪ Uᶜ
have apply : (f ⁻¹' f '' U)ᶜ ⊆ Uᶜ
Tactic: apply union_subset_union_right (f ⁻¹' s)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (hypothesis)
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 ∈ Uᶜ
have hx₁ : ¬∃ x_2 ∈ U, f x_2 = f x
Tactic: push _ ∈ _ at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (hypothesis)
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 ∉ U
have hx₁ : ∀ (x_2 : 𝕜) (_ : x_2 ∈ U), f x_2 ≠ f x
Tactic: push Not at hx
Cleared hypotheses: hx