Theorem: ComplexInverseFun.Cinv.inv_fst (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 ∈ i.he.target, (↑i.he.symm x).1 = x.1
Tactic:
intro x m
State after:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
x : ℂ × ℂ
m : x ∈ i.he.target
⊢ (↑i.he.symm x).1 = x.1

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
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

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
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

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
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

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
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

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]
State after:
no goals