internlm/Lean-Github huggingface dataset:
Theorem: ComplexInverseFun.Cinv.inv_fst
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
x : ℂ × ℂ
m : x ∈ i.he.target
e : ↑i.he (↑i.he.symm x) = x
q : ℂ × ℂ
hq : ↑i.he.symm x = q
⊢ q.1 = x.1
Tactic:
rw [hq] at e
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
x : ℂ × ℂ
m : x ∈ i.he.target
q : ℂ × ℂ
e : ↑i.he q = x
hq : ↑i.he.symm x = q
⊢ q.1 = x.1
Theorem: ComplexInverseFun.Cinv.inv_fst
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
x : ℂ × ℂ
m : x ∈ i.he.target
q : ℂ × ℂ
e : ↑i.he q = x
hq : ↑i.he.symm x = q
⊢ q.1 = x.1
Tactic:
rw [Cinv.he, ContDiffAt.toPartialHomeomorph_coe i.ha.contDiffAt i.has_dhe le_top, Cinv.h] at e
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
x : ℂ × ℂ
m : x ∈ i.he.target
q : ℂ × ℂ
e : (q.1, i.f' q) = x
hq : ↑i.he.symm x = q
⊢ q.1 = x.1
Theorem: ComplexInverseFun.Cinv.inv_fst
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
x : ℂ × ℂ
m : x ∈ i.he.target
q : ℂ × ℂ
e : (q.1, i.f' q) = x
hq : ↑i.he.symm x = q
⊢ q.1 = x.1
Tactic:
rw [← e]
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
⊢ ∀ᶠ (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
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
⊢ ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (i.g x.1 x.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
⊢ ∀ᶠ (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
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
⊢ ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (i.g x.1 x.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
⊢ ∀ᶠ (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
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
⊢ ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (i.g x.1 x.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
⊢ ∀ᶠ (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]
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
⊢ ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (i.g x.1 x.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) 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) ?_)
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,
    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
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,
    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
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 ∈ 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
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 ∈ 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
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
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
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
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
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
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
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
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]
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
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
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
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
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
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
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
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
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
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
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.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
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
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
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
⊢ 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]
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
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