awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
inst_3 : PathConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ : C(E, X) } he).range
γ γ' : C((↑I : Type), A)
Γ Γ' : C((↑I : Type), E)
γ_0 : (γ : (a : (↑I : Type)) → A) 0 = a₀
γ'_0 : (γ' : (a : (↑I : Type)) → A) 0 = a₀
Γ_0 : (Γ : (a : (↑I : Type)) → E) 0 = e₀
Γ'_0 : (Γ' : (a : (↑I : Type)) → E) 0 = e₀
Γ_lifts : Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
Γ'_lifts : Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ' : (a : (↑I : Type)) → E)) (⇑(f.comp γ') : (a : (↑I : Type)) → X)
γγ'1 : Eq (α := A) ((γ : (a : (↑I : Type)) → A) 1 : A) ((γ' : (a : (↑I : Type)) → A) 1 : A)
pγ : Path a₀ ((γ : (a : (↑I : Type)) → A) 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ ((γ : (a : (↑I : Type)) → A) 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
refine_2 :
  (↑(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)) :
      E) =
    (↑(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)) :
      E)
⊢ Eq (α := E) ((cov.liftPath (f.comp γ) e₀ ⋯ : (a : (↑I : Type)) → E) 1 : E)
    ((cov.liftPath (f.comp γ') e₀ ⋯ : (a : (↑I : Type)) → E) 1 : E)

Tactic:
change (cov.monodromy (.mk <| pγ.map f.continuous) ⟨e₀, he⟩).1 =
    (cov.monodromy (.mk <| pγ'.map f.continuous) ⟨e₀, he⟩).1

Premises used: ContinuousMap.continuous, Path.map, IsCoveringMap.monodromy, Subtype.mk, Subtype.val, Path.Homotopic.Quotient.mk
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
inst_3 : PathConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ : C(E, X) } he).range
γ γ' : C((↑I : Type), A)
Γ Γ' : C((↑I : Type), E)
γ_0 : (γ : (a : (↑I : Type)) → A) 0 = a₀
γ'_0 : (γ' : (a : (↑I : Type)) → A) 0 = a₀
Γ_0 : (Γ : (a : (↑I : Type)) → E) 0 = e₀
Γ'_0 : (Γ' : (a : (↑I : Type)) → E) 0 = e₀
Γ_lifts : Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
Γ'_lifts : Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ' : (a : (↑I : Type)) → E)) (⇑(f.comp γ') : (a : (↑I : Type)) → X)
γγ'1 : Eq (α := A) ((γ : (a : (↑I : Type)) → A) 1 : A) ((γ' : (a : (↑I : Type)) → A) 1 : A)
pγ : Path a₀ ((γ : (a : (↑I : Type)) → A) 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ ((γ : (a : (↑I : Type)) → A) 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
refine_2 :
  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) =
    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)
⊢ (↑(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)) :
      E) =
    (↑(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)) :
      E)

Tactic:
rw [← Subtype.ext_iff]

Premises used: Subtype.ext_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 : 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' := ⋯ }
refine_2 :
  cov.monodromy (Path.Homotopic.Quotient.mk (pγ'.map ⋯).symm)
      (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)) =
    cov.monodromy (Path.Homotopic.Quotient.mk (pγ'.map ⋯).symm)
      (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))
⊢ 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) =
    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)

