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
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'
⊢ ∃
    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 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
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)
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} ∧
    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')
  {x : (↑U : Type u_1) |
    ∃ (t : Set 𝕜), (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ (↑x : 𝕜) ∈ t}
Tactic: simp only [isOpen_induced h₂t', mem_preimage, h₃t', and_self, and_true]
-- 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
hU : IsConnected U
⊢ (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
have this : ConnectedSpace.{u_1} (↑U : Type u_1)
Tactic: have : ConnectedSpace U := Subtype.connectedSpace hU
-- 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
hU : IsConnected U
this : ConnectedSpace.{u_1} (↑U : Type u_1)
⊢ (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
have obtain : ∀ (v : (↑U : Type u_1)),
  (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
Tactic: obtain ⟨v⟩ : Nonempty U := inferInstance
-- 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
hU : IsConnected U
this_1 : ConnectedSpace.{u_1} (↑U : Type u_1)
v : (↑U : Type u_1)
this :
  (∀ (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 : 𝕜) ≠ ⊤
have inl : ∀ (this : ∀ (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: tauto
Cleared hypotheses: this
-- 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
hU : IsConnected U
this_1 : ConnectedSpace.{u_1} (↑U : Type u_1)
v : (↑U : Type u_1)
this :
  (∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ∨ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) = ⊤
inl :
  ∀ (this : ∀ (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 : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
have inr : ∀ (this : ∀ (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: tauto
Cleared hypotheses: this
-- 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
hU : IsConnected U
this_1 : ConnectedSpace.{u_1} (↑U : Type u_1)
v : (↑U : Type u_1)
this :
  (∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ∨ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) = ⊤
inl :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inr :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) = ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inl₁ :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inr₁ :
  ∀ (this : ∀ (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 : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
have inl₂ : ∀ (this : ∀ (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: tauto
Cleared hypotheses: this
-- 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
hU : IsConnected U
this_1 : ConnectedSpace.{u_1} (↑U : Type u_1)
v : (↑U : Type u_1)
this :
  (∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ∨ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) = ⊤
inl :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inr :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) = ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inl₁ :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inr₁ :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) = ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inl₂ :
  ∀ (this : ∀ (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 : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
have inl₃ : ∀ (this : ∀ (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: tauto
Cleared hypotheses: this
-- 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
hU : IsConnected U
this_1 : ConnectedSpace.{u_1} (↑U : Type u_1)
v : (↑U : Type u_1)
this :
  (∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ∨ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) = ⊤
inl :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inr :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) = ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inl₁ :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inr₁ :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) = ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inl₂ :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) → ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inl₃ :
  ∀ (this : ∀ (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 : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
have inr₂ : ∀ (this : ∀ (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: tauto
Cleared hypotheses: this
-- 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
hU : IsConnected U
this_1 : ConnectedSpace.{u_1} (↑U : Type u_1)
v : (↑U : Type u_1)
this :
  (∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ∨ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) = ⊤
inl :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inr :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) = ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inl₁ :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inr₁ :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) = ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inl₂ :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) → ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inl₃ :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤),
    (∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) → ∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inr₂ :
  ∀ (this : ∀ (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 : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
have inr₃ : ∀ (this : ∀ (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: tauto
Cleared hypotheses: this
-- 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
hU : IsConnected U
this_1 : ConnectedSpace.{u_1} (↑U : Type u_1)
v : (↑U : Type u_1)
this :
  (∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ∨ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) = ⊤
inl :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inr :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) = ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inl₁ :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inr₁ :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) = ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inl₂ :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) → ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inl₃ :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤),
    (∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) → ∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inr₂ :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) = ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) → ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inr₃ :
  ∀ (this : ∀ (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 : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
have inl₄ : ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) (w : (↑U : Type u_1)),
  analyticOrderAt f (↑w : 𝕜) ≠ ⊤ → ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
Tactic: tauto
Cleared hypotheses: this
-- 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
hU : IsConnected U
this_1 : ConnectedSpace.{u_1} (↑U : Type u_1)
v : (↑U : Type u_1)
this :
  (∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ∨ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) = ⊤
inl :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inr :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) = ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inl₁ :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inr₁ :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) = ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inl₂ :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) → ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inl₃ :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤),
    (∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) → ∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inr₂ :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) = ⊤),
    (∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) → ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inr₃ :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) = ⊤),
    (∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) → ∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inl₄ inl₅ inl₆ :
  ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤) (w : (↑U : Type u_1)),
    analyticOrderAt f (↑w : 𝕜) ≠ ⊤ → ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
inl₇ inl₈ inl₉ :
  ∀ (this : ∀ (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 : 𝕜) ≠ ⊤) ↔ ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
have inr₄ : ∀ (this : ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) = ⊤) (w : (↑U : Type u_1)),
  analyticOrderAt f (↑w : 𝕜) ≠ ⊤ → ∀ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
Tactic: tauto
Cleared hypotheses: this
-- 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
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 : 𝕜) ≠ ⊤
have suffices : (∀ (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
-- 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
x y : 𝕜
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
h₁x : x ∈ U
hy : y ∈ U
h₂x : analyticOrderAt f x ≠ ⊤
⊢ ∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
have w : (↑U : Type u_1)
Tactic: use ⟨x, h₁x⟩
-- 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
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)
⊢ ∃ (u : (↑U : Type u_1)), analyticOrderAt f (↑u : 𝕜) ≠ ⊤
have h : analyticOrderAt f (↑(Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ U) x h₁x) : 𝕜) ≠ ⊤
Tactic: use ⟨x, h₁x⟩
-- 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
⊢ Membership.mem (γ := Filter (↑U : Type u_1)) (codiscrete (↑U : Type u_1))
    {u : (↑U : Type u_1) | analyticOrderAt f (↑u : 𝕜) = 0 ∨ analyticOrderAt f (↑u : 𝕜) = ⊤}
have 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
Tactic: simp_rw [mem_codiscrete_subtype_iff_mem_codiscreteWithin, mem_codiscreteWithin,
    disjoint_principal_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
x : 𝕜
hx : 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
have 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
Tactic: rcases (hf x hx).eventually_eq_zero_or_eventually_ne_zero with h₁f | h₁f
-- 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
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
⊢ (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
have 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
Tactic: rcases (hf x hx).eventually_eq_zero_or_eventually_ne_zero with h₁f | h₁f
-- 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
x : 𝕜
hx : x ∈ U
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
have 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 : 𝕜) = ⊤})ᶜ
Tactic: filter_upwards [eventually_nhdsWithin_of_eventually_nhds h₁f.eventually_nhds] with a ha
-- 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
x : 𝕜
hx : x ∈ U
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
have 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 : 𝕜) = ⊤})ᶜ
Tactic: filter_upwards [h₁f] with a ha
-- 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
⊢ {u : 𝕜 | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤} ∈ codiscreteWithin U
have simp_rw : ∀ x ∈ U, (U \ {u : 𝕜 | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤})ᶜ ∈ 𝓝[≠] x
Tactic: simp_rw [mem_codiscreteWithin, disjoint_principal_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
x : 𝕜
hx : x ∈ U
⊢ (U \ {u : 𝕜 | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤})ᶜ ∈ 𝓝[≠] x
have inl : ∀ (h₁f : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = 0), (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