awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Order
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 : 𝕜) = ⊤}
right : IsOpen[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 : 𝕜) = ⊤}

Tactic:
constructor
-- Module: Mathlib.Analysis.Analytic.Order
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 :
  ∀ (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
⊢ IsClosed[instTopologicalSpaceSubtype] {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_forall_mem_open]

Premises used: isOpen_iff_forall_mem_open, isOpen_compl_iff
-- Module: Mathlib.Analysis.Analytic.Order
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
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

Tactic:
rcases (hf z.1 z.2).eventually_eq_zero_or_eventually_ne_zero with h | h

Premises used: AnalyticAt.eventually_eq_zero_or_eventually_ne_zero, Subtype.val, Subtype.property
-- Module: Mathlib.Analysis.Analytic.Order
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
⊢ analyticOrderAt f (↑z : 𝕜) = ⊤

Tactic:
rw [← analyticOrderAt_eq_top] at h

Premises used: analyticOrderAt_eq_top
-- Module: Mathlib.Analysis.Analytic.Order
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 : analyticOrderAt f (↑z : 𝕜) = ⊤
⊢ ∃ t ⊆ {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t

Tactic:
tauto
-- Module: Mathlib.Analysis.Analytic.Order
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
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
⊢ ∃ 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)

Premises used: eventually_nhds_iff, eventually_nhdsWithin_iff, Iff.mp
-- Module: Mathlib.Analysis.Analytic.Order
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 : 𝕜) = ⊤}ᶜ ∧
    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
⊢ ∃ t ⊆ {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t

Tactic:
use Subtype.val ⁻¹' t'

Premises used: Subtype.val
-- Module: Mathlib.Analysis.Analytic.Order
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 : 𝕜) = ⊤}ᶜ
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
⊢ 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:
constructor
-- Module: Mathlib.Analysis.Analytic.Order
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 : 𝕜) = ⊤
neg : ∀ (h₁w : ¬w = z), ¬analyticOrderAt f (↑w : 𝕜) = ⊤
⊢ ¬analyticOrderAt f (↑w : 𝕜) = ⊤

Tactic:
by_cases h₁w : w = z
-- Module: Mathlib.Analysis.Analytic.Order
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
pos pos₁ pos₂ pos₃ : ¬analyticOrderAt f (↑z : 𝕜) = ⊤
⊢ ¬analyticOrderAt f (↑w : 𝕜) = ⊤

Tactic:
rwa [h₁w]
-- Module: Mathlib.Analysis.Analytic.Order
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
neg : ¬Eq (α := ℕ∞) 0 ⊤
⊢ ¬analyticOrderAt f (↑w : 𝕜) = ⊤

