awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (hypothesis)
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)
⊢ IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)
have this₁ : ⋃ (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⟩
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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})
⊢ IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)
have 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)
Tactic: have ⟨W, hWx, hWV⟩ := isClosedMap_iff_comap_nhds_le.mp hf this
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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
⊢ IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)
have inl : IsEmpty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1) → IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)
Tactic: cases isEmpty_or_nonempty (f ⁻¹' {x})
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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)
⊢ IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)
have inr : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1) → IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)
Tactic: cases isEmpty_or_nonempty (f ⁻¹' {x})
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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)
⊢ IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)
have inr : ∀ (U : Set X) (hUW : U ⊆ W) (hU : IsOpen[inst_1] U) (hxU : x ∈ U), IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)
Tactic: have ⟨U, hUW, hU, hxU⟩ := mem_nhds_iff.mp hWx
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (hypothesis)
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
⊢ IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)
have this₁ : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
Tactic: have : Finite (f ⁻¹' {x}) := fin
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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] (f '' V' e)
have h₁ : ∀ a ∈ V' e, (↑(φ e) : E → X) = f
Tactic: convert! ← (φ e).isOpen_image_of_subset_source (hV' _) inter_subset_right
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (hypothesis)
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)
⊢ IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)
have hU' : 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
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (hypothesis)
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'
⊢ IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)
have hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
Tactic: have hUV e : U' ⊆ f '' V' e := inter_subset_right.trans (iInter_subset ..)
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (hypothesis)
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
⊢ IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)
have this₁ : Nonempty E
Tactic: have : Nonempty E := ⟨Classical.arbitrary (f ⁻¹' {x})⟩
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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)
have inr : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)) (s : Set X) (hs : s ⊆ U') (h : IsOpen[inst_1] s), IsOpen[inst] (f ⁻¹' s ∩ V' e)
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⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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)
⊢ IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)
have inr₁ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)) (s : Set X) (hs : s ⊆ U') (h : IsOpen[inst] (f ⁻¹' s ∩ V' e)), IsOpen[inst_1] s
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⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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
⊢ IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)
have inr₂ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), InjOn f (V' e)
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⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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] (f ⁻¹' s ∩ V' e)
have h₁ : f ⁻¹' s ∩ V' e = (φ e).source ∩ (↑(φ e) : E → X) ⁻¹' s ∩ V (↑e : E)
Tactic: convert! ((φ e).isOpen_inter_preimage h).inter (hV e).2 using 1
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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).source ∩ (↑(φ e) : E → X) ⁻¹' s ∩ V (↑e : E)
have h₁ : f ⁻¹' s ∩ (V (↑e : E) ∩ (φ e).source) = (φ e).source ∩ f ⁻¹' s ∩ V (↑e : E)
Tactic: simp_rw [(hφ e).2, V']
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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 ⊆ (φ e).target
have rw : f '' V' e ⊆ f '' (φ e).source
Tactic: rw [← (φ e).image_source_eq_target, (hφ e).2]
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (hypothesis)
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)
⊢ IsOpen[inst_1] s
have this₁ : 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