Theorem: Har.flip (Ray/Hartogs/Hartogs.lean)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
⊢ ∀ (c0 c1 : ℂ), (c0, c1) ∈ swap '' s → AnalyticAt ℂ (fun z0 => (f ∘ swap) (z0, c1)) c0
Tactic:
intro c0 c1 cs
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
c0 c1 : ℂ
cs : (c0, c1) ∈ swap '' s
⊢ AnalyticAt ℂ (fun z0 => (f ∘ swap) (z0, c1)) c0

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
c0 c1 : ℂ
cs : (c0, c1) ∈ swap '' s
⊢ AnalyticAt ℂ (fun z0 => (f ∘ swap) (z0, c1)) c0
Tactic:
simp only [Function.comp_apply, Prod.swap_prod_mk]
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
c0 c1 : ℂ
cs : (c0, c1) ∈ swap '' s
⊢ AnalyticAt ℂ (fun z0 => f (c1, z0)) c0

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
c0 c1 : ℂ
cs : (c0, c1) ∈ swap '' s
⊢ AnalyticAt ℂ (fun z0 => f (c1, z0)) c0
Tactic:
rw [swap_mem] at cs
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
c0 c1 : ℂ
cs : (c1, c0) ∈ s
⊢ AnalyticAt ℂ (fun z0 => f (c1, z0)) c0

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
c0 c1 : ℂ
cs : (c1, c0) ∈ s
⊢ AnalyticAt ℂ (fun z0 => f (c1, z0)) c0
Tactic:
exact h.fa1 c1 c0 cs
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
⊢ ∀ (c0 c1 : ℂ), (c0, c1) ∈ swap '' s → AnalyticAt ℂ (fun z1 => (f ∘ swap) (c0, z1)) c1
Tactic:
intro c0 c1 cs
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
c0 c1 : ℂ
cs : (c0, c1) ∈ swap '' s
⊢ AnalyticAt ℂ (fun z1 => (f ∘ swap) (c0, z1)) c1

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
c0 c1 : ℂ
cs : (c0, c1) ∈ swap '' s
⊢ AnalyticAt ℂ (fun z1 => (f ∘ swap) (c0, z1)) c1
Tactic:
simp only [Function.comp_apply, Prod.swap_prod_mk]
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
c0 c1 : ℂ
cs : (c0, c1) ∈ swap '' s
⊢ AnalyticAt ℂ (fun z1 => f (z1, c0)) c1

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
c0 c1 : ℂ
cs : (c0, c1) ∈ swap '' s
⊢ AnalyticAt ℂ (fun z1 => f (z1, c0)) c1
Tactic:
rw [swap_mem] at cs
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
c0 c1 : ℂ
cs : (c1, c0) ∈ s
⊢ AnalyticAt ℂ (fun z1 => f (z1, c0)) c1

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
c0 c1 : ℂ
cs : (c1, c0) ∈ s
⊢ AnalyticAt ℂ (fun z1 => f (z1, c0)) c1
Tactic:
exact h.fa0 c1 c0 cs
State after:
no goals