-- Mathlib/Topology/IsLocalHomeomorph.lean
theorem isTopologicalBasis (hf : IsLocalHomeomorph f) : IsTopologicalBasis
    {U : Set X | ∃ V : Set Y, IsOpen V ∧ ∃ s : C(V,X), f ∘ s = (↑) ∧ Set.range s = U}

Proof state:
case refine_1.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
U : Set Y
hU : IsOpen U
s : C(↑U, X)
hs : f ∘ ⇑s = Subtype.val
⊢ IsOpen (Set.range ⇑s)

Tactic:
refine (isOpenEmbedding_of_comp hf (hs ▸ ⟨IsEmbedding.subtypeVal, ?_⟩)
  s.continuous).isOpen_range

Result:
case refine_1.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
U : Set Y
hU : IsOpen U
s : C(↑U, X)
hs : f ∘ ⇑s = Subtype.val
⊢ IsOpen (Set.range Subtype.val)

Proof state:
case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
⊢ ∀ u ∈ {U | ∃ V, IsOpen V ∧ ∃ s, f ∘ ⇑s = Subtype.val ∧ Set.range ⇑s = U}, IsOpen u

Tactic:
rintro _ ⟨U, hU, s, hs, rfl⟩

Result:
case refine_1.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
U : Set Y
hU : IsOpen U
s : C(↑U, X)
hs : f ∘ ⇑s = Subtype.val
⊢ IsOpen (Set.range ⇑s)

Proof state:
case refine_2.intro.intro.refine_1.h
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen U
f : PartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph ↑f
y : ↑(f.target ∩ ↑f.symm ⁻¹' U)
⊢ (↑f ∘ ⇑{ toFun := (f.target ∩ ↑f.symm ⁻¹' U).restrict f.invFun, continuous_toFun := ⋯ }) y = ↑y

Tactic:
exact f.right_inv y.2.1

Result:
no goals

Proof state:
case refine_2.intro.intro.refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen U
f : PartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph ↑f
⊢ ↑f ∘ ⇑{ toFun := (f.target ∩ ↑f.symm ⁻¹' U).restrict f.invFun, continuous_toFun := ⋯ } = Subtype.val

Tactic:
ext y

Result:
case refine_2.intro.intro.refine_1.h
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen U
f : PartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph ↑f
y : ↑(f.target ∩ ↑f.symm ⁻¹' U)
⊢ (↑f ∘ ⇑{ toFun := (f.target ∩ ↑f.symm ⁻¹' U).restrict f.invFun, continuous_toFun := ⋯ }) y = ↑y

Proof state:
case refine_2.intro.intro.refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen U
f : PartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph ↑f
⊢ f.source ∩ ↑f ⁻¹' (f.target ∩ ↑f.symm ⁻¹' U) = f.source ∩ U

Tactic:
rw [Set.preimage_inter, ← Set.inter_assoc, Set.inter_eq_self_of_subset_left
  f.source_preimage_target, f.source_inter_preimage_inv_preimage]

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
U : Set Y
hU : IsOpen U
s : C(↑U, X)
hs : f ∘ ⇑s = Subtype.val
⊢ IsOpen (Set.range Subtype.val)

Tactic:
rwa [Subtype.range_val]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
⊢ IsTopologicalBasis {U | ∃ V, IsOpen V ∧ ∃ s, f ∘ ⇑s = Subtype.val ∧ Set.range ⇑s = U}

Tactic:
refine isTopologicalBasis_of_isOpen_of_nhds ?_ fun x U hx hU ↦ ?_

Result:
case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
⊢ ∀ u ∈ {U | ∃ V, IsOpen V ∧ ∃ s, f ∘ ⇑s = Subtype.val ∧ Set.range ⇑s = U}, IsOpen u

case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
x : X
U : Set X
hx : x ∈ U
hU : IsOpen U
⊢ ∃ v ∈ {U | ∃ V, IsOpen V ∧ ∃ s, f ∘ ⇑s = Subtype.val ∧ Set.range ⇑s = U}, x ∈ v ∧ v ⊆ U

Proof state:
case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
x : X
U : Set X
hx : x ∈ U
hU : IsOpen U
⊢ ∃ v ∈ {U | ∃ V, IsOpen V ∧ ∃ s, f ∘ ⇑s = Subtype.val ∧ Set.range ⇑s = U}, x ∈ v ∧ v ⊆ U

Tactic:
obtain ⟨f, hxf, rfl⟩ := hf x

Result:
case refine_2.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen U
f : PartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph ↑f
⊢ ∃ v ∈ {U | ∃ V, IsOpen V ∧ ∃ s, ↑f ∘ ⇑s = Subtype.val ∧ Set.range ⇑s = U}, x ∈ v ∧ v ⊆ U

Proof state:
case refine_2.intro.intro.refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen U
f : PartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph ↑f
⊢ f.toPartialEquiv.2 '' (f.target ∩ ↑f.symm ⁻¹' U) = f.source ∩ U

Tactic:
apply (f.symm_image_target_inter_eq _).trans

Result:
case refine_2.intro.intro.refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen U
f : PartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph ↑f
⊢ f.source ∩ ↑f ⁻¹' (f.target ∩ ↑f.symm ⁻¹' U) = f.source ∩ U

Proof state:
case refine_2.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen U
f : PartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph ↑f
⊢ ∃ v ∈ {U | ∃ V, IsOpen V ∧ ∃ s, ↑f ∘ ⇑s = Subtype.val ∧ Set.range ⇑s = U}, x ∈ v ∧ v ⊆ U

Tactic:
refine ⟨f.source ∩ U, ⟨f.target ∩ f.symm ⁻¹' U, f.symm.isOpen_inter_preimage hU,
  ⟨_, continuousOn_iff_continuous_restrict.mp (f.continuousOn_invFun.mono fun _ h ↦ h.1)⟩,
  ?_, (Set.range_restrict _ _).trans ?_⟩, ⟨hxf, hx⟩, fun _ h ↦ h.2⟩

Result:
case refine_2.intro.intro.refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen U
f : PartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph ↑f
⊢ ↑f ∘ ⇑{ toFun := (f.target ∩ ↑f.symm ⁻¹' U).restrict f.invFun, continuous_toFun := ⋯ } = Subtype.val

case refine_2.intro.intro.refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen U
f : PartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph ↑f
⊢ f.toPartialEquiv.2 '' (f.target ∩ ↑f.symm ⁻¹' U) = f.source ∩ U