Theorem: PartialHomeomorph.extend_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
e : PartialHomeomorph M H
x : E
hx : x ∈ ↑(e.extend I) '' e.source
⊢ (↑(e.extend I) ∘ ↑(e.extend I).symm) x = x
Tactic:
have : I.invFun x ∈ e.target := by aesop
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
e : PartialHomeomorph M H
x : E
hx : x ∈ ↑(e.extend I) '' e.source
this : I.invFun x ∈ e.target
⊢ (↑(e.extend I) ∘ ↑(e.extend I).symm) 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
e : PartialHomeomorph M H
x : E
hx : x ∈ ↑(e.extend I) '' e.source
this : I.invFun x ∈ e.target
⊢ (↑(e.extend I) ∘ ↑(e.extend I).symm) x = x
Tactic:
have aux : ∀ y : H, y ∈ e.target → (e ∘ e.invFun) y = y := by intros; aesop
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
e : PartialHomeomorph M H
x : E
hx : x ∈ ↑(e.extend I) '' e.source
this : I.invFun x ∈ e.target
aux : ∀ y ∈ e.target, (↑e ∘ e.invFun) y = y
⊢ (↑(e.extend I) ∘ ↑(e.extend I).symm) 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
e : PartialHomeomorph M H
x : E
hx : x ∈ ↑(e.extend I) '' e.source
this : I.invFun x ∈ e.target
aux : ∀ y ∈ e.target, (↑e ∘ e.invFun) y = y
⊢ (↑(e.extend I) ∘ ↑(e.extend I).symm) x = x
Tactic:
calc ((e.extend I) ∘ (e.extend I).symm) x
  _ = I ((e ∘ e.invFun) (I.invFun x)) := rfl
  _ = I (I.invFun x) := by simp_rw [aux (I.invFun x) this]
  _ = x := I.right_inv'' x
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
e : PartialHomeomorph M H
x : E
hx : x ∈ ↑(e.extend I) '' e.source
⊢ I.invFun x ∈ e.target
Tactic:
aesop
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
e : PartialHomeomorph M H
x : E
hx : x ∈ ↑(e.extend I) '' e.source
this : I.invFun x ∈ e.target
⊢ ∀ y ∈ e.target, (↑e ∘ e.invFun) y = y
Tactic:
intros
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
e : PartialHomeomorph M H
x : E
hx : x ∈ ↑(e.extend I) '' e.source
this : I.invFun x ∈ e.target
y✝ : H
a✝ : y✝ ∈ e.target
⊢ (↑e ∘ e.invFun) y✝ = 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
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
x : E
hx : x ∈ ↑(e.extend I) '' e.source
this : I.invFun x ∈ e.target
y✝ : H
a✝ : y✝ ∈ e.target
⊢ (↑e ∘ e.invFun) y✝ = y✝
Tactic:
aesop
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
e : PartialHomeomorph M H
x : E
hx : x ∈ ↑(e.extend I) '' e.source
this : I.invFun x ∈ e.target
aux : ∀ y ∈ e.target, (↑e ∘ e.invFun) y = y
⊢ ↑I ((↑e ∘ e.invFun) (I.invFun x)) = ↑I (I.invFun x)
Tactic:
simp_rw [aux (I.invFun x) this]
State after:
no goals