-- Mathlib/Geometry/Manifold/IsManifold/Basic.lean
theorem locallyCompactSpace [LocallyCompactSpace E] (I : ModelWithCorners 𝕜 E H) :
    LocallyCompactSpace H

Proof state:
case intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
this : ∀ (x : H), (𝓝 x).HasBasis (fun s => s ∈ 𝓝 (↑I x) ∧ IsCompact s) fun s => ↑I.symm '' (s ∩ range ↑I)
x : H
s : Set E
hsc : IsCompact s
⊢ IsCompact (↑I.symm '' (s ∩ range ↑I))

Tactic:
exact (hsc.inter_right I.isClosed_range).image I.continuous_symm

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
⊢ LocallyCompactSpace H

Tactic:
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 _

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
this : ∀ (x : H), (𝓝 x).HasBasis (fun s => s ∈ 𝓝 (↑I x) ∧ IsCompact s) fun s => ↑I.symm '' (s ∩ range ↑I)
⊢ LocallyCompactSpace H

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
x : H
⊢ (𝓝 x).HasBasis (fun s => s ∈ 𝓝 (↑I x) ∧ IsCompact s) fun s => ↑I.symm '' (s ∩ range ↑I)

Tactic:
rw [← I.symm_map_nhdsWithin_range]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
x : H
⊢ (map (↑I.symm) (𝓝[range ↑I] ↑I x)).HasBasis (fun s => s ∈ 𝓝 (↑I x) ∧ IsCompact s) fun s => ↑I.symm '' (s ∩ range ↑I)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
x : H
⊢ (map (↑I.symm) (𝓝[range ↑I] ↑I x)).HasBasis (fun s => s ∈ 𝓝 (↑I x) ∧ IsCompact s) fun s => ↑I.symm '' (s ∩ range ↑I)

Tactic:
exact ((compact_basis_nhds (I x)).inf_principal _).map _

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
this : ∀ (x : H), (𝓝 x).HasBasis (fun s => s ∈ 𝓝 (↑I x) ∧ IsCompact s) fun s => ↑I.symm '' (s ∩ range ↑I)
⊢ ∀ (x : H) (i : Set E), i ∈ 𝓝 (↑I x) ∧ IsCompact i → IsCompact (↑I.symm '' (i ∩ range ↑I))

Tactic:
rintro x s ⟨-, hsc⟩

Result:
case intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
this : ∀ (x : H), (𝓝 x).HasBasis (fun s => s ∈ 𝓝 (↑I x) ∧ IsCompact s) fun s => ↑I.symm '' (s ∩ range ↑I)
x : H
s : Set E
hsc : IsCompact s
⊢ IsCompact (↑I.symm '' (s ∩ range ↑I))

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
this : ∀ (x : H), (𝓝 x).HasBasis (fun s => s ∈ 𝓝 (↑I x) ∧ IsCompact s) fun s => ↑I.symm '' (s ∩ range ↑I)
⊢ LocallyCompactSpace H

Tactic:
refine .of_hasBasis this ?_

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
this : ∀ (x : H), (𝓝 x).HasBasis (fun s => s ∈ 𝓝 (↑I x) ∧ IsCompact s) fun s => ↑I.symm '' (s ∩ range ↑I)
⊢ ∀ (x : H) (i : Set E), i ∈ 𝓝 (↑I x) ∧ IsCompact i → IsCompact (↑I.symm '' (i ∩ range ↑I))