internlm/Lean-Github huggingface dataset:
Theorem: PartialHomeomorph.extend_symm_isOpenMapOn_target
Proof 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
Proof state after:
no goals
Theorem: PartialHomeomorph.extend_symm_isOpenMapOn_target
Proof 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
Proof 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
Theorem: PartialHomeomorph.extend_symm_isOpenMapOn_target
Proof 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
Proof 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
Theorem: PartialHomeomorph.extend_symm_isOpenMapOn_target
Proof 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
Proof state after:
no goals
Theorem: PartialHomeomorph.extend_symm_isOpenMapOn_target
Proof 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]
Proof state after:
no goals
Theorem: PartialHomeomorph.extend_image_mem_nhds_symm
Proof 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
n : Set E
hn : n ∈ 𝓝 x
hn' : n ⊆ (e.extend I).target
⊢ ↑(e.extend I).symm '' n ∈ 𝓝 (↑(e.extend I).symm x)
Tactic:
rcases mem_nhds_iff.mp hn with ⟨t', ht's', ht'open, hxt'⟩
Proof state after:
case intro.intro.intro
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
n : Set E
hn : n ∈ 𝓝 x
hn' : n ⊆ (e.extend I).target
t' : Set E
ht's' : t' ⊆ n
ht'open : IsOpen t'
hxt' : x ∈ t'
⊢ ↑(e.extend I).symm '' n ∈ 𝓝 (↑(e.extend I).symm x)
Theorem: PartialHomeomorph.extend_image_mem_nhds_symm
Proof state before:
case intro.intro.intro
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
n : Set E
hn : n ∈ 𝓝 x
hn' : n ⊆ (e.extend I).target
t' : Set E
ht's' : t' ⊆ n
ht'open : IsOpen t'
hxt' : x ∈ t'
⊢ ↑(e.extend I).symm '' n ∈ 𝓝 (↑(e.extend I).symm x)
Tactic:
rw [mem_nhds_iff]
Proof state after:
case intro.intro.intro
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
n : Set E
hn : n ∈ 𝓝 x
hn' : n ⊆ (e.extend I).target
t' : Set E
ht's' : t' ⊆ n
ht'open : IsOpen t'
hxt' : x ∈ t'
⊢ ∃ t ⊆ ↑(e.extend I).symm '' n, IsOpen t ∧ ↑(e.extend I).symm x ∈ t
Theorem: PartialHomeomorph.extend_image_mem_nhds_symm
Proof state before:
case intro.intro.intro
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
n : Set E
hn : n ∈ 𝓝 x
hn' : n ⊆ (e.extend I).target
t' : Set E
ht's' : t' ⊆ n
ht'open : IsOpen t'
hxt' : x ∈ t'
⊢ ∃ t ⊆ ↑(e.extend I).symm '' n, IsOpen t ∧ ↑(e.extend I).symm x ∈ t
Tactic:
refine ⟨(e.extend I).symm '' t', image_subset _ ht's', ?_, ?_⟩
Proof state after:
case intro.intro.intro.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
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
x : E
n : Set E
hn : n ∈ 𝓝 x
hn' : n ⊆ (e.extend I).target
t' : Set E
ht's' : t' ⊆ n
ht'open : IsOpen t'
hxt' : x ∈ t'
⊢ IsOpen (↑(e.extend I).symm '' t')

case intro.intro.intro.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
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
x : E
n : Set E
hn : n ∈ 𝓝 x
hn' : n ⊆ (e.extend I).target
t' : Set E
ht's' : t' ⊆ n
ht'open : IsOpen t'
hxt' : x ∈ t'
⊢ ↑(e.extend I).symm x ∈ ↑(e.extend I).symm '' t'
Theorem: PartialHomeomorph.extend_image_mem_nhds_symm
Proof state before:
case intro.intro.intro.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
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
x : E
n : Set E
hn : n ∈ 𝓝 x
hn' : n ⊆ (e.extend I).target
t' : Set E
ht's' : t' ⊆ n
ht'open : IsOpen t'
hxt' : x ∈ t'
⊢ IsOpen (↑(e.extend I).symm '' t')
Tactic:
apply e.extend_symm_isOpenMapOn_target _ ht'open (Subset.trans ht's' hn')
Proof state after:
no goals
Theorem: PartialHomeomorph.extend_image_mem_nhds_symm
Proof state before:
case intro.intro.intro.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
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
x : E
n : Set E
hn : n ∈ 𝓝 x
hn' : n ⊆ (e.extend I).target
t' : Set E
ht's' : t' ⊆ n
ht'open : IsOpen t'
hxt' : x ∈ t'
⊢ ↑(e.extend I).symm x ∈ ↑(e.extend I).symm '' t'
Tactic:
exact mem_image_of_mem (e.extend I).symm hxt'
Proof state after:
no goals
Theorem: unused_extendedChart_leftInverse'
Proof 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
e : PartialHomeomorph M H
t : Set E
ht : t ⊆ ↑(e.extend I) '' e.source
⊢ ↑(e.extend I) ∘ ↑(e.extend I).symm '' t = t
Tactic:
sorry
Proof state after:
no goals
Theorem: extendedChart_image_nhds_on
Proof 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 : M
n : Set M
hn : n ∈ 𝓝 x
hn₂ : n ⊆ e.source
⊢ ↑I ∘ ↑e '' n ∈ 𝓝 (↑(e.extend I) x)
Tactic:
rw [image_comp]
Proof 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 : M
n : Set M
hn : n ∈ 𝓝 x
hn₂ : n ⊆ e.source
⊢ ↑I '' (↑e '' n) ∈ 𝓝 (↑(e.extend I) x)
Theorem: extendedChart_image_nhds_on
Proof 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 : M
n : Set M
hn : n ∈ 𝓝 x
hn₂ : n ⊆ e.source
⊢ ↑I '' (↑e '' n) ∈ 𝓝 (↑(e.extend I) x)
Tactic:
apply I.toOpenEmbedding.isOpenMap.image_mem_nhds (e.image_mem_nhds (hn₂ (mem_of_mem_nhds hn)) hn)
Proof state after:
no goals
Theorem: PartialHomeomorph.mapsTo_extend_symm
Proof 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
e : PartialHomeomorph M H
⊢ MapsTo (↑(e.extend I).symm) (↑(e.extend I) '' e.source) e.source
Tactic:
rintro x ⟨s, hs, rfl⟩
Proof state after:
case intro.intro
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
e : PartialHomeomorph M H
s : M
hs : s ∈ e.source
⊢ ↑(e.extend I).symm (↑(e.extend I) s) ∈ e.source
Theorem: PartialHomeomorph.mapsTo_extend_symm
Proof state before:
case intro.intro
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
e : PartialHomeomorph M H
s : M
hs : s ∈ e.source
⊢ ↑(e.extend I).symm (↑(e.extend I) s) ∈ e.source
Tactic:
have : (e.extend I).symm (e.extend I s) = s := e.extend_left_inv _ hs
Proof state after:
case intro.intro
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
e : PartialHomeomorph M H
s : M
hs : s ∈ e.source
this : ↑(e.extend I).symm (↑(e.extend I) s) = s
⊢ ↑(e.extend I).symm (↑(e.extend I) s) ∈ e.source
Theorem: PartialHomeomorph.mapsTo_extend_symm
Proof state before:
case intro.intro
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
e : PartialHomeomorph M H
s : M
hs : s ∈ e.source
this : ↑(e.extend I).symm (↑(e.extend I) s) = s
⊢ ↑(e.extend I).symm (↑(e.extend I) s) ∈ e.source
Tactic:
rw [this]
Proof state after:
case intro.intro
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
e : PartialHomeomorph M H
s : M
hs : s ∈ e.source
this : ↑(e.extend I).symm (↑(e.extend I) s) = s
⊢ s ∈ e.source
Theorem: PartialHomeomorph.mapsTo_extend_symm
Proof state before:
case intro.intro
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
e : PartialHomeomorph M H
s : M
hs : s ∈ e.source
this : ↑(e.extend I).symm (↑(e.extend I) s) = s
⊢ s ∈ e.source
Tactic:
exact hs
Proof state after:
no goals
Theorem: ModelWithCorners.right_inv''
Proof 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
Proof 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
Theorem: ModelWithCorners.right_inv''
Proof 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
Proof state after:
no goals
Theorem: ModelWithCorners.right_inv''
Proof 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]
Proof 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
Theorem: ModelWithCorners.right_inv''
Proof 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
Proof state after:
no goals
Theorem: PartialHomeomorph.extend_right_inv
Proof 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
Proof 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
Theorem: PartialHomeomorph.extend_right_inv
Proof 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
Proof 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
Theorem: PartialHomeomorph.extend_right_inv
Proof 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
Proof state after:
no goals
Theorem: PartialHomeomorph.extend_right_inv
Proof 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
Proof state after:
no goals
Theorem: PartialHomeomorph.extend_right_inv
Proof 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
Proof 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✝
Theorem: PartialHomeomorph.extend_right_inv
Proof 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
Proof state after:
no goals
Theorem: PartialHomeomorph.extend_right_inv
Proof 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]
Proof state after:
no goals
Theorem: bijective_iff_inverses'
Proof 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
X : Type u_7
Y : Type u_8
inst✝³ : NormedAddCommGroup X
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f : X →L[ℝ] Y
g : Y →L[ℝ] X
h1 : g.comp f = ContinuousLinearMap.id ℝ X
h2 : f.comp g = ContinuousLinearMap.id ℝ Y
⊢ Bijective ⇑f
Tactic:
have h : f.toFun ∘ g.toFun = id := calc f.toFun ∘ g.toFun
  _ = (f.comp g).toFun := rfl
  _ = (ContinuousLinearMap.id ℝ Y).toFun := by rw [h2]
  _ = id := rfl
Proof 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
X : Type u_7
Y : Type u_8
inst✝³ : NormedAddCommGroup X
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f : X →L[ℝ] Y
g : Y →L[ℝ] X
h1 : g.comp f = ContinuousLinearMap.id ℝ X
h2 : f.comp g = ContinuousLinearMap.id ℝ Y
h : f.toFun ∘ g.toFun = id
⊢ Bijective ⇑f