Theorem: ComplexInverseFun.Cinv.left_inv (Ray/AnalyticManifold/Inverse.lean)

State before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i.g x.1 (f x.1 x.2) = x.2
Tactic:
generalize ht :
    ((extChartAt II (c, z)).source ∩ extChartAt II (c, z) ⁻¹' i.he.source : Set (ℂ × S)) = t
State after:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i.g x.1 (f x.1 x.2) = x.2

State before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i.g x.1 (f x.1 x.2) = x.2
Tactic:
have o : IsOpen t := by
  rw [← ht]
  exact (continuousOn_extChartAt _ _).isOpen_inter_preimage (isOpen_extChartAt_source _ _)
    i.he.open_source
State after:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i.g x.1 (f x.1 x.2) = x.2

State before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i.g x.1 (f x.1 x.2) = x.2
Tactic:
have m : (c, z) ∈ t := by
  simp only [mem_inter_iff, mem_preimage, mem_extChartAt_source, true_and_iff, ← ht]
  exact ContDiffAt.mem_toPartialHomeomorph_source i.ha.contDiffAt i.has_dhe le_top
State after:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m : (c, z) ∈ t
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i.g x.1 (f x.1 x.2) = x.2

State before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m : (c, z) ∈ t
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i.g x.1 (f x.1 x.2) = x.2
Tactic:
apply Filter.eventuallyEq_of_mem (o.mem_nhds m)
State after:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m : (c, z) ∈ t
⊢ EqOn (fun x => i.g x.1 (f x.1 x.2)) (fun x => x.2) t

State before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m : (c, z) ∈ t
⊢ EqOn (fun x => i.g x.1 (f x.1 x.2)) (fun x => x.2) t
Tactic:
intro x m
State after:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x ∈ t
⊢ (fun x => i.g x.1 (f x.1 x.2)) x = (fun x => x.2) x

State before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x ∈ t
⊢ (fun x => i.g x.1 (f x.1 x.2)) x = (fun x => x.2) x
Tactic:
simp only [mem_inter_iff, mem_preimage, extChartAt_prod, extChartAt_eq_refl, ← ht,
  PartialEquiv.prod_source, PartialEquiv.refl_source, mem_prod_eq, mem_univ, true_and_iff,
  PartialEquiv.prod_coe, PartialEquiv.refl_coe, id] at m
State after:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
⊢ (fun x => i.g x.1 (f x.1 x.2)) x = (fun x => x.2) x

State before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
⊢ (fun x => i.g x.1 (f x.1 x.2)) x = (fun x => x.2) x
Tactic:
have inv := i.he.left_inv m.2
State after:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
inv : ↑i.he.symm (↑i.he (x.1, ↑(extChartAt I z) x.2)) = (x.1, ↑(extChartAt I z) x.2)
⊢ (fun x => i.g x.1 (f x.1 x.2)) x = (fun x => x.2) x

State before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
inv : ↑i.he.symm (↑i.he (x.1, ↑(extChartAt I z) x.2)) = (x.1, ↑(extChartAt I z) x.2)
⊢ (fun x => i.g x.1 (f x.1 x.2)) x = (fun x => x.2) x
Tactic:
simp only [Cinv.g]
State after:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
inv : ↑i.he.symm (↑i.he (x.1, ↑(extChartAt I z) x.2)) = (x.1, ↑(extChartAt I z) x.2)
⊢ ↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) (f x.1 x.2))).2 = x.2

State before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
inv : ↑i.he.symm (↑i.he (x.1, ↑(extChartAt I z) x.2)) = (x.1, ↑(extChartAt I z) x.2)
⊢ ↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) (f x.1 x.2))).2 = x.2
Tactic:
generalize hq : i.he.symm = q
State after:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
inv : ↑i.he.symm (↑i.he (x.1, ↑(extChartAt I z) x.2)) = (x.1, ↑(extChartAt I z) x.2)
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
hq : i.he.symm = q
⊢ ↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) (f x.1 x.2))).2 = x.2

State before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
inv : ↑i.he.symm (↑i.he (x.1, ↑(extChartAt I z) x.2)) = (x.1, ↑(extChartAt I z) x.2)
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
hq : i.he.symm = q
⊢ ↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) (f x.1 x.2))).2 = x.2
Tactic:
rw [hq] at inv
State after:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
inv : ↑q (↑i.he (x.1, ↑(extChartAt I z) x.2)) = (x.1, ↑(extChartAt I z) x.2)
hq : i.he.symm = q
⊢ ↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) (f x.1 x.2))).2 = x.2

State before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
inv : ↑q (↑i.he (x.1, ↑(extChartAt I z) x.2)) = (x.1, ↑(extChartAt I z) x.2)
hq : i.he.symm = q
⊢ ↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) (f x.1 x.2))).2 = x.2
Tactic:
rw [Cinv.he, ContDiffAt.toPartialHomeomorph_coe i.ha.contDiffAt i.has_dhe le_top] at inv
State after:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
inv : ↑q (i.h (x.1, ↑(extChartAt I z) x.2)) = (x.1, ↑(extChartAt I z) x.2)
hq : i.he.symm = q
⊢ ↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) (f x.1 x.2))).2 = x.2

State before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
inv : ↑q (i.h (x.1, ↑(extChartAt I z) x.2)) = (x.1, ↑(extChartAt I z) x.2)
hq : i.he.symm = q
⊢ ↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) (f x.1 x.2))).2 = x.2
Tactic:
simp only [Cinv.h, Cinv.f', PartialEquiv.left_inv _ m.1] at inv
State after:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
hq : i.he.symm = q
inv : ↑q (x.1, ↑(extChartAt I (f c z)) (f x.1 x.2)) = (x.1, ↑(extChartAt I z) x.2)
⊢ ↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) (f x.1 x.2))).2 = x.2

State before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
hq : i.he.symm = q
inv : ↑q (x.1, ↑(extChartAt I (f c z)) (f x.1 x.2)) = (x.1, ↑(extChartAt I z) x.2)
⊢ ↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) (f x.1 x.2))).2 = x.2
Tactic:
simp only [inv, PartialEquiv.left_inv _ m.1]
State after:
no goals

State before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
⊢ IsOpen t
Tactic:
rw [← ht]
State after:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
⊢ IsOpen ((extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source)

State before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
⊢ IsOpen ((extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source)
Tactic:
exact (continuousOn_extChartAt _ _).isOpen_inter_preimage (isOpen_extChartAt_source _ _)
  i.he.open_source
State after:
no goals

State before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
⊢ (c, z) ∈ t
Tactic:
simp only [mem_inter_iff, mem_preimage, mem_extChartAt_source, true_and_iff, ← ht]
State after:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
⊢ ↑(extChartAt (I.prod I) (c, z)) (c, z) ∈ i.he.source

State before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
⊢ ↑(extChartAt (I.prod I) (c, z)) (c, z) ∈ i.he.source
Tactic:
exact ContDiffAt.mem_toPartialHomeomorph_source i.ha.contDiffAt i.has_dhe le_top
State after:
no goals