Tactic:
apply (cov.monodromy_bijective <| .mk (pγ'.map f.continuous).symm).1

Premises used: ContinuousMap.continuous, Path.map, Path.symm, And.left, IsCoveringMap.monodromy_bijective, Path.Homotopic.Quotient.mk
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
inst_3 : PathConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ : C(E, X) } he).range
γ γ' : C((↑I : Type), A)
Γ Γ' : C((↑I : Type), E)
γ_0 : (γ : (a : (↑I : Type)) → A) 0 = a₀
γ'_0 : (γ' : (a : (↑I : Type)) → A) 0 = a₀
Γ_0 : (Γ : (a : (↑I : Type)) → E) 0 = e₀
Γ'_0 : (Γ' : (a : (↑I : Type)) → E) 0 = e₀
Γ_lifts : Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
Γ'_lifts : Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ' : (a : (↑I : Type)) → E)) (⇑(f.comp γ') : (a : (↑I : Type)) → X)
γγ'1 : Eq (α := A) ((γ : (a : (↑I : Type)) → A) 1 : A) ((γ' : (a : (↑I : Type)) → A) 1 : A)
pγ : Path a₀ ((γ : (a : (↑I : Type)) → A) 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ ((γ : (a : (↑I : Type)) → A) 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
refine_2 :
  cov.monodromy (Path.Homotopic.Quotient.mk ((pγ.map ⋯).trans (pγ'.map ⋯).symm))
      (Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' singleton (α := X) ((f : (a : A) → X) a₀ : X)) e₀ he) =
    cov.monodromy (Path.Homotopic.Quotient.mk ((pγ'.map ⋯).trans (pγ'.map ⋯).symm))
      (Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' singleton (α := X) ((f : (a : A) → X) a₀ : X)) e₀ he)
⊢ cov.monodromy (Path.Homotopic.Quotient.mk (pγ'.map ⋯).symm)
      (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)) =
    cov.monodromy (Path.Homotopic.Quotient.mk (pγ'.map ⋯).symm)
      (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))

Tactic:
simp_rw [← monodromy_trans_apply, ← mk_trans]

Premises used: IsCoveringMap.monodromy_trans_apply, Path.Homotopic.Quotient.mk_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 : 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' := ⋯ }
rw : id (Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' singleton (α := X) ((f : (a : A) → X) a₀ : X)) e₀ he)
| cov.monodromy (Path.Homotopic.Quotient.mk ((pγ'.map ⋯).trans (pγ'.map ⋯).symm))
    (Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' singleton (α := X) ((f : (a : A) → X) a₀ : X)) e₀ he)

Tactic:
rw [← eq.2 ⟨.reflTransSymm _⟩, mk_refl, monodromy_refl]

Premises used: Iff.mpr, Path.Homotopy.reflTransSymm, IsCoveringMap.monodromy_refl, Nonempty.intro, Path.Homotopic.Quotient.eq, Path.Homotopic.Quotient.mk_refl
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
inst_3 : PathConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ : C(E, X) } he).range
γ γ' : C((↑I : Type), A)
Γ Γ' : C((↑I : Type), E)
γ_0 : (γ : (a : (↑I : Type)) → A) 0 = a₀
γ'_0 : (γ' : (a : (↑I : Type)) → A) 0 = a₀
Γ_0 : (Γ : (a : (↑I : Type)) → E) 0 = e₀
Γ'_0 : (Γ' : (a : (↑I : Type)) → E) 0 = e₀
Γ_lifts : Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
Γ'_lifts : Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ' : (a : (↑I : Type)) → E)) (⇑(f.comp γ') : (a : (↑I : Type)) → X)
γγ'1 : Eq (α := A) ((γ : (a : (↑I : Type)) → A) 1 : A) ((γ' : (a : (↑I : Type)) → A) 1 : A)
pγ : Path a₀ ((γ : (a : (↑I : Type)) → A) 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ ((γ : (a : (↑I : Type)) → A) 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
refine_2 :
  cov.monodromy (Path.Homotopic.Quotient.mk ((pγ.map ⋯).trans (pγ'.map ⋯).symm))
      (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)
⊢ cov.monodromy (Path.Homotopic.Quotient.mk ((pγ.map ⋯).trans (pγ'.map ⋯).symm))
      (Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' singleton (α := X) ((f : (a : A) → X) a₀ : X)) e₀ he) =
    cov.monodromy (Path.Homotopic.Quotient.mk ((pγ'.map ⋯).trans (pγ'.map ⋯).symm))
      (Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' singleton (α := X) ((f : (a : A) → X) a₀ : X)) e₀ he)

Tactic:
conv_rhs => rw [← eq.2 ⟨.reflTransSymm _⟩, mk_refl, monodromy_refl]

Premises used: Iff.mpr, Path.Homotopy.reflTransSymm, IsCoveringMap.monodromy_refl, Nonempty.intro, Path.Homotopic.Quotient.eq, Path.Homotopic.Quotient.mk_refl
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
inst_3 : PathConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ : C(E, X) } he).range
γ γ' : C((↑I : Type), A)
Γ Γ' : C((↑I : Type), E)
γ_0 : (γ : (a : (↑I : Type)) → A) 0 = a₀
γ'_0 : (γ' : (a : (↑I : Type)) → A) 0 = a₀
Γ_0 : (Γ : (a : (↑I : Type)) → E) 0 = e₀
Γ'_0 : (Γ' : (a : (↑I : Type)) → E) 0 = e₀
Γ_lifts : Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
Γ'_lifts : Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ' : (a : (↑I : Type)) → E)) (⇑(f.comp γ') : (a : (↑I : Type)) → X)
γγ'1 : Eq (α := A) ((γ : (a : (↑I : Type)) → A) 1 : A) ((γ' : (a : (↑I : Type)) → A) 1 : A)
pγ : Path a₀ ((γ : (a : (↑I : Type)) → A) 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ ((γ : (a : (↑I : Type)) → A) 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
refine_2 :
  cov.monodromy (Path.Homotopic.Quotient.mk ((pγ.trans pγ'.symm).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)
⊢ cov.monodromy (Path.Homotopic.Quotient.mk ((pγ.map ⋯).trans (pγ'.map ⋯).symm))
      (Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' singleton (α := X) ((f : (a : A) → X) a₀ : X)) e₀ he) =
    id (Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' singleton (α := X) ((f : (a : A) → X) a₀ : X)) e₀ he)

Tactic:
rw [Path.map_symm, ← Path.map_trans]

Premises used: Path.map_trans, Path.map_symm
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
inst_3 : PathConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ : C(E, X) } he).range
γ γ' : C((↑I : Type), A)
Γ Γ' : C((↑I : Type), E)
γ_0 : (γ : (a : (↑I : Type)) → A) 0 = a₀
γ'_0 : (γ' : (a : (↑I : Type)) → A) 0 = a₀
Γ_0 : (Γ : (a : (↑I : Type)) → E) 0 = e₀
Γ'_0 : (Γ' : (a : (↑I : Type)) → E) 0 = e₀
Γ_lifts : Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
Γ'_lifts : Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ' : (a : (↑I : Type)) → E)) (⇑(f.comp γ') : (a : (↑I : Type)) → X)
γγ'1 : Eq (α := A) ((γ : (a : (↑I : Type)) → A) 1 : A) ((γ' : (a : (↑I : Type)) → A) 1 : A)
pγ : Path a₀ ((γ : (a : (↑I : Type)) → A) 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ ((γ : (a : (↑I : Type)) → A) 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
refine_2 :
  let pγγ' := pγ.trans pγ'.symm;
  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)
⊢ cov.monodromy (Path.Homotopic.Quotient.mk ((pγ.trans pγ'.symm).map ⋯))
      (Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' singleton (α := X) ((f : (a : A) → X) a₀ : X)) e₀ he) =
    id (Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' singleton (α := X) ((f : (a : A) → X) a₀ : X)) e₀ he)

Tactic:
set pγγ' : Path a₀ a₀ := pγ.trans pγ'.symm

Premises used: Path.symm, Path.trans, Path
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
inst_3 : PathConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ : C(E, X) } he).range
γ γ' : C((↑I : Type), A)
Γ Γ' : C((↑I : Type), E)
γ_0 : (γ : (a : (↑I : Type)) → A) 0 = a₀
γ'_0 : (γ' : (a : (↑I : Type)) → A) 0 = a₀
Γ_0 : (Γ : (a : (↑I : Type)) → E) 0 = e₀
Γ'_0 : (Γ' : (a : (↑I : Type)) → E) 0 = e₀
Γ_lifts : Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
Γ'_lifts : Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ' : (a : (↑I : Type)) → E)) (⇑(f.comp γ') : (a : (↑I : Type)) → X)
γγ'1 : Eq (α := A) ((γ : (a : (↑I : Type)) → A) 1 : A) ((γ' : (a : (↑I : Type)) → A) 1 : A)
pγ : Path a₀ ((γ : (a : (↑I : Type)) → A) 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ ((γ : (a : (↑I : Type)) → A) 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
pγγ' : Path a₀ a₀ := pγ.trans pγ'.symm
refine_2 :
  ∀ (pΓΓ' : FundamentalGroup E e₀)
    (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₀))
            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)
⊢ cov.monodromy (Path.Homotopic.Quotient.mk (pγγ'.map ⋯))
      (Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' singleton (α := X) ((f : (a : A) → X) a₀ : X)) e₀ he) =
    id (Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' singleton (α := X) ((f : (a : A) → X) a₀ : X)) e₀ he)

Tactic:
have ⟨pΓΓ', eq⟩ := le ⟨fromPath (.mk pγγ'), 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
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ΓΓ' : FundamentalGroup E e₀
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₀))
        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))
refine_2 :
  ∀ (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)
⊢ cov.monodromy (Path.Homotopic.Quotient.mk (pγγ'.map ⋯))
      (Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' singleton (α := X) ((f : (a : A) → X) a₀ : X)) e₀ he) =
    id (Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' singleton (α := X) ((f : (a : A) → X) a₀ : X)) e₀ he)

Tactic:
obtain ⟨pΓΓ', rfl⟩ := mk_surjective pΓΓ'

Premises used: rfl, Path.Homotopic.Quotient.mk_surjective
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
inst_3 : PathConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ : C(E, X) } he).range
γ γ' : C((↑I : Type), A)
Γ Γ' : C((↑I : Type), E)
γ_0 : (γ : (a : (↑I : Type)) → A) 0 = a₀
γ'_0 : (γ' : (a : (↑I : Type)) → A) 0 = a₀
Γ_0 : (Γ : (a : (↑I : Type)) → E) 0 = e₀
Γ'_0 : (Γ' : (a : (↑I : Type)) → E) 0 = e₀
Γ_lifts : Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
Γ'_lifts : Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ' : (a : (↑I : Type)) → E)) (⇑(f.comp γ') : (a : (↑I : Type)) → X)
γγ'1 : Eq (α := A) ((γ : (a : (↑I : Type)) → A) 1 : A) ((γ' : (a : (↑I : Type)) → A) 1 : A)
pγ : Path a₀ ((γ : (a : (↑I : Type)) → A) 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ ((γ : (a : (↑I : Type)) → A) 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
pγγ' : Path a₀ a₀ := pγ.trans pγ'.symm
pΓΓ' : Path { as := e₀ : FundamentalGroupoid E }.as { as := e₀ }.as
eq :
  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))
⊢ fromPath (Path.Homotopic.Quotient.mk ((pΓΓ'.map ⋯).cast ⋯ ⋯)) = Path.Homotopic.Quotient.mk (pγγ'.map ⋯)

Tactic:
rw [mapOfEq_apply, map_apply, ← mk_map] at eq

Premises used: FundamentalGroup.map_apply, Path.Homotopic.Quotient.mk_map, FundamentalGroup.mapOfEq_apply