internlm/Lean-Github huggingface dataset:
Theorem: ComplexInverseFun.Cinv.inv_at
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
a : ⋯.localInverse ⋯ ⋯ (i.h (c, i.z')) = (c, i.z')
⊢ (↑i.he.symm (c, ↑(extChartAt I (f c z)) (f c z))).2 = ↑(extChartAt I z) z
Tactic:
have e : ContDiffAt.localInverse i.ha.contDiffAt i.has_dhe le_top = i.he.symm := rfl
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
a : ⋯.localInverse ⋯ ⋯ (i.h (c, i.z')) = (c, i.z')
e : ⋯.localInverse ⋯ ⋯ = ↑i.he.symm
⊢ (↑i.he.symm (c, ↑(extChartAt I (f c z)) (f c z))).2 = ↑(extChartAt I z) z
Theorem: ComplexInverseFun.Cinv.inv_at
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
a : ⋯.localInverse ⋯ ⋯ (i.h (c, i.z')) = (c, i.z')
e : ⋯.localInverse ⋯ ⋯ = ↑i.he.symm
⊢ (↑i.he.symm (c, ↑(extChartAt I (f c z)) (f c z))).2 = ↑(extChartAt I z) z
Tactic:
rw [e] at a
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
a : ↑i.he.symm (i.h (c, i.z')) = (c, i.z')
e : ⋯.localInverse ⋯ ⋯ = ↑i.he.symm
⊢ (↑i.he.symm (c, ↑(extChartAt I (f c z)) (f c z))).2 = ↑(extChartAt I z) z
Theorem: ComplexInverseFun.Cinv.inv_at
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
a : ↑i.he.symm (i.h (c, i.z')) = (c, i.z')
e : ⋯.localInverse ⋯ ⋯ = ↑i.he.symm
⊢ (↑i.he.symm (c, ↑(extChartAt I (f c z)) (f c z))).2 = ↑(extChartAt I z) z
Tactic:
clear 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
a : ↑i.he.symm (i.h (c, i.z')) = (c, i.z')
⊢ (↑i.he.symm (c, ↑(extChartAt I (f c z)) (f c z))).2 = ↑(extChartAt I z) z
Theorem: ComplexInverseFun.Cinv.inv_at
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
a : ↑i.he.symm (i.h (c, i.z')) = (c, i.z')
⊢ (↑i.he.symm (c, ↑(extChartAt I (f c z)) (f c z))).2 = ↑(extChartAt I z) z
Tactic:
simp only [Cinv.z', Cinv.h, Cinv.f', PartialEquiv.left_inv _ (mem_extChartAt_source _ _)] at a
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
a : ↑i.he.symm (c, ↑(extChartAt I (f c z)) (f c z)) = (c, ↑(extChartAt I z) z)
⊢ (↑i.he.symm (c, ↑(extChartAt I (f c z)) (f c z))).2 = ↑(extChartAt I z) z
Theorem: ComplexInverseFun.Cinv.inv_at
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
a : ↑i.he.symm (c, ↑(extChartAt I (f c z)) (f c z)) = (c, ↑(extChartAt I z) z)
⊢ (↑i.he.symm (c, ↑(extChartAt I (f c z)) (f c z))).2 = ↑(extChartAt I z) z
Tactic:
rw [a]
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.left_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 : ℂ × S) in 𝓝 (c, z), i.g x.1 (f x.1 x.2) = x.2
Tactic:
generalize ht :
    ((extChartAt II (c, z)).source ∩ extChartAt II (c, z) ⁻¹' i.he.source : Set (ℂ × S)) = t
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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i.g x.1 (f x.1 x.2) = x.2
Theorem: ComplexInverseFun.Cinv.left_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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i.g x.1 (f x.1 x.2) = x.2
Tactic:
have o : IsOpen t := by
  rw [← ht]
  exact (continuousOn_extChartAt _ _).isOpen_inter_preimage (isOpen_extChartAt_source _ _)
    i.he.open_source
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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i.g x.1 (f x.1 x.2) = x.2
Theorem: ComplexInverseFun.Cinv.left_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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i.g x.1 (f x.1 x.2) = x.2
Tactic:
have m : (c, z) ∈ t := by
  simp only [mem_inter_iff, mem_preimage, mem_extChartAt_source, true_and_iff, ← ht]
  exact ContDiffAt.mem_toPartialHomeomorph_source i.ha.contDiffAt i.has_dhe le_top
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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m : (c, z) ∈ t
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i.g x.1 (f x.1 x.2) = x.2
Theorem: ComplexInverseFun.Cinv.left_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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m : (c, z) ∈ t
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i.g x.1 (f x.1 x.2) = x.2
Tactic:
apply Filter.eventuallyEq_of_mem (o.mem_nhds m)
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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m : (c, z) ∈ t
⊢ EqOn (fun x => i.g x.1 (f x.1 x.2)) (fun x => x.2) t
Theorem: ComplexInverseFun.Cinv.left_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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m : (c, z) ∈ t
⊢ EqOn (fun x => i.g x.1 (f x.1 x.2)) (fun x => x.2) t
Tactic:
intro x m
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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x ∈ t
⊢ (fun x => i.g x.1 (f x.1 x.2)) x = (fun x => x.2) x
Theorem: ComplexInverseFun.Cinv.left_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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x ∈ t
⊢ (fun x => i.g x.1 (f x.1 x.2)) x = (fun x => x.2) x
Tactic:
simp only [mem_inter_iff, mem_preimage, extChartAt_prod, extChartAt_eq_refl, ← ht,
  PartialEquiv.prod_source, PartialEquiv.refl_source, mem_prod_eq, mem_univ, true_and_iff,
  PartialEquiv.prod_coe, PartialEquiv.refl_coe, id] at m
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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
⊢ (fun x => i.g x.1 (f x.1 x.2)) x = (fun x => x.2) x
Theorem: ComplexInverseFun.Cinv.left_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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
⊢ (fun x => i.g x.1 (f x.1 x.2)) x = (fun x => x.2) x
Tactic:
have inv := i.he.left_inv m.2
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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
inv : ↑i.he.symm (↑i.he (x.1, ↑(extChartAt I z) x.2)) = (x.1, ↑(extChartAt I z) x.2)
⊢ (fun x => i.g x.1 (f x.1 x.2)) x = (fun x => x.2) x
Theorem: ComplexInverseFun.Cinv.left_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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
inv : ↑i.he.symm (↑i.he (x.1, ↑(extChartAt I z) x.2)) = (x.1, ↑(extChartAt I z) x.2)
⊢ (fun x => i.g x.1 (f x.1 x.2)) x = (fun x => x.2) x
Tactic:
simp only [Cinv.g]
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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
inv : ↑i.he.symm (↑i.he (x.1, ↑(extChartAt I z) x.2)) = (x.1, ↑(extChartAt I z) x.2)
⊢ ↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) (f x.1 x.2))).2 = x.2
Theorem: ComplexInverseFun.Cinv.left_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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
inv : ↑i.he.symm (↑i.he (x.1, ↑(extChartAt I z) x.2)) = (x.1, ↑(extChartAt I z) x.2)
⊢ ↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) (f x.1 x.2))).2 = x.2
Tactic:
generalize hq : i.he.symm = q
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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
inv : ↑i.he.symm (↑i.he (x.1, ↑(extChartAt I z) x.2)) = (x.1, ↑(extChartAt I z) x.2)
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
hq : i.he.symm = q
⊢ ↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) (f x.1 x.2))).2 = x.2
Theorem: ComplexInverseFun.Cinv.left_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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
inv : ↑i.he.symm (↑i.he (x.1, ↑(extChartAt I z) x.2)) = (x.1, ↑(extChartAt I z) x.2)
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
hq : i.he.symm = q
⊢ ↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) (f x.1 x.2))).2 = x.2
Tactic:
rw [hq] at inv
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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
inv : ↑q (↑i.he (x.1, ↑(extChartAt I z) x.2)) = (x.1, ↑(extChartAt I z) x.2)
hq : i.he.symm = q
⊢ ↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) (f x.1 x.2))).2 = x.2
Theorem: ComplexInverseFun.Cinv.left_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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
inv : ↑q (↑i.he (x.1, ↑(extChartAt I z) x.2)) = (x.1, ↑(extChartAt I z) x.2)
hq : i.he.symm = q
⊢ ↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) (f x.1 x.2))).2 = x.2
Tactic:
rw [Cinv.he, ContDiffAt.toPartialHomeomorph_coe i.ha.contDiffAt i.has_dhe le_top] at inv
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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
inv : ↑q (i.h (x.1, ↑(extChartAt I z) x.2)) = (x.1, ↑(extChartAt I z) x.2)
hq : i.he.symm = q
⊢ ↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) (f x.1 x.2))).2 = x.2
Theorem: ComplexInverseFun.Cinv.left_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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
inv : ↑q (i.h (x.1, ↑(extChartAt I z) x.2)) = (x.1, ↑(extChartAt I z) x.2)
hq : i.he.symm = q
⊢ ↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) (f x.1 x.2))).2 = x.2
Tactic:
simp only [Cinv.h, Cinv.f', PartialEquiv.left_inv _ m.1] at inv
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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
hq : i.he.symm = q
inv : ↑q (x.1, ↑(extChartAt I (f c z)) (f x.1 x.2)) = (x.1, ↑(extChartAt I z) x.2)
⊢ ↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) (f x.1 x.2))).2 = x.2
Theorem: ComplexInverseFun.Cinv.left_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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
m✝ : (c, z) ∈ t
x : ℂ × S
m : x.2 ∈ (extChartAt I z).source ∧ (x.1, ↑(extChartAt I z) x.2) ∈ i.he.source
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
hq : i.he.symm = q
inv : ↑q (x.1, ↑(extChartAt I (f c z)) (f x.1 x.2)) = (x.1, ↑(extChartAt I z) x.2)
⊢ ↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) (f x.1 x.2))).2 = x.2
Tactic:
simp only [inv, PartialEquiv.left_inv _ m.1]
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.left_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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = 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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
⊢ IsOpen ((extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source)
Theorem: ComplexInverseFun.Cinv.left_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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
⊢ IsOpen ((extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source)
Tactic:
exact (continuousOn_extChartAt _ _).isOpen_inter_preimage (isOpen_extChartAt_source _ _)
  i.he.open_source
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.left_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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
⊢ (c, z) ∈ t
Tactic:
simp only [mem_inter_iff, mem_preimage, mem_extChartAt_source, true_and_iff, ← ht]
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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
⊢ ↑(extChartAt (I.prod I) (c, z)) (c, z) ∈ i.he.source
Theorem: ComplexInverseFun.Cinv.left_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 (ℂ × S)
ht : (extChartAt (I.prod I) (c, z)).source ∩ ↑(extChartAt (I.prod I) (c, z)) ⁻¹' i.he.source = t
o : IsOpen t
⊢ ↑(extChartAt (I.prod I) (c, z)) (c, z) ∈ i.he.source
Tactic:
exact ContDiffAt.mem_toPartialHomeomorph_source i.ha.contDiffAt i.has_dhe le_top
Proof state after:
no goals
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 ∈ i.he.target, (↑i.he.symm x).1 = x.1
Tactic:
intro x 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
x : ℂ × ℂ
m : x ∈ i.he.target
⊢ (↑i.he.symm x).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
⊢ (↑i.he.symm x).1 = x.1
Tactic:
have e : i.he (i.he.symm x) = x := i.he.right_inv 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
x : ℂ × ℂ
m : x ∈ i.he.target
e : ↑i.he (↑i.he.symm x) = x
⊢ (↑i.he.symm x).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
e : ↑i.he (↑i.he.symm x) = x
⊢ (↑i.he.symm x).1 = x.1
Tactic:
generalize hq : i.he.symm x = 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
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