awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
cov : IsCoveringMap p
inst_3 : PathConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ : C(E, X) } he).range
γ γ' : C((↑I : Type), A)
Γ Γ' : C((↑I : Type), E)
γ_0 : (γ : (a : (↑I : Type)) → A) 0 = a₀
γ'_0 : (γ' : (a : (↑I : Type)) → A) 0 = a₀
Γ_0 : (Γ : (a : (↑I : Type)) → E) 0 = e₀
Γ'_0 : (Γ' : (a : (↑I : Type)) → E) 0 = e₀
Γ_lifts : Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
Γ'_lifts : Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ' : (a : (↑I : Type)) → E)) (⇑(f.comp γ') : (a : (↑I : Type)) → X)
γγ'1 : Eq (α := A) ((γ : (a : (↑I : Type)) → A) 1 : A) ((γ' : (a : (↑I : Type)) → A) 1 : A)
pγ : Path a₀ ((γ : (a : (↑I : Type)) → A) 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ ((γ : (a : (↑I : Type)) → A) 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
pγγ' : Path a₀ a₀ := pγ.trans pγ'.symm
pΓΓ' : Path { as := e₀ : FundamentalGroupoid E }.as { as := e₀ }.as
eq : fromPath (Path.Homotopic.Quotient.mk ((pΓΓ'.map ⋯).cast ⋯ ⋯)) = Path.Homotopic.Quotient.mk (pγγ'.map ⋯)
⊢ cov.monodromy (Path.Homotopic.Quotient.mk (pγγ'.map ⋯))
      (Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' singleton (α := X) ((f : (a : A) → X) a₀ : X)) e₀ he) =
    id (Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' singleton (α := X) ((f : (a : A) → X) a₀ : X)) e₀ he)

Tactic:
eq ▸ Subtype.ext (congr_arg (·.1) (cov.monodromy_map (.mk pΓΓ')))

Premises used: Eq.rec, Subtype.ext
-- 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
cov : IsCoveringMap p
inst_3 : PathConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ : C(E, X) } he).range
γ γ' : C((↑I : Type), A)
Γ Γ' : C((↑I : Type), E)
γ_0 : (γ : (a : (↑I : Type)) → A) 0 = a₀
γ'_0 : (γ' : (a : (↑I : Type)) → A) 0 = a₀
Γ_0 : (Γ : (a : (↑I : Type)) → E) 0 = e₀
Γ'_0 : (Γ' : (a : (↑I : Type)) → E) 0 = e₀
Γ_lifts : Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
Γ'_lifts : Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ' : (a : (↑I : Type)) → E)) (⇑(f.comp γ') : (a : (↑I : Type)) → X)
γγ'1 : Eq (α := A) ((γ : (a : (↑I : Type)) → A) 1 : A) ((γ' : (a : (↑I : Type)) → A) 1 : A)
pγ : Path a₀ ((γ : (a : (↑I : Type)) → A) 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ ((γ : (a : (↑I : Type)) → A) 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
pγγ' : Path a₀ a₀ := pγ.trans pγ'.symm
pΓΓ' : Path { as := e₀ : FundamentalGroupoid E }.as { as := e₀ }.as
eq : fromPath (Path.Homotopic.Quotient.mk ((pΓΓ'.map ⋯).cast ⋯ ⋯)) = Path.Homotopic.Quotient.mk (pγγ'.map ⋯)
⊢ cov.monodromy (Path.Homotopic.Quotient.mk (pγγ'.map ⋯))
      (Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' singleton (α := X) ((f : (a : A) → X) a₀ : X)) e₀ he) =
    id (Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' singleton (α := X) ((f : (a : A) → X) a₀ : X)) e₀ he)

Tactic:
exact eq ▸ Subtype.ext (congr_arg (·.1) (cov.monodromy_map (.mk pΓΓ')))
-- 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
inst_3 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
hs : ∀ (a : A), Membership.mem (α := X) s ((f : (a : A) → X) a : X)
f' : ContinuousMap.{u_3, u_2} A (↑s : Type u_2)
⊢ Continuous[instTopologicalSpaceSubtype, inst_1] (Subtype.val (p := fun (x : X) ↦ x ∈ s))

Tactic:
fun_prop
-- 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
inst_3 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
hs : ∀ (a : A), Membership.mem (α := X) s ((f : (a : A) → X) a : X)
⊢ Continuous[inst_2, instTopologicalSpaceSubtype] fun (a : A) ↦
    Subtype.mk (p := fun (x : X) ↦ x ∈ s) ((f : (a : A) → X) a) ⋯

Tactic:
fun_prop
-- 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
inst_3 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
hs : ∀ (a : A), Membership.mem (α := X) s ((f : (a : A) → X) a : X)
obtain :
  ∀ (f : ContinuousMap.{u_3, u_2} A (↑s : Type u_2))
    (he :
      p e₀ =
        (ContinuousMap.comp
              { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
            (a : A) → X)
          a₀)
    (hs :
      ∀ (a : A),
        Membership.mem (α := X) s
          ((ContinuousMap.comp
                  { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) }
                  f :
                (a : A) → X)
              a :
            X)),
    ∃! F : C(A, E),
      (F : (a : A) → E) a₀ = e₀ ∧
        Eq (α := A → X) (p ∘ (⇑F : (a : A) → E))
          (⇑(ContinuousMap.comp
                { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) }
                f) :
            (a : A) → X)
⊢ ∃! F : C(A, E), (F : (a : A) → E) a₀ = e₀ ∧ Eq (α := A → X) (p ∘ (⇑F : (a : A) → E)) (⇑f : (a : A) → X)

Tactic:
obtain ⟨f, rfl⟩ : ∃ f' : C(A, s), f = .comp ⟨Subtype.val, by fun_prop⟩ f' :=
    ⟨⟨fun a ↦ ⟨f a, hs a⟩, by fun_prop⟩, rfl⟩

Premises used: rfl
-- 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
inst_3 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
e₀ : E
f : ContinuousMap.{u_3, u_2} A (↑s : Type u_2)
he :
  p e₀ =
    (ContinuousMap.comp
          { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
        (a : A) → X)
      a₀
hs :
  ∀ (a : A),
    Membership.mem (α := X) s
      ((ContinuousMap.comp
              { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
            (a : A) → X)
          a :
        X)
rw :
  Membership.mem (α := X) s
    ((ContinuousMap.comp
            { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
          (a : A) → X)
        a₀ :
      X)
⊢ e₀ ∈ p ⁻¹' s

Tactic:
rw [Set.mem_preimage, he]

Premises used: Set.mem_preimage
-- 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
inst_3 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
e₀ : E
f : ContinuousMap.{u_3, u_2} A (↑s : Type u_2)
he :
  p e₀ =
    (ContinuousMap.comp
          { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
        (a : A) → X)
      a₀
hs :
  ∀ (a : A),
    Membership.mem (α := X) s
      ((ContinuousMap.comp
              { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
            (a : A) → X)
          a :
        X)
⊢ Membership.mem (α := X) s
    ((ContinuousMap.comp
            { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
          (a : A) → X)
        a₀ :
      X)

Tactic:
apply hs
-- 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
inst_3 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
e₀ : E
f : ContinuousMap.{u_3, u_2} A (↑s : Type u_2)
he :
  p e₀ =
    (ContinuousMap.comp
          { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
        (a : A) → X)
      a₀
hs :
  ∀ (a : A),
    Membership.mem (α := X) s
      ((ContinuousMap.comp
              { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
            (a : A) → X)
          a :
        X)
lift :
  ∀ (e₀ : { x : E // x ∈ p ⁻¹' s })
    (he :
      p (↑e₀ : E) =
        (ContinuousMap.comp
              { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
            (a : A) → X)
          a₀),
    ∃! F : C(A, E),
      (F : (a : A) → E) a₀ = (↑e₀ : E) ∧
        Eq (α := A → X) (p ∘ (⇑F : (a : A) → E))
          (⇑(ContinuousMap.comp
                { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) }
                f) :
            (a : A) → X)
⊢ ∃! F : C(A, E),
    (F : (a : A) → E) a₀ = e₀ ∧
      Eq (α := A → X) (p ∘ (⇑F : (a : A) → E))
        (⇑(ContinuousMap.comp
              { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f) :
          (a : A) → X)

Tactic:
lift e₀ to p ⁻¹' s using by rw [Set.mem_preimage, he]; apply hs
-- 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
inst_3 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
f : ContinuousMap.{u_3, u_2} A (↑s : Type u_2)
hs :
  ∀ (a : A),
    Membership.mem (α := X) s
      ((ContinuousMap.comp
              { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
            (a : A) → X)
          a :
        X)
e₀ : { x : E // x ∈ p ⁻¹' s }
he :
  p (↑e₀ : E) =
    (ContinuousMap.comp
          { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
        (a : A) → X)
      a₀
rcases :
  ∀ (F : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1))
    (hF :
      Eq (α := A → (↑s : Type u_2)) (s.restrictPreimage p ∘ (⇑F : (a : A) → (↑(p ⁻¹' s) : Type u_1)))
        (⇑f : (a : A) → (↑s : Type u_2)))
    (he :
      p (↑((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀) : E) =
        (ContinuousMap.comp
              { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
            (a : A) → X)
          a₀)
    (hF_unique :
      ∀ (y : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)),
        (fun (F_1 : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)) ↦
              Eq.{u_1 + 1} (α := (↑(p ⁻¹' s) : Type u_1))
                  ((F_1 : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀ : (↑(p ⁻¹' s) : Type u_1))
                  ((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀ : (↑(p ⁻¹' s) : Type u_1)) ∧
                Eq (α := A → (↑s : Type u_2)) (s.restrictPreimage p ∘ (⇑F_1 : (a : A) → (↑(p ⁻¹' s) : Type u_1)))
                  (⇑f : (a : A) → (↑s : Type u_2)))
            y →
          y = F),
    ∃! F_1 : C(A, E),
      Eq.{u_1 + 1} (α := E) ((F_1 : (a : A) → E) a₀ : E) ((↑((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀) : E) : E) ∧
        Eq (α := A → X) (p ∘ (⇑F_1 : (a : A) → E))
          (⇑(ContinuousMap.comp
                { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) }
                f) :
            (a : A) → X)
⊢ ∃! F : C(A, E),
    (F : (a : A) → E) a₀ = (↑e₀ : E) ∧
      Eq (α := A → X) (p ∘ (⇑F : (a : A) → E))
        (⇑(ContinuousMap.comp
              { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f) :
          (a : A) → X)

Tactic:
rcases cov.isCoveringMap_restrictPreimage.existsUnique_continuousMap_lifts f a₀ e₀
    (Subtype.ext he) with ⟨F, ⟨rfl, hF⟩, hF_unique⟩

Premises used: IsCoveringMapOn.isCoveringMap_restrictPreimage, IsCoveringMap.existsUnique_continuousMap_lifts, rfl, Subtype.ext
-- 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
inst_3 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
f : ContinuousMap.{u_3, u_2} A (↑s : Type u_2)
hs :
  ∀ (a : A),
    Membership.mem (α := X) s
      ((ContinuousMap.comp
              { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
            (a : A) → X)
          a :
        X)
F : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)
hF :
  Eq (α := A → (↑s : Type u_2)) (s.restrictPreimage p ∘ (⇑F : (a : A) → (↑(p ⁻¹' s) : Type u_1)))
    (⇑f : (a : A) → (↑s : Type u_2))
he :
  p (↑((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀) : E) =
    (ContinuousMap.comp
          { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
        (a : A) → X)
      a₀
hF_unique :
  ∀ (y : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)),
    (fun (F_1 : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)) ↦
          Eq.{u_1 + 1} (α := (↑(p ⁻¹' s) : Type u_1))
              ((F_1 : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀ : (↑(p ⁻¹' s) : Type u_1))
              ((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀ : (↑(p ⁻¹' s) : Type u_1)) ∧
            Eq (α := A → (↑s : Type u_2)) (s.restrictPreimage p ∘ (⇑F_1 : (a : A) → (↑(p ⁻¹' s) : Type u_1)))
              (⇑f : (a : A) → (↑s : Type u_2)))
        y →
      y = F
⊢ Continuous[instTopologicalSpaceSubtype, inst] (Subtype.val (p := fun (x : E) ↦ x ∈ p ⁻¹' s))

Tactic:
fun_prop
-- 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
inst_3 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
f : ContinuousMap.{u_3, u_2} A (↑s : Type u_2)
hs :
  ∀ (a : A),
    Membership.mem (α := X) s
      ((ContinuousMap.comp
              { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
            (a : A) → X)
          a :
        X)
F : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)
hF :
  Eq (α := A → (↑s : Type u_2)) (s.restrictPreimage p ∘ (⇑F : (a : A) → (↑(p ⁻¹' s) : Type u_1)))
    (⇑f : (a : A) → (↑s : Type u_2))
he :
  p (↑((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀) : E) =
    (ContinuousMap.comp
          { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
        (a : A) → X)
      a₀
hF_unique :
  ∀ (y : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)),
    (fun (F_1 : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)) ↦
          Eq.{u_1 + 1} (α := (↑(p ⁻¹' s) : Type u_1))
              ((F_1 : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀ : (↑(p ⁻¹' s) : Type u_1))
              ((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀ : (↑(p ⁻¹' s) : Type u_1)) ∧
            Eq (α := A → (↑s : Type u_2)) (s.restrictPreimage p ∘ (⇑F_1 : (a : A) → (↑(p ⁻¹' s) : Type u_1)))
              (⇑f : (a : A) → (↑s : Type u_2)))
        y →
      y = F
refine_1 :
  Eq (α := A → X)
    (p ∘
      (⇑(ContinuousMap.comp
            { toFun := Subtype.val (p := fun (x : E) ↦ x ∈ p ⁻¹' s), continuous_toFun := ⋯ :
              C({ x : E // x ∈ p ⁻¹' s }, E) }
            F) :
        (a : A) → E))
    (⇑(ContinuousMap.comp
          { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f) :
      (a : A) → X)
refine_2 :
  ∀ (y : C(A, E)),
    (fun (F_1 : C(A, E)) ↦
          Eq.{u_1 + 1} (α := E) ((F_1 : (a : A) → E) a₀ : E) ((↑((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀) : E) : E) ∧
            Eq (α := A → X) (p ∘ (⇑F_1 : (a : A) → E))
              (⇑(ContinuousMap.comp
                    { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ :
                      C({ x : X // x ∈ s }, X) }
                    f) :
                (a : A) → X))
        y →
      y = ContinuousMap.comp { toFun := Subtype.val (p := fun (x : E) ↦ x ∈ p ⁻¹' s), continuous_toFun := ⋯ } F
⊢ ∃! F_1 : C(A, E),
    Eq.{u_1 + 1} (α := E) ((F_1 : (a : A) → E) a₀ : E) ((↑((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀) : E) : E) ∧
      Eq (α := A → X) (p ∘ (⇑F_1 : (a : A) → E))
        (⇑(ContinuousMap.comp
              { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f) :
          (a : A) → X)

Tactic:
refine ⟨.comp ⟨Subtype.val, by fun_prop⟩ F, ⟨rfl, ?_⟩, ?_⟩
-- 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
inst_3 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
f : ContinuousMap.{u_3, u_2} A (↑s : Type u_2)
hs :
  ∀ (a : A),
    Membership.mem (α := X) s
      ((ContinuousMap.comp
              { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
            (a : A) → X)
          a :
        X)
F : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)
hF :
  Eq (α := A → (↑s : Type u_2)) (s.restrictPreimage p ∘ (⇑F : (a : A) → (↑(p ⁻¹' s) : Type u_1)))
    (⇑f : (a : A) → (↑s : Type u_2))
he :
  p (↑((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀) : E) =
    (ContinuousMap.comp
          { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
        (a : A) → X)
      a₀
hF_unique :
  ∀ (y : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)),
    (fun (F_1 : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)) ↦
          Eq.{u_1 + 1} (α := (↑(p ⁻¹' s) : Type u_1))
              ((F_1 : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀ : (↑(p ⁻¹' s) : Type u_1))
              ((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀ : (↑(p ⁻¹' s) : Type u_1)) ∧
            Eq (α := A → (↑s : Type u_2)) (s.restrictPreimage p ∘ (⇑F_1 : (a : A) → (↑(p ⁻¹' s) : Type u_1)))
              (⇑f : (a : A) → (↑s : Type u_2)))
        y →
      y = F
⊢ Eq (α := A → X)
    (p ∘
      (⇑(ContinuousMap.comp
            { toFun := Subtype.val (p := fun (x : E) ↦ x ∈ p ⁻¹' s), continuous_toFun := ⋯ :
              C({ x : E // x ∈ p ⁻¹' s }, E) }
            F) :
        (a : A) → E))
    (⇑(ContinuousMap.comp
          { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f) :
      (a : A) → X)

Tactic:
simp [← hF, Function.comp_def]

Premises used: Function.comp_def
-- 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
inst_3 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
f : ContinuousMap.{u_3, u_2} A (↑s : Type u_2)
hs :
  ∀ (a : A),
    Membership.mem (α := X) s
      ((ContinuousMap.comp
              { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
            (a : A) → X)
          a :
        X)
F : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)
hF :
  Eq (α := A → (↑s : Type u_2)) (s.restrictPreimage p ∘ (⇑F : (a : A) → (↑(p ⁻¹' s) : Type u_1)))
    (⇑f : (a : A) → (↑s : Type u_2))
he :
  p (↑((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀) : E) =
    (ContinuousMap.comp
          { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
        (a : A) → X)
      a₀
hF_unique :
  ∀ (y : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)),
    (fun (F_1 : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)) ↦
          Eq.{u_1 + 1} (α := (↑(p ⁻¹' s) : Type u_1))
              ((F_1 : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀ : (↑(p ⁻¹' s) : Type u_1))
              ((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀ : (↑(p ⁻¹' s) : Type u_1)) ∧
            Eq (α := A → (↑s : Type u_2)) (s.restrictPreimage p ∘ (⇑F_1 : (a : A) → (↑(p ⁻¹' s) : Type u_1)))
              (⇑f : (a : A) → (↑s : Type u_2)))
        y →
      y = F
F' : C(A, E)
hF'₁ : Eq.{u_1 + 1} (α := E) ((F' : (a : A) → E) a₀ : E) ((↑((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀) : E) : E)
hF'₂ :
  Eq (α := A → X) (p ∘ (⇑F' : (a : A) → E))
    (⇑(ContinuousMap.comp
          { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f) :
      (a : A) → X)
⊢ ∀ (x : A), p ((F' : (a : A) → E) x) = (↑((f : (a : A) → { x : X // x ∈ s }) x) : X)

Tactic:
simp only [ContinuousMap.coe_comp, ContinuousMap.coe_mk, funext_iff,
      Function.comp_apply] at hF'₂

Premises used: ContinuousMap.coe_comp, funext_iff, ContinuousMap.coe_mk, Function.comp_apply
-- 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
inst_3 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
f : ContinuousMap.{u_3, u_2} A (↑s : Type u_2)
hs :
  ∀ (a : A),
    Membership.mem (α := X) s
      ((ContinuousMap.comp
              { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
            (a : A) → X)
          a :
        X)
F : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)
hF :
  Eq (α := A → (↑s : Type u_2)) (s.restrictPreimage p ∘ (⇑F : (a : A) → (↑(p ⁻¹' s) : Type u_1)))
    (⇑f : (a : A) → (↑s : Type u_2))
he :
  p (↑((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀) : E) =
    (ContinuousMap.comp
          { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
        (a : A) → X)
      a₀
hF_unique :
  ∀ (y : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)),
    (fun (F_1 : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)) ↦
          Eq.{u_1 + 1} (α := (↑(p ⁻¹' s) : Type u_1))
              ((F_1 : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀ : (↑(p ⁻¹' s) : Type u_1))
              ((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀ : (↑(p ⁻¹' s) : Type u_1)) ∧
            Eq (α := A → (↑s : Type u_2)) (s.restrictPreimage p ∘ (⇑F_1 : (a : A) → (↑(p ⁻¹' s) : Type u_1)))
              (⇑f : (a : A) → (↑s : Type u_2)))
        y →
      y = F
F' : C(A, E)
hF'₁ : Eq.{u_1 + 1} (α := E) ((F' : (a : A) → E) a₀ : E) ((↑((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀) : E) : E)
hF'₂ : ∀ (x : A), p ((F' : (a : A) → E) x) = (↑((f : (a : A) → { x : X // x ∈ s }) x) : X)
a : A
rw : (↑((f : (a : A) → { x : X // x ∈ s }) a) : X) ∈ s
⊢ Membership.mem (α := E) (p ⁻¹' s) ((F' : (a : A) → E) a : E)

Tactic:
rw [Set.mem_preimage, hF'₂]

Premises used: Set.mem_preimage