Theorem: ComplexInverseFun.Cinv.right_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 : ℂ × T) in 𝓝 (c, f c z), f x.1 (i.g x.1 x.2) = x.2
Tactic:
generalize ht : ((extChartAt II (c, f c z)).source ∩ extChartAt II (c, f c z) ⁻¹' i.he.target
    : Set (ℂ × T)) = 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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
⊢ ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (i.g 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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
⊢ ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (i.g 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_target
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
⊢ ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (i.g 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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
⊢ ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (i.g x.1 x.2) = x.2
Tactic:
have m' : (c, extChartAt I (f c z) (f c z)) ∈ i.he.toPartialEquiv.target := by
  have m := ContDiffAt.image_mem_toPartialHomeomorph_target i.ha.contDiffAt i.has_dhe le_top
  have e : i.h (c, i.z') = (c, extChartAt I (f c z) (f c z)) := by
    simp only [Cinv.h, Cinv.z', Cinv.f', PartialEquiv.left_inv _ (mem_extChartAt_source _ _)]
  rw [e] at m; exact 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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
⊢ ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (i.g 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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
⊢ ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (i.g x.1 x.2) = x.2
Tactic:
have m : (c, f c z) ∈ t := by
  simp only [m', mem_inter_iff, mem_preimage, mem_extChartAt_source, true_and_iff, ← ht,
    extChartAt_prod, PartialEquiv.prod_coe, extChartAt_eq_refl, PartialEquiv.refl_coe, id,
    PartialEquiv.prod_source, prod_mk_mem_set_prod_eq, PartialEquiv.refl_source, mem_univ]
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (i.g 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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
fm :
  ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
⊢ ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (i.g x.1 x.2) = x.2
Tactic:
refine fm.mp (Filter.eventually_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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
fm :
  ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
⊢ ∀ x ∈ t,
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source →
      f x.1 (i.g 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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
fm :
  ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
⊢ ∀ x ∈ t,
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source →
      f x.1 (i.g x.1 x.2) = x.2
Tactic:
intro x m mf
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m✝ : (c, f c z) ∈ t
fm :
  ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
x : ℂ × T
m : x ∈ t
mf : f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
⊢ f x.1 (i.g 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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m✝ : (c, f c z) ∈ t
fm :
  ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
x : ℂ × T
m : x ∈ t
mf : f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
⊢ f x.1 (i.g x.1 x.2) = x.2
Tactic:
simp only [mem_inter_iff, mem_preimage, extChartAt_prod, extChartAt_eq_refl,
  PartialEquiv.prod_source, PartialEquiv.refl_source, mem_prod_eq, mem_univ, true_and_iff,
  PartialEquiv.prod_coe, PartialEquiv.refl_coe, id, ← ht] 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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m✝ : (c, f c z) ∈ t
fm :
  ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
x : ℂ × T
mf : f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
m : x.2 ∈ (extChartAt I (f c z)).source ∧ (x.1, ↑(extChartAt I (f c z)) x.2) ∈ i.he.target
⊢ f x.1 (i.g 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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m✝ : (c, f c z) ∈ t
fm :
  ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
x : ℂ × T
mf : f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
m : x.2 ∈ (extChartAt I (f c z)).source ∧ (x.1, ↑(extChartAt I (f c z)) x.2) ∈ i.he.target
⊢ f x.1 (i.g x.1 x.2) = x.2
Tactic:
have inv := i.he.right_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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m✝ : (c, f c z) ∈ t
fm :
  ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
x : ℂ × T
mf : f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
m : x.2 ∈ (extChartAt I (f c z)).source ∧ (x.1, ↑(extChartAt I (f c z)) x.2) ∈ i.he.target
inv : ↑i.he (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)) = (x.1, ↑(extChartAt I (f c z)) x.2)
⊢ f x.1 (i.g 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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m✝ : (c, f c z) ∈ t
fm :
  ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
x : ℂ × T
mf : f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
m : x.2 ∈ (extChartAt I (f c z)).source ∧ (x.1, ↑(extChartAt I (f c z)) x.2) ∈ i.he.target
inv : ↑i.he (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)) = (x.1, ↑(extChartAt I (f c z)) x.2)
⊢ f x.1 (i.g x.1 x.2) = x.2
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m✝ : (c, f c z) ∈ t
fm :
  ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
x : ℂ × T
mf : f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
m : x.2 ∈ (extChartAt I (f c z)).source ∧ (x.1, ↑(extChartAt I (f c z)) x.2) ∈ i.he.target
inv : ↑i.he (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)) = (x.1, ↑(extChartAt I (f c z)) x.2)
⊢ f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) 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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m✝ : (c, f c z) ∈ t
fm :
  ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
x : ℂ × T
mf : f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
m : x.2 ∈ (extChartAt I (f c z)).source ∧ (x.1, ↑(extChartAt I (f c z)) x.2) ∈ i.he.target
inv : ↑i.he (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)) = (x.1, ↑(extChartAt I (f c z)) x.2)
⊢ f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) 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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m✝ : (c, f c z) ∈ t
fm :
  ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
x : ℂ × T
mf : f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
m : x.2 ∈ (extChartAt I (f c z)).source ∧ (x.1, ↑(extChartAt I (f c z)) x.2) ∈ i.he.target
inv : ↑i.he (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)) = (x.1, ↑(extChartAt I (f c z)) x.2)
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
hq : i.he.symm = q
⊢ f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) 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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m✝ : (c, f c z) ∈ t
fm :
  ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
x : ℂ × T
mf : f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
m : x.2 ∈ (extChartAt I (f c z)).source ∧ (x.1, ↑(extChartAt I (f c z)) x.2) ∈ i.he.target
inv : ↑i.he (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)) = (x.1, ↑(extChartAt I (f c z)) x.2)
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
hq : i.he.symm = q
⊢ f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2) = x.2
Tactic:
rw [hq] at inv mf
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m✝ : (c, f c z) ∈ t
fm :
  ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
x : ℂ × T
m : x.2 ∈ (extChartAt I (f c z)).source ∧ (x.1, ↑(extChartAt I (f c z)) x.2) ∈ i.he.target
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
mf : f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
inv : ↑i.he (↑q (x.1, ↑(extChartAt I (f c z)) x.2)) = (x.1, ↑(extChartAt I (f c z)) x.2)
hq : i.he.symm = q
⊢ f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) 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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m✝ : (c, f c z) ∈ t
fm :
  ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
