awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (hypothesis)
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 :
  Eq.{u_2 + 1} (α := FundamentalGroup X ((f : (a : A) → X) a₀ : X))
    ((mapOfEq { toFun := p, continuous_toFun := ⋯ : C(E, X) } he :
          (a : FundamentalGroup E e₀) → FundamentalGroup X ((f : (a : A) → X) a₀))
        (Path.Homotopic.Quotient.mk pΓΓ') :
      FundamentalGroup X ((f : (a : A) → X) a₀ : X))
    ((FundamentalGroup.map f a₀ : (a : FundamentalGroup A a₀) → FundamentalGroup X ((f : (a : A) → X) a₀))
        (fromPath (Path.Homotopic.Quotient.mk pγγ')) :
      FundamentalGroup X ((f : (a : A) → X) a₀ : X))
⊢ 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)
have eq₁ : fromPath (Path.Homotopic.Quotient.mk ((pΓΓ'.map sorry).cast sorry sorry)) = Path.Homotopic.Quotient.mk (pγγ'.map sorry)
Tactic: rw [mapOfEq_apply, map_apply, ← mk_map] at eq
Cleared hypotheses: eq
-- 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
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 : C(A, E), (F : (a : A) → E) a₀ = e₀ ∧ Eq (α := A → X) (p ∘ (⇑F : (a : A) → E)) (⇑f : (a : A) → X)
have 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 := sorry : 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 := sorry : 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 := sorry : C({ x : X // x ∈ s }, X) } 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⟩
Cleared hypotheses: f, he, hs
-- 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
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)
⊢ e₀ ∈ p ⁻¹' s
have rw : Membership.mem (α := X) s
  ((ContinuousMap.comp
          { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := sorry : C({ x : X // x ∈ s }, X) } f :
        (a : A) → X)
      a₀ :
    X)
Tactic: rw [Set.mem_preimage, he]
-- 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
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)
⊢ ∃! 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)
have lift : ∀ (e₀ : { x : E // x ∈ p ⁻¹' s })
  (he :
    p (↑e₀ : E) =
      (ContinuousMap.comp
            { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := sorry : 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 := sorry : 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
Cleared hypotheses: e₀, he
-- 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
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₀
⊢ ∃! 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)
have 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 := sorry : 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 := sorry : 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⟩
Cleared hypotheses: e₀, he
-- 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
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_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)
have refine_1 : Eq (α := A → X)
  (p ∘
    (⇑(ContinuousMap.comp
          { toFun := Subtype.val (p := fun (x : E) ↦ x ∈ p ⁻¹' s), continuous_toFun := sorry :
            C({ x : E // x ∈ p ⁻¹' s }, E) }
          F) :
      (a : A) → E))
  (⇑(ContinuousMap.comp
        { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := sorry : C({ x : X // x ∈ s }, X) } f) :
    (a : A) → X)
Tactic: refine ⟨.comp ⟨Subtype.val, by fun_prop⟩ F, ⟨rfl, ?_⟩, ?_⟩
-- 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
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)
⊢ ∃! 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)
have 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 := sorry : 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 := sorry } F
Tactic: refine ⟨.comp ⟨Subtype.val, by fun_prop⟩ F, ⟨rfl, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (hypothesis)
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)
⊢ F' = ContinuousMap.comp { toFun := Subtype.val (p := fun (x : E) ↦ x ∈ p ⁻¹' s), continuous_toFun := ⋯ } F
have hF'₃ : ∀ (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'₂
Cleared hypotheses: hF'₂
-- 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
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
⊢ Membership.mem (α := E) (p ⁻¹' s) ((F' : (a : A) → E) a : E)
have rw : (↑((f : (a : A) → { x : X // x ∈ s }) a) : X) ∈ s
Tactic: rw [Set.mem_preimage, hF'₂]
-- 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
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)
⊢ F' = ContinuousMap.comp { toFun := Subtype.val (p := fun (x : E) ↦ x ∈ p ⁻¹' s), continuous_toFun := ⋯ } F
have refine_2 : Eq (α := A → (↑s : Type u_2))
  (s.restrictPreimage p ∘
    (⇑{ toFun := fun (a : A) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' s) ((F' : (a : A) → E) a) sorry,
          continuous_toFun := sorry } :
      (a : A) → (↑(p ⁻¹' s) : Type u_1)))
  (⇑f : (a : A) → (↑s : Type u_2))
Tactic: specialize hF_unique
      ⟨fun a ↦ ⟨F' a, by rw [Set.mem_preimage, hF'₂]; exact (f a).2⟩, by fun_prop⟩
      ⟨Subtype.ext hF'₁, ?_⟩
-- 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
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)
refine_2 :
  Eq (α := A → (↑s : Type u_2))
    (s.restrictPreimage p ∘
      (⇑{ toFun := fun (a : A) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' s) ((F' : (a : A) → E) a) ⋯,
            continuous_toFun := ⋯ } :
        (a : A) → (↑(p ⁻¹' s) : Type u_1)))
    (⇑f : (a : A) → (↑s : Type u_2))
⊢ F' = ContinuousMap.comp { toFun := Subtype.val (p := fun (x : E) ↦ x ∈ p ⁻¹' s), continuous_toFun := ⋯ } F
have refine_2₁ : ∀
  (hF_unique :
    { toFun := fun (a : A) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' s) ((F' : (a : A) → E) a) sorry,
        continuous_toFun := sorry } =
      F),
  F' = ContinuousMap.comp { toFun := Subtype.val (p := fun (x : E) ↦ x ∈ p ⁻¹' s), continuous_toFun := sorry } F
Tactic: specialize hF_unique
      ⟨fun a ↦ ⟨F' a, by rw [Set.mem_preimage, hF'₂]; exact (f a).2⟩, by fun_prop⟩
      ⟨Subtype.ext hF'₁, ?_⟩
Cleared hypotheses: hF_unique