-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C((↑I : Type), X)
e : E
γ_0 : (γ : (a : (↑I : Type)) → X) 0 = p e
U : (x : X) → Set X :=
  fun (x : X) ↦
    ⋯.choose (p := fun (U : Set X) ↦
      x ∈ U ∧
        IsOpen[inst_1] U ∧
          IsOpen[inst] (p ⁻¹' U) ∧
            ∃ (H : (↑(p ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_1} (↑U : Type u_2) (↑(p ⁻¹' {x}) : Type u_1)),
              ∀ (x_1 : (↑(p ⁻¹' U) : Type u_1)),
                (↑((H : (a : (↑(p ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(p ⁻¹' {x}) : Type u_1)) x_1).1 : X) =
                  p (↑x_1 : E))
mem_base :
  ∀ (x : X),
    x ∈
      ⋯.choose (p := fun (U : Set X) ↦
        x ∈ U ∧
          IsOpen[inst_1] U ∧
            IsOpen[inst] (p ⁻¹' U) ∧
              ∃ (H : (↑(p ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_1} (↑U : Type u_2) (↑(p ⁻¹' {x}) : Type u_1)),
                ∀ (x_1 : (↑(p ⁻¹' U) : Type u_1)),
                  (↑((H : (a : (↑(p ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(p ⁻¹' {x}) : Type u_1)) x_1).1 : X) =
                    p (↑x_1 : E))
U_open :
  ∀ (x : X),
    IsOpen[inst_1]
      (⋯.choose (p := fun (U : Set X) ↦
        x ∈ U ∧
          IsOpen[inst_1] U ∧
            IsOpen[inst] (p ⁻¹' U) ∧
              ∃ (H : (↑(p ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_1} (↑U : Type u_2) (↑(p ⁻¹' {x}) : Type u_1)),
                ∀ (x_1 : (↑(p ⁻¹' U) : Type u_1)),
                  (↑((H : (a : (↑(p ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(p ⁻¹' {x}) : Type u_1)) x_1).1 : X) =
                    p (↑x_1 : E)))
h :
  ∀ (x : X),
    IsOpen[inst]
      (p ⁻¹'
        ⋯.choose (p := fun (U : Set X) ↦
          x ∈ U ∧
            IsOpen[inst_1] U ∧
              IsOpen[inst] (p ⁻¹' U) ∧
                ∃ (H : (↑(p ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_1} (↑U : Type u_2) (↑(p ⁻¹' {x}) : Type u_1)),
                  ∀ (x_1 : (↑(p ⁻¹' U) : Type u_1)),
                    (↑((H : (a : (↑(p ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(p ⁻¹' {x}) : Type u_1)) x_1).1 : X) =
                      p (↑x_1 : E)))
H :
  (x : X) →
    (↑(p ⁻¹'
            ⋯.choose (p := fun (U : Set X) ↦
              x ∈ U ∧
                IsOpen[inst_1] U ∧
                  IsOpen[inst] (p ⁻¹' U) ∧
                    ∃ (H : (↑(p ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_1} (↑U : Type u_2) (↑(p ⁻¹' {x}) : Type u_1)),
                      ∀ (x_1 : (↑(p ⁻¹' U) : Type u_1)),
                        (↑((H : (a : (↑(p ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(p ⁻¹' {x}) : Type u_1)) x_1).1 :
                            X) =
                          p (↑x_1 : E))) :
        Type u_1) ≃ₜ
      Prod.{u_2, u_1}
        (↑(⋯.choose (p := fun (U : Set X) ↦
              x ∈ U ∧
                IsOpen[inst_1] U ∧
                  IsOpen[inst] (p ⁻¹' U) ∧
                    ∃ (H : (↑(p ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_1} (↑U : Type u_2) (↑(p ⁻¹' {x}) : Type u_1)),
                      ∀ (x_1 : (↑(p ⁻¹' U) : Type u_1)),
                        (↑((H : (a : (↑(p ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(p ⁻¹' {x}) : Type u_1)) x_1).1 :
                            X) =
                          p (↑x_1 : E))) :
          Type u_2)
        (↑(p ⁻¹' {x}) : Type u_1)
h_1 :
  ∀ (x : X)
    (x_1 :
      (↑(p ⁻¹'
            ⋯.choose (p := fun (U : Set X) ↦
              x ∈ U ∧
                IsOpen[inst_1] U ∧
                  IsOpen[inst] (p ⁻¹' U) ∧
                    ∃ (H : (↑(p ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_1} (↑U : Type u_2) (↑(p ⁻¹' {x}) : Type u_1)),
                      ∀ (x_1 : (↑(p ⁻¹' U) : Type u_1)),
                        (↑((H : (a : (↑(p ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(p ⁻¹' {x}) : Type u_1)) x_1).1 :
                            X) =
                          p (↑x_1 : E))) :
        Type u_1)),
    (↑((H x : (a : (↑(p ⁻¹' ⋯.choose) : Type u_1)) → (↑⋯.choose : Type u_2) × (↑(p ⁻¹' {x}) : Type u_1)) x_1).1 : X) =
      p (↑x_1 : E)
t : ℕ → (↑I : Type)
t_0 : t 0 = 0
t_mono : Monotone t
t_sub :
  ∀ (n : ℕ),
    ∃ (i : X),
      Set.Icc (t n) (t (n + 1)) ⊆
        (⇑γ : (a : (↑I : Type)) → X) ⁻¹'
          ⋯.choose (p := fun (U : Set X) ↦
            i ∈ U ∧
              IsOpen[inst_1] U ∧
                IsOpen[inst] (p ⁻¹' U) ∧
                  ∃ (H : (↑(p ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_1} (↑U : Type u_2) (↑(p ⁻¹' {i}) : Type u_1)),
                    ∀ (x : (↑(p ⁻¹' U) : Type u_1)),
                      (↑((H : (a : (↑(p ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(p ⁻¹' {i}) : Type u_1)) x).1 : X) =
                        p (↑x : E))
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
suffices :
  ∀ (n : ℕ),
    ∃ (Γ : (↑I : Type) → E),
      ContinuousOn Γ (Set.Icc 0 (t n)) ∧ Set.EqOn (p ∘ Γ) (⇑γ : (a : (↑I : Type)) → X) (Set.Icc 0 (t n)) ∧ Γ 0 = e
⊢ ∃ (Γ : C((↑I : Type), E)),
    Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑γ : (a : (↑I : Type)) → X) ∧
      (Γ : (a : (↑I : Type)) → E) 0 = e

Tactic:
suffices ∀ n, ∃ Γ : I → E, ContinuousOn Γ (Set.Icc 0 (t n)) ∧
      (Set.Icc 0 (t n)).EqOn (p ∘ Γ) γ ∧ Γ 0 = e by
    obtain ⟨Γ, cont, eqOn, Γ_0⟩ := this n_max
    rw [h_max _ le_rfl] at cont eqOn
    exact ⟨⟨Γ, continuousOn_univ.mp
      (by convert! cont; rw [eq_comm, Set.eq_univ_iff_forall]; exact fun t ↦ ⟨bot_le, le_top⟩)⟩,
      funext fun _ ↦ eqOn ⟨bot_le, le_top⟩, Γ_0⟩