awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ (↑p.symm : X → E) ∘ (⇑f : (a : A) → X) =ᶠ[𝓝 a] F
have refine_1 : ∀ (x : A) (hxU : x ∈ U),
  Membership.mem (γ := Set A) {x : A | (fun (x : A) ↦ ((↑p.symm : X → E) ∘ (⇑f : (a : A) → X)) x = F x) x} x
Tactic: refine Filter.mem_of_superset haU fun x hxU ↦ ?_
-- 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
⊢ Membership.mem (γ := Set A) {x : A | (fun (x : A) ↦ ((↑p.symm : X → E) ∘ (⇑f : (a : A) → X)) x = F x) x} x
have refine_1 : ∀ (γ : Path a x) (hγ : ∀ (t : (↑I : Type)), Membership.mem (α := A) U ((γ : (a : (↑I : Type)) → A) t : A)),
  Membership.mem (γ := Set A) {x : A | (fun (x : A) ↦ ((↑p.symm : X → E) ∘ (⇑f : (a : A) → X)) x = F x) x} x
Tactic: have ⟨γ, hγ⟩ := U_conn.joinedIn _ (mem_of_mem_nhds haU) _ hxU
-- 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' := ⋯ }
⊢ Membership.mem (γ := Set A) {x : A | (fun (x : A) ↦ ((↑p.symm : X → E) ∘ (⇑f : (a : A) → X)) x = F x) x} x
have refine_1 : Eq (α := (↑I : Type) → X) ((↑p : E → X) ∘ (⇑(↑(Γ'.trans (γ.map' sorry)) : C((↑I : Type), E)) : (a : (↑I : Type)) → E))
  (⇑(f.comp (↑(Path.trans (somePath a₀ a) γ) : C((↑I : Type), A))) : (a : (↑I : Type)) → 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)
-- 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' := ⋯ }
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)
⊢ Membership.mem (γ := Set A) {x : A | (fun (x : A) ↦ ((↑p.symm : X → E) ∘ (⇑f : (a : A) → X)) x = F x) x} x
have refine_1₁ : ∀
  (uniq :
    Eq (α := E) (((↑(Γ'.trans (γ.map' sorry)) : C((↑I : Type), E)) : (a : (↑I : Type)) → E) 1 : E)
      ((Γ (Path.toContinuousMap (somePath a₀ x)) sorry : (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
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)
Cleared hypotheses: uniq
-- 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' := ⋯ }
⊢ 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)
have refine_1 : ∀ (x_1 : (↑I : Type)),
  ((↑p : E → X) ∘ (⇑(↑(Γ'.trans (γ.map' sorry)) : C((↑I : Type), E)) : (a : (↑I : Type)) → E)) x_1 =
    (f.comp (↑(Path.trans (somePath a₀ a) γ) : C((↑I : Type), A)) : (a : (↑I : Type)) → X) x_1
Tactic: ext
-- 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)
⊢ ((↑p : E → X) ∘ (⇑(↑(Γ'.trans (γ.map' ⋯)) : C((↑I : Type), E)) : (a : (↑I : Type)) → E)) x_1 =
    (f.comp (↑(Path.trans (somePath a₀ a) γ) : C((↑I : Type), A)) : (a : (↑I : Type)) → X) x_1
have refine_1 : (↑p : E → X)
    (if h : (↑x_1 : ℝ) ≤ 1 / 2 then
      (Γ' : (a : (↑I : Type)) → E) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ)) sorry)
    else (γ.map' sorry : (a : (↑I : Type)) → E) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ) - 1) sorry)) =
  (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 : ℝ)) sorry)
    else (γ : (a : (↑I : Type)) → A) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ) - 1) sorry))
Tactic: simp only [Function.comp, ContinuousMap.coe_coe, Path.trans_apply, ContinuousMap.coe_comp]
-- 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)
⊢ (↑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 pos : ∀ (h : (↑x_1 : ℝ) ≤ 1 / 2),
  (↑p : E → X) ((Γ' : (a : (↑I : Type)) → E) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ)) sorry)) =
    (f : (a : A) → X)
      ((somePath a₀ a : (a : (↑I : Type)) → A) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ)) sorry) : A)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C((↑I : Type), X)
