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
simp_rw :
  ∀ x ∈ U,
    (U \
          image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
            {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = 0 ∨ analyticOrderAt f (↑u : 𝕜) = ⊤})ᶜ ∈
      𝓝[≠] x
⊢ Membership.mem (γ := Filter (↑U : Type u_1)) (codiscrete (↑U : Type u_1))
    {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = 0 ∨ analyticOrderAt f (↑u : 𝕜) = ⊤}

Tactic:
simp_rw [mem_codiscrete_subtype_iff_mem_codiscreteWithin, mem_codiscreteWithin,
    disjoint_principal_right]

Premises used: mem_codiscreteWithin, mem_codiscrete_subtype_iff_mem_codiscreteWithin, Filter.disjoint_principal_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
x : 𝕜
hx : x ∈ U
inl :
  ∀ (h₁f : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = 0),
    (U \
          image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
            {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = 0 ∨ analyticOrderAt f (↑u : 𝕜) = ⊤})ᶜ ∈
      𝓝[≠] x
inr :
  ∀ (h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ≠ 0),
    (U \
          image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
            {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = 0 ∨ analyticOrderAt f (↑u : 𝕜) = ⊤})ᶜ ∈
      𝓝[≠] x
⊢ (U \
        image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
          {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = 0 ∨ analyticOrderAt f (↑u : 𝕜) = ⊤})ᶜ ∈
    𝓝[≠] x

Tactic:
rcases (hf x hx).eventually_eq_zero_or_eventually_ne_zero with h₁f | h₁f

Premises used: AnalyticAt.eventually_eq_zero_or_eventually_ne_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
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = 0
h :
  ∀ (a : 𝕜) (ha : ∀ᶠ (x : 𝕜) in 𝓝 a, f x = 0),
    a ∈
      (U \
          image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
            {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = 0 ∨ analyticOrderAt f (↑u : 𝕜) = ⊤})ᶜ
⊢ (U \
        image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
          {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = 0 ∨ analyticOrderAt f (↑u : 𝕜) = ⊤})ᶜ ∈
    𝓝[≠] x

Tactic:
filter_upwards [eventually_nhdsWithin_of_eventually_nhds h₁f.eventually_nhds] with a ha

Premises used: Filter.Eventually.eventually_nhds, eventually_nhdsWithin_of_eventually_nhds
-- 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
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = 0
a : 𝕜
ha : ∀ᶠ (x : 𝕜) in 𝓝 a, f x = 0
⊢ a ∈
    (U \
        image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
          {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = 0 ∨ analyticOrderAt f (↑u : 𝕜) = ⊤})ᶜ

Tactic:
simp [analyticOrderAt_eq_top, ha]

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
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ≠ 0
h :
  ∀ (a : 𝕜) (ha : f a ≠ 0),
    a ∈
      (U \
          image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
            {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = 0 ∨ analyticOrderAt f (↑u : 𝕜) = ⊤})ᶜ
⊢ (U \
        image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
          {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = 0 ∨ analyticOrderAt f (↑u : 𝕜) = ⊤})ᶜ ∈
    𝓝[≠] x

Tactic:
filter_upwards [h₁f] with a ha
-- 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
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ≠ 0
a : 𝕜
ha : f a ≠ 0
⊢ a ∈
    (U \
        image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
          {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = 0 ∨ analyticOrderAt f (↑u : 𝕜) = ⊤})ᶜ

Tactic:
simp +contextual [(hf a _).analyticOrderAt_eq_zero, ha]

Premises used: 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
simp_rw : ∀ x ∈ U, (U \ {u : 𝕜 | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤})ᶜ ∈ 𝓝[≠] x
⊢ {u : 𝕜 | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤} ∈ codiscreteWithin U

Tactic:
simp_rw [mem_codiscreteWithin, disjoint_principal_right]

Premises used: mem_codiscreteWithin, Filter.disjoint_principal_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
x : 𝕜
hx : x ∈ U
inl : ∀ (h₁f : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = 0), (U \ {u : 𝕜 | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤})ᶜ ∈ 𝓝[≠] x
inr :
  ∀ (h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ≠ 0), (U \ {u : 𝕜 | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤})ᶜ ∈ 𝓝[≠] x
⊢ (U \ {u : 𝕜 | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤})ᶜ ∈ 𝓝[≠] x

Tactic:
rcases (hf x hx).eventually_eq_zero_or_eventually_ne_zero with h₁f | h₁f

Premises used: AnalyticAt.eventually_eq_zero_or_eventually_ne_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
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = 0
h : ∀ (a : 𝕜) (ha : ∀ᶠ (x : 𝕜) in 𝓝 a, f x = 0), a ∈ (U \ {u : 𝕜 | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤})ᶜ
⊢ (U \ {u : 𝕜 | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤})ᶜ ∈ 𝓝[≠] x

