Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_2
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
f : C(↑I × A, X)
g : ↑I × A → E
g_lifts : p ∘ g = ⇑f
cont_0 : Continuous[inst✝, inst✝²] fun x ↦ g (0, x)
a : A
cont_a : Continuous[_, inst✝²] fun x ↦ g (x, a)
q : E → OpenPartialHomeomorph E X
mem_source : ∀ (x : E), x ∈ (q x).source
hpq : ∀ (x : E), p = ↑(q x)
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a)) ⁻¹' (q i).source
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
x✝ :
  ∃ N,
    a ∈ N ∧
      IsOpen[inst✝] N ∧
        ∃ g',
          ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N) ∧
            p ∘ g' = ⇑f ∧ (∀ (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✝] N
g' : ↑I × A → E
cont_g' : ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N)
g'_lifts : p ∘ g' = ⇑f
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 ↦ g (x, a)) ⁻¹' (q e).source
this : Set.Icc (t n) (t (n + 1)) ×ˢ {a} ⊆ ⇑f ⁻¹' (q e).target
u : Set ↑I
v : Set A
v_open : IsOpen[inst✝] v
hu : Set.Icc (t n) (t (n + 1)) ⊆ u
hav : {a} ⊆ v
huv : u ×ˢ v ⊆ ⇑f ⁻¹' (q e).target
⊢ ∃ N,
    a ∈ N ∧
      IsOpen[inst✝] N ∧
        ∃ g',
          ContinuousOn g' (Set.Icc 0 (t n.succ) ×ˢ N) ∧
            p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n.succ, g' (t', a) = g (t', a)

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_ofPred.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($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($g'_lifts ta)
    · rw [hpq e, (q e).right_inv hv]
    · exact congr($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($g_lifts _).symm
    · rfl

Goal state after: