-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
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
⊢ ∃ (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)
have 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
Tactic: classical
  /- Use the inverse of `q e` to extend g' from [0, tₙ] × Nₙ₊₁ to [0, tₙ₊₁] × Nₙ₊₁, where
    Nₙ₊₁ ⊆ v ∩ Nₙ is such that {tₙ} × Nₙ₊₁ is mapped to the domain (`source`) of `q e` by `g'`. -/
  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 ↦ ?_⟩
  · refine ⟨Set.singleton_subset_iff.mp hav, haN, ?_⟩
    change g' (t n, a) ∈ (q e).source; rw [g'_a _ le_rfl]
    exact h_sub ⟨le_rfl, t_mono n.le_succ⟩
  · rw [← t_0]; exact ⟨t_mono n.zero_le, le_rfl⟩
  · have ht := Set.mem_setOf.mp (frontier_le_subset_eq continuous_fst continuous_const hfr)
    have : f ta ∈ (q e).target := huv ⟨hu (by rw [ht]; exact ⟨le_rfl, t_mono n.le_succ⟩), hav⟩
    rw [if_pos this]
    -- here we use that {tₙ} × Nₙ₊₁ is mapped to the domain of `q e`
    apply (q e).injOn (by rwa [← ta.eta, ht]) ((q e).map_target this)
    rw [(q e).right_inv this, ← hpq e]; exact congr_fun g'_lifts ta
  · rw [closure_le_eq continuous_fst continuous_const] at ht
    exact ⟨⟨hta.1.1, ht⟩, hta.2.2.1⟩
  · simp_rw [not_le]; exact (ContinuousOn.congr ((q e).continuousOn_invFun.comp f.2.continuousOn
      fun _ h ↦ huv ⟨hu ⟨h.2, h.1.1.2⟩, h.1.2.1⟩)
      fun _ h ↦ if_pos <| huv ⟨hu ⟨h.2, h.1.1.2⟩, h.1.2.1⟩).mono
        (Set.inter_subset_inter_right _ <| closure_lt_subset_le continuous_const continuous_fst)
  · ext ta; rw [Function.comp_apply]; split_ifs with _ hv
    · exact congr_fun g'_lifts ta
    · rw [hpq e, (q e).right_inv hv]
    · exact congr_fun g_lifts ta
  · rw [← g'_0]; exact if_pos bot_le
  · dsimp only; split_ifs with htn hf
    · exact g'_a t0 htn
    · apply (q e).injOn ((q e).map_target hf) (h_sub ⟨le_of_not_ge htn, htn1⟩)
      rw [(q e).right_inv hf, ← hpq e]; exact (congr_fun g_lifts _).symm
    · rfl