Tactic:
filter_upwards [eventually_nhdsWithin_of_eventually_nhds h₁f.eventually_nhds] with a ha

Premises used: Filter.Eventually.eventually_nhds, eventually_nhdsWithin_of_eventually_nhds
-- 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
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = 0
a : 𝕜
ha : ∀ᶠ (x : 𝕜) in 𝓝 a, f x = 0
⊢ a ∈ (U \ {u : 𝕜 | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤})ᶜ

Tactic:
simp [analyticOrderAt_eq_top, ha]

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
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ≠ 0
h : ∀ (a : 𝕜) (ha : f a ≠ 0), a ∈ (U \ {u : 𝕜 | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤})ᶜ
⊢ (U \ {u : 𝕜 | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤})ᶜ ∈ 𝓝[≠] x

Tactic:
filter_upwards [h₁f] with a ha
-- 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
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ≠ 0
a : 𝕜
ha : f a ≠ 0
⊢ a ∈ (U \ {u : 𝕜 | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤})ᶜ

Tactic:
simp +contextual [(hf a _).analyticOrderAt_eq_zero, ha]

Premises used: 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
x : 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
h₂f : f x ≠ 0
hx : x ∈ U
hU : IsConnected U
h : ∀ (a : 𝕜) (ha : analyticOrderAt f a = 0 ∨ analyticOrderAt f a = ⊤) (h₂a : a ∈ U), a ∈ f ⁻¹' {0}ᶜ
⊢ f ⁻¹' {0}ᶜ ∈ codiscreteWithin U

Tactic:
filter_upwards [h₁f.codiscreteWithin_setOf_analyticOrderAt_eq_zero_or_top,
    self_mem_codiscreteWithin U] with a ha h₂a

Premises used: AnalyticOnNhd.codiscreteWithin_setOf_analyticOrderAt_eq_zero_or_top, Filter.self_mem_codiscreteWithin
-- 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 : 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
h₂f : f x ≠ 0
hx : x ∈ U
hU : IsConnected U
a : 𝕜
ha : analyticOrderAt f a = 0 ∨ analyticOrderAt f a = ⊤
h₂a : a ∈ U
h :
  ∀ (h₂f : analyticOrderAt f x = 0) (hx : x ∈ U) (hU : IsConnected U) (a : 𝕜)
    (ha : analyticOrderAt f a = 0 ∨ analyticOrderAt f a = ⊤) (h₂a : a ∈ U), a ∈ f ⁻¹' {0}ᶜ
⊢ a ∈ f ⁻¹' {0}ᶜ

Tactic:
rw [← (h₁f x hx).analyticOrderAt_eq_zero] at h₂f

Premises used: 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
x : 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
h₂f : analyticOrderAt f x = 0
hx : x ∈ U
hU : IsConnected U
a : 𝕜
ha : analyticOrderAt f a = 0 ∨ analyticOrderAt f a = ⊤
h₂a : a ∈ U
u : (↑U : Type u_1)
a₁ : ∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
⊢ analyticOrderAt f (↑u : 𝕜) ≠ ⊤

Tactic:
apply (h₁f.exists_analyticOrderAt_ne_top_iff_forall hU).1

Premises used: AnalyticOnNhd.exists_analyticOrderAt_ne_top_iff_forall, 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 : 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
h₂f : analyticOrderAt f x = 0
hx : x ∈ U
hU : IsConnected U
a : 𝕜
ha : analyticOrderAt f a = 0 ∨ analyticOrderAt f a = ⊤
h₂a : a ∈ U
u : (↑U : Type u_1)
h : analyticOrderAt f (↑(Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ U) x hx) : 𝕜) ≠ ⊤
⊢ ∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤

Tactic:
use ⟨x, hx⟩
-- 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 : 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
h₂f : analyticOrderAt f x = 0
hx : x ∈ U
hU : IsConnected U
a : 𝕜
ha : analyticOrderAt f a = 0 ∨ analyticOrderAt f a = ⊤
h₂a : a ∈ U
u : (↑U : Type u_1)
⊢ analyticOrderAt f (↑(Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ U) x hx) : 𝕜) ≠ ⊤

Tactic:
simp_all
-- 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 : 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
h₂f : analyticOrderAt f x = 0
hx : x ∈ U
hU : IsConnected U
a : 𝕜
ha : analyticOrderAt f a = 0 ∨ analyticOrderAt f a = ⊤
h₂a : a ∈ U
⊢ ∀ {u : (↑U : Type u_1)}, analyticOrderAt f (↑u : 𝕜) ≠ ⊤

Tactic:
have {u : U} : analyticOrderAt f u ≠ ⊤ := by
    apply (h₁f.exists_analyticOrderAt_ne_top_iff_forall hU).1
    use ⟨x, hx⟩
    simp_all
