-- 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
inst_3 : PathConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
Γ : (γ : C((↑I : Type), A)) → (γ : (a : (↑I : Type)) → A) 0 = a₀ → C((↑I : Type), E)
Γ_0 : ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀), (Γ γ a : (a : (↑I : Type)) → E) 0 = e₀
F : (a : A) → E := fun (a : A) ↦ (Γ (Path.toContinuousMap (somePath a₀ a)) ⋯ : (a : (↑I : Type)) → E) 1
a : A
p : OpenPartialHomeomorph E X
hep : F a ∈ p.source
homeo : IsLocalHomeomorph (↑p : E → X)
he : (↑p : E → X) e₀ = (f : (a : A) → X) a₀
uniq :
  ∀ (γ γ' : C((↑I : Type), A)) (Γ Γ' : C((↑I : Type), E)),
    (γ : (a : (↑I : Type)) → A) 0 = a₀ →
      (γ' : (a : (↑I : Type)) → A) 0 = a₀ →
        (Γ : (a : (↑I : Type)) → E) 0 = e₀ →
          (Γ' : (a : (↑I : Type)) → E) 0 = e₀ →
            Eq (α := (↑I : Type) → X) ((↑p : E → X) ∘ (⇑Γ : (a : (↑I : Type)) → E))
                (⇑(f.comp γ) : (a : (↑I : Type)) → X) →
              Eq (α := (↑I : Type) → X) ((↑p : E → X) ∘ (⇑Γ' : (a : (↑I : Type)) → E))
                  (⇑(f.comp γ') : (a : (↑I : Type)) → X) →
                Eq (α := A) ((γ : (a : (↑I : Type)) → A) 1 : A) ((γ' : (a : (↑I : Type)) → A) 1 : A) →
                  Eq (α := E) ((Γ : (a : (↑I : Type)) → E) 1 : E) ((Γ' : (a : (↑I : Type)) → E) 1 : E)
Γ_lifts :
  ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀),
    Eq (α := (↑I : Type) → X) ((↑p : E → X) ∘ (⇑(Γ γ a) : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
this : ∀ (a : A), (↑p : E → X) (F a) = (f : (a : A) → X) a
hfap : Membership.mem (α := X) p.target ((f : (a : A) → X) a : X)
U : Set A
haU : U ∈ 𝓝 a
U_conn : IsPathConnected U
hUp : id U ⊆ (⇑f : (a : A) → X) ⁻¹' p.target
x : A
hxU : x ∈ U
γ : Path a x
hγ : ∀ (t : (↑I : Type)), Membership.mem (α := A) U ((γ : (a : (↑I : Type)) → A) t : A)
Γ' : Path e₀ (((↑p.symm : X → E) ∘ (⇑f : (a : A) → X)) a) :=
  { toContinuousMap := Γ (Path.toContinuousMap (somePath a₀ a)) ⋯, source' := ⋯, target' := ⋯ }
x_1 : (↑I : Type)
pos :
  ∀ (h : (↑x_1 : ℝ) ≤ 1 / 2),
    (↑p : E → X) ((Γ' : (a : (↑I : Type)) → E) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ)) ⋯)) =
      (f : (a : A) → X)
        ((somePath a₀ a : (a : (↑I : Type)) → A) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ)) ⋯) : A)
⊢ (↑p : E → X)
      (if h : (↑x_1 : ℝ) ≤ 1 / 2 then
        (Γ' : (a : (↑I : Type)) → E) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ)) ⋯)
      else (γ.map' ⋯ : (a : (↑I : Type)) → E) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ) - 1) ⋯)) =
    (f : (a : A) → X)
      (if h : (↑x_1 : ℝ) ≤ 1 / 2 then
        (somePath a₀ a : (a : (↑I : Type)) → A) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ)) ⋯)
      else (γ : (a : (↑I : Type)) → A) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ) - 1) ⋯))
have neg : ∀ (h : ¬(↑x_1 : ℝ) ≤ 1 / 2),
  (↑p : E → X) ((γ.map' sorry : (a : (↑I : Type)) → E) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ) - 1) sorry)) =
    (f : (a : A) → X) ((γ : (a : (↑I : Type)) → A) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ) - 1) sorry) : A)
Tactic: split_ifs