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
x : X × ι
hx : Membership.mem.{max u_2 ?u.94810, max u_2 ?u.94810} (SProd.sprod (β := Set ι) V Set.univ) x
⊢ (if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1) ∈ f ⁻¹' V
have rw : inv x.2 sorry ∈ f ⁻¹' V
Tactic: rw [dif_pos hx.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
e : E
he : e ∈ f ⁻¹' V
⊢ (if hx : (f e, if he : f e ∈ V then idx e he else Classical.arbitrary ι).1 ∈ V then
      inv (f e, if he : f e ∈ V then idx e he else Classical.arbitrary ι).2 hx
    else Classical.arbitrary (X → E) (f e, if he : f e ∈ V then idx e he else Classical.arbitrary ι).1) =
    e
have simp_rw : inv (idx e sorry) sorry = e
Tactic: simp_rw [dif_pos (id he : f e ∈ 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
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
x : X × ι
hx : Membership.mem.{max u_2 ?u.94810, max u_2 ?u.94810} (SProd.sprod (β := Set ι) V Set.univ) x
⊢ Eq.{(max u_2 ?u.94810) + 1}
    (f (if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1),
      if he : f (if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1) ∈ V then
        idx (if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1) he
      else Classical.arbitrary ι)
    x
have rw : Eq.{(max u_2 ?u.94810) + 1}
  (f (inv x.2 sorry), if he : f (inv x.2 sorry) ∈ V then idx (inv x.2 sorry) he else Classical.arbitrary ι) x
Tactic: rw [dif_pos hx.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
x : X × ι
hx : Membership.mem.{max u_2 ?u.94810, max u_2 ?u.94810} (SProd.sprod (β := Set ι) V Set.univ) x
⊢ Eq.{(max u_2 ?u.94810) + 1}
    (f (inv x.2 ⋯), if he : f (inv x.2 ⋯) ∈ V then idx (inv x.2 ⋯) he else Classical.arbitrary ι) x
have refine : (f (inv x.2 sorry), if he : f (inv x.2 sorry) ∈ V then idx (inv x.2 sorry) he else Classical.arbitrary ι).2 = x.2
Tactic: refine Prod.ext (f_inv _ hx.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
x : X × ι
hx : Membership.mem.{max u_2 ?u.94810, max u_2 ?u.94810} (SProd.sprod (β := Set ι) V Set.univ) x
⊢ (f (inv x.2 ⋯), if he : f (inv x.2 ⋯) ∈ V then idx (inv x.2 ⋯) he else Classical.arbitrary ι).2 = x.2
have rw : (f (inv x.2 sorry), idx (inv x.2 sorry) sorry).2 = x.2
Tactic: rw [dif_pos ((f_inv _ hx.1).symm ▸ hx.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
x : X × ι
hx : Membership.mem.{max u_2 ?u.94810, max u_2 ?u.94810} (SProd.sprod (β := Set ι) V Set.univ) x
⊢ (f (inv x.2 ⋯), idx (inv x.2 ⋯) ⋯).2 = x.2
have by_contra : ∀ (h : ¬(f (inv x.2 sorry), idx (inv x.2 sorry) sorry).2 = x.2), False
Tactic: by_contra h
-- 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' := ⋯ }
W : Set X
hWV : W ⊆ V
open_W : IsOpen[inst_1] W
⊢ IsOpen[inst] (f ⁻¹' W)
have h : f ⁻¹' W = ⋃ (i : ι), f ⁻¹' W ∩ U i
Tactic: convert! isOpen_iUnion (fun i ↦ (open_iff i hWV).mp 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' := ⋯ }
W : Set X
hWV : W ⊆ V
open_W : IsOpen[inst_1] W
⊢ f ⁻¹' W = ⋃ (i : ι), f ⁻¹' W ∩ U i
have h : f ⁻¹' W ⊆ ⋃ (i : ι), U i
Tactic: rw [← Set.inter_iUnion, eq_comm, Set.inter_eq_left]
-- 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
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' := ⋯ }
⊢ Trivialization ι f
have open_preim : ∀ {W : Set X} (hWV : W ⊆ V) (open_W : IsOpen[inst_1] W), IsOpen[inst] (f ⁻¹' W)
Tactic: have open_preim {W} (hWV : W ⊆ V) (open_W : IsOpen W) : IsOpen (f ⁻¹' W) := by
    convert! isOpen_iUnion (fun i ↦ (open_iff i hWV).mp open_W)
    rw [← Set.inter_iUnion, eq_comm, Set.inter_eq_left]
    exact (Set.preimage_mono hWV).trans exhaustive'
-- 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
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)
⊢ Trivialization ι f
have open_source : IsOpen[inst] (PartialEquiv.source.{u_1, max u_2 ?u.94810} F)
Tactic: have open_source : IsOpen F.source := open_preim subset_rfl open_V
-- 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
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)
⊢ Trivialization ι f
have cont_f : ContinuousOn f (PartialEquiv.source.{u_1, max u_2 ?u.94810} F)
Tactic: have cont_f : ContinuousOn f F.source := (continuousOn_open_iff open_source).mpr
    fun W open_W ↦ open_preim Set.inter_subset_left (open_V.inter 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)
⊢ Trivialization ι f
have refine_1 : ∀ (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),
  Membership.mem (γ := Set 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'
Tactic: refine
  { toPartialEquiv := F,
    open_source := open_source,
    open_target := open_V.prod isOpen_univ,
    continuousOn_toFun := cont_f.prodMk <| continuousOn_of_forall_continuousAt fun e he ↦
      continuous_const (y := idx e he) |>.continuousAt.congr <| mem_nhds_iff.mpr
        ⟨U (idx e he) ∩ F.source, fun e' he' ↦ ?_, ?_, idx_U e he, he⟩
    continuousOn_invFun := continuousOn_prod_of_discrete_right.mpr fun i ↦ ?_,
    baseSet := V,
    open_baseSet := open_V,
    source_eq := rfl,
    target_eq := rfl,
    proj_toFun _ _ := 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)
refine_1 :
  ∀ (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),
    Membership.mem (γ := Set 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'
⊢ Trivialization ι f
have refine_2 : ∀ (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)
Tactic: refine
  { toPartialEquiv := F,
    open_source := open_source,
    open_target := open_V.prod isOpen_univ,
    continuousOn_toFun := cont_f.prodMk <| continuousOn_of_forall_continuousAt fun e he ↦
      continuous_const (y := idx e he) |>.continuousAt.congr <| mem_nhds_iff.mpr
        ⟨U (idx e he) ∩ F.source, fun e' he' ↦ ?_, ?_, idx_U e he, he⟩
    continuousOn_invFun := continuousOn_prod_of_discrete_right.mpr fun i ↦ ?_,
    baseSet := V,
    open_baseSet := open_V,
    source_eq := rfl,
    target_eq := rfl,
    proj_toFun _ _ := 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)
refine_1 :
  ∀ (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),
    Membership.mem (γ := Set 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'
refine_2 :
  ∀ (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)
⊢ Trivialization ι f
have refine_3 : ∀ (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)}
Tactic: refine
  { toPartialEquiv := F,
    open_source := open_source,
    open_target := open_V.prod isOpen_univ,
    continuousOn_toFun := cont_f.prodMk <| continuousOn_of_forall_continuousAt fun e he ↦
      continuous_const (y := idx e he) |>.continuousAt.congr <| mem_nhds_iff.mpr
        ⟨U (idx e he) ∩ F.source, fun e' he' ↦ ?_, ?_, idx_U e he, he⟩
    continuousOn_invFun := continuousOn_prod_of_discrete_right.mpr fun i ↦ ?_,
    baseSet := V,
    open_baseSet := open_V,
    source_eq := rfl,
    target_eq := rfl,
    proj_toFun _ _ := 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)
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
⊢ Membership.mem (γ := Set 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'
have refine_1 : ∀
  (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
Tactic: by_contra h