-- 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 : 𝕜
h₁f : AnalyticOnNhd 𝕜 f U
h₂f : analyticOrderAt f x = 0
hx : x ∈ U
hU : IsConnected U
a : 𝕜
ha : analyticOrderAt f a = 0 ∨ analyticOrderAt f a = ⊤
h₂a : a ∈ U
this : ∀ {u : (↑U : Type u_1)}, analyticOrderAt f (↑u : 𝕜) ≠ ⊤
⊢ a ∈ f ⁻¹' {0}ᶜ

Tactic:
simp_all [(h₁f a h₂a).analyticOrderAt_eq_zero]

Premises used: 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
f : 𝕜 → E
inst_3 : ConnectedSpace 𝕜
x : 𝕜
hf : AnalyticOnNhd 𝕜 f univ
hx : f x ≠ 0
⊢ f ⁻¹' {0}ᶜ ∈ codiscrete 𝕜

Tactic:
hf.preimage_zero_mem_codiscreteWithin hx trivial isConnected_univ

Premises used: trivial, Set.Mem, isConnected_univ, AnalyticOnNhd.preimage_zero_mem_codiscreteWithin
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : PreconnectedSpace 𝕜
f : 𝕜 → E
z : 𝕜
hf : ∀ (z₀ : 𝕜), AnalyticAt 𝕜 f z₀
⊢ f = 0 → ∀ᶠ (z : 𝕜) in 𝓝 z, f z = 0

Tactic:
simp +contextual
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : PreconnectedSpace 𝕜
f : 𝕜 → E
z : 𝕜
hf : ∀ (z₀ : 𝕜), AnalyticAt 𝕜 f z₀
refine : ∀ (h : ∀ᶠ (z : 𝕜) in 𝓝 z, f z = 0), EqOn f 0 univ
⊢ analyticOrderAt f z = ⊤ ↔ f = 0

Tactic:
refine analyticOrderAt_eq_top.trans ⟨fun h ↦ eqOn_univ .. |>.mp ?_, by simp +contextual⟩

Premises used: analyticOrderAt_eq_top, Set.eqOn_univ, Iff.intro, Iff.mp, Iff.trans
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : PreconnectedSpace 𝕜
f : 𝕜 → E
z : 𝕜
hf : ∀ (z₀ : 𝕜), AnalyticAt 𝕜 f z₀
h : ∀ᶠ (z : 𝕜) in 𝓝 z, f z = 0
apply : ∃ᶠ (z : 𝕜) in 𝓝[≠] z, f z = 0
apply₁ : 𝕜
⊢ EqOn f 0 univ

Tactic:
apply eqOn_zero_of_preconnected_of_frequently_eq_zero (fun z _ ↦ hf z) isPreconnected_univ trivial

Premises used: trivial, AnalyticOnNhd.eqOn_zero_of_preconnected_of_frequently_eq_zero, PreconnectedSpace.isPreconnected_univ
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : PreconnectedSpace 𝕜
f : 𝕜 → E
z : 𝕜
hf : ∀ (z₀ : 𝕜), AnalyticAt 𝕜 f z₀
h : ∀ᶠ (z : 𝕜) in 𝓝 z, f z = 0
⊢ ∃ᶠ (z : 𝕜) in 𝓝[≠] z, f z = 0

Tactic:
hf z |>.frequently_eq_iff_eventually_eq analyticAt_const |>.mpr h

Premises used: Iff.mpr, analyticAt_const, AnalyticAt.frequently_eq_iff_eventually_eq
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f : 𝕜 → E
⊢ (∀ z ∈ s, analyticOrderAt f z = ⊤) ↔ EqOn f 0 s

Tactic:
⟨(EventuallyEq.eq_of_nhds <| analyticOrderAt_eq_top.mp <| · · ·), fun hzero z hz ↦ ?_⟩

Premises used: Filter.EventuallyEq.eq_of_nhds, analyticOrderAt_eq_top, Iff.intro, 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
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f : 𝕜 → E
refine : ∀ (hzero : EqOn f 0 s) (z : 𝕜) (hz : z ∈ s), analyticOrderAt f z = ⊤
⊢ (∀ z ∈ s, analyticOrderAt f z = ⊤) ↔ EqOn f 0 s

Tactic:
refine ⟨(EventuallyEq.eq_of_nhds <| analyticOrderAt_eq_top.mp <| · · ·), fun hzero z hz ↦ ?_⟩
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f : 𝕜 → E
hzero : EqOn f 0 s
z : 𝕜
hz : z ∈ s
apply : ∀ᶠ (z : 𝕜) in 𝓝 z, f z = 0
⊢ analyticOrderAt f z = ⊤

