Theorem: ModelWithCorners.right_inv'' (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
inst✝ : I.Boundaryless
x : E
⊢ (↑I ∘ I.invFun) x = x
Tactic:
have : x ∈ range I := by rw [I.range_eq_univ]; exact trivial
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
inst✝ : I.Boundaryless
x : E
this : x ∈ range ↑I
⊢ (↑I ∘ I.invFun) x = x

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
inst✝ : I.Boundaryless
x : E
this : x ∈ range ↑I
⊢ (↑I ∘ I.invFun) x = x
Tactic:
exact I.right_inv this
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
inst✝ : I.Boundaryless
x : E
⊢ x ∈ range ↑I
Tactic:
rw [I.range_eq_univ]
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
inst✝ : I.Boundaryless
x : E
⊢ x ∈ univ

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
inst✝ : I.Boundaryless
x : E
⊢ x ∈ univ
Tactic:
exact trivial
State after:
no goals