awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this_1 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X
hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : (e : (↑(f ⁻¹' {x}) : Type u_1)) → Set E := fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦ V (↑e : E) ∩ (φ e).source
hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
this_2 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e
h_1 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst_1] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ (e : (↑(f ⁻¹' {x}) : Type u_1)), f '' V' e
this_3 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
this : Nonempty E
⊢ IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)

Tactic:
.of_trivialization (t := hU'.trivializationDiscrete _ _
    (fun e s hs ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩) (fun e ↦ ?_)
    (fun e ↦ .mono subset_rfl (hUV e) (surjOn_image f _))
    (pairwise_disjoint_mono disj.subtype fun e ↦ inter_subset_left)
    ((preimage_mono (inter_subset_left.trans hUW)).trans hWV))
    ⟨hxU, Set.mem_iInter.mpr fun e ↦ ⟨e, ⟨(hV e).1, (hφ e).1⟩, e.2⟩⟩

Premises used: Iff.mpr, Set.mem_iInter, And.left, And.intro, Exists.intro, IsEvenlyCovered.of_trivialization, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this_1 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X
hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : (e : (↑(f ⁻¹' {x}) : Type u_1)) → Set E := fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦ V (↑e : E) ∩ (φ e).source
hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
this_2 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e
h_1 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst_1] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ (e : (↑(f ⁻¹' {x}) : Type u_1)), f '' V' e
this_3 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
this : Nonempty E
inr : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)) (s : Set X) (hs : s ⊆ U') (h : IsOpen[inst_1] s), IsOpen[inst] (f ⁻¹' s ∩ V' e)
inr₁ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)) (s : Set X) (hs : s ⊆ U') (h : IsOpen[inst] (f ⁻¹' s ∩ V' e)), IsOpen[inst_1] s
inr₂ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), InjOn f (V' e)
⊢ IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)

Tactic:
refine .of_trivialization (t := hU'.trivializationDiscrete _ _
    (fun e s hs ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩) (fun e ↦ ?_)
    (fun e ↦ .mono subset_rfl (hUV e) (surjOn_image f _))
    (pairwise_disjoint_mono disj.subtype fun e ↦ inter_subset_left)
    ((preimage_mono (inter_subset_left.trans hUW)).trans hWV))
    ⟨hxU, Set.mem_iInter.mpr fun e ↦ ⟨e, ⟨(hV e).1, (hφ e).1⟩, e.2⟩⟩
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h_1 : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this_1 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X
hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : (e : (↑(f ⁻¹' {x}) : Type u_1)) → Set E := fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦ V (↑e : E) ∩ (φ e).source
hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
this_2 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e
h_2 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst_1] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ (e : (↑(f ⁻¹' {x}) : Type u_1)), f '' V' e
this_3 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
this : Nonempty E
e : (↑(f ⁻¹' {x}) : Type u_1)
s : Set X
hs : s ⊆ U'
h : IsOpen[inst_1] s
⊢ IsOpen[inst] ((φ e).source ∩ (↑(φ e) : E → X) ⁻¹' s ∩ V (↑e : E))

Tactic:
((φ e).isOpen_inter_preimage h).inter (hV e).2

Premises used: OpenPartialHomeomorph.isOpen_inter_preimage, And.right, IsOpen.inter, Subtype.val
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h_1 : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this_1 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X
hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : (e : (↑(f ⁻¹' {x}) : Type u_1)) → Set E := fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦ V (↑e : E) ∩ (φ e).source
hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
this_2 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e
h_2 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst_1] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ (e : (↑(f ⁻¹' {x}) : Type u_1)), f '' V' e
this_3 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
this : Nonempty E
e : (↑(f ⁻¹' {x}) : Type u_1)
s : Set X
hs : s ⊆ U'
h : IsOpen[inst_1] s
h₁ : f ⁻¹' s ∩ V' e = (φ e).source ∩ (↑(φ e) : E → X) ⁻¹' s ∩ V (↑e : E)
⊢ IsOpen[inst] (f ⁻¹' s ∩ V' e)

Tactic:
convert! ((φ e).isOpen_inter_preimage h).inter (hV e).2 using 1

Premises used: OpenPartialHomeomorph.isOpen_inter_preimage, And.right, IsOpen.inter, Subtype.val
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h_1 : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this_1 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X
hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : (e : (↑(f ⁻¹' {x}) : Type u_1)) → Set E := fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦ V (↑e : E) ∩ (φ e).source
hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
this_2 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e
h_2 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst_1] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ (e : (↑(f ⁻¹' {x}) : Type u_1)), f '' V' e
this_3 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
this : Nonempty E
e : (↑(f ⁻¹' {x}) : Type u_1)
s : Set X
hs : s ⊆ U'
h : IsOpen[inst_1] s
h₁ : f ⁻¹' s ∩ (V (↑e : E) ∩ (φ e).source) = (φ e).source ∩ f ⁻¹' s ∩ V (↑e : E)
⊢ f ⁻¹' s ∩ V' e = (φ e).source ∩ (↑(φ e) : E → X) ⁻¹' s ∩ V (↑e : E)

Tactic:
simp_rw [(hφ e).2, V']

Premises used: And.right
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h_1 : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this_1 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X
hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : (e : (↑(f ⁻¹' {x}) : Type u_1)) → Set E := fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦ V (↑e : E) ∩ (φ e).source
hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
this_2 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e
h_2 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst_1] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ (e : (↑(f ⁻¹' {x}) : Type u_1)), f '' V' e
this_3 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
this : Nonempty E
e : (↑(f ⁻¹' {x}) : Type u_1)
s : Set X
hs : s ⊆ U'
h : IsOpen[inst_1] s
⊢ f ⁻¹' s ∩ (V (↑e : E) ∩ (φ e).source) = (φ e).source ∩ f ⁻¹' s ∩ V (↑e : E)

Tactic:
ac_rfl
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h_1 : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this_1 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X
hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : (e : (↑(f ⁻¹' {x}) : Type u_1)) → Set E := fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦ V (↑e : E) ∩ (φ e).source
hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
this_2 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e
h_2 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst_1] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ (e : (↑(f ⁻¹' {x}) : Type u_1)), f '' V' e
this_3 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
this : Nonempty E
e : (↑(f ⁻¹' {x}) : Type u_1)
s : Set X
hs : s ⊆ U'
h : IsOpen[inst] (f ⁻¹' s ∩ V' e)
rw : f '' V' e ⊆ f '' (φ e).source
⊢ f '' V' e ⊆ (φ e).target

Tactic:
rw [← (φ e).image_source_eq_target, (hφ e).2]

Premises used: OpenPartialHomeomorph.image_source_eq_target, And.right
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h_1 : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this_1 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X
hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : (e : (↑(f ⁻¹' {x}) : Type u_1)) → Set E := fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦ V (↑e : E) ∩ (φ e).source
hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
this_2 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e
h_2 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst_1] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ (e : (↑(f ⁻¹' {x}) : Type u_1)), f '' V' e
this_3 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
this : Nonempty E
e : (↑(f ⁻¹' {x}) : Type u_1)
s : Set X
hs : s ⊆ U'
h : IsOpen[inst] (f ⁻¹' s ∩ V' e)
⊢ f '' V' e ⊆ f '' (φ e).source

Tactic:
image_mono inter_subset_right

Premises used: Set.image_mono, Set.inter_subset_right
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h_1 : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this_1 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X
hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : (e : (↑(f ⁻¹' {x}) : Type u_1)) → Set E := fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦ V (↑e : E) ∩ (φ e).source
hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
this_2 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e
h_2 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst_1] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ (e : (↑(f ⁻¹' {x}) : Type u_1)), f '' V' e
this_3 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
this : Nonempty E
e : (↑(f ⁻¹' {x}) : Type u_1)
s : Set X
hs : s ⊆ U'
h : IsOpen[inst] (f ⁻¹' s ∩ V' e)
⊢ f '' V' e ⊆ f '' (φ e).source

Tactic:
exact image_mono inter_subset_right

Premises used: Set.image_mono, Set.inter_subset_right
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h_1 : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this_1 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X
hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : (e : (↑(f ⁻¹' {x}) : Type u_1)) → Set E := fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦ V (↑e : E) ∩ (φ e).source
hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
this_2 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e
h_2 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst_1] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ (e : (↑(f ⁻¹' {x}) : Type u_1)), f '' V' e
this_3 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
this : Nonempty E
e : (↑(f ⁻¹' {x}) : Type u_1)
s : Set X
hs : s ⊆ U'
h : IsOpen[inst] (f ⁻¹' s ∩ V' e)
⊢ s ⊆ (φ e).target

Tactic:
have : s ⊆ (φ e).target := hs.trans <| (hUV e).trans <| by
      rw [← (φ e).image_source_eq_target, (hφ e).2]; exact image_mono inter_subset_right
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h_1 : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this_1 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X
hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : (e : (↑(f ⁻¹' {x}) : Type u_1)) → Set E := fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦ V (↑e : E) ∩ (φ e).source
hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
this_2 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e
h_2 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst_1] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ (e : (↑(f ⁻¹' {x}) : Type u_1)), f '' V' e
this_3 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
this_4 : Nonempty E
e : (↑(f ⁻¹' {x}) : Type u_1)
s : Set X
hs : s ⊆ U'
h : IsOpen[inst] (f ⁻¹' s ∩ V' e)
this : s ⊆ (φ e).target
inr : IsOpen[inst] (f ⁻¹' s ∩ (φ e).source)
⊢ IsOpen[inst_1] s

Tactic:
rw [← (φ e).isOpen_symm_image_iff_of_subset_target this,
      (φ e).symm_image_eq_source_inter_preimage this, (hφ e).2, inter_comm]

Premises used: Set.inter_comm, OpenPartialHomeomorph.isOpen_symm_image_iff_of_subset_target, And.right, OpenPartialHomeomorph.symm_image_eq_source_inter_preimage
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h_1 : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this_1 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X
hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : (e : (↑(f ⁻¹' {x}) : Type u_1)) → Set E := fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦ V (↑e : E) ∩ (φ e).source
hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
this_2 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e
h_2 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst_1] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ (e : (↑(f ⁻¹' {x}) : Type u_1)), f '' V' e
this_3 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
this_4 : Nonempty E
e : (↑(f ⁻¹' {x}) : Type u_1)
s : Set X
hs : s ⊆ U'
h : IsOpen[inst] (f ⁻¹' s ∩ V' e)
this : s ⊆ (φ e).target
⊢ IsOpen[inst] (f ⁻¹' s ∩ V' e)

Tactic:
h
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h_1 : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this_1 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X
hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : (e : (↑(f ⁻¹' {x}) : Type u_1)) → Set E := fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦ V (↑e : E) ∩ (φ e).source
hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
this_2 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e
h_2 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst_1] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ (e : (↑(f ⁻¹' {x}) : Type u_1)), f '' V' e
this_3 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
this_4 : Nonempty E
e : (↑(f ⁻¹' {x}) : Type u_1)
s : Set X
hs : s ⊆ U'
h : IsOpen[inst] (f ⁻¹' s ∩ V' e)
this : s ⊆ (φ e).target
h₁ : f ⁻¹' s ∩ (φ e).source = f ⁻¹' s ∩ V' e
⊢ IsOpen[inst] (f ⁻¹' s ∩ (φ e).source)

Tactic:
convert! h using 1
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h_1 : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this_1 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X
hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : (e : (↑(f ⁻¹' {x}) : Type u_1)) → Set E := fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦ V (↑e : E) ∩ (φ e).source
hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
this_2 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e
h_2 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst_1] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ (e : (↑(f ⁻¹' {x}) : Type u_1)), f '' V' e
this_3 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
this_4 : Nonempty E
e : (↑(f ⁻¹' {x}) : Type u_1)
s : Set X
hs : s ⊆ U'
h : IsOpen[inst] (f ⁻¹' s ∩ V' e)
this : s ⊆ (φ e).target
⊢ f ⁻¹' s ∩ (φ e).source = f ⁻¹' s ∩ V' e

Tactic:
inter_eq_inter_iff_left.mpr ⟨fun e' h ↦ h.2.2, fun e' h ↦ ⟨?_ , h.2⟩⟩

Premises used: Iff.mpr, Set.inter_eq_inter_iff_left, And.right, And.intro
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h_1 : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this_1 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X
hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : (e : (↑(f ⁻¹' {x}) : Type u_1)) → Set E := fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦ V (↑e : E) ∩ (φ e).source
hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
this_2 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e
h_2 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst_1] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ (e : (↑(f ⁻¹' {x}) : Type u_1)), f '' V' e
this_3 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
this_4 : Nonempty E
e : (↑(f ⁻¹' {x}) : Type u_1)
s : Set X
hs : s ⊆ U'
h : IsOpen[inst] (f ⁻¹' s ∩ V' e)
this : s ⊆ (φ e).target
h₁ : ∀ (e' : E) (h : e' ∈ f ⁻¹' s ∩ (φ e).source), e' ∈ V (↑e : E)
⊢ f ⁻¹' s ∩ (φ e).source = f ⁻¹' s ∩ V' e

Tactic:
refine inter_eq_inter_iff_left.mpr ⟨fun e' h ↦ h.2.2, fun e' h ↦ ⟨?_ , h.2⟩⟩