x : ℂ × T
m : x.2 ∈ (extChartAt I (f c z)).source ∧ (x.1, ↑(extChartAt I (f c z)) x.2) ∈ i.he.target
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
mf : f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
inv : ↑i.he (↑q (x.1, ↑(extChartAt I (f c z)) x.2)) = (x.1, ↑(extChartAt I (f c z)) x.2)
hq : i.he.symm = q
⊢ f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) 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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m✝ : (c, f c z) ∈ t
fm :
  ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
x : ℂ × T
m : x.2 ∈ (extChartAt I (f c z)).source ∧ (x.1, ↑(extChartAt I (f c z)) x.2) ∈ i.he.target
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
mf : f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
inv : i.h (↑q (x.1, ↑(extChartAt I (f c z)) x.2)) = (x.1, ↑(extChartAt I (f c z)) x.2)
hq : i.he.symm = q
⊢ f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) 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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m✝ : (c, f c z) ∈ t
fm :
  ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
x : ℂ × T
m : x.2 ∈ (extChartAt I (f c z)).source ∧ (x.1, ↑(extChartAt I (f c z)) x.2) ∈ i.he.target
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
mf : f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
inv : i.h (↑q (x.1, ↑(extChartAt I (f c z)) x.2)) = (x.1, ↑(extChartAt I (f c z)) x.2)
hq : i.he.symm = q
⊢ f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2) = x.2
Tactic:
have q1 : (q (x.1, extChartAt I (f c z) x.2)).1 = x.1 := by simp only [← hq, i.inv_fst _ 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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m✝ : (c, f c z) ∈ t
fm :
  ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
x : ℂ × T
m : x.2 ∈ (extChartAt I (f c z)).source ∧ (x.1, ↑(extChartAt I (f c z)) x.2) ∈ i.he.target
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
mf : f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
inv : i.h (↑q (x.1, ↑(extChartAt I (f c z)) x.2)) = (x.1, ↑(extChartAt I (f c z)) x.2)
hq : i.he.symm = q
q1 : (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).1 = x.1
⊢ f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) 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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m✝ : (c, f c z) ∈ t
fm :
  ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
