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
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 :
  ∀ (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
⊢ 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)

Tactic:
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
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)
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 : ℝ)) ⋯)
      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) ⋯))
⊢ ((↑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

Tactic:
simp only [Function.comp, ContinuousMap.coe_coe, Path.trans_apply, ContinuousMap.coe_comp]

Premises used: ContinuousMap.coe_comp, Function.comp, Path.trans_apply, ContinuousMap.coe_coe
-- 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' := ⋯ }
x_1 : (↑I : Type)
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)

Tactic:
apply congr_fun (Γ_lifts ..)

Premises used: congr_fun
-- 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' := ⋯ }
x_1 : (↑I : Type)
h : ¬(↑x_1 : ℝ) ≤ 1 / 2
⊢ (↑p : E → X) ((γ.map' ⋯ : (a : (↑I : Type)) → E) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ) - 1) ⋯)) =
    (f : (a : A) → X) ((γ : (a : (↑I : Type)) → A) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ) - 1) ⋯) : A)

Tactic:
simp [Path.map', p.right_inv (hUp (hγ _))]

Premises used: Path.map', OpenPartialHomeomorph.right_inv
-- 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₀
Γ_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' := ⋯ }
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

Tactic:
simpa using uniq
-- 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
homeo : IsLocalHomeomorph 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₀
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 ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X) →
              Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ' : (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)
Γ : (γ : 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₀
Γ_lifts :
  ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀),
    Eq (α := (↑I : Type) → X) (p ∘ (⇑(Γ γ a) : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
F : (a : A) → E := fun (a : A) ↦ (Γ (Path.toContinuousMap (somePath a₀ a)) ⋯ : (a : (↑I : Type)) → E) 1
this : ∀ (a : A), p (F a) = (f : (a : A) → X) a
⊢ Eq (α := (↑I : Type) → X) (p ∘ (⇑(ContinuousMap.const (↑I : Type) e₀) : (a : (↑I : Type)) → E))
    (⇑(f.comp (ContinuousMap.const (↑I : Type) a₀)) : (a : (↑I : Type)) → X)

Tactic:
simpa
-- 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
homeo : IsLocalHomeomorph 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₀
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 ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X) →
              Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ' : (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)
Γ : (γ : 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₀
Γ_lifts :
  ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀),
    Eq (α := (↑I : Type) → X) (p ∘ (⇑(Γ γ a) : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
F : (a : A) → E := fun (a : A) ↦ (Γ (Path.toContinuousMap (somePath a₀ a)) ⋯ : (a : (↑I : Type)) → E) 1
this : ∀ (a : A), p (F a) = (f : (a : A) → X) a
⊢ ({ toFun := F, continuous_toFun := ⋯ } : (a : A) → E) a₀ = e₀

Tactic:
exact uniq _ (.const I a₀) _ (.const I e₀) (somePath a₀ a₀).source rfl (Γ_0 ..) rfl (Γ_lifts ..)
      (by simpa) (Path.target _)

Premises used: Set.Elem, PathConnectedSpace.somePath, Path.source, ContinuousMap.const, Path.target, unitInterval, 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
homeo : IsLocalHomeomorph 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₀
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 ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X) →
              Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ' : (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)
Γ : (γ : 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₀
Γ_lifts :
  ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀),
    Eq (α := (↑I : Type) → X) (p ∘ (⇑(Γ γ a) : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
F : (a : A) → E := fun (a : A) ↦ (Γ (Path.toContinuousMap (somePath a₀ a)) ⋯ : (a : (↑I : Type)) → E) 1
this : ∀ (a : A), p (F a) = (f : (a : A) → X) a
F' : C(A, E)
h : (fun (F : C(A, E)) ↦ (F : (a : A) → E) a₀ = e₀ ∧ Eq (α := A → X) (p ∘ (⇑F : (a : A) → E)) (⇑f : (a : A) → X)) F'
F'_0 : (F' : (a : A) → E) a₀ = e₀
hpF' : Eq (α := A → X) (p ∘ (⇑F' : (a : A) → E)) (⇑f : (a : A) → X)
a : A
γ : Path a₀ a := somePath a₀ a
⊢ (F'.comp (↑γ : C((↑I : Type), A)) : (a : (↑I : Type)) → E) 0 = e₀

Tactic:
simpa
-- 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
homeo : IsLocalHomeomorph 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₀
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 ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X) →
              Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ' : (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)
Γ : (γ : 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₀
Γ_lifts :
  ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀),
    Eq (α := (↑I : Type) → X) (p ∘ (⇑(Γ γ a) : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
F : (a : A) → E := fun (a : A) ↦ (Γ (Path.toContinuousMap (somePath a₀ a)) ⋯ : (a : (↑I : Type)) → E) 1
this : ∀ (a : A), p (F a) = (f : (a : A) → X) a
F' : C(A, E)
h : (fun (F : C(A, E)) ↦ (F : (a : A) → E) a₀ = e₀ ∧ Eq (α := A → X) (p ∘ (⇑F : (a : A) → E)) (⇑f : (a : A) → X)) F'
F'_0 : (F' : (a : A) → E) a₀ = e₀
hpF' : Eq (α := A → X) (p ∘ (⇑F' : (a : A) → E)) (⇑f : (a : A) → X)
a : A
γ : Path a₀ a := somePath a₀ a
⊢ Eq (α := (↑I : Type) → X) (p ∘ (⇑(F'.comp (↑γ : C((↑I : Type), A))) : (a : (↑I : Type)) → E))
    (⇑(f.comp γ.toContinuousMap) : (a : (↑I : Type)) → X)

Tactic:
simp [← Function.comp_assoc, hpF']

Premises used: Function.comp_assoc
-- 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
homeo : IsLocalHomeomorph 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₀
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 ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X) →
              Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ' : (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)
Γ : (γ : 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₀
Γ_lifts :
  ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀),
    Eq (α := (↑I : Type) → X) (p ∘ (⇑(Γ γ a) : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
F : (a : A) → E := fun (a : A) ↦ (Γ (Path.toContinuousMap (somePath a₀ a)) ⋯ : (a : (↑I : Type)) → E) 1
this : ∀ (a : A), p (F a) = (f : (a : A) → X) a
F' : C(A, E)
h : (fun (F : C(A, E)) ↦ (F : (a : A) → E) a₀ = e₀ ∧ Eq (α := A → X) (p ∘ (⇑F : (a : A) → E)) (⇑f : (a : A) → X)) F'
F'_0 : (F' : (a : A) → E) a₀ = e₀
hpF' : Eq (α := A → X) (p ∘ (⇑F' : (a : A) → E)) (⇑f : (a : A) → X)
a : A
γ : Path a₀ a := somePath a₀ a
⊢ Eq.{u_1 + 1} (α := E) ((F' : (a : A) → E) a : E) (({ toFun := F, continuous_toFun := ⋯ } : (a : A) → E) a : E)

Tactic:
simpa using uniq _ _ (F'.comp γ) (Γ _ γ.source) γ.source γ.source (by simpa) (Γ_0 ..)
      (by simp [← Function.comp_assoc, hpF']) (Γ_lifts ..) rfl

Premises used: ContinuousMap.comp, toContinuousMap, Path.source, rfl
-- Module: Mathlib.Topology.Homotopy.Lifting
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
⊢ Eq (α := (↑I : Type) → X) (p ∘ (⇑(cov.liftPath γ e γ_0) : (a : (↑I : Type)) → E)) (⇑γ : (a : (↑I : Type)) → X)

Tactic:
(cov.exists_path_lifts γ e γ_0).choose_spec.1

Premises used: Exists.choose_spec, IsCoveringMap.exists_path_lifts, And.left
-- Module: Mathlib.Topology.Homotopy.Lifting
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
⊢ (cov.liftPath γ e γ_0 : (a : (↑I : Type)) → E) 0 = e

Tactic:
(cov.exists_path_lifts γ e γ_0).choose_spec.2

Premises used: Exists.choose_spec, IsCoveringMap.exists_path_lifts, And.right
-- Module: Mathlib.Topology.Homotopy.Lifting
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
Γ : (↑I : Type) → E
⊢ Γ = (⇑(cov.liftPath γ e γ_0) : (a : (↑I : Type)) → E) ↔
    Continuous[_, inst] Γ ∧ p ∘ Γ = (⇑γ : (a : (↑I : Type)) → X) ∧ Γ 0 = e

Tactic:
have lifts := cov.liftPath_lifts γ e γ_0
  have zero := cov.liftPath_zero γ e γ_0
  ⟨(· ▸ ⟨(cov.liftPath γ e γ_0).2, lifts, zero⟩), fun ⟨Γ_cont, Γ_lifts, Γ_0⟩ ↦ cov.eq_of_comp_eq
    Γ_cont (cov.liftPath γ e γ_0).continuous (Γ_lifts ▸ lifts.symm) 0 (Γ_0 ▸ zero.symm)⟩

Premises used: ContinuousMap.continuous, IsCoveringMap.liftPath_zero, Eq.rec, IsCoveringMap.liftPath, _private.0.IsCoveringMap.eq_liftPath_iff.match_1, ContinuousMap.continuous_toFun, And.intro, IsCoveringMap.liftPath_lifts, Iff.intro, OfNat.ofNat, Eq.symm, IsCoveringMap.eq_of_comp_eq, Eq, DFunLike.coe