awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r : ℕ
hr : ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 (g z₀) ∧ g_1 (g z₀) ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • g_1 z
s : ℕ
hs : (↑s : ℕ∞) = analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
⊢ ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z
have neg : ∀ (F : 𝕜 → E) (hFa : AnalyticAt 𝕜 F (g z₀)) (hFne : F (g z₀) ≠ 0)
  (hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z),
  ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z
Tactic: rcases hr with ⟨F, hFa, hFne, hfF⟩
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r s : ℕ
hs : (↑s : ℕ∞) = analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F (g z₀)
hFne : F (g z₀) ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z
⊢ ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z
have neg : ∀ (hs : ∃ (g_1 : 𝕜 → 𝕜), AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z - g z₀ = (z - z₀) ^ s • g_1 z)
  (F : 𝕜 → E) (hFa : AnalyticAt 𝕜 F (g z₀)) (hFne : F (g z₀) ≠ 0)
  (hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z),
  ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z
Tactic: rw [Eq.comm, AnalyticAt.analyticOrderAt_eq_natCast (by fun_prop)] at hs
Cleared hypotheses: hs, F, hFa, hFne, hfF
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r s : ℕ
hs : ∃ (g_1 : 𝕜 → 𝕜), AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z - g z₀ = (z - z₀) ^ s • g_1 z
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F (g z₀)
hFne : F (g z₀) ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z
⊢ ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z
have neg : ∀ (G : 𝕜 → 𝕜) (hGa : AnalyticAt 𝕜 G z₀) (hGne : G z₀ ≠ 0) (hgG : ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z - g z₀ = (z - z₀) ^ s • G z),
  ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z
Tactic: rcases hs with ⟨G, hGa, hGne, hgG⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r s : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F (g z₀)
hFne : F (g z₀) ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z
G : 𝕜 → 𝕜
hGa : AnalyticAt 𝕜 G z₀
hGne : G z₀ ≠ 0
hgG : ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z - g z₀ = (z - z₀) ^ s • G z
⊢ ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z
have neg : ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = HSMul.hSMul (β := E) ((z - z₀) ^ (r * s)) ((fun (z : 𝕜) ↦ G z ^ r • F (g z)) z)
Tactic: refine ⟨fun z ↦ (G z) ^ r • F (g z), by fun_prop, by aesop, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r s : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F (g z₀)
hFne : F (g z₀) ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z
G : 𝕜 → 𝕜
hGa : AnalyticAt 𝕜 G z₀
hGne : G z₀ ≠ 0
hgG : ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z - g z₀ = (z - z₀) ^ s • G z
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = HSMul.hSMul (β := E) ((z - z₀) ^ (r * s)) ((fun (z : 𝕜) ↦ G z ^ r • F (g z)) z)
have h : ∀ (z : 𝕜) (hfz : (f ∘ g) z = ((fun (x : 𝕜) ↦ (x - g z₀) ^ r • F x) ∘ g) z) (hgz : g z - g z₀ = (z - z₀) ^ s • G z),
  (f ∘ g) z = (z - z₀) ^ (r * s) • G z ^ r • F (g z)
