-- 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_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 : 𝕜) ≠ ⊤
inr₄ inr₅ 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 : 𝕜) ≠ ⊤
inr₇ inr₈ 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 : 𝕜) = ⊤ → False
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 : 𝕜) ≠ ⊤
inr₁₀ inr₁₁ 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 : 𝕜) = ⊤ → False
inr₁₃ inr₁₄ 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 : 𝕜) = ⊤ → False
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 : 𝕜) ≠ ⊤
inr₁₆ inr₁₇ 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 : 𝕜) = ⊤ → False
inr₁₉ inr₂₀ 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₂₃ :
  ∀ (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 : 𝕜) = ⊤ → False
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 : 𝕜) ≠ ⊤
inr₂₂ 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 : 𝕜) = ⊤ → False
inr₂₄ 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 : 𝕜) ≠ ⊤

Tactic:
tauto