-- 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_3
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
let let₁ let₂ : Trivialization ι f
let₃ :
  (open_preim : ∀ {W : Set X} (hWV : W ⊆ V) (open_W : IsOpen[inst_1] W), IsOpen[inst] (f ⁻¹' W)) → Trivialization ι f
let₄ :
  let F :=
    { 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' := ⋯ : PartialEquiv E (X × ι) };
  (open_preim : ∀ {W : Set X} (hWV : W ⊆ V) (open_W : IsOpen[inst_1] W), IsOpen[inst] (f ⁻¹' W)) →
    (open_source : IsOpen[inst] F.source) → Trivialization ι f
let₅ :
  let F :=
    { 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' := ⋯ : PartialEquiv E (X × ι) };
  (open_preim : ∀ {W : Set X} (hWV : W ⊆ V) (open_W : IsOpen[inst_1] W), IsOpen[inst] (f ⁻¹' W)) →
    (open_source : IsOpen[inst] F.source) → (cont_f : ContinuousOn f F.source) → Trivialization ι f
refine_1 :
  let F :=
    { 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' := ⋯ : PartialEquiv E (X × ι) };
  ∀ (open_preim : ∀ {W : Set X} (hWV : W ⊆ V) (open_W : IsOpen[inst_1] W), IsOpen[inst] (f ⁻¹' W))
    (open_source : IsOpen[inst] F.source) (cont_f : ContinuousOn f F.source) (e : E) (he : e ∈ F.source) (e' : E)
    (he' : e' ∈ U (idx e he) ∩ F.source),
    Membership.mem (γ := Set E)
      {x : E |
        (fun (x : E) ↦
            Eq.{u_3 + 1} (α := ι) ((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 :
  let F :=
    { 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' := ⋯ : PartialEquiv E (X × ι) };
  ∀ (open_preim : ∀ {W : Set X} (hWV : W ⊆ V) (open_W : IsOpen[inst_1] W), IsOpen[inst] (f ⁻¹' W))
    (open_source : IsOpen[inst] F.source) (cont_f : ContinuousOn f F.source) (e : E) (he : e ∈ F.source),
    IsOpen[inst] (U (idx e he) ∩ F.source)
refine_3 :
  let F :=
    { 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' := ⋯ : PartialEquiv E (X × ι) };
  ∀ (open_preim : ∀ {W : Set X} (hWV : W ⊆ V) (open_W : IsOpen[inst_1] W), IsOpen[inst] (f ⁻¹' W))
    (open_source : IsOpen[inst] F.source) (cont_f : ContinuousOn f F.source) (i : ι),
    ContinuousOn.{u_2, u_1} (Y := E) (fun (x : X) ↦ F.invFun (x, i)) {a : X | (a, i) ∈ F.target}
refine_2₁ :
  let F :=
    { 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' := ⋯ : PartialEquiv E (X × ι) };
  ∀ (open_preim : ∀ {W : Set X} (hWV : W ⊆ V) (open_W : IsOpen[inst_1] W), IsOpen[inst] (f ⁻¹' W))
    (open_source : IsOpen[inst] F.source) (cont_f : ContinuousOn f F.source) (e : E) (he : e ∈ F.source),
    IsOpen[inst] (U (idx e he) ∩ F.source)
refine_3₁ refine_3₂ :
  let F :=
    { 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' := ⋯ : PartialEquiv E (X × ι) };
  ∀ (open_preim : ∀ {W : Set X} (hWV : W ⊆ V) (open_W : IsOpen[inst_1] W), IsOpen[inst] (f ⁻¹' W))
    (open_source : IsOpen[inst] F.source) (cont_f : ContinuousOn f F.source) (i : ι),
    ContinuousOn.{u_2, u_1} (Y := E) (fun (x : X) ↦ F.invFun (x, i)) {a : X | (a, i) ∈ F.target}
⊢ Trivialization ι f

Tactic:
classical
  let F : PartialEquiv E (X × ι) :=
  { toFun e := (f e, if he : f e ∈ V then idx e he else Classical.arbitrary ι),
    invFun x := if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1,
    source := f ⁻¹' V,
    target := V ×ˢ Set.univ,
    map_source' x hx := ⟨hx, ⟨⟩⟩
    map_target' x hx := by rw [dif_pos hx.1]; apply (f_inv _ hx.1).symm ▸ hx.1,
    left_inv' e he := by
      simp_rw [dif_pos (id he : f e ∈ V)]
      exact inj _ (inv_U _ he) (idx_U e he) (f_inv _ _)
    right_inv' x hx := by
      rw [dif_pos hx.1]
      refine Prod.ext (f_inv _ hx.1) ?_
      rw [dif_pos ((f_inv _ hx.1).symm ▸ hx.1)]
      by_contra h; exact (disjoint h).le_bot ⟨idx_U .., inv_U _ _⟩ }
  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'
  have open_source : IsOpen F.source := open_preim subset_rfl open_V
  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)
  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 }
  · by_contra h; apply (disjoint h).le_bot
    · dsimp only; rw [dif_pos (by exact he'.2)]; exact ⟨he'.1, idx_U ..⟩
  · rwa [Set.inter_comm, ← open_iff _ subset_rfl]
  · simp_rw [F, Set.prodMk_mem_set_prod_eq, Set.mem_univ, and_true]
    refine (continuousOn_open_iff open_V).mpr fun W open_W ↦ ?_
    rw [open_iff i Set.inter_subset_left]
    convert! ((open_iff i subset_rfl).mp open_V).inter open_W using 1
    refine Set.ext fun e ↦ and_right_comm.trans (and_congr_right fun ⟨hV, hU⟩ ↦ ?_)
    rw [Set.mem_preimage, dif_pos hV, inj i (inv_U i _) hU (f_inv i _)]

Premises used: Iff.mpr, Set.ext, and_true, dif_pos, Set.prodMk_mem_set_prod_eq, and_congr_right, Set.inter_comm, and_right_comm, Set.mem_univ, Iff.trans, continuousOn_open_iff, subset_rfl, Set.mem_preimage