-- 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_1 :
  ∀ (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
n : ℕ
Γ : (↑I : Type) → E
cont : ContinuousOn Γ (Set.Icc 0 (t n))
eqOn : Set.EqOn (p ∘ Γ) (⇑γ : (a : (↑I : Type)) → X) (Set.Icc 0 (t n))
Γ_0 : Γ 0 = e
x : X
t_sub :
  Set.Icc (t n) (t (n + 1)) ⊆
    (⇑γ : (a : (↑I : Type)) → 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))
pΓtn : p (Γ (t n)) = (γ : (a : (↑I : Type)) → X) (t n)
this : Nonempty.{u_1 + 1} (↑(p ⁻¹' {x}) : Type u_1)
q : Bundle.Trivialization (↑(p ⁻¹' {x}) : Type u_1) p := ⋯.toTrivialization
succ :
  ∀ (s : (↑I : Type)) (hs : s ∈ Set.Icc 0 (t (n + 1)) ∩ frontier {a : (↑I : Type) | a ≤ t n}),
    Γ s = q.invFun ((γ : (a : (↑I : Type)) → X) s, ((↑q : E → X × (↑(p ⁻¹' {x}) : Type u_1)) (Γ (t n))).2)
succ₁ : ∀ (x : (↑I : Type)) (h : x ∈ Set.Icc 0 (t (n + 1)) ∩ closure {a : (↑I : Type) | a ≤ t n}), x ∈ Set.Icc 0 (t n)
succ₂ :
  ContinuousOn.{0, u_1} (Y := E)
    (fun (s : (↑I : Type)) ↦
      q.invFun ((γ : (a : (↑I : Type)) → X) s, ((↑q : E → X × (↑(p ⁻¹' {x}) : Type u_1)) (Γ (t n))).2))
    (Set.Icc 0 (t (n + 1)) ∩ closure {a : (↑I : Type) | ¬a ≤ t n})
succ₃ :
  ∀ (s : (↑I : Type)) (hs : s ∈ Set.Icc 0 (t (n + 1))),
    (p ∘ fun (s : (↑I : Type)) ↦
          if s ≤ t n then Γ s
          else q.invFun ((γ : (a : (↑I : Type)) → X) s, ((↑q : E → X × (↑(p ⁻¹' {x}) : Type u_1)) (Γ (t n))).2))
        s =
      (γ : (a : (↑I : Type)) → X) s
succ₄ :
  (fun (s : (↑I : Type)) ↦
        if s ≤ t n then Γ s
        else q.invFun ((γ : (a : (↑I : Type)) → X) s, ((↑q : E → X × (↑(p ⁻¹' {x}) : Type u_1)) (Γ (t n))).2))
      0 =
    e
⊢ ∃ (Γ : (↑I : Type) → E),
    ContinuousOn Γ (Set.Icc 0 (t (n + 1))) ∧
      Set.EqOn (p ∘ Γ) (⇑γ : (a : (↑I : Type)) → X) (Set.Icc 0 (t (n + 1))) ∧ Γ 0 = e

Tactic:
refine ⟨fun s ↦ if s ≤ t n then Γ s else q.invFun (γ s, (q (Γ (t n))).2),
    .if (fun s hs ↦ ?_) (cont.mono fun _ h ↦ ?_) ?_, fun s hs ↦ ?_, ?_⟩