𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
I✝ : ModelWithCorners 𝕜 E H
inst✝ : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
this :
  ∀ (x : H), HasBasis (𝓝 x) (fun s => s ∈ 𝓝 (↑I x) ∧ IsCompact s) fun s => ↑(ModelWithCorners.symm I) '' (s ∩ range ↑I)
⊢ LocallyCompactSpace H
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
I✝ : ModelWithCorners 𝕜 E H
inst✝ : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
⊢ LocallyCompactSpace H
have : ∀ x : H, (𝓝 x).HasBasis (fun s => s ∈ 𝓝 (I x) ∧ IsCompact s)
    fun s => I.symm '' (s ∩ range I) := fun x ↦ by
  rw [← I.symm_map_nhdsWithin_range]
  exact ((compact_basis_nhds (I x)).inf_principal _).map _
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
I✝ : ModelWithCorners 𝕜 E H
inst✝ : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
this :
  ∀ (x : H), HasBasis (𝓝 x) (fun s => s ∈ 𝓝 (↑I x) ∧ IsCompact s) fun s => ↑(ModelWithCorners.symm I) '' (s ∩ range ↑I)
⊢ ∀ (x : H) (i : Set E), i ∈ 𝓝 (↑I x) ∧ IsCompact i → IsCompact (↑(ModelWithCorners.symm I) '' (i ∩ range ↑I))
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
I✝ : ModelWithCorners 𝕜 E H
inst✝ : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
this :
  ∀ (x : H), HasBasis (𝓝 x) (fun s => s ∈ 𝓝 (↑I x) ∧ IsCompact s) fun s => ↑(ModelWithCorners.symm I) '' (s ∩ range ↑I)
⊢ LocallyCompactSpace H
refine' locallyCompactSpace_of_hasBasis this _
case intro
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
I✝ : ModelWithCorners 𝕜 E H
inst✝ : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
this :
  ∀ (x : H), HasBasis (𝓝 x) (fun s => s ∈ 𝓝 (↑I x) ∧ IsCompact s) fun s => ↑(ModelWithCorners.symm I) '' (s ∩ range ↑I)
x : H
s : Set E
hsc : IsCompact s
⊢ IsCompact (↑(ModelWithCorners.symm I) '' (s ∩ range ↑I))
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
I✝ : ModelWithCorners 𝕜 E H
inst✝ : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
this :
  ∀ (x : H), HasBasis (𝓝 x) (fun s => s ∈ 𝓝 (↑I x) ∧ IsCompact s) fun s => ↑(ModelWithCorners.symm I) '' (s ∩ range ↑I)
⊢ ∀ (x : H) (i : Set E), i ∈ 𝓝 (↑I x) ∧ IsCompact i → IsCompact (↑(ModelWithCorners.symm I) '' (i ∩ range ↑I))
rintro x s ⟨-, hsc⟩
no goals
case intro
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
I✝ : ModelWithCorners 𝕜 E H
inst✝ : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
this :
  ∀ (x : H), HasBasis (𝓝 x) (fun s => s ∈ 𝓝 (↑I x) ∧ IsCompact s) fun s => ↑(ModelWithCorners.symm I) '' (s ∩ range ↑I)
x : H
s : Set E
hsc : IsCompact s
⊢ IsCompact (↑(ModelWithCorners.symm I) '' (s ∩ range ↑I))
exact (hsc.inter_right I.closed_range).image I.continuous_symm
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
I✝ : ModelWithCorners 𝕜 E H
inst✝ : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
x : H
⊢ HasBasis (map (↑(ModelWithCorners.symm I)) (𝓝[range ↑I] ↑I x)) (fun s => s ∈ 𝓝 (↑I x) ∧ IsCompact s) fun s =>
    ↑(ModelWithCorners.symm I) '' (s ∩ range ↑I)
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
I✝ : ModelWithCorners 𝕜 E H
inst✝ : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
x : H
⊢ HasBasis (𝓝 x) (fun s => s ∈ 𝓝 (↑I x) ∧ IsCompact s) fun s => ↑(ModelWithCorners.symm I) '' (s ∩ range ↑I)
rw [← I.symm_map_nhdsWithin_range]
no goals
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
I✝ : ModelWithCorners 𝕜 E H
inst✝ : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
x : H
⊢ HasBasis (map (↑(ModelWithCorners.symm I)) (𝓝[range ↑I] ↑I x)) (fun s => s ∈ 𝓝 (↑I x) ∧ IsCompact s) fun s =>
    ↑(ModelWithCorners.symm I) '' (s ∩ range ↑I)
exact ((compact_basis_nhds (I x)).inf_principal _).map _