Tactic:
apply analyticOrderAt_eq_top.mpr

Premises used: Iff.mpr, 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
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f : 𝕜 → E
hzero : EqOn f 0 s
z : 𝕜
hz : z ∈ s
h : ∀ a ∈ s, f a = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z, f z = 0

Tactic:
filter_upwards [hs.mem_nhds hz]

Premises used: IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f : 𝕜 → E
hzero : EqOn f 0 s
z : 𝕜
hz : z ∈ s
⊢ ∀ a ∈ s, f a = 0

Tactic:
fun _ ↦ hzero.eq_of_mem

Premises used: Set.EqOn.eq_of_mem
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f : 𝕜 → E
hzero : EqOn f 0 s
z : 𝕜
hz : z ∈ s
⊢ ∀ a ∈ s, f a = 0

Tactic:
exact fun _ ↦ hzero.eq_of_mem

Premises used: Set.EqOn.eq_of_mem
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
s : Set E
inst_4 : NormedRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f s z
p : A[X]
⊢ AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) p) s z

Tactic:
p.induction_on (fun k ↦ ?_) (fun p q hp hq ↦ ?_) fun p i hp ↦ ?_

Premises used: Polynomial.induction_on
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
s : Set E
inst_4 : NormedRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f s z
p : A[X]
refine_1 :
  ∀ (k : A),
    AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B)
      (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) ((C : (a : A) → A[X]) k : A[X])) s z
refine_2 :
  ∀ (p q : A[X]) (hp : AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) p) s z)
    (hq : AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) q) s z),
    AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) (p + q)) s z
refine_3 :
  ∀ (p : ℕ) (i : A)
    (hp :
      AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B)
        (fun (x : E) ↦
          (aeval (f x) : (a : A[X]) → B)
            (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X p)))
        s z),
    AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B)
      (fun (x : E) ↦
        (aeval (f x) : (a : A[X]) → B)
          (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X (p + 1))))
      s z
⊢ AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) p) s z

Tactic:
refine p.induction_on (fun k ↦ ?_) (fun p q hp hq ↦ ?_) fun p i hp ↦ ?_
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
s : Set E
inst_4 : NormedRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f s z
p : A[X]
k : A
refine_1 : AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (algebraMap A B : (a : A) → B) k) s z
⊢ AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) ((C : (a : A) → A[X]) k : A[X])) s z

Tactic:
simp_rw [aeval_C]

Premises used: Polynomial.aeval_C
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
s : Set E
inst_4 : NormedRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f s z
p : A[X]
k : A
⊢ AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (algebraMap A B : (a : A) → B) k) s z

Tactic:
apply analyticWithinAt_const

Premises used: analyticWithinAt_const
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
s : Set E
inst_4 : NormedRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f s z
p_1 p q : A[X]
hp : AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) p) s z
hq : AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) q) s z
refine_2 :
  AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦
      HAdd.hAdd (α := B) (β := B) ((aeval (f x) : (a : A[X]) → B) p : B) ((aeval (f x) : (a : A[X]) → B) q : B))
    s z
⊢ AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) (p + q)) s z

Tactic:
simp_rw [aeval_add]

Premises used: Polynomial.aeval_add
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
s : Set E
inst_4 : NormedRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f s z
p_1 p q : A[X]
hp : AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) p) s z
hq : AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) q) s z
⊢ AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦
      HAdd.hAdd (α := B) (β := B) ((aeval (f x) : (a : A[X]) → B) p : B) ((aeval (f x) : (a : A[X]) → B) q : B))
    s z

Tactic:
hp.add hq

Premises used: AnalyticWithinAt.add
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
s : Set E
inst_4 : NormedRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f s z
p_1 p q : A[X]
hp : AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) p) s z
hq : AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : A[X]) → B) q) s z
⊢ AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦
      HAdd.hAdd (α := B) (β := B) ((aeval (f x) : (a : A[X]) → B) p : B) ((aeval (f x) : (a : A[X]) → B) q : B))
    s z

Tactic:
exact hp.add hq

Premises used: AnalyticWithinAt.add
-- Module: Mathlib.Analysis.Analytic.Polynomial
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
s : Set E
inst_4 : NormedRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f s z
p_1 : A[X]
p : ℕ
i : A
hp :
  AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦
      (aeval (f x) : (a : A[X]) → B)
        (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X p)))
    s z
⊢ AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := B)
    (fun (x : E) ↦
      HMul.hMul (α := B)
        ((aeval (f x) : (a : A[X]) → B)
            (HMul.hMul (α := A[X]) ((C : (a : A) → A[X]) i : A[X]) (HPow.hPow (α := A[X]) X p)) :
          B)
        (f x))
    s z

Tactic:
hp.mul hf

Premises used: AnalyticWithinAt.mul