awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
e₀ e₁ : E
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (β :=
    Path.Homotopic.Quotient (X := X) (({ toFun := p, continuous_toFun := ⋯ : C(E, X) } : (a : E) → X) e₀ : X)
      (({ toFun := p, continuous_toFun := ⋯ : C(E, X) } : (a : E) → X) e₁ : X))
    fun (γ : Path.Homotopic.Quotient e₀ e₁) ↦ γ.map { toFun := p, continuous_toFun := ⋯ }

Tactic:
Quotient.ind₂ fun γ₀ γ₁ ↦ ?_

Premises used: Quotient.ind₂, Path.Homotopic.Quotient, Function.Injective
-- 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
e₀ e₁ : E
refine :
  ∀ (γ₀ γ₁ : Path e₀ e₁),
    Eq.{u_2 + 1} (α :=
        Path.Homotopic.Quotient (X := X) (({ toFun := p, continuous_toFun := ⋯ : C(E, X) } : (a : E) → X) e₀ : X)
          (({ toFun := p, continuous_toFun := ⋯ : C(E, X) } : (a : E) → X) e₁ : X))
        ((fun (γ : Path.Homotopic.Quotient e₀ e₁) ↦ γ.map { toFun := p, continuous_toFun := ⋯ : C(E, X) }) ⟦γ₀⟧)
        ((fun (γ : Path.Homotopic.Quotient e₀ e₁) ↦ γ.map { toFun := p, continuous_toFun := ⋯ : C(E, X) }) ⟦γ₁⟧) →
      Eq (α := Path.Homotopic.Quotient e₀ e₁) ⟦γ₀⟧ ⟦γ₁⟧
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (β :=
    Path.Homotopic.Quotient (X := X) (({ toFun := p, continuous_toFun := ⋯ : C(E, X) } : (a : E) → X) e₀ : X)
      (({ toFun := p, continuous_toFun := ⋯ : C(E, X) } : (a : E) → X) e₁ : X))
    fun (γ : Path.Homotopic.Quotient e₀ e₁) ↦ γ.map { toFun := p, continuous_toFun := ⋯ }

Tactic:
refine Quotient.ind₂ fun γ₀ γ₁ ↦ ?_
-- 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
e₀ e₁ : E
γ₀ γ₁ : Path e₀ e₁
rw : (γ₀.map ⋯).Homotopic (γ₁.map ⋯) → Path.Homotopic.Quotient.mk γ₀ = Path.Homotopic.Quotient.mk γ₁
⊢ Path.Homotopic.Quotient.mk (γ₀.map ⋯) = Path.Homotopic.Quotient.mk (γ₁.map ⋯) →
    Path.Homotopic.Quotient.mk γ₀ = Path.Homotopic.Quotient.mk γ₁

Tactic:
rw [Path.Homotopic.Quotient.eq]

Premises used: Path.Homotopic.Quotient.eq
-- 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
e₀ e₁ : E
γ₀ γ₁ : Path e₀ e₁
rw : (γ₀.map ⋯).Homotopic (γ₁.map ⋯) → γ₀.Homotopic γ₁
⊢ (γ₀.map ⋯).Homotopic (γ₁.map ⋯) → Path.Homotopic.Quotient.mk γ₀ = Path.Homotopic.Quotient.mk γ₁

Tactic:
rw [Path.Homotopic.Quotient.eq]

Premises used: Path.Homotopic.Quotient.eq
-- 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
e₀ e₁ : E
γ₀ γ₁ : Path e₀ e₁
iterate : (γ₀.map ⋯).Homotopic (γ₁.map ⋯) → γ₀.Homotopic γ₁
⊢ Path.Homotopic.Quotient.mk (γ₀.map ⋯) = Path.Homotopic.Quotient.mk (γ₁.map ⋯) →
    Path.Homotopic.Quotient.mk γ₀ = Path.Homotopic.Quotient.mk γ₁

Tactic:
iterate 2 rw [Path.Homotopic.Quotient.eq]

Premises used: Path.Homotopic.Quotient.eq
-- 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
e₀ e₁ : E
γ₀ γ₁ : Path e₀ e₁
⊢ (γ₀.map ⋯).Homotopic (γ₁.map ⋯) → γ₀.Homotopic γ₁

Tactic:
(cov.homotopicRel_iff_comp ⟨0, .inl rfl, γ₀.source.trans γ₁.source.symm⟩).mpr

Premises used: Iff.mpr, ContinuousMap.HomotopicRel, ContinuousMap.comp, IsCoveringMap.homotopicRel_iff_comp, And.intro, Exists.intro, Path.source, Path.Homotopic, OfNat.ofNat, Eq.symm, Eq.trans
-- 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
e₀ e₁ : E
γ₀ γ₁ : Path e₀ e₁
⊢ (γ₀.map ⋯).Homotopic (γ₁.map ⋯) → γ₀.Homotopic γ₁

