awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
e : E
he : e ∈ PartialEquiv.source.{u_1, max u_2 ?u.94810} F
e' : E
he' : e' ∈ U (idx e he) ∩ PartialEquiv.source.{u_1, max u_2 ?u.94810} F
h :
  e' ∉
    {x : E |
      (fun (x : E) ↦
          Eq (α := ι) ((fun (x : E) ↦ idx e he) x)
            ((fun (x : E) ↦ (if he : f x ∈ V then idx x he else Classical.arbitrary ι : ι)) x))
        x}
⊢ False
have refine_1 : e' ∈
  U ((fun (x : E) ↦ idx e he) e') ⊓
    U ((fun (x : E) ↦ (if he : f x ∈ V then idx x he else Classical.arbitrary ι : ι)) e')
Tactic: apply (disjoint h).le_bot
-- 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
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)
e : E
he : e ∈ PartialEquiv.source.{u_1, max u_2 ?u.94810} F
e' : E
he' : e' ∈ U (idx e he) ∩ PartialEquiv.source.{u_1, max u_2 ?u.94810} F
h :
  e' ∉
    {x : E |
      (fun (x : E) ↦
          Eq (α := ι) ((fun (x : E) ↦ idx e he) x)
            ((fun (x : E) ↦ (if he : f x ∈ V then idx x he else Classical.arbitrary ι : ι)) x))
        x}
⊢ e' ∈ U (idx e he) ⊓ U (if he : f e' ∈ V then idx e' he else Classical.arbitrary ι)
have refine_1 : e' ∈ U (idx e he) ⊓ U (idx e' sorry)
Tactic: rw [dif_pos (by exact he'.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
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)
e : E
he : e ∈ PartialEquiv.source.{u_1, max u_2 ?u.94810} F
⊢ IsOpen[inst] (U (idx e he) ∩ PartialEquiv.source.{u_1, max u_2 ?u.94810} F)
have refine_2 : IsOpen[inst] (PartialEquiv.source.{u_1, max u_2 ?u.94810} F ∩ U (idx e he))
Tactic: rwa [Set.inter_comm, ← open_iff _ subset_rfl]
-- 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
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 : ι
⊢ ContinuousOn.{u_2, u_1} (Y := E) (fun (x : X) ↦ PartialEquiv.invFun.{u_1, max ?u.94810 u_2} F (x, i))
    {a : X | Membership.mem.{max ?u.94810 u_2, max u_2 ?u.94810} (PartialEquiv.target.{u_1, max ?u.94810 u_2} F) (a, i)}
have refine_3 : ContinuousOn.{u_2, u_1} (Y := E) (fun (x : X) ↦ if h : x ∈ V then inv i sorry else Classical.arbitrary (X → E) x)
  {a : X | a ∈ V}
Tactic: simp_rw [F, Set.prodMk_mem_set_prod_eq, Set.mem_univ, and_true]
-- 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
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 : ι
⊢ ContinuousOn.{u_2, u_1} (Y := E) (fun (x : X) ↦ if h : x ∈ V then inv i ⋯ else Classical.arbitrary (X → E) x)
    {a : X | a ∈ V}
have refine_3 : ∀ (W : Set E) (open_W : IsOpen[inst] W),
  IsOpen[inst_1] (V ∩ (fun (x : X) ↦ if h : x ∈ V then inv i sorry else Classical.arbitrary (X → E) x) ⁻¹' W)
Tactic: refine (continuousOn_open_iff open_V).mpr fun W open_W ↦ ?_
-- 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
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
⊢ IsOpen[inst_1] (V ∩ (fun (x : X) ↦ if h : x ∈ V then inv i ⋯ else Classical.arbitrary (X → E) x) ⁻¹' W)
have refine_3 : IsOpen[inst] (f ⁻¹' (V ∩ (fun (x : X) ↦ if h : x ∈ V then inv i sorry else Classical.arbitrary (X → E) x) ⁻¹' W) ∩ U i)
Tactic: rw [open_iff i Set.inter_subset_left]
-- 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
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
⊢ IsOpen[inst] (f ⁻¹' (V ∩ (fun (x : X) ↦ if h : x ∈ V then inv i ⋯ else Classical.arbitrary (X → E) x) ⁻¹' W) ∩ U i)
have h : f ⁻¹' (V ∩ (fun (x : X) ↦ if h : x ∈ V then inv i sorry else Classical.arbitrary (X → E) x) ⁻¹' W) ∩ U i = f ⁻¹' V ∩ U i ∩ W
Tactic: convert! ((open_iff i subset_rfl).mp open_V).inter open_W 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
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
⊢ f ⁻¹' (V ∩ (fun (x : X) ↦ if h : x ∈ V then inv i ⋯ else Classical.arbitrary (X → E) x) ⁻¹' W) ∩ U i =
    f ⁻¹' V ∩ U i ∩ W
have h : ∀ (e : E),
  f e ∈ V ∧ e ∈ U i →
    ∀ (hV : f e ∈ V) (hU : e ∈ U i),
      Membership.mem (γ := Set X) ((fun (x : X) ↦ if h : x ∈ V then inv i sorry else Classical.arbitrary (X → E) x) ⁻¹' W)
          (f e) ↔
        e ∈ W
Tactic: refine Set.ext fun e ↦ and_right_comm.trans (and_congr_right fun ⟨hV, hU⟩ ↦ ?_)
-- 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
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 : f e ∈ V ∧ e ∈ U i
hV : f e ∈ V
hU : e ∈ U i
⊢ 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
have h : (if h : f e ∈ V then inv i sorry else Classical.arbitrary (X → E) (f e)) ∈ W ↔ e ∈ W
Tactic: rw [Set.mem_preimage, dif_pos hV, inj i (inv_U i _) hU (f_inv i _)]
-- 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
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
⊢ 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
have h₁ : inv i sorry ∈ W ↔ e ∈ W
Tactic: rw [Set.mem_preimage, dif_pos hV, inj i (inv_U i _) hU (f_inv i _)]
-- 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
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
⊢ 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
have h₂ : e ∈ W ↔ e ∈ W
Tactic: rw [Set.mem_preimage, dif_pos hV, inj i (inv_U i _) hU (f_inv i _)]
-- 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
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
⊢ ∃ (U : Set E), IsOpen[inst] U ∧ U ∩ t = {e}
have 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}
Tactic: obtain ⟨φ, hφ, rfl⟩ := hf e he
Cleared hypotheses: f, htx, hf
-- 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
⊢ IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)
have this : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
Tactic: have : DiscreteTopology (f ⁻¹' {x}) :=
    (IsDiscrete.of_openPartialHomeomorph f subset_rfl 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 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
⊢ IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)
have 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)
Tactic: choose φ hφ using fun e : f ⁻¹' {x} ↦ h e 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 : 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
⊢ IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)
have 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)
Tactic: have ⟨V, hV, disj⟩ := fin.t2_separation
-- 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
⊢ IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)
have hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
Tactic: have hV' e : IsOpen (V' e) := (hV e).2.inter (φ e).open_source