e : E
γ_0 : (γ : (a : (↑I : Type)) → X) 0 = p e
Γ : C((↑I : Type), E)
⊢ Γ = cov.liftPath γ e γ_0 ↔
    Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑γ : (a : (↑I : Type)) → X) ∧
      (Γ : (a : (↑I : Type)) → E) 0 = e
have simp_rw : Eq (α := (a : (↑I : Type)) → E) (⇑Γ : (a : (↑I : Type)) → E) (⇑(cov.liftPath γ e γ_0) : (a : (↑I : Type)) → E) ↔
  Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑γ : (a : (↑I : Type)) → X) ∧
    (Γ : (a : (↑I : Type)) → E) 0 = e
Tactic: simp_rw [← DFunLike.coe_fn_eq, eq_liftPath_iff, and_iff_right (ContinuousMap.continuous _)]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C((↑I : Type), X)
e : E
γ_0 : (γ : (a : (↑I : Type)) → X) 0 = p e
Γ : C((↑I : Type), E)
simp_rw :
  Eq (α := (a : (↑I : Type)) → E) (⇑Γ : (a : (↑I : Type)) → E) (⇑(cov.liftPath γ e γ_0) : (a : (↑I : Type)) → E) ↔
    Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑γ : (a : (↑I : Type)) → X) ∧
      (Γ : (a : (↑I : Type)) → E) 0 = e
⊢ Γ = cov.liftPath γ e γ_0 ↔
    Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑γ : (a : (↑I : Type)) → X) ∧
      (Γ : (a : (↑I : Type)) → E) 0 = e
have simp_rw₁ : Continuous[_, inst] (⇑Γ : (a : (↑I : Type)) → E) ∧
    Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑γ : (a : (↑I : Type)) → X) ∧
      (Γ : (a : (↑I : Type)) → E) 0 = e ↔
  Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑γ : (a : (↑I : Type)) → X) ∧
    (Γ : (a : (↑I : Type)) → E) 0 = e
Tactic: simp_rw [← DFunLike.coe_fn_eq, eq_liftPath_iff, and_iff_right (ContinuousMap.continuous _)]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
x y z : X
e : E
hpe : x = p e
γ : Path x y
γ' : Path y z
⊢ cov.liftPath (↑(γ.trans γ') : C((↑I : Type), X)) e ⋯ =
    (↑({ toContinuousMap := cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯, source' := ⋯, target' := ⋯ :
              Path e ((cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯ : (a : (↑I : Type)) → E) 1) }.trans
          {
            toContinuousMap :=
              cov.liftPath (↑γ' : C((↑I : Type), X))
                ((cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯ : (a : (↑I : Type)) → E) 1) ⋯,
            source' := ⋯, target' := ⋯ :
            Path ((cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯ : (a : (↑I : Type)) → E) 1)
              ((cov.liftPath (↑γ' : C((↑I : Type), X))
                    ((cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯ : (a : (↑I : Type)) → E) 1) ⋯).toFun
                1) }) :
      C((↑I : Type), E))
have refine : ∀ (x_1 : (↑I : Type)),
  (p ∘
        (⇑(↑({ toContinuousMap := cov.liftPath (↑γ : C((↑I : Type), X)) e sorry, source' := sorry, target' := sorry :
                      Path e ((cov.liftPath (↑γ : C((↑I : Type), X)) e sorry : (a : (↑I : Type)) → E) 1) }.trans
                  {
                    toContinuousMap :=
                      cov.liftPath (↑γ' : C((↑I : Type), X))
                        ((cov.liftPath (↑γ : C((↑I : Type), X)) e sorry : (a : (↑I : Type)) → E) 1) sorry,
                    source' := sorry, target' := sorry :
                    Path ((cov.liftPath (↑γ : C((↑I : Type), X)) e sorry : (a : (↑I : Type)) → E) 1)
                      ((cov.liftPath (↑γ' : C((↑I : Type), X))
                            ((cov.liftPath (↑γ : C((↑I : Type), X)) e sorry : (a : (↑I : Type)) → E) 1) sorry).toFun
                        1) }) :
              C((↑I : Type), E)) :
          (a : (↑I : Type)) → E))
      x_1 =
    ((↑(γ.trans γ') : C((↑I : Type), X)) : (a : (↑I : Type)) → X) x_1
Tactic: refine .symm <| (cov.eq_liftPath_iff' _).mpr ⟨funext fun _ ↦ ?_, by simp⟩