x : ℂ × T
m : x.2 ∈ (extChartAt I (f c z)).source ∧ (x.1, ↑(extChartAt I (f c z)) x.2) ∈ i.he.target
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
mf : f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
inv : i.h (↑q (x.1, ↑(extChartAt I (f c z)) x.2)) = (x.1, ↑(extChartAt I (f c z)) x.2)
hq : i.he.symm = q
q1 : (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).1 = x.1
⊢ f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2) = x.2
Tactic:
simp only [Cinv.h, Cinv.f', Prod.eq_iff_fst_eq_snd_eq, q1] 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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m✝ : (c, f c z) ∈ t
fm :
  ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
x : ℂ × T
m : x.2 ∈ (extChartAt I (f c z)).source ∧ (x.1, ↑(extChartAt I (f c z)) x.2) ∈ i.he.target
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
mf : f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
hq : i.he.symm = q
q1 : (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).1 = x.1
inv :
  True ∧
    ↑(extChartAt I (f c z)) (f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2)) =
      ↑(extChartAt I (f c z)) x.2
⊢ f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) 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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m✝ : (c, f c z) ∈ t
fm :
  ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
x : ℂ × T
m : x.2 ∈ (extChartAt I (f c z)).source ∧ (x.1, ↑(extChartAt I (f c z)) x.2) ∈ i.he.target
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
mf : f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
hq : i.he.symm = q
q1 : (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).1 = x.1
inv :
  True ∧
    ↑(extChartAt I (f c z)) (f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2)) =
      ↑(extChartAt I (f c z)) x.2
⊢ f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2) = x.2
Tactic:
nth_rw 2 [← PartialEquiv.left_inv _ m.1]
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m✝ : (c, f c z) ∈ t
fm :
  ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
x : ℂ × T
m : x.2 ∈ (extChartAt I (f c z)).source ∧ (x.1, ↑(extChartAt I (f c z)) x.2) ∈ i.he.target
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
mf : f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
hq : i.he.symm = q
q1 : (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).1 = x.1
inv :
  True ∧
    ↑(extChartAt I (f c z)) (f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2)) =
      ↑(extChartAt I (f c z)) x.2
⊢ f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2) =
    ↑(extChartAt I (f c z)).symm (↑(extChartAt I (f c z)) 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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m✝ : (c, f c z) ∈ t
fm :
  ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
x : ℂ × T
m : x.2 ∈ (extChartAt I (f c z)).source ∧ (x.1, ↑(extChartAt I (f c z)) x.2) ∈ i.he.target
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
mf : f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
hq : i.he.symm = q
q1 : (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).1 = x.1
inv :
  True ∧
    ↑(extChartAt I (f c z)) (f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2)) =
      ↑(extChartAt I (f c z)) x.2
⊢ f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2) =
    ↑(extChartAt I (f c z)).symm (↑(extChartAt I (f c z)) x.2)
Tactic:
nth_rw 2 [← inv.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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m✝ : (c, f c z) ∈ t
fm :
  ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
x : ℂ × T
m : x.2 ∈ (extChartAt I (f c z)).source ∧ (x.1, ↑(extChartAt I (f c z)) x.2) ∈ i.he.target
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
mf : f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
hq : i.he.symm = q
q1 : (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).1 = x.1
inv :
  True ∧
    ↑(extChartAt I (f c z)) (f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2)) =
      ↑(extChartAt I (f c z)) x.2
⊢ f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2) =
    ↑(extChartAt I (f c z)).symm
      (↑(extChartAt I (f c z)) (f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m✝ : (c, f c z) ∈ t
fm :
  ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
x : ℂ × T
m : x.2 ∈ (extChartAt I (f c z)).source ∧ (x.1, ↑(extChartAt I (f c z)) x.2) ∈ i.he.target
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
mf : f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
hq : i.he.symm = q
q1 : (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).1 = x.1
inv :
  True ∧
    ↑(extChartAt I (f c z)) (f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2)) =
      ↑(extChartAt I (f c z)) x.2
⊢ f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2) =
    ↑(extChartAt I (f c z)).symm
      (↑(extChartAt I (f c z)) (f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2)))
