-- 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
n : ℕ
succ :
  ∀ (n : ℕ)
    (ih :
      ∃ (Γ : (↑I : Type) → E),
        ContinuousOn Γ (Set.Icc 0 (t n)) ∧ Set.EqOn (p ∘ Γ) (⇑γ : (a : (↑I : Type)) → X) (Set.Icc 0 (t n)) ∧ Γ 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
⊢ ∃ (Γ : (↑I : Type) → E),
    ContinuousOn Γ (Set.Icc 0 (t n)) ∧ Set.EqOn (p ∘ Γ) (⇑γ : (a : (↑I : Type)) → X) (Set.Icc 0 (t n)) ∧ Γ 0 = e

Tactic:
induction n with
  | zero =>
    refine ⟨fun _ ↦ e, continuous_const.continuousOn, fun t ht ↦ ?_, rfl⟩
    rw [t_0, Set.Icc_self, Set.mem_singleton_iff] at ht; subst ht; exact γ_0.symm
  | succ n ih => ?_

Premises used: Set.Icc_self, Set.mem_singleton_iff, Eq.symm