Theorem: PartialHomeomorph.extend_symm_isOpenMapOn_target (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
t : Set E
hopen : IsOpen t
ht : t ⊆ (e.extend I).target
⊢ IsOpen (↑(e.extend I).symm '' t)
Tactic:
have h : IsOpen (I.invFun '' t) := I.toOpenEmbedding_symm.open_iff_image_open.mp hopen
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
t : Set E
hopen : IsOpen t
ht : t ⊆ (e.extend I).target
h : IsOpen (I.invFun '' t)
⊢ IsOpen (↑(e.extend I).symm '' t)

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
t : Set E
hopen : IsOpen t
ht : t ⊆ (e.extend I).target
h : IsOpen (I.invFun '' t)
⊢ IsOpen (↑(e.extend I).symm '' t)
Tactic:
have : (e.extend I).target = I.symm ⁻¹' e.target := by
  let r := e.extend_target I
  rw [I.range_eq_univ, inter_univ] at r
  exact r
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
t : Set E
hopen : IsOpen t
ht : t ⊆ (e.extend I).target
h : IsOpen (I.invFun '' t)
this : (e.extend I).target = ↑I.symm ⁻¹' e.target
⊢ IsOpen (↑(e.extend I).symm '' t)

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
t : Set E
hopen : IsOpen t
ht : t ⊆ (e.extend I).target
h : IsOpen (I.invFun '' t)
this : (e.extend I).target = ↑I.symm ⁻¹' e.target
⊢ IsOpen (↑(e.extend I).symm '' t)
Tactic:
have : I.symm '' t ⊆ e.target := calc I.symm '' t
  _ ⊆ I.symm '' ((e.extend I).target) := image_subset _ ht
  _ = I.symm '' (I.symm ⁻¹' e.target) := by rw [this]
  _ ⊆ e.target := image_preimage_subset I.symm e.target
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
t : Set E
hopen : IsOpen t
ht : t ⊆ (e.extend I).target
h : IsOpen (I.invFun '' t)
this✝ : (e.extend I).target = ↑I.symm ⁻¹' e.target
this : ↑I.symm '' t ⊆ e.target
⊢ IsOpen (↑(e.extend I).symm '' t)

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
t : Set E
hopen : IsOpen t
ht : t ⊆ (e.extend I).target
h : IsOpen (I.invFun '' t)
this✝ : (e.extend I).target = ↑I.symm ⁻¹' e.target
this : ↑I.symm '' t ⊆ e.target
⊢ IsOpen (↑(e.extend I).symm '' t)
Tactic:
rw [extend_coe_symm, 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
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
t : Set E
hopen : IsOpen t
ht : t ⊆ (e.extend I).target
h : IsOpen (I.invFun '' t)
this✝ : (e.extend I).target = ↑I.symm ⁻¹' e.target
this : ↑I.symm '' t ⊆ e.target
⊢ IsOpen (↑e.symm '' (↑I.symm '' t))

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
t : Set E
hopen : IsOpen t
ht : t ⊆ (e.extend I).target
h : IsOpen (I.invFun '' t)
this✝ : (e.extend I).target = ↑I.symm ⁻¹' e.target
this : ↑I.symm '' t ⊆ e.target
⊢ IsOpen (↑e.symm '' (↑I.symm '' t))
Tactic:
exact e.symm_isOpenMapOn_target h 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
e : PartialHomeomorph M H
t : Set E
hopen : IsOpen t
ht : t ⊆ (e.extend I).target
h : IsOpen (I.invFun '' t)
⊢ (e.extend I).target = ↑I.symm ⁻¹' e.target
Tactic:
let r := e.extend_target 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
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
t : Set E
hopen : IsOpen t
ht : t ⊆ (e.extend I).target
h : IsOpen (I.invFun '' t)
r : (e.extend I).target = ↑I.symm ⁻¹' e.target ∩ range ↑I := extend_target e I
⊢ (e.extend I).target = ↑I.symm ⁻¹' e.target

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
t : Set E
hopen : IsOpen t
ht : t ⊆ (e.extend I).target
h : IsOpen (I.invFun '' t)
r : (e.extend I).target = ↑I.symm ⁻¹' e.target ∩ range ↑I := extend_target e I
⊢ (e.extend I).target = ↑I.symm ⁻¹' e.target
Tactic:
rw [I.range_eq_univ, inter_univ] at r
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
t : Set E
hopen : IsOpen t
ht : t ⊆ (e.extend I).target
h : IsOpen (I.invFun '' t)
r : (e.extend I).target = ↑I.symm ⁻¹' e.target
⊢ (e.extend I).target = ↑I.symm ⁻¹' e.target

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
t : Set E
hopen : IsOpen t
ht : t ⊆ (e.extend I).target
h : IsOpen (I.invFun '' t)
r : (e.extend I).target = ↑I.symm ⁻¹' e.target
⊢ (e.extend I).target = ↑I.symm ⁻¹' e.target
Tactic:
exact r
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
t : Set E
hopen : IsOpen t
ht : t ⊆ (e.extend I).target
h : IsOpen (I.invFun '' t)
this : (e.extend I).target = ↑I.symm ⁻¹' e.target
⊢ ↑I.symm '' (e.extend I).target = ↑I.symm '' (↑I.symm ⁻¹' e.target)
Tactic:
rw [this]
State after:
no goals