Theorem: osgood_at' (Ray/Hartogs/Osgood.lean)

State before:
E : Type
f : ℂ × ℂ → E
c : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
h :
  ∀ᶠ (x : ℂ × ℂ) in 𝓝 c,
    ContinuousAt f x ∧ AnalyticAt ℂ (fun z => f (z, x.2)) x.1 ∧ AnalyticAt ℂ (fun z => f (x.1, z)) x.2
⊢ AnalyticAt ℂ f c
Tactic:
rcases eventually_nhds_iff.mp h with ⟨s, h, o, cs⟩
State after:
case intro.intro.intro
E : Type
f : ℂ × ℂ → E
c : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
h✝ :
  ∀ᶠ (x : ℂ × ℂ) in 𝓝 c,
    ContinuousAt f x ∧ AnalyticAt ℂ (fun z => f (z, x.2)) x.1 ∧ AnalyticAt ℂ (fun z => f (x.1, z)) x.2
s : Set (ℂ × ℂ)
h : ∀ x ∈ s, ContinuousAt f x ∧ AnalyticAt ℂ (fun z => f (z, x.2)) x.1 ∧ AnalyticAt ℂ (fun z => f (x.1, z)) x.2
o : IsOpen s
cs : c ∈ s
⊢ AnalyticAt ℂ f c

State before:
case intro.intro.intro
E : Type
f : ℂ × ℂ → E
c : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
h✝ :
  ∀ᶠ (x : ℂ × ℂ) in 𝓝 c,
    ContinuousAt f x ∧ AnalyticAt ℂ (fun z => f (z, x.2)) x.1 ∧ AnalyticAt ℂ (fun z => f (x.1, z)) x.2
s : Set (ℂ × ℂ)
h : ∀ x ∈ s, ContinuousAt f x ∧ AnalyticAt ℂ (fun z => f (z, x.2)) x.1 ∧ AnalyticAt ℂ (fun z => f (x.1, z)) x.2
o : IsOpen s
cs : c ∈ s
⊢ AnalyticAt ℂ f c
Tactic:
exact osgood o (fun _ m ↦ (h _ m).1.continuousWithinAt) (fun _ _ m ↦ (h _ m).2.1)
  (fun _ _ m ↦ (h _ m).2.2) c cs
State after:
no goals