Tactic:
refine (PartialEquiv.left_inv _ mf).symm
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = 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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
⊢ IsOpen ((extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target)

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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
⊢ IsOpen ((extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target)
Tactic:
exact (continuousOn_extChartAt _ _).isOpen_inter_preimage (isOpen_extChartAt_source _ _)
  i.he.open_target
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
⊢ (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
Tactic:
have m := ContDiffAt.image_mem_toPartialHomeomorph_target 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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m : i.h (c, i.z') ∈ (ContDiffAt.toPartialHomeomorph i.h ⋯ ⋯ ⋯).target
⊢ (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target

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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m : i.h (c, i.z') ∈ (ContDiffAt.toPartialHomeomorph i.h ⋯ ⋯ ⋯).target
⊢ (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
Tactic:
have e : i.h (c, i.z') = (c, extChartAt I (f c z) (f c z)) := by
  simp only [Cinv.h, Cinv.z', Cinv.f', PartialEquiv.left_inv _ (mem_extChartAt_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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m : i.h (c, i.z') ∈ (ContDiffAt.toPartialHomeomorph i.h ⋯ ⋯ ⋯).target
e : i.h (c, i.z') = (c, ↑(extChartAt I (f c z)) (f c z))
⊢ (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target

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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m : i.h (c, i.z') ∈ (ContDiffAt.toPartialHomeomorph i.h ⋯ ⋯ ⋯).target
e : i.h (c, i.z') = (c, ↑(extChartAt I (f c z)) (f c z))
⊢ (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
Tactic:
rw [e] 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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ (ContDiffAt.toPartialHomeomorph i.h ⋯ ⋯ ⋯).target
e : i.h (c, i.z') = (c, ↑(extChartAt I (f c z)) (f c z))
⊢ (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target

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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ (ContDiffAt.toPartialHomeomorph i.h ⋯ ⋯ ⋯).target
e : i.h (c, i.z') = (c, ↑(extChartAt I (f c z)) (f c z))
⊢ (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
Tactic:
exact m
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m : i.h (c, i.z') ∈ (ContDiffAt.toPartialHomeomorph i.h ⋯ ⋯ ⋯).target
⊢ i.h (c, i.z') = (c, ↑(extChartAt I (f c z)) (f c z))
Tactic:
simp only [Cinv.h, Cinv.z', Cinv.f', PartialEquiv.left_inv _ (mem_extChartAt_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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
⊢ (c, f c z) ∈ t
Tactic:
simp only [m', mem_inter_iff, mem_preimage, mem_extChartAt_source, true_and_iff, ← ht,
  extChartAt_prod, PartialEquiv.prod_coe, extChartAt_eq_refl, PartialEquiv.refl_coe, id,
  PartialEquiv.prod_source, prod_mk_mem_set_prod_eq, PartialEquiv.refl_source, mem_univ]
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
Tactic:
refine ContinuousAt.eventually_mem ?_ (extChartAt_source_mem_nhds' I ?_)
State after:
case refine_1
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ContinuousAt (fun x => f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2)) (c, f c z)

case refine_2
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ f (c, f c z).1 (↑(extChartAt I z).symm (↑i.he.symm ((c, f c z).1, ↑(extChartAt I (f c z)) (c, f c z).2)).2) ∈
    (extChartAt I (f c z)).source

State before:
case refine_1
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ContinuousAt (fun x => f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2)) (c, f c z)
Tactic:
apply i.fa.continuousAt.comp₂_of_eq continuousAt_fst
State after:
case refine_1.hh
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ContinuousAt (fun x => (extChartAt I z).symm.1 (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) (c, f c z)

case refine_1.e
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ((c, f c z).1, (extChartAt I z).symm.1 (↑i.he.symm ((c, f c z).1, ↑(extChartAt I (f c z)) (c, f c z).2)).2) = (c, z)

State before:
case refine_1.hh
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ContinuousAt (fun x => (extChartAt I z).symm.1 (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) (c, f c z)
Tactic:
refine ContinuousAt.comp ?_ ?_
State after:
case refine_1.hh.refine_1
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ContinuousAt (extChartAt I z).invFun (↑i.he.symm ((c, f c z).1, ↑(extChartAt I (f c z)) (c, f c z).2)).2

case refine_1.hh.refine_2
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ContinuousAt (fun x => (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) (c, f c z)

State before:
case refine_1.hh.refine_1
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ContinuousAt (extChartAt I z).invFun (↑i.he.symm ((c, f c z).1, ↑(extChartAt I (f c z)) (c, f c z).2)).2
Tactic:
simp only [i.inv_at]
State after:
case refine_1.hh.refine_1
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ContinuousAt (extChartAt I z).invFun (↑(extChartAt I z) z)

State before:
case refine_1.hh.refine_1
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ContinuousAt (extChartAt I z).invFun (↑(extChartAt I z) z)
Tactic:
exact continuousAt_extChartAt_symm I _
State after:
no goals

State before:
case refine_1.hh.refine_2
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ContinuousAt (fun x => (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) (c, f c z)
Tactic:
apply continuousAt_snd.comp
State after:
case refine_1.hh.refine_2
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ContinuousAt (fun x => ↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)) (c, f c z)

State before:
case refine_1.hh.refine_2
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ContinuousAt (fun x => ↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)) (c, f c z)
Tactic:
refine (PartialHomeomorph.continuousAt i.he.symm ?_).comp ?_
State after:
case refine_1.hh.refine_2.refine_1
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ((c, f c z).1, ↑(extChartAt I (f c z)) (c, f c z).2) ∈ i.he.symm.source

case refine_1.hh.refine_2.refine_2
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ContinuousAt (fun x => (x.1, ↑(extChartAt I (f c z)) x.2)) (c, f c z)

State before:
case refine_1.hh.refine_2.refine_1
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ((c, f c z).1, ↑(extChartAt I (f c z)) (c, f c z).2) ∈ i.he.symm.source
Tactic:
simp only [m', (he i).symm_source]
State after:
no goals

State before:
case refine_1.hh.refine_2.refine_2
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ContinuousAt (fun x => (x.1, ↑(extChartAt I (f c z)) x.2)) (c, f c z)
Tactic:
apply continuousAt_fst.prod
State after:
case refine_1.hh.refine_2.refine_2
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ContinuousAt (fun x => ↑(extChartAt I (f c z)) x.2) (c, f c z)

State before:
case refine_1.hh.refine_2.refine_2
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ContinuousAt (fun x => ↑(extChartAt I (f c z)) x.2) (c, f c z)
Tactic:
apply (continuousAt_extChartAt I _).comp_of_eq
State after:
case refine_1.hh.refine_2.refine_2.hf
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ContinuousAt (fun x => x.2) (c, f c z)

case refine_1.hh.refine_2.refine_2.hy
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ (c, f c z).2 = f c z

State before:
case refine_1.hh.refine_2.refine_2.hf
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ContinuousAt (fun x => x.2) (c, f c z)
Tactic:
exact continuousAt_snd
State after:
no goals

State before:
case refine_1.hh.refine_2.refine_2.hy
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ (c, f c z).2 = f c z
Tactic:
rfl
State after:
no goals

State before:
case refine_1.e
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ((c, f c z).1, (extChartAt I z).symm.1 (↑i.he.symm ((c, f c z).1, ↑(extChartAt I (f c z)) (c, f c z).2)).2) = (c, z)
Tactic:
simp only [i.inv_at, PartialEquiv.left_inv _ (mem_extChartAt_source _ _),
  PartialEquiv.invFun_as_coe]
State after:
no goals

State before:
case refine_2
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ f (c, f c z).1 (↑(extChartAt I z).symm (↑i.he.symm ((c, f c z).1, ↑(extChartAt I (f c z)) (c, f c z).2)).2) ∈
    (extChartAt I (f c z)).source
Tactic:
simp only [i.inv_at, PartialEquiv.left_inv _ (mem_extChartAt_source _ _)]
State after:
case refine_2
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ f c z ∈ (extChartAt I (f c z)).source

State before:
case refine_2
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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ f c z ∈ (extChartAt I (f c z)).source
Tactic:
apply mem_extChartAt_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 (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m✝ : (c, f c z) ∈ t
fm :
  ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
x : ℂ × T
m : x.2 ∈ (extChartAt I (f c z)).source ∧ (x.1, ↑(extChartAt I (f c z)) x.2) ∈ i.he.target
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
mf : f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
inv : i.h (↑q (x.1, ↑(extChartAt I (f c z)) x.2)) = (x.1, ↑(extChartAt I (f c z)) x.2)
hq : i.he.symm = q
⊢ (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).1 = x.1
Tactic:
simp only [← hq, i.inv_fst _ m.2]
State after:
no goals