Theorem: Pair.hartogs_at (Ray/Hartogs/Hartogs.lean)

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

State before:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
c : ℂ × ℂ
fa0 : ∀ᶠ (p : ℂ × ℂ) in 𝓝 c, AnalyticAt ℂ (fun z0 => f (z0, p.2)) p.1
fa1 : ∀ᶠ (p : ℂ × ℂ) in 𝓝 c, AnalyticAt ℂ (fun z1 => f (p.1, z1)) p.2
s : Set (ℂ × ℂ)
fa : ∀ x ∈ s, AnalyticAt ℂ (fun z0 => f (z0, x.2)) x.1 ∧ AnalyticAt ℂ (fun z1 => f (x.1, z1)) x.2
o : IsOpen s
cs : c ∈ s
⊢ AnalyticAt ℂ f c
Tactic:
exact Pair.hartogs o (fun c0 c1 m ↦ (fa _ m).1) (fun c0 c1 m ↦ (fa _ m).2) c cs
State after:
no goals