Theorem: diffeo_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
r : ℕ
hr : 1 ≤ r
f : M ≃ₘ^↑r⟮I, J⟯ N
x : M
⊢ Bijective ⇑(mfderiv I J (⇑f) x)
Tactic:
refine diffeoOn_differential_bijective I J hr isOpen_univ isOpen_univ trivial (mapsTo_univ f.toFun univ) (mapsTo_univ f.invFun univ) ?_ ?_ ?_ ?_
State after:
case refine_1
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
r : ℕ
hr : 1 ≤ r
f : M ≃ₘ^↑r⟮I, J⟯ N
x : M
⊢ ∀ x ∈ univ, f.invFun (f x) = x

case refine_2
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
r : ℕ
hr : 1 ≤ r
f : M ≃ₘ^↑r⟮I, J⟯ N
x : M
⊢ ∀ y ∈ univ, f (f.invFun y) = y

case refine_3
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
r : ℕ
hr : 1 ≤ r
f : M ≃ₘ^↑r⟮I, J⟯ N
x : M
⊢ ContMDiffOn I J (↑r) (⇑f) univ

case refine_4
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
r : ℕ
hr : 1 ≤ r
f : M ≃ₘ^↑r⟮I, J⟯ N
x : M
⊢ ContMDiffOn J I (↑r) f.invFun univ

State before:
case refine_1
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
r : ℕ
hr : 1 ≤ r
f : M ≃ₘ^↑r⟮I, J⟯ N
x : M
⊢ ∀ x ∈ univ, f.invFun (f x) = x
Tactic:
exact fun _ hx ↦ f.toPartialEquiv.left_inv' hx
State after:
no goals

State before:
case refine_2
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
r : ℕ
hr : 1 ≤ r
f : M ≃ₘ^↑r⟮I, J⟯ N
x : M
⊢ ∀ y ∈ univ, f (f.invFun y) = y
Tactic:
exact fun _ hy ↦ f.toPartialEquiv.right_inv' hy
State after:
no goals

State before:
case refine_3
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
r : ℕ
hr : 1 ≤ r
f : M ≃ₘ^↑r⟮I, J⟯ N
x : M
⊢ ContMDiffOn I J (↑r) (⇑f) univ
Tactic:
exact contMDiffOn_univ.mpr f.contMDiff_toFun
State after:
no goals

State before:
case refine_4
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
r : ℕ
hr : 1 ≤ r
f : M ≃ₘ^↑r⟮I, J⟯ N
x : M
⊢ ContMDiffOn J I (↑r) f.invFun univ
Tactic:
exact contMDiffOn_univ.mpr f.contMDiff_invFun
State after:
no goals