-- 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
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' := ⋯ }
refine_1 :
  Eq (α := (↑I : Type) → X) ((↑p : E → X) ∘ (⇑(↑(Γ'.trans (γ.map' ⋯)) : C((↑I : Type), E)) : (a : (↑I : Type)) → E))
    (⇑(f.comp (↑(Path.trans (somePath a₀ a) γ) : C((↑I : Type), A))) : (a : (↑I : Type)) → X)
refine_1₁ :
  ∀
    (uniq :
      Eq (α := E) (((↑(Γ'.trans (γ.map' ⋯)) : C((↑I : Type), E)) : (a : (↑I : Type)) → E) 1 : E)
        ((Γ (Path.toContinuousMap (somePath a₀ x)) ⋯ : (a : (↑I : Type)) → E) 1 : E)),
    Membership.mem (γ := Set A) {x : A | (fun (x : A) ↦ ((↑p.symm : X → E) ∘ (⇑f : (a : A) → X)) x = F x) x} x
⊢ Membership.mem (γ := Set A) {x : A | (fun (x : A) ↦ ((↑p.symm : X → E) ∘ (⇑f : (a : A) → X)) x = F x) x} x

Tactic:
specialize uniq ((somePath a₀ a).trans γ) _ (Γ'.trans <| γ.map' <| p.continuousOn_symm.comp
      f.2.continuousOn <| by rintro _ ⟨t, rfl⟩; exact hUp (hγ _)) _ (by simp) (somePath a₀ x).source
      (by simp) (Γ_0 _ (somePath a₀ x).source) _ (Γ_lifts ..) (by simp)

Premises used: Continuous.continuousOn, Path.trans, toContinuousMap, ContinuousOn.comp, ContinuousMap.continuous_toFun, PathConnectedSpace.somePath, Path.source, OpenPartialHomeomorph.continuousOn_symm, Path.map'