Tactic: filter_upwards [EventuallyEq.comp_tendsto hfF hg.continuousAt, hgG] with z hfz hgz
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hg : AnalyticAt 𝕜 g z₀
hg' : deriv g z₀ ≠ 0
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀)
have pos : ∀ (hf : AnalyticAt 𝕜 f (g z₀)), analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀)
Tactic: by_cases hf : AnalyticAt 𝕜 f (g z₀)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hg : AnalyticAt 𝕜 g z₀
hg' : deriv g z₀ ≠ 0
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
pos : ∀ (hf : AnalyticAt 𝕜 f (g z₀)), analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀)
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀)
have neg : ∀ (hf : ¬AnalyticAt 𝕜 f (g z₀)), analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀)
Tactic: by_cases hf : AnalyticAt 𝕜 f (g z₀)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hg : AnalyticAt 𝕜 g z₀
hg' : deriv g z₀ ≠ 0
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
hf : ¬AnalyticAt 𝕜 f (g z₀)
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀)
have neg : ¬AnalyticAt 𝕜 (f ∘ g) z₀
Tactic: rw [analyticOrderAt_of_not_analyticAt hf, analyticOrderAt_of_not_analyticAt]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
⊢ IsClopen.{u_1} (X := (↑U : Type u_1)) {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}
have left : IsClosed[instTopologicalSpaceSubtype] {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
left : IsClosed[instTopologicalSpaceSubtype] {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}
⊢ IsClopen.{u_1} (X := (↑U : Type u_1)) {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}
have right : IsOpen[instTopologicalSpaceSubtype] {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
⊢ IsClosed[instTopologicalSpaceSubtype] {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}
have left : ∀ (x : (↑U : Type u_1)),
  Membership.mem (γ := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ x →
    ∃ t ⊆ {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ x ∈ t
Tactic: rw [← isOpen_compl_iff, isOpen_iff_forall_mem_open]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : (↑U : Type u_1)
hz : Membership.mem (γ := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ z
⊢ ∃ t ⊆ {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t
have left : ∀ (h : ∀ᶠ (z : 𝕜) in 𝓝 (↑z : 𝕜), f z = 0),
  ∃ t ⊆ {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t
Tactic: rcases (hf z.1 z.2).eventually_eq_zero_or_eventually_ne_zero with h | h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : (↑U : Type u_1)
hz : Membership.mem (γ := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ z
left :
  ∀ (h : ∀ᶠ (z : 𝕜) in 𝓝 (↑z : 𝕜), f z = 0),
    ∃ t ⊆ {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t
⊢ ∃ t ⊆ {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t
have left₁ : ∀ (h : ∀ᶠ (z : 𝕜) in 𝓝[≠] (↑z : 𝕜), f z ≠ 0),
  ∃ t ⊆ {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t
Tactic: rcases (hf z.1 z.2).eventually_eq_zero_or_eventually_ne_zero with h | h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : (↑U : Type u_1)
hz : Membership.mem (γ := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ z
h : ∀ᶠ (z : 𝕜) in 𝓝 (↑z : 𝕜), f z = 0
⊢ ∃ t ⊆ {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t
have h₁ : analyticOrderAt f (↑z : 𝕜) = ⊤
Tactic: rw [← analyticOrderAt_eq_top] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : (↑U : Type u_1)
hz : Membership.mem (γ := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ z
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] (↑z : 𝕜), f z ≠ 0
⊢ ∃ t ⊆ {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t
have left : ∀ (t' : Set 𝕜) (h₁t' : ∀ y ∈ t', Membership.mem (γ := Set 𝕜) {(↑z : 𝕜)}ᶜ y → f y ≠ 0)
  (h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t') (h₃t' : (↑z : 𝕜) ∈ t'),
  ∃ t ⊆ {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t
Tactic: obtain ⟨t', h₁t', h₂t', h₃t'⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 h)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : (↑U : Type u_1)
hz : Membership.mem (γ := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ z
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] (↑z : 𝕜), f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', Membership.mem (γ := Set 𝕜) {(↑z : 𝕜)}ᶜ y → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : (↑z : 𝕜) ∈ t'
⊢ ∃ t ⊆ {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t
have h₁ : Subset (α := Set (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U) ⁻¹' t')
    {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ ∧
  IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U) ⁻¹' t') ∧
    Membership.mem (γ := Set (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U) ⁻¹' t') z
Tactic: use Subtype.val ⁻¹' t'
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : (↑U : Type u_1)
hz : Membership.mem (γ := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ z
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] (↑z : 𝕜), f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', Membership.mem (γ := Set 𝕜) {(↑z : 𝕜)}ᶜ y → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : (↑z : 𝕜) ∈ t'
⊢ Subset (α := Set (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U) ⁻¹' t')
      {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ ∧
    IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U) ⁻¹' t') ∧
      Membership.mem (γ := Set (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U) ⁻¹' t') z
have h₁ : Subset (α := Set (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U) ⁻¹' t')
  {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : (↑U : Type u_1)
hz : Membership.mem (γ := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ z
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] (↑z : 𝕜), f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', Membership.mem (γ := Set 𝕜) {(↑z : 𝕜)}ᶜ y → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : (↑z : 𝕜) ∈ t'
h₁ :
  Subset (α := Set (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U) ⁻¹' t')
    {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ
⊢ Subset (α := Set (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U) ⁻¹' t')
      {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ ∧
    IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U) ⁻¹' t') ∧
      Membership.mem (γ := Set (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U) ⁻¹' t') z
have h₂ : IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U) ⁻¹' t') ∧
  Membership.mem (γ := Set (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U) ⁻¹' t') z
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : (↑U : Type u_1)
hz : Membership.mem (γ := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ z
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] (↑z : 𝕜), f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', Membership.mem (γ := Set 𝕜) {(↑z : 𝕜)}ᶜ y → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : (↑z : 𝕜) ∈ t'
w : (↑U : Type u_1)
hw : Membership.mem (γ := Set (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U) ⁻¹' t') w
⊢ ¬analyticOrderAt f (↑w : 𝕜) = ⊤
have pos : ∀ (h₁w : w = z), ¬analyticOrderAt f (↑w : 𝕜) = ⊤
Tactic: by_cases h₁w : w = z
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : (↑U : Type u_1)
hz : Membership.mem (γ := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ z
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] (↑z : 𝕜), f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', Membership.mem (γ := Set 𝕜) {(↑z : 𝕜)}ᶜ y → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : (↑z : 𝕜) ∈ t'
w : (↑U : Type u_1)
hw : Membership.mem (γ := Set (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U) ⁻¹' t') w
pos : ∀ (h₁w : w = z), ¬analyticOrderAt f (↑w : 𝕜) = ⊤
⊢ ¬analyticOrderAt f (↑w : 𝕜) = ⊤
have neg : ∀ (h₁w : ¬w = z), ¬analyticOrderAt f (↑w : 𝕜) = ⊤
Tactic: by_cases h₁w : w = z
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : (↑U : Type u_1)
hz : Membership.mem (γ := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ z
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] (↑z : 𝕜), f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', Membership.mem (γ := Set 𝕜) {(↑z : 𝕜)}ᶜ y → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : (↑z : 𝕜) ∈ t'
w : (↑U : Type u_1)
hw : Membership.mem (γ := Set (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U) ⁻¹' t') w
h₁w : w = z
⊢ ¬analyticOrderAt f (↑w : 𝕜) = ⊤
have pos : ¬analyticOrderAt f (↑z : 𝕜) = ⊤
Tactic: rwa [h₁w]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : (↑U : Type u_1)
hz : Membership.mem (γ := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ z
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] (↑z : 𝕜), f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', Membership.mem (γ := Set 𝕜) {(↑z : 𝕜)}ᶜ y → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : (↑z : 𝕜) ∈ t'
w : (↑U : Type u_1)
hw : Membership.mem (γ := Set (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U) ⁻¹' t') w
h₁w : ¬w = z
⊢ ¬analyticOrderAt f (↑w : 𝕜) = ⊤
have neg : ¬Eq (α := ℕ∞) 0 ⊤
Tactic: rw [(hf _ w.2).analyticOrderAt_eq_zero.2 ((h₁t' w hw) (Subtype.coe_ne_coe.mpr h₁w))]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
⊢ IsOpen[instTopologicalSpaceSubtype] {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}
have right : ∀ (x : (↑U : Type u_1)),
  Membership.mem (γ := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤} x →
    ∃ t ⊆ {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}, IsOpen[instTopologicalSpaceSubtype] t ∧ x ∈ t
Tactic: apply isOpen_iff_forall_mem_open.mpr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : (↑U : Type u_1)
hz : Membership.mem (γ := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤} z
| ∃ t ⊆ {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t
have arg : fun (t : Set (↑U : Type u_1)) ↦
  t ⊆ {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤} ∧ IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t
Tactic: arg 1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : (↑U : Type u_1)
hz : Membership.mem (γ := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤} z
x : Set (↑U : Type u_1)
| x ⊆ {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤} ∧ IsOpen[instTopologicalSpaceSubtype] x ∧ z ∈ x
have h : x ⊆ {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : (↑U : Type u_1)
hz : Membership.mem (γ := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤} z
x : Set (↑U : Type u_1)
| x ⊆ {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}
have h : {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : (↑U : Type u_1)
hz : Membership.mem (γ := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤} z
x : Set (↑U : Type u_1)
x_1 : (↑U : Type u_1)
| analyticOrderAt f (↑x_1 : 𝕜) = ⊤
have h : ∃ (t : Set 𝕜), (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ (↑x_1 : 𝕜) ∈ t
Tactic: rw [analyticOrderAt_eq_top, eventually_nhds_iff]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : (↑U : Type u_1)
hz : Membership.mem (γ := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤} z
| ∃ t ⊆ {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t
have h : ∀ (x : Set (↑U : Type u_1)) (x : (↑U : Type u_1)),
  ∃ (t : Set 𝕜), (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ (↑x : 𝕜) ∈ t
Tactic: arg 1; intro; left; right; arg 1; intro
      rw [analyticOrderAt_eq_top, eventually_nhds_iff]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : (↑U : Type u_1)
hz : Membership.mem (γ := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤} z
⊢ ∃ t ⊆ {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t
have right : ∃
  x ⊆
    {x : (↑U : Type u_1) |
      ∃ (t : Set 𝕜), (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ (↑x : 𝕜) ∈ t},
  IsOpen[instTopologicalSpaceSubtype] x ∧ z ∈ x
Tactic: conv =>
      arg 1; intro; left; right; arg 1; intro
      rw [analyticOrderAt_eq_top, eventually_nhds_iff]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : (↑U : Type u_1)
hz : analyticOrderAt f (↑z : 𝕜) = ⊤
⊢ ∃
    x ⊆
      {x : (↑U : Type u_1) |
        ∃ (t : Set 𝕜),
          (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ (↑x : 𝕜) ∈ t},
    IsOpen[instTopologicalSpaceSubtype] x ∧ z ∈ x
have hz₁ : ∃ (t : Set 𝕜), (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ (↑z : 𝕜) ∈ t
Tactic: rw [analyticOrderAt_eq_top, eventually_nhds_iff] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : (↑U : Type u_1)
hz : ∃ (t : Set 𝕜), (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ (↑z : 𝕜) ∈ t
⊢ ∃
    x ⊆
      {x : (↑U : Type u_1) |
        ∃ (t : Set 𝕜),
          (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ (↑x : 𝕜) ∈ t},
    IsOpen[instTopologicalSpaceSubtype] x ∧ z ∈ x
have right : ∀ (t' : Set 𝕜) (h₁t' : ∀ y ∈ t', f y = 0) (h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t')
  (h₃t' : (↑z : 𝕜) ∈ t'),
  ∃
    x ⊆
      {x : (↑U : Type u_1) |
        ∃ (t : Set 𝕜),
          (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ (↑x : 𝕜) ∈ t},
    IsOpen[instTopologicalSpaceSubtype] x ∧ z ∈ x
Tactic: obtain ⟨t', h₁t', h₂t', h₃t'⟩ := hz
Cleared hypotheses: hz