Tactic:
rw [(hf _ w.2).analyticOrderAt_eq_zero.2 ((h₁t' w hw) (Subtype.coe_ne_coe.mpr h₁w))]

Premises used: Iff.mpr, Subtype.val, Subtype.coe_ne_coe, Subtype.property, AnalyticAt.analyticOrderAt_eq_zero
-- Module: Mathlib.Analysis.Analytic.Order
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
⊢ ¬Eq (α := ℕ∞) 0 ⊤

Tactic:
ENat.zero_ne_top

Premises used: ENat.zero_ne_top
-- Module: Mathlib.Analysis.Analytic.Order
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
⊢ ¬Eq (α := ℕ∞) 0 ⊤

Tactic:
exact ENat.zero_ne_top

Premises used: ENat.zero_ne_top
-- Module: Mathlib.Analysis.Analytic.Order
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'
⊢ 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:
⟨isOpen_induced h₂t', h₃t'⟩

Premises used: isOpen_induced, And.intro
-- Module: Mathlib.Analysis.Analytic.Order
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'
⊢ 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:
exact ⟨isOpen_induced h₂t', h₃t'⟩
-- Module: Mathlib.Analysis.Analytic.Order
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
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
⊢ IsOpen[instTopologicalSpaceSubtype] {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}

Tactic:
apply isOpen_iff_forall_mem_open.mpr

Premises used: Iff.mpr, isOpen_iff_forall_mem_open
-- Module: Mathlib.Analysis.Analytic.Order
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
arg :
  fun (t : Set (↑U : Type u_1)) ↦
    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

Tactic:
arg 1
-- Module: Mathlib.Analysis.Analytic.Order
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)
h : x ⊆ {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}
| x ⊆ {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤} ∧ IsOpen[instTopologicalSpaceSubtype] x ∧ z ∈ x

Tactic:
left
-- Module: Mathlib.Analysis.Analytic.Order
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)
h : {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}
| x ⊆ {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}

Tactic:
right
-- Module: Mathlib.Analysis.Analytic.Order
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)
h : ∃ (t : Set 𝕜), (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ (↑x_1 : 𝕜) ∈ t
| analyticOrderAt f (↑x_1 : 𝕜) = ⊤

Tactic:
rw [analyticOrderAt_eq_top, eventually_nhds_iff]

Premises used: analyticOrderAt_eq_top, eventually_nhds_iff
-- Module: Mathlib.Analysis.Analytic.Order
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 :
  ∀ (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
| ∃ t ⊆ {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t

Tactic:
arg 1; intro; left; right; arg 1; intro
      rw [analyticOrderAt_eq_top, eventually_nhds_iff]

Premises used: analyticOrderAt_eq_top, eventually_nhds_iff
-- Module: Mathlib.Analysis.Analytic.Order
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
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
⊢ ∃ t ⊆ {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = ⊤}, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t

Tactic:
conv =>
      arg 1; intro; left; right; arg 1; intro
      rw [analyticOrderAt_eq_top, eventually_nhds_iff]

Premises used: analyticOrderAt_eq_top, eventually_nhds_iff
-- Module: Mathlib.Analysis.Analytic.Order
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 : 𝕜) = ⊤
⊢ ∃ (t : Set 𝕜), (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ (↑z : 𝕜) ∈ t

Tactic:
rw [analyticOrderAt_eq_top, eventually_nhds_iff] at hz

Premises used: analyticOrderAt_eq_top, eventually_nhds_iff
-- Module: Mathlib.Analysis.Analytic.Order
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
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
⊢ ∃
    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
-- Module: Mathlib.Analysis.Analytic.Order
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)
t' : Set 𝕜
h₁t' : ∀ y ∈ t', 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')
      {x : (↑U : Type u_1) |
        ∃ (t : Set 𝕜),
          (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ (↑x : 𝕜) ∈ t} ∧
    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
⊢ ∃
    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:
use Subtype.val ⁻¹' t'

Premises used: Subtype.val
-- Module: Mathlib.Analysis.Analytic.Order
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)
t' : Set 𝕜
h₁t' : ∀ y ∈ t', 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')
    {x : (↑U : Type u_1) |
      ∃ (t : Set 𝕜), (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ (↑x : 𝕜) ∈ t}
⊢ Subset (α := Set (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U) ⁻¹' t')
      {x : (↑U : Type u_1) |
        ∃ (t : Set 𝕜),
          (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ (↑x : 𝕜) ∈ t} ∧
    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:
simp only [isOpen_induced h₂t', mem_preimage, h₃t', and_self, and_true]

Premises used: and_true, and_self, isOpen_induced, Set.mem_preimage
-- Module: Mathlib.Analysis.Analytic.Order
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)
t' : Set 𝕜
h₁t' : ∀ y ∈ t', 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')
    {x : (↑U : Type u_1) |
      ∃ (t : Set 𝕜), (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ (↑x : 𝕜) ∈ t}

Tactic:
grind
-- Module: Mathlib.Analysis.Analytic.Order
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
hU : IsConnected U
⊢ ConnectedSpace.{u_1} (↑U : Type u_1)

Tactic:
have : ConnectedSpace U := Subtype.connectedSpace hU
-- Module: Mathlib.Analysis.Analytic.Order
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
hU : IsConnected U
this : ConnectedSpace.{u_1} (↑U : Type u_1)
⊢ Nonempty.{u_1 + 1} (↑U : Type u_1)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Analysis.Analytic.Order
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
hU : IsConnected U
this : ConnectedSpace.{u_1} (↑U : Type u_1)
obtain :
  ∀ (v : (↑U : Type u_1)),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
⊢ (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤

Tactic:
obtain ⟨v⟩ : Nonempty U := inferInstance

Premises used: Set.Elem, Nonempty
-- Module: Mathlib.Analysis.Analytic.Order
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
hU : IsConnected U
this : ConnectedSpace.{u_1} (↑U : Type u_1)
v : (↑U : Type u_1)
suffices :
  (∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ∨ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) = ⊤
⊢ (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤

Tactic:
suffices (∀ (u : U), analyticOrderAt f u ≠ ⊤) ∨ ∀ (u : U), analyticOrderAt f u = ⊤ by tauto
-- Module: Mathlib.Analysis.Analytic.Order
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
hU : IsConnected U
this : ConnectedSpace.{u_1} (↑U : Type u_1)
v : (↑U : Type u_1)
⊢ (∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ∨ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) = ⊤

Tactic:
simpa [Set.eq_empty_iff_forall_notMem, Set.eq_univ_iff_forall] using
      isClopen_iff.1 hf.isClopen_setOf_analyticOrderAt_eq_top

Premises used: Set.eq_univ_iff_forall, isClopen_iff, Set.eq_empty_iff_forall_notMem, AnalyticOnNhd.isClopen_setOf_analyticOrderAt_eq_top, Iff.mp
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
x y : 𝕜
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
h₁x : x ∈ U
hy : y ∈ U
h₂x : analyticOrderAt f x ≠ ⊤
w : (↑U : Type u_1)
h : analyticOrderAt f (↑(Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ U) x h₁x) : 𝕜) ≠ ⊤
⊢ ∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤

Tactic:
use ⟨x, h₁x⟩