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
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)
have 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)
Tactic: refine cov.isLocalHomeomorph.existsUnique_continuousMap_lifts f a₀ e₀ he (fun γ γ_0 ↦ ?_)
    fun γ γ' Γ Γ' γ_0 γ'_0 Γ_0 Γ'_0 Γ_lifts Γ'_lifts γγ'1 ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
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)
⊢ ∃! F : C(A, E), (F : (a : A) → E) a₀ = e₀ ∧ Eq (α := A → X) (p ∘ (⇑F : (a : A) → E)) (⇑f : (a : A) → X)
have 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)
Tactic: refine cov.isLocalHomeomorph.existsUnique_continuousMap_lifts f a₀ e₀ he (fun γ γ_0 ↦ ?_)
    fun γ γ' Γ Γ' γ_0 γ'_0 Γ_0 Γ'_0 Γ_lifts Γ'_lifts γγ'1 ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
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)
⊢ Eq (α := E) ((Γ : (a : (↑I : Type)) → E) 1 : E) ((Γ' : (a : (↑I : Type)) → E) 1 : E)
have refine_2 : Eq (α := E) ((cov.liftPath (f.comp γ) e₀ sorry : (a : (↑I : Type)) → E) 1 : E)
  ((cov.liftPath (f.comp γ') e₀ sorry : (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⟩]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
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' := ⋯ }
⊢ Eq (α := E) ((cov.liftPath (f.comp γ) e₀ ⋯ : (a : (↑I : Type)) → E) 1 : E)
    ((cov.liftPath (f.comp γ') e₀ ⋯ : (a : (↑I : Type)) → E) 1 : E)
have refine_2 : (↑(cov.monodromy (Path.Homotopic.Quotient.mk (pγ.map sorry))
        (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 sorry))
        (Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' singleton (α := X) ((f : (a : A) → X) a₀ : X)) e₀ he)) :
    E)
Tactic: change (cov.monodromy (.mk <| pγ.map f.continuous) ⟨e₀, he⟩).1 =
    (cov.monodromy (.mk <| pγ'.map f.continuous) ⟨e₀, he⟩).1
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
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' := ⋯ }
⊢ (↑(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)
have refine_2 : cov.monodromy (Path.Homotopic.Quotient.mk (pγ.map sorry))
    (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 sorry))
    (Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' singleton (α := X) ((f : (a : A) → X) a₀ : X)) e₀ he)
Tactic: rw [← Subtype.ext_iff]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
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' := ⋯ }
⊢ 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)
have refine_2 : cov.monodromy (Path.Homotopic.Quotient.mk (pγ'.map sorry).symm)
    (cov.monodromy (Path.Homotopic.Quotient.mk (pγ.map sorry))
      (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 sorry).symm)
    (cov.monodromy (Path.Homotopic.Quotient.mk (pγ'.map sorry))
      (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
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
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' := ⋯ }
⊢ 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))
have refine_2 : cov.monodromy (Path.Homotopic.Quotient.mk ((pγ.map sorry).trans (pγ'.map sorry).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 sorry).trans (pγ'.map sorry).symm))
    (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]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
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' := ⋯ }
| 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)
have rw : id (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]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
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' := ⋯ }
⊢ 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)
have refine_2 : cov.monodromy (Path.Homotopic.Quotient.mk ((pγ.map sorry).trans (pγ'.map sorry).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: conv_rhs => rw [← eq.2 ⟨.reflTransSymm _⟩, mk_refl, monodromy_refl]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
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' := ⋯ }
⊢ 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)
have refine_2 : cov.monodromy (Path.Homotopic.Quotient.mk ((pγ.trans pγ'.symm).map sorry))
    (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]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
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
⊢ cov.monodromy (Path.Homotopic.Quotient.mk (pγγ'.map ⋯))
      (Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' singleton (α := X) ((f : (a : A) → X) a₀ : X)) e₀ he) =
    id (Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' singleton (α := X) ((f : (a : A) → X) a₀ : X)) e₀ he)
have refine_2 : ∀ (pΓΓ' : FundamentalGroup E e₀)
  (eq :
    Eq.{u_2 + 1} (α := FundamentalGroup X ((f : (a : A) → X) a₀ : X))
      ((mapOfEq { toFun := p, continuous_toFun := sorry : 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 sorry))
      (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⟩
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
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))
⊢ cov.monodromy (Path.Homotopic.Quotient.mk (pγγ'.map ⋯))
      (Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' singleton (α := X) ((f : (a : A) → X) a₀ : X)) e₀ he) =
    id (Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' singleton (α := X) ((f : (a : A) → X) a₀ : X)) e₀ he)
have 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 := sorry : 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 sorry))
      (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ΓΓ'
Cleared hypotheses: pΓΓ', eq