Theorem: diffeoOn_differential_bijective (Sard/ManifoldAux.lean)

State before:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
⊢ Bijective ⇑(mfderiv I J f x)
Tactic:
set A := mfderiv I J f x
State after:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
⊢ Bijective ⇑A

State before:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
⊢ Bijective ⇑A
Tactic:
let y := f x
State after:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
⊢ Bijective ⇑A

State before:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
⊢ Bijective ⇑A
Tactic:
have hyx : g y = x := hleft_inv x hx
State after:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
⊢ Bijective ⇑A

State before:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
⊢ Bijective ⇑A
Tactic:
have hysource : y ∈ t := hst hx
State after:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
⊢ Bijective ⇑A

State before:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
⊢ Bijective ⇑A
Tactic:
have : f '' s = t := subset_antisymm (mapsTo'.mp hst) (fun y hy ↦ ⟨g y, hts hy, hright_inv y hy⟩)
State after:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this : f '' s = t
⊢ Bijective ⇑A

State before:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this : f '' s = t
⊢ Bijective ⇑A
Tactic:
have : g '' t = s := by
  rw [← this, ← image_comp]
  exact EqOn.image_eq_self hleft_inv
State after:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
⊢ Bijective ⇑A

State before:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
⊢ Bijective ⇑A
Tactic:
have hopen : IsOpen (g '' t) := by rw [this]; exact hs
State after:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
hopen : IsOpen (g '' t)
⊢ Bijective ⇑A

State before:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
hopen : IsOpen (g '' t)
⊢ Bijective ⇑A
Tactic:
have hx2 : x ∈ g '' t := by simp_rw [this]; exact hx
State after:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
hopen : IsOpen (g '' t)
hx2 : x ∈ g '' t
⊢ Bijective ⇑A

State before:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
hopen : IsOpen (g '' t)
hx2 : x ∈ g '' t
⊢ Bijective ⇑A
Tactic:
let A' := mfderiv J I g y
State after:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
hopen : IsOpen (g '' t)
hx2 : x ∈ g '' t
A' : TangentSpace J y →L[ℝ] TangentSpace I (g y) := mfderiv J I g y
⊢ Bijective ⇑A

State before:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
hopen : IsOpen (g '' t)
hx2 : x ∈ g '' t
A' : TangentSpace J y →L[ℝ] TangentSpace I (g y) := mfderiv J I g y
⊢ Bijective ⇑A
Tactic:
have hr : 1 ≤ (r : ℕ∞) := Nat.one_le_cast.mpr (Nat.one_le_of_lt hr)
State after:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr✝ : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
hopen : IsOpen (g '' t)
hx2 : x ∈ g '' t
A' : TangentSpace J y →L[ℝ] TangentSpace I (g y) := mfderiv J I g y
hr : 1 ≤ ↑r
⊢ Bijective ⇑A

State before:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr✝ : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
hopen : IsOpen (g '' t)
hx2 : x ∈ g '' t
A' : TangentSpace J y →L[ℝ] TangentSpace I (g y) := mfderiv J I g y
hr : 1 ≤ ↑r
⊢ Bijective ⇑A
Tactic:
have hgat : MDifferentiableAt J I g y :=
  (hg.contMDiffAt (ht.mem_nhds (hst hx))).mdifferentiableAt hr
State after:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr✝ : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
hopen : IsOpen (g '' t)
hx2 : x ∈ g '' t
A' : TangentSpace J y →L[ℝ] TangentSpace I (g y) := mfderiv J I g y
hr : 1 ≤ ↑r
hgat : MDifferentiableAt J I g y
⊢ Bijective ⇑A

State before:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr✝ : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
hopen : IsOpen (g '' t)
hx2 : x ∈ g '' t
A' : TangentSpace J y →L[ℝ] TangentSpace I (g y) := mfderiv J I g y
hr : 1 ≤ ↑r
hgat : MDifferentiableAt J I g y
⊢ Bijective ⇑A
Tactic:
have hfat : MDifferentiableAt I J f x :=
  (hf.contMDiffAt (hs.mem_nhds hx)).mdifferentiableAt hr
State after:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr✝ : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
hopen : IsOpen (g '' t)
hx2 : x ∈ g '' t
A' : TangentSpace J y →L[ℝ] TangentSpace I (g y) := mfderiv J I g y
hr : 1 ≤ ↑r
hgat : MDifferentiableAt J I g y
hfat : MDifferentiableAt I J f x
⊢ Bijective ⇑A

State before:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr✝ : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
hopen : IsOpen (g '' t)
hx2 : x ∈ g '' t
A' : TangentSpace J y →L[ℝ] TangentSpace I (g y) := mfderiv J I g y
hr : 1 ≤ ↑r
hgat : MDifferentiableAt J I g y
hfat : MDifferentiableAt I J f x
⊢ Bijective ⇑A
Tactic:
have inv1 := calc A'.comp A
  _ = mfderiv I I (g ∘ f) x := (mfderiv_comp x hgat hfat).symm
  _ = mfderivWithin I I (g ∘ f) (g '' t) x := (mfderivWithin_of_isOpen hopen hx2).symm
  _ = mfderivWithin I I id (g '' t) x :=
    mfderivWithin_congr (hopen.uniqueMDiffWithinAt hx2) (this ▸ hleft_inv) (hleft_inv x (this ▸ hx2))
  _ = mfderiv I I id x := mfderivWithin_of_isOpen hopen hx2
  _ = ContinuousLinearMap.id ℝ (TangentSpace I x) := mfderiv_id I
State after:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr✝ : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
hopen : IsOpen (g '' t)
hx2 : x ∈ g '' t
A' : TangentSpace J y →L[ℝ] TangentSpace I (g y) := mfderiv J I g y
hr : 1 ≤ ↑r
hgat : MDifferentiableAt J I g y
hfat : MDifferentiableAt I J f x
inv1 : A'.comp A = ContinuousLinearMap.id ℝ (TangentSpace I x)
⊢ Bijective ⇑A

State before:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr✝ : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
hopen : IsOpen (g '' t)
hx2 : x ∈ g '' t
A' : TangentSpace J y →L[ℝ] TangentSpace I (g y) := mfderiv J I g y
hr : 1 ≤ ↑r
hgat : MDifferentiableAt J I g y
hfat : MDifferentiableAt I J f x
inv1 : A'.comp A = ContinuousLinearMap.id ℝ (TangentSpace I x)
⊢ Bijective ⇑A
Tactic:
have inv2 := calc A.comp A'
  _ = mfderiv J J (f ∘ g) y := by
        rw [← (hleft_inv x hx)] at hfat
        exact (hyx ▸ (mfderiv_comp (f x) hfat hgat)).symm
  _ = mfderivWithin J J (f ∘ g) t y := (mfderivWithin_of_isOpen ht hysource).symm
  _ = mfderivWithin J J id t y :=
        mfderivWithin_congr (ht.uniqueMDiffWithinAt hysource) hright_inv (hright_inv y hysource)
  _ = mfderiv J J id y := mfderivWithin_of_isOpen ht hysource
  _ = ContinuousLinearMap.id ℝ (TangentSpace J (f x)) := mfderiv_id J
State after:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr✝ : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
hopen : IsOpen (g '' t)
hx2 : x ∈ g '' t
A' : TangentSpace J y →L[ℝ] TangentSpace I (g y) := mfderiv J I g y
hr : 1 ≤ ↑r
hgat : MDifferentiableAt J I g y
hfat : MDifferentiableAt I J f x
inv1 : A'.comp A = ContinuousLinearMap.id ℝ (TangentSpace I x)
inv2 : A.comp A' = ContinuousLinearMap.id ℝ (TangentSpace J (f x))
⊢ Bijective ⇑A

State before:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr✝ : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
hopen : IsOpen (g '' t)
hx2 : x ∈ g '' t
A' : TangentSpace J y →L[ℝ] TangentSpace I (g y) := mfderiv J I g y
hr : 1 ≤ ↑r
hgat : MDifferentiableAt J I g y
hfat : MDifferentiableAt I J f x
inv1 : A'.comp A = ContinuousLinearMap.id ℝ (TangentSpace I x)
inv2 : A.comp A' = ContinuousLinearMap.id ℝ (TangentSpace J (f x))
⊢ Bijective ⇑A
Tactic:
exact bijective_iff_inverses' inv1 inv2
State after:
no goals

State before:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this : f '' s = t
⊢ g '' t = s
Tactic:
rw [← this, ← image_comp]
State after:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this : f '' s = t
⊢ g ∘ f '' s = s

State before:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this : f '' s = t
⊢ g ∘ f '' s = s
Tactic:
exact EqOn.image_eq_self hleft_inv
State after:
no goals

State before:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
⊢ IsOpen (g '' t)
Tactic:
rw [this]
State after:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
⊢ IsOpen s

State before:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
⊢ IsOpen s
Tactic:
exact hs
State after:
no goals

State before:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
hopen : IsOpen (g '' t)
⊢ x ∈ g '' t
Tactic:
simp_rw [this]
State after:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
hopen : IsOpen (g '' t)
⊢ x ∈ s

State before:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
hopen : IsOpen (g '' t)
⊢ x ∈ s
Tactic:
exact hx
State after:
no goals

State before:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr✝ : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
hopen : IsOpen (g '' t)
hx2 : x ∈ g '' t
A' : TangentSpace J y →L[ℝ] TangentSpace I (g y) := mfderiv J I g y
hr : 1 ≤ ↑r
hgat : MDifferentiableAt J I g y
hfat : MDifferentiableAt I J f x
inv1 : A'.comp A = ContinuousLinearMap.id ℝ (TangentSpace I x)
⊢ A.comp A' = mfderiv J J (f ∘ g) y
Tactic:
rw [← (hleft_inv x hx)] at hfat
State after:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr✝ : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
hopen : IsOpen (g '' t)
hx2 : x ∈ g '' t
A' : TangentSpace J y →L[ℝ] TangentSpace I (g y) := mfderiv J I g y
hr : 1 ≤ ↑r
hgat : MDifferentiableAt J I g y
hfat : MDifferentiableAt I J f (g (f x))
inv1 : A'.comp A = ContinuousLinearMap.id ℝ (TangentSpace I x)
⊢ A.comp A' = mfderiv J J (f ∘ g) y

State before:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
H : Type u_2
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr✝ : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
hopen : IsOpen (g '' t)
hx2 : x ∈ g '' t
A' : TangentSpace J y →L[ℝ] TangentSpace I (g y) := mfderiv J I g y
hr : 1 ≤ ↑r
hgat : MDifferentiableAt J I g y
hfat : MDifferentiableAt I J f (g (f x))
inv1 : A'.comp A = ContinuousLinearMap.id ℝ (TangentSpace I x)
⊢ A.comp A' = mfderiv J J (f ∘ g) y
Tactic:
exact (hyx ▸ (mfderiv_comp (f x) hfat hgat)).symm
State after:
no goals