Tactic:
exact (cov.homotopicRel_iff_comp ⟨0, .inl rfl, γ₀.source.trans γ₁.source.symm⟩).mpr

Premises used: Iff.mpr, IsCoveringMap.homotopicRel_iff_comp, And.intro, Exists.intro, Path.source, OfNat.ofNat, Eq.symm, Eq.trans
-- 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 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
⊢ ∃! F : C(A, E), (F : (a : A) → E) a₀ = e₀ ∧ Eq (α := A → X) (p ∘ (⇑F : (a : A) → E)) (⇑f : (a : A) → X)

Tactic:
cov.isLocalHomeomorph.existsUnique_continuousMap_lifts f a₀ e₀ he (fun γ γ_0 ↦ ?_)
    fun γ γ' Γ Γ' γ_0 γ'_0 Γ_0 Γ'_0 Γ_lifts Γ'_lifts γγ'1 ↦ ?_

Premises used: IsLocalHomeomorph.existsUnique_continuousMap_lifts, IsCoveringMap.isLocalHomeomorph
-- 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 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
refine_1 :
  ∀ (γ : C((↑I : Type), A)) (γ_0 : (γ : (a : (↑I : Type)) → A) 0 = a₀),
    ∃ (Γ : C((↑I : Type), E)),
      (Γ : (a : (↑I : Type)) → E) 0 = e₀ ∧
        Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
refine_2 :
  ∀ (γ γ' : 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)),
    Eq (α := E) ((Γ : (a : (↑I : Type)) → E) 1 : E) ((Γ' : (a : (↑I : Type)) → E) 1 : E)
⊢ ∃! F : C(A, E), (F : (a : A) → E) a₀ = e₀ ∧ Eq (α := A → X) (p ∘ (⇑F : (a : A) → E)) (⇑f : (a : A) → X)

Tactic:
refine cov.isLocalHomeomorph.existsUnique_continuousMap_lifts f a₀ e₀ he (fun γ γ_0 ↦ ?_)
    fun γ γ' Γ Γ' γ_0 γ'_0 Γ_0 Γ'_0 Γ_lifts Γ'_lifts γγ'1 ↦ ?_

Premises used: IsLocalHomeomorph.existsUnique_continuousMap_lifts, IsCoveringMap.isLocalHomeomorph
-- 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 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
γ : C((↑I : Type), A)
γ_0 : (γ : (a : (↑I : Type)) → A) 0 = a₀
⊢ (f.comp γ : (a : (↑I : Type)) → X) 0 = p e₀

Tactic:
simp [γ_0, he]
-- 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 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
γ : C((↑I : Type), A)
γ_0 : (γ : (a : (↑I : Type)) → A) 0 = a₀
⊢ ∃ (Γ : C((↑I : Type), E)),
    (Γ : (a : (↑I : Type)) → E) 0 = e₀ ∧
      Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)

Tactic:
simpa [and_comm] using cov.exists_path_lifts (f.comp γ) e₀ (by simp [γ_0, he])

Premises used: ContinuousMap.comp, IsCoveringMap.exists_path_lifts, and_comm
-- 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 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
γ γ' : 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' := ⋯ }
⊢ (f.comp pγ.toContinuousMap : (a : (↑I : Type)) → X) 0 = p e₀

Tactic:
simp [he]
-- 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 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
γ γ' : 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' := ⋯ }
⊢ (f.comp pγ'.toContinuousMap : (a : (↑I : Type)) → X) 0 = p e₀

Tactic:
simp [he]
-- 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 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
γ γ' : 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' := ⋯ }
h : Γ = cov.liftPath (f.comp pγ.toContinuousMap) e₀ ⋯
h₁ : Γ' = cov.liftPath (f.comp pγ'.toContinuousMap) e₀ ⋯
⊢ Eq (α := E) ((Γ : (a : (↑I : Type)) → E) 1 : E) ((Γ' : (a : (↑I : Type)) → E) 1 : E)

Tactic:
convert!
    cov.liftPath_apply_one_eq_of_homotopicRel
      (ContinuousMap.HomotopicRel.comp_continuousMap (SimplyConnectedSpace.paths_homotopic pγ pγ')
        f)
      e₀ (by simp [he]) (by simp [he])

Premises used: IsCoveringMap.liftPath_apply_one_eq_of_homotopicRel, ContinuousMap.HomotopicRel.comp_continuousMap, SimplyConnectedSpace.paths_homotopic
-- 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 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
γ γ' : 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' := ⋯ }
h :
  Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp pγ.toContinuousMap) : (a : (↑I : Type)) → X) ∧
    (Γ : (a : (↑I : Type)) → E) 0 = e₀
⊢ Γ = cov.liftPath (f.comp pγ.toContinuousMap) e₀ ⋯

