internlm/Lean-Github huggingface dataset:
Theorem: ComplexInverseFun.Cinv.right_inv
Proof 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
Proof 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
Theorem: ComplexInverseFun.Cinv.right_inv
Proof 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]
Proof 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)
Theorem: ComplexInverseFun.Cinv.right_inv
Proof 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]
Proof 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)))
Theorem: ComplexInverseFun.Cinv.right_inv
Proof 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
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.right_inv
Proof 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]
Proof 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)
Theorem: ComplexInverseFun.Cinv.right_inv
Proof 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
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.right_inv
Proof 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
Proof 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
Theorem: ComplexInverseFun.Cinv.right_inv
Proof 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 _ _)]
Proof 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
Theorem: ComplexInverseFun.Cinv.right_inv
Proof 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
Proof 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
Theorem: ComplexInverseFun.Cinv.right_inv
Proof 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
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.right_inv
Proof 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 _ _)]
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.right_inv
Proof 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]
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.right_inv
Proof 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 ?_)
Proof 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
Theorem: ComplexInverseFun.Cinv.right_inv
Proof 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
Proof 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)
Theorem: ComplexInverseFun.Cinv.right_inv
Proof 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 ?_ ?_
Proof 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)
Theorem: ComplexInverseFun.Cinv.right_inv
Proof 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]
Proof 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)
Theorem: ComplexInverseFun.Cinv.right_inv
Proof 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 _
Proof state after:
no goals