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
s : Set X
inst_2 : Nonempty (X → E)
ι : Type ?u.94810
inst_3 : Nonempty ι
inst_4 : TopologicalSpace ι
inst_5 : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst_1] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst_1] W ↔ IsOpen[inst] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ (i : ι), U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : (i : ι) → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
F : PartialEquiv.{u_1, max ?u.94810 u_2} E (X × ι) :=
  { toFun := fun (e : E) ↦ (f e, if he : f e ∈ V then idx e he else Classical.arbitrary ι),
    invFun := fun (x : X × ι) ↦ if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1, source := f ⁻¹' V,
    target := SProd.sprod (β := Set ι) V Set.univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }
open_preim : ∀ {W : Set X} (hWV : W ⊆ V) (open_W : IsOpen[inst_1] W), IsOpen[inst] (f ⁻¹' W)
open_source : IsOpen[inst] (PartialEquiv.source.{u_1, max u_2 ?u.94810} F)
cont_f : ContinuousOn f (PartialEquiv.source.{u_1, max u_2 ?u.94810} F)
i : ι
W : Set E
open_W : IsOpen[inst] W
e : E
h_1 : f e ∈ V ∧ e ∈ U i
hV : f e ∈ V
hU : e ∈ U i
h : (if h : f e ∈ V then inv i ⋯ else Classical.arbitrary (X → E) (f e)) ∈ W ↔ e ∈ W
h₁ : inv i ⋯ ∈ W ↔ e ∈ W
h₂ h₃ : e ∈ W ↔ e ∈ W
⊢ Membership.mem (γ := Set X) ((fun (x : X) ↦ if h : x ∈ V then inv i ⋯ else Classical.arbitrary (X → E) x) ⁻¹' W)
      (f e) ↔
    e ∈ W

Tactic:
rw [Set.mem_preimage, dif_pos hV, inj i (inv_U i _) hU (f_inv i _)]

Premises used: dif_pos, Set.mem_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
t : Set E
x : X
htx : t ⊆ f ⁻¹' {x}
hf : ∀ e ∈ t, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
e : E
he : e ∈ t
obtain :
  ∀ (φ : OpenPartialHomeomorph E X) (hφ : e ∈ φ.source) (htx : t ⊆ (↑φ : E → X) ⁻¹' {x})
    (hf : ∀ e ∈ t, ∃ (φ_1 : OpenPartialHomeomorph E X), e ∈ φ_1.source ∧ (↑φ_1 : E → X) = (↑φ : E → X)),
    ∃ (U : Set E), IsOpen[inst] U ∧ U ∩ t = {e}
⊢ ∃ (U : Set E), IsOpen[inst] U ∧ U ∩ t = {e}

Tactic:
obtain ⟨φ, hφ, rfl⟩ := hf e he

Premises used: rfl
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
t : Set E
x : X
e : E
he : e ∈ t
φ : OpenPartialHomeomorph E X
hφ : e ∈ φ.source
htx : t ⊆ (↑φ : E → X) ⁻¹' {x}
hf : ∀ e ∈ t, ∃ (φ_1 : OpenPartialHomeomorph E X), e ∈ φ_1.source ∧ (↑φ_1 : E → X) = (↑φ : E → X)
⊢ ∃ (U : Set E), IsOpen[inst] U ∧ U ∩ t = {e}

Tactic:
⟨_, φ.open_source, subset_antisymm (fun e' he' ↦ φ.injOn he'.1 hφ <|
      (htx he'.2).trans (htx he).symm) <| Set.singleton_subset_iff.mpr ⟨hφ, he⟩⟩

Premises used: Iff.mpr, Set.singleton_subset_iff, OpenPartialHomeomorph.open_source, subset_antisymm, And.intro, OpenPartialHomeomorph.injOn, Exists.intro, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
t : Set E
x : X
e : E
he : e ∈ t
φ : OpenPartialHomeomorph E X
hφ : e ∈ φ.source
htx : t ⊆ (↑φ : E → X) ⁻¹' {x}
hf : ∀ e ∈ t, ∃ (φ_1 : OpenPartialHomeomorph E X), e ∈ φ_1.source ∧ (↑φ_1 : E → X) = (↑φ : E → X)
⊢ ∃ (U : Set E), IsOpen[inst] U ∧ U ∩ t = {e}

Tactic:
exact ⟨_, φ.open_source, subset_antisymm (fun e' he' ↦ φ.injOn he'.1 hφ <|
      (htx he'.2).trans (htx he).symm) <| Set.singleton_subset_iff.mpr ⟨hφ, he⟩⟩
-- 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
⊢ DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)

Tactic:
have : DiscreteTopology (f ⁻¹' {x}) :=
    (IsDiscrete.of_openPartialHomeomorph f subset_rfl h).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 : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
choose :
  ∀ (φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X)
    (hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f),
    IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)
⊢ IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)

Tactic:
choose φ hφ using fun e : f ⁻¹' {x} ↦ h e e.2

Premises used: 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 : 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
have :
  ∀ (V : E → Set E) (hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)) (disj : (f ⁻¹' {x}).PairwiseDisjoint V),
    IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)
⊢ IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)

Tactic:
have ⟨V, hV, disj⟩ := fin.t2_separation
-- 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 : 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
⊢ ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)

Tactic:
have hV' e : IsOpen (V' e) := (hV e).2.inter (φ e).open_source
-- 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 : 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)
⊢ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})

Tactic:
have : ⋃ e, V' e ∈ nhdsSet (f ⁻¹' {x}) :=
    (isOpen_iUnion hV').mem_nhdsSet.2 fun e he ↦ mem_iUnion_of_mem ⟨e, he⟩ ⟨(hV e).1, (hφ _).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 : ∀ 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 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
have :
  ∀ (W : Set X) (hWx : W ∈ 𝓝 x) (hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e),
    IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)
⊢ IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)

Tactic:
have ⟨W, hWx, hWV⟩ := isClosedMap_iff_comap_nhds_le.mp hf this
-- 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 : ⋃ (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
inl : IsEmpty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1) → IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)
inr : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1) → IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)
⊢ IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)

Tactic:
cases isEmpty_or_nonempty (f ⁻¹' {x})

Premises used: Set.Elem, isEmpty_or_nonempty, Set.preimage, Singleton.singleton
-- 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 : ⋃ (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 : IsEmpty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
⊢ f ⁻¹' W = ∅

Tactic:
simpa using hWV
-- 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 : ⋃ (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 : IsEmpty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
⊢ IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)

Tactic:
exact .of_preimage_eq_empty _ hWx (by simpa using hWV)
-- 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 : ⋃ (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)
inr : ∀ (U : Set X) (hUW : U ⊆ W) (hU : IsOpen[inst_1] U) (hxU : x ∈ U), IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)
⊢ IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)

Tactic:
have ⟨U, hUW, hU, hxU⟩ := mem_nhds_iff.mp hWx
-- 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 : ⋃ (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
⊢ Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)

Tactic:
have : Finite (f ⁻¹' {x}) := fin
-- 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 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
e : (↑(f ⁻¹' {x}) : Type u_1)
⊢ IsOpen[inst_1] ((↑(φ e) : E → X) '' V' e)

Tactic:
(φ e).isOpen_image_of_subset_source (hV' _) inter_subset_right

Premises used: OpenPartialHomeomorph.isOpen_image_of_subset_source, 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 : ∀ 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 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
e : (↑(f ⁻¹' {x}) : Type u_1)
h₁ : ∀ a ∈ V' e, (↑(φ e) : E → X) = f
⊢ IsOpen[inst_1] (f '' V' e)

Tactic:
convert! ← (φ e).isOpen_image_of_subset_source (hV' _) inter_subset_right

Premises used: OpenPartialHomeomorph.isOpen_image_of_subset_source, 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 : ∀ 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 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
e : (↑(f ⁻¹' {x}) : Type u_1)
a : E
h_2 : a ∈ V' e
⊢ (↑(φ e) : E → X) = f

Tactic:
(hφ e).2

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 : ∀ 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 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
e : (↑(f ⁻¹' {x}) : Type u_1)
a : E
h_2 : a ∈ V' e
⊢ (↑(φ e) : E → X) = f

Tactic:
exact (hφ e).2

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 : ∀ 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 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
⊢ IsOpen[inst_1] U'

Tactic:
have hU' : IsOpen U' := hU.inter <| isOpen_iInter_of_finite fun e ↦ by
    convert! ← (φ e).isOpen_image_of_subset_source (hV' _) inter_subset_right; exact (hφ 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 : ∀ 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 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
⊢ ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e

Tactic:
have hUV e : U' ⊆ f '' V' e := inter_subset_right.trans (iInter_subset ..)
-- 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 : 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
⊢ Nonempty E

Tactic:
have : Nonempty E := ⟨Classical.arbitrary (f ⁻¹' {x})⟩