Tactic:
rw [eq_liftPath_iff']

Premises used: IsCoveringMap.eq_liftPath_iff'
-- 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 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
γ γ' : 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' := ⋯ }
⊢ Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp pγ.toContinuousMap) : (a : (↑I : Type)) → X) ∧
    (Γ : (a : (↑I : Type)) → E) 0 = e₀

Tactic:
⟨Γ_lifts, Γ_0⟩

Premises used: And.intro
-- 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 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
γ γ' : 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' := ⋯ }
⊢ Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ' : (a : (↑I : Type)) → E))
      (⇑(f.comp pγ'.toContinuousMap) : (a : (↑I : Type)) → X) ∧
    (Γ' : (a : (↑I : Type)) → E) 0 = e₀

Tactic:
⟨Γ'_lifts, Γ'_0⟩

Premises used: And.intro
-- 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 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
γ γ' : 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' := ⋯ }
⊢ Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp pγ.toContinuousMap) : (a : (↑I : Type)) → X) ∧
    (Γ : (a : (↑I : Type)) → E) 0 = e₀

Tactic:
exacts [⟨Γ_lifts, Γ_0⟩, ⟨Γ'_lifts, Γ'_0⟩]
-- 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
⊢ ∃! F : C(A, E), (F : (a : A) → E) a₀ = e₀ ∧ Eq (α := A → X) (p ∘ (⇑F : (a : A) → E)) (⇑f : (a : A) → X)

Tactic:
cov.isLocalHomeomorph.existsUnique_continuousMap_lifts f a₀ e₀ he (fun γ γ_0 ↦ ?_)
    fun γ γ' Γ Γ' γ_0 γ'_0 Γ_0 Γ'_0 Γ_lifts Γ'_lifts γγ'1 ↦ ?_

Premises used: IsLocalHomeomorph.existsUnique_continuousMap_lifts, IsCoveringMap.isLocalHomeomorph
-- 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
refine_1 :
  ∀ (γ : C((↑I : Type), A)) (γ_0 : (γ : (a : (↑I : Type)) → A) 0 = a₀),
    ∃ (Γ : C((↑I : Type), E)),
      (Γ : (a : (↑I : Type)) → E) 0 = e₀ ∧
        Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
refine_2 :
  ∀ (γ γ' : 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)),
    Eq (α := E) ((Γ : (a : (↑I : Type)) → E) 1 : E) ((Γ' : (a : (↑I : Type)) → E) 1 : E)
⊢ ∃! F : C(A, E), (F : (a : A) → E) a₀ = e₀ ∧ Eq (α := A → X) (p ∘ (⇑F : (a : A) → E)) (⇑f : (a : A) → X)

Tactic:
refine cov.isLocalHomeomorph.existsUnique_continuousMap_lifts f a₀ e₀ he (fun γ γ_0 ↦ ?_)
    fun γ γ' Γ Γ' γ_0 γ'_0 Γ_0 Γ'_0 Γ_lifts Γ'_lifts γγ'1 ↦ ?_

Premises used: IsLocalHomeomorph.existsUnique_continuousMap_lifts, IsCoveringMap.isLocalHomeomorph
-- 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)
γ_0 : (γ : (a : (↑I : Type)) → A) 0 = a₀
⊢ (f.comp γ : (a : (↑I : Type)) → X) 0 = p e₀

Tactic:
simp [γ_0, he]
-- 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)
γ_0 : (γ : (a : (↑I : Type)) → A) 0 = a₀
⊢ ∃ (Γ : C((↑I : Type), E)),
    (Γ : (a : (↑I : Type)) → E) 0 = e₀ ∧
      Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)

Tactic:
simpa [and_comm] using cov.exists_path_lifts (f.comp γ) e₀ (by simp [γ_0, he])

Premises used: ContinuousMap.comp, IsCoveringMap.exists_path_lifts, and_comm
-- 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)
⊢ (f.comp γ : (a : (↑I : Type)) → X) 0 = p e₀

Tactic:
simp [γ_0, he]
-- 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)
⊢ (f.comp γ' : (a : (↑I : Type)) → X) 0 = p e₀

Tactic:
simp [γ'_0, he]
-- 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)
refine_2 :
  Eq (α := E) ((cov.liftPath (f.comp γ) e₀ ⋯ : (a : (↑I : Type)) → E) 1 : E)
    ((cov.liftPath (f.comp γ') e₀ ⋯ : (a : (↑I : Type)) → E) 1 : E)
⊢ Eq (α := E) ((Γ : (a : (↑I : Type)) → E) 1 : E) ((Γ' : (a : (↑I : Type)) → E) 1 : E)

Tactic:
rw [(cov.eq_liftPath_iff' <| by simp [γ_0, he]).mpr ⟨Γ_lifts, Γ_0⟩,
    (cov.eq_liftPath_iff' <| by simp [γ'_0, he]).mpr ⟨Γ'_lifts, Γ'_0⟩]

Premises used: Iff.mpr, IsCoveringMap.eq_liftPath_iff', And.intro