-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
f : ContinuousMap.{u_3, u_2} ((↑I : Type) × A) X
g : (↑I : Type) × A → E
g_lifts : p ∘ g = (⇑f : (a : (↑I : Type) × A) → X)
cont_0 : Continuous[inst_2, inst] fun (x : A) ↦ g (0, x)
a : A
cont_a : Continuous[_, inst] fun (x : (↑I : Type)) ↦ g (x, a)
q : (x : E) → OpenPartialHomeomorph E X
mem_source : ∀ (x : E), x ∈ (q x).source
hpq : ∀ (x : E), p = (↑(q x) : E → X)
t : ℕ → (↑I : Type)
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ (i : E), Set.Icc (t n) (t (n + 1)) ⊆ (fun (x : (↑I : Type)) ↦ g (x, a)) ⁻¹' (q i).source
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
h :
  ∃ (N : Set A),
    a ∈ N ∧
      IsOpen[inst_2] N ∧
        ∃ (g' : (↑I : Type) × A → E),
          ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N) ∧
            p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X) ∧
              (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n, g' (t', a) = g (t', a)
N : Set A
haN : a ∈ N
N_open : IsOpen[inst_2] N
g' : (↑I : Type) × A → E
cont_g' : ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N)
g'_lifts : p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X)
g'_0 : ∀ (a : A), g' (0, a) = g (0, a)
g'_a : ∀ t' ≤ t n, g' (t', a) = g (t', a)
e : E
h_sub : Set.Icc (t n) (t (n + 1)) ⊆ (fun (x : (↑I : Type)) ↦ g (x, a)) ⁻¹' (q e).source
this : SProd.sprod (β := Set A) (Set.Icc (t n) (t (n + 1))) {a} ⊆ (⇑f : (a : (↑I : Type) × A) → X) ⁻¹' (q e).target
u : Set (↑I : Type)
v : Set A
v_open : IsOpen[inst_2] v
hu : Set.Icc (t n) (t (n + 1)) ⊆ u
hav : {a} ⊆ v
huv : u ×ˢ v ⊆ (⇑f : (a : (↑I : Type) × A) → X) ⁻¹' (q e).target
refine_2 : a ∈ v ∩ (N ∩ (g' ∘ fun (y : A) ↦ (t n, y)) ⁻¹' (q e).source)
refine_2₁ : ∀ (a : A) (ha : a ∈ N), (t n, a).1 ∈ Set.Icc 0 (t n)
refine_2₂ :
  ∀
    ta ∈
      Set.Icc 0 (t n.succ) ×ˢ (v ∩ (N ∩ (g' ∘ fun (y : A) ↦ (t n, y)) ⁻¹' (q e).source)) ∩
        frontier {a : (↑I : Type) × A | a.1 ≤ t n},
    ta.1 ∈ Set.Icc 0 (t n.succ) →
      ∀ (hav : ta.2 ∈ v),
        ta.2 ∈ N →
          ∀ (ha : Membership.mem (γ := Set A) ((g' ∘ fun (y : A) ↦ (t n, y)) ⁻¹' (q e).source) ta.2)
            (hfr : Membership.mem (γ := Set ((↑I : Type) × A)) (frontier {a : (↑I : Type) × A | a.1 ≤ t n}) ta),
            g' ta =
              if Membership.mem (α := X) (q e).target ((f : (a : (↑I : Type) × A) → X) ta : X) then
                (↑(q e).symm : X → E) ((f : (a : (↑I : Type) × A) → X) ta)
              else g ta
refine_2₃ :
  ∀
    ta ∈
      Set.Icc 0 (t n.succ) ×ˢ (v ∩ (N ∩ (g' ∘ fun (y : A) ↦ (t n, y)) ⁻¹' (q e).source)) ∩
        closure[instTopologicalSpaceProd] {a : (↑I : Type) × A | a.1 ≤ t n},
    ∀ (hta : ta ∈ Set.Icc 0 (t n.succ) ×ˢ (v ∩ (N ∩ (g' ∘ fun (y : A) ↦ (t n, y)) ⁻¹' (q e).source)))
      (ht :
        Membership.mem (γ := Set ((↑I : Type) × A))
          (closure[instTopologicalSpaceProd] {a : (↑I : Type) × A | a.1 ≤ t n}) ta),
      ta ∈ Set.Icc 0 (t n) ×ˢ N
refine_2₄ :
  ContinuousOn.{u_3, u_1} (Y := E)
    (fun (ta : (↑I : Type) × A) ↦
      if Membership.mem (α := X) (q e).target ((f : (a : (↑I : Type) × A) → X) ta : X) then
        (↑(q e).symm : X → E) ((f : (a : (↑I : Type) × A) → X) ta)
      else g ta)
    (Set.Icc 0 (t n.succ) ×ˢ (v ∩ (N ∩ (g' ∘ fun (y : A) ↦ (t n, y)) ⁻¹' (q e).source)) ∩
      closure[instTopologicalSpaceProd] {a : (↑I : Type) × A | ¬a.1 ≤ t n})
refine_2₅ :
  Eq (α := (↑I : Type) × A → X)
    (p ∘ fun (ta : (↑I : Type) × A) ↦
      if ta.1 ≤ t n then g' ta
      else
        if Membership.mem (α := X) (q e).target ((f : (a : (↑I : Type) × A) → X) ta : X) then
          (↑(q e).symm : X → E) ((f : (a : (↑I : Type) × A) → X) ta)
        else g ta)
    (⇑f : (a : (↑I : Type) × A) → X)
refine_2₆ :
  ∀ (a : A),
    (fun (ta : (↑I : Type) × A) ↦
          if ta.1 ≤ t n then g' ta
          else
            if Membership.mem (α := X) (q e).target ((f : (a : (↑I : Type) × A) → X) ta : X) then
              (↑(q e).symm : X → E) ((f : (a : (↑I : Type) × A) → X) ta)
            else g ta)
        (0, a) =
      g (0, a)
refine_2₇ :
  ∀ (t0 : (↑I : Type)) (htn1 : t0 ≤ t n.succ),
    (fun (ta : (↑I : Type) × A) ↦
          if ta.1 ≤ t n then g' ta
          else
            if Membership.mem (α := X) (q e).target ((f : (a : (↑I : Type) × A) → X) ta : X) then
              (↑(q e).symm : X → E) ((f : (a : (↑I : Type) × A) → X) ta)
            else g ta)
        (t0, a) =
      g (t0, a)
⊢ ∃ (N : Set A),
    a ∈ N ∧
      IsOpen[inst_2] N ∧
        ∃ (g' : (↑I : Type) × A → E),
          ContinuousOn g' (Set.Icc 0 (t n.succ) ×ˢ N) ∧
            p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X) ∧
              (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n.succ, g' (t', a) = g (t', a)

Tactic:
refine ⟨_, ?_, v_open.inter <| (cont_g'.comp (Continuous.prodMk_right <| t n).continuousOn
      fun a ha ↦ ⟨?_, ha⟩).isOpen_inter_preimage N_open (q e).open_source,
    fun ta ↦ if ta.1 ≤ t n then g' ta else if f ta ∈ (q e).target then (q e).symm (f ta) else g ta,
    .if (fun ta ⟨⟨_, hav, _, ha⟩, hfr⟩ ↦ ?_) (cont_g'.mono fun ta ⟨hta, ht⟩ ↦ ?_) ?_,
    ?_, fun a ↦ ?_, fun t0 htn1 ↦ ?_⟩