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
H : ContinuousMap.{u_3, u_2} ((↑I : Type) × A) X
f : C(A, E)
H_0 : ∀ (a : A), (H : (a : (↑I : Type) × A) → X) (0, a) = p ((f : (a : A) → E) a)
f₀ f₁ : C(A, X)
S : Set A
F : f₀.HomotopyRel f₁ S
inst_3 : PreconnectedSpace A
f₀' f₁' : C(A, E)
he : ∃ a ∈ S, Eq.{u_1 + 1} (α := E) ((f₀' : (a : A) → E) a : E) ((f₁' : (a : A) → E) a : E)
h₀ : Eq (α := A → X) (p ∘ (⇑f₀' : (a : A) → E)) (⇑f₀ : (a : A) → X)
h₁ : Eq (α := A → X) (p ∘ (⇑f₁' : (a : A) → E)) (⇑f₁ : (a : A) → X)
F_0 : ∀ (a : A), (F : (a : (↑I : Type) × A) → X) (0, a) = p ((f₀' : (a : A) → E) a)
rel :
  ∀ (t : (↑I : Type)),
    ∀ a ∈ S,
      Eq.{u_1 + 1} (α := E)
        ((cov.liftHomotopy (↑F : C((↑I : Type) × A, X)) f₀' F_0 : (a : (↑I : Type) × A) → E) (t, a) : E)
        ((f₀' : (a : A) → E) a : E)
⊢ ∀ (x : A), (cov.liftHomotopy (↑F : C((↑I : Type) × A, X)) f₀' F_0).toFun (1, x) = (f₁' : (a : A) → E) x
have obtain : ∀ (a : A) (ha : a ∈ S) (he : Eq.{u_1 + 1} (α := E) ((f₀' : (a : A) → E) a : E) ((f₁' : (a : A) → E) a : E)) (x : A),
  (cov.liftHomotopy (↑F : C((↑I : Type) × A, X)) f₀' F_0).toFun (1, x) = (f₁' : (a : A) → E) x
Tactic: obtain ⟨a, ha, he⟩ := he
Cleared hypotheses: he
-- 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
H : ContinuousMap.{u_3, u_2} ((↑I : Type) × A) X
f : C(A, E)
H_0 : ∀ (a : A), (H : (a : (↑I : Type) × A) → X) (0, a) = p ((f : (a : A) → E) a)
f₀ f₁ : C(A, X)
S : Set A
F : f₀.HomotopyRel f₁ S
inst_3 : PreconnectedSpace A
f₀' f₁' : C(A, E)
h₀ : Eq (α := A → X) (p ∘ (⇑f₀' : (a : A) → E)) (⇑f₀ : (a : A) → X)
h₁ : Eq (α := A → X) (p ∘ (⇑f₁' : (a : A) → E)) (⇑f₁ : (a : A) → X)
F_0 : ∀ (a : A), (F : (a : (↑I : Type) × A) → X) (0, a) = p ((f₀' : (a : A) → E) a)
rel :
  ∀ (t : (↑I : Type)),
    ∀ a ∈ S,
      Eq.{u_1 + 1} (α := E)
        ((cov.liftHomotopy (↑F : C((↑I : Type) × A, X)) f₀' F_0 : (a : (↑I : Type) × A) → E) (t, a) : E)
        ((f₀' : (a : A) → E) a : E)
a : A
ha : a ∈ S
he : Eq.{u_1 + 1} (α := E) ((f₀' : (a : A) → E) a : E) ((f₁' : (a : A) → E) a : E)
⊢ ∀ (x : A), (cov.liftHomotopy (↑F : C((↑I : Type) × A, X)) f₀' F_0).toFun (1, x) = (f₁' : (a : A) → E) x
have simp_rw : ∀ (x : A),
  Eq.{u_1 + 1} (α := E)
    (((((cov.liftHomotopy (↑F : C((↑I : Type) × A, X)) f₀' F_0).curry : (a : (↑I : Type)) → C(A, E)) 1 : C(A, E)) :
          (a : A) → E)
        x :
      E)
    ((f₁' : (a : A) → E) x : E)
Tactic: simp_rw [toFun_eq_coe, ← curry_apply]
-- 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
H : ContinuousMap.{u_3, u_2} ((↑I : Type) × A) X
f : C(A, E)
H_0 : ∀ (a : A), (H : (a : (↑I : Type) × A) → X) (0, a) = p ((f : (a : A) → E) a)
f₀ f₁ : C(A, X)
S : Set A
F : f₀.HomotopyRel f₁ S
inst_3 : PreconnectedSpace A
f₀' f₁' : C(A, E)
h₀ : Eq (α := A → X) (p ∘ (⇑f₀' : (a : A) → E)) (⇑f₀ : (a : A) → X)
h₁ : Eq (α := A → X) (p ∘ (⇑f₁' : (a : A) → E)) (⇑f₁ : (a : A) → X)
F_0 : ∀ (a : A), (F : (a : (↑I : Type) × A) → X) (0, a) = p ((f₀' : (a : A) → E) a)
rel :
  ∀ (t : (↑I : Type)),
    ∀ a ∈ S,
      Eq.{u_1 + 1} (α := E)
        ((cov.liftHomotopy (↑F : C((↑I : Type) × A, X)) f₀' F_0 : (a : (↑I : Type) × A) → E) (t, a) : E)
        ((f₀' : (a : A) → E) a : E)
a : A
ha : a ∈ S
he : Eq.{u_1 + 1} (α := E) ((f₀' : (a : A) → E) a : E) ((f₁' : (a : A) → E) a : E)
⊢ ∀ (x : A),
    Eq.{u_1 + 1} (α := E)
      (((((cov.liftHomotopy (↑F : C((↑I : Type) × A, X)) f₀' F_0).curry : (a : (↑I : Type)) → C(A, E)) 1 : C(A, E)) :
            (a : A) → E)
          x :
        E)
      ((f₁' : (a : A) → E) x : E)
have refine : Eq (α := A → X)
  (p ∘
    (⇑(((cov.liftHomotopy (↑F : C((↑I : Type) × A, X)) f₀' F_0).curry : (a : (↑I : Type)) → C(A, E)) 1 : C(A, E)) :
      (a : A) → E))
  (p ∘ (⇑f₁' : (a : A) → E))
Tactic: refine congr_fun (cov.eq_of_comp_eq
        (ContinuousMap.continuous _) f₁'.continuous ?_ a <| (rel 1 a ha).trans he)
-- 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
H : ContinuousMap.{u_3, u_2} ((↑I : Type) × A) X
f : C(A, E)
H_0 : ∀ (a : A), (H : (a : (↑I : Type) × A) → X) (0, a) = p ((f : (a : A) → E) a)
f₀ f₁ : C(A, X)
S : Set A
F : f₀.HomotopyRel f₁ S
inst_3 : PreconnectedSpace A
f₀' f₁' : C(A, E)
h₀ : Eq (α := A → X) (p ∘ (⇑f₀' : (a : A) → E)) (⇑f₀ : (a : A) → X)
h₁ : Eq (α := A → X) (p ∘ (⇑f₁' : (a : A) → E)) (⇑f₁ : (a : A) → X)
F_0 : ∀ (a : A), (F : (a : (↑I : Type) × A) → X) (0, a) = p ((f₀' : (a : A) → E) a)
rel :
  ∀ (t : (↑I : Type)),
    ∀ a ∈ S,
      Eq.{u_1 + 1} (α := E)
        ((cov.liftHomotopy (↑F : C((↑I : Type) × A, X)) f₀' F_0 : (a : (↑I : Type) × A) → E) (t, a) : E)
        ((f₀' : (a : A) → E) a : E)
a : A
ha : a ∈ S
he : Eq.{u_1 + 1} (α := E) ((f₀' : (a : A) → E) a : E) ((f₁' : (a : A) → E) a : E)
⊢ Eq (α := A → X)
    (p ∘
      (⇑(((cov.liftHomotopy (↑F : C((↑I : Type) × A, X)) f₀' F_0).curry : (a : (↑I : Type)) → C(A, E)) 1 : C(A, E)) :
        (a : A) → E))
    (p ∘ (⇑f₁' : (a : A) → E))
have h : ∀ (a : A),
  (p ∘
        (⇑(((cov.liftHomotopy (↑F : C((↑I : Type) × A, X)) f₀' F_0).curry : (a : (↑I : Type)) → C(A, E)) 1 : C(A, E)) :
          (a : A) → E))
      a =
    (p ∘ (⇑f₁' : (a : A) → E)) a
Tactic: ext a
-- 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
H : ContinuousMap.{u_3, u_2} ((↑I : Type) × A) X
f : C(A, E)
H_0 : ∀ (a : A), (H : (a : (↑I : Type) × A) → X) (0, a) = p ((f : (a : A) → E) a)
f₀ f₁ : C(A, X)
S : Set A
F : f₀.HomotopyRel f₁ S
inst_3 : PreconnectedSpace A
f₀' f₁' : C(A, E)
h₀ : Eq (α := A → X) (p ∘ (⇑f₀' : (a : A) → E)) (⇑f₀ : (a : A) → X)
h₁ : Eq (α := A → X) (p ∘ (⇑f₁' : (a : A) → E)) (⇑f₁ : (a : A) → X)
F_0 : ∀ (a : A), (F : (a : (↑I : Type) × A) → X) (0, a) = p ((f₀' : (a : A) → E) a)
rel :
  ∀ (t : (↑I : Type)),
    ∀ a ∈ S,
      Eq.{u_1 + 1} (α := E)
        ((cov.liftHomotopy (↑F : C((↑I : Type) × A, X)) f₀' F_0 : (a : (↑I : Type) × A) → E) (t, a) : E)
        ((f₀' : (a : A) → E) a : E)
a_1 : A
ha : a_1 ∈ S
he : Eq.{u_1 + 1} (α := E) ((f₀' : (a : A) → E) a_1 : E) ((f₁' : (a : A) → E) a_1 : E)
a : A
⊢ (p ∘
        (⇑(((cov.liftHomotopy (↑F : C((↑I : Type) × A, X)) f₀' F_0).curry : (a : (↑I : Type)) → C(A, E)) 1 : C(A, E)) :
          (a : A) → E))
      a =
    (p ∘ (⇑f₁' : (a : A) → E)) a
have h : p ((cov.liftHomotopy (↑F : C((↑I : Type) × A, X)) f₀' F_0 : (a : (↑I : Type) × A) → E) (1, a)) = (f₁ : (a : A) → X) a
Tactic: rw [h₁, Function.comp_apply, curry_apply]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ₀ γ₁ : C((↑I : Type), X)
h : γ₀.HomotopicRel γ₁ {0, 1}
e : E
h₀ : (γ₀ : (a : (↑I : Type)) → X) 0 = p e
h₁ : (γ₁ : (a : (↑I : Type)) → X) 0 = p e
⊢ Eq (α := E) ((cov.liftPath γ₀ e h₀ : (a : (↑I : Type)) → E) 1 : E)
    ((cov.liftPath γ₁ e h₁ : (a : (↑I : Type)) → E) 1 : E)
have obtain : ∀ (H : γ₀.HomotopyRel γ₁ {0, 1}),
  Eq (α := E) ((cov.liftPath γ₀ e h₀ : (a : (↑I : Type)) → E) 1 : E)
    ((cov.liftPath γ₁ e h₁ : (a : (↑I : Type)) → E) 1 : E)
Tactic: obtain ⟨H⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ₀ γ₁ : C((↑I : Type), X)
e : E
h₀ : (γ₀ : (a : (↑I : Type)) → X) 0 = p e
h₁ : (γ₁ : (a : (↑I : Type)) → X) 0 = p e
H : γ₀.HomotopyRel γ₁ {0, 1}
⊢ Eq (α := E) ((cov.liftPath γ₀ e h₀ : (a : (↑I : Type)) → E) 1 : E)
    ((cov.liftPath γ₁ e h₁ : (a : (↑I : Type)) → E) 1 : E)
have have : ∀ (this : (cov.liftPath γ₀ e h₀).HomotopyRel (cov.liftPath γ₁ e h₁) {0, 1}),
  Eq (α := E) ((cov.liftPath γ₀ e h₀ : (a : (↑I : Type)) → E) 1 : E)
    ((cov.liftPath γ₁ e h₁ : (a : (↑I : Type)) → E) 1 : E)
Tactic: have := cov.liftHomotopyRel (f₀' := cov.liftPath γ₀ e h₀) (f₁' := cov.liftPath γ₁ e h₁) H
    ⟨0, .inl rfl, by simp_rw [liftPath_zero]⟩ (liftPath_lifts ..) (liftPath_lifts ..)
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ₀ γ₁ : C((↑I : Type), X)
e : E
h₀ : (γ₀ : (a : (↑I : Type)) → X) 0 = p e
h₁ : (γ₁ : (a : (↑I : Type)) → X) 0 = p e
H : γ₀.HomotopyRel γ₁ {0, 1}
this : (cov.liftPath γ₀ e h₀).HomotopyRel (cov.liftPath γ₁ e h₁) {0, 1}
⊢ Eq (α := E) ((cov.liftPath γ₀ e h₀ : (a : (↑I : Type)) → E) 1 : E)
    ((cov.liftPath γ₁ e h₁ : (a : (↑I : Type)) → E) 1 : E)
have rw : Eq (α := E) ((this : (a : (↑I : Type) × (↑I : Type)) → E) (0, 1) : E)
  ((cov.liftPath γ₁ e h₁ : (a : (↑I : Type)) → E) 1 : E)
Tactic: rw [← this.eq_fst 0 (.inr rfl), ← this.eq_snd 0 (.inr rfl)]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ₀ γ₁ : C((↑I : Type), X)
e : E
h₀ : (γ₀ : (a : (↑I : Type)) → X) 0 = p e
h₁ : (γ₁ : (a : (↑I : Type)) → X) 0 = p e
H : γ₀.HomotopyRel γ₁ {0, 1}
this : (cov.liftPath γ₀ e h₀).HomotopyRel (cov.liftPath γ₁ e h₁) {0, 1}
rw :
  Eq (α := E) ((this : (a : (↑I : Type) × (↑I : Type)) → E) (0, 1) : E)
    ((cov.liftPath γ₁ e h₁ : (a : (↑I : Type)) → E) 1 : E)
⊢ Eq (α := E) ((cov.liftPath γ₀ e h₀ : (a : (↑I : Type)) → E) 1 : E)
    ((cov.liftPath γ₁ e h₁ : (a : (↑I : Type)) → E) 1 : E)
have rw₁ : Eq (α := E) ((this : (a : (↑I : Type) × (↑I : Type)) → E) (0, 1) : E)
  ((this : (a : (↑I : Type) × (↑I : Type)) → E) (0, 1) : E)
Tactic: rw [← this.eq_fst 0 (.inr rfl), ← this.eq_snd 0 (.inr rfl)]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
x y : E
γ : Path.Homotopic.Quotient x y
⊢ (↑(cov.monodromy (γ.map { toFun := p, continuous_toFun := ⋯ : C(E, X) })
          (Subtype.mk (p := fun (x_1 : E) ↦
            x_1 ∈ p ⁻¹' singleton (α := X) (({ toFun := p, continuous_toFun := ⋯ : C(E, X) } : (a : E) → X) x : X)) x
            ⋯)) :
      E) =
    (↑(Subtype.mk (p := fun (x : E) ↦
          x ∈ p ⁻¹' singleton (α := X) (({ toFun := p, continuous_toFun := ⋯ : C(E, X) } : (a : E) → X) y : X)) y ⋯) :
      E)
have mk : ∀ (γ : Path x y),
  (↑(cov.monodromy
          (Path.Homotopic.Quotient.map (Quot.mk (⇑(Path.Homotopic.setoid x y) : Path x y → Path x y → Prop) γ)
            { toFun := p, continuous_toFun := sorry : C(E, X) })
          (Subtype.mk (p := fun (x_1 : E) ↦
            x_1 ∈ p ⁻¹' singleton (α := X) (({ toFun := p, continuous_toFun := sorry : C(E, X) } : (a : E) → X) x : X)) x
            sorry)) :
      E) =
    (↑(Subtype.mk (p := fun (x : E) ↦
          x ∈ p ⁻¹' singleton (α := X) (({ toFun := p, continuous_toFun := sorry : C(E, X) } : (a : E) → X) y : X)) y sorry) :
      E)
Tactic: obtain ⟨γ⟩ := γ
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
x y z : X
γ : Path.Homotopic.Quotient x y
γ' : Path.Homotopic.Quotient y z
e : (↑(p ⁻¹' {x}) : Type u_1)
⊢ cov.monodromy (γ.trans γ') e = cov.monodromy γ' (cov.monodromy γ e)
have mk : ∀ (γ : Path x y),
  cov.monodromy
      (Path.Homotopic.Quotient.trans (Quot.mk (⇑(Path.Homotopic.setoid x y) : Path x y → Path x y → Prop) γ) γ') e =
    cov.monodromy γ' (cov.monodromy (Quot.mk (⇑(Path.Homotopic.setoid x y) : Path x y → Path x y → Prop) γ) e)
Tactic: obtain ⟨γ⟩ := γ
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
x y z : X
γ_1 : Path.Homotopic.Quotient x y
γ' : Path.Homotopic.Quotient y z
e : (↑(p ⁻¹' {x}) : Type u_1)
γ : Path x y
⊢ cov.monodromy
      (Path.Homotopic.Quotient.trans (Quot.mk (⇑(Path.Homotopic.setoid x y) : Path x y → Path x y → Prop) γ) γ') e =
    cov.monodromy γ' (cov.monodromy (Quot.mk (⇑(Path.Homotopic.setoid x y) : Path x y → Path x y → Prop) γ) e)
have mk : ∀ (γ' : Path y z),
  cov.monodromy
      (Path.Homotopic.Quotient.trans (Quot.mk (⇑(Path.Homotopic.setoid x y) : Path x y → Path x y → Prop) γ)
        (Quot.mk (⇑(Path.Homotopic.setoid y z) : Path y z → Path y z → Prop) γ'))
      e =
    cov.monodromy (Quot.mk (⇑(Path.Homotopic.setoid y z) : Path y z → Path y z → Prop) γ')
      (cov.monodromy (Quot.mk (⇑(Path.Homotopic.setoid x y) : Path x y → Path x y → Prop) γ) e)
Tactic: obtain ⟨γ'⟩ := γ'
-- 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
H : ContinuousMap.{u_3, u_2} ((↑I : Type) × A) X
f : C(A, E)
H_0 : ∀ (a : A), (H : (a : (↑I : Type) × A) → X) (0, a) = p ((f : (a : A) → E) a)
f₀ f₁ : C(A, X)
S : Set A
F : f₀.HomotopyRel f₁ S
x : FundamentalGroupoid X
⊢ ↾cov.monodromy (𝟙 x) = 𝟙 (↑(p ⁻¹' {x.as}) : Type u_1)
have h : ∀ (x_1 : (↑(p ⁻¹' {x.as}) : Type u_1)),
  TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (↾cov.monodromy (𝟙 x))) x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (↑(p ⁻¹' {x.as}) : Type u_1))).toFun x_1
Tactic: ext x : 3
-- 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
H : ContinuousMap.{u_3, u_2} ((↑I : Type) × A) X
f : C(A, E)
H_0 : ∀ (a : A), (H : (a : (↑I : Type) × A) → X) (0, a) = p ((f : (a : A) → E) a)
f₀ f₁ : C(A, X)
S : Set A
F : f₀.HomotopyRel f₁ S
X_1 Y Z : FundamentalGroupoid X
x : X_1 ⟶ Y
x_1 : Y ⟶ Z
⊢ ↾cov.monodromy (x ≫ x_1) = ↾cov.monodromy x ≫ ↾cov.monodromy x_1
have h : ∀ (x_2 : (↑(p ⁻¹' {X_1.as}) : Type u_1)),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (↾cov.monodromy (x ≫ x_1))).toFun x_2 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (↾cov.monodromy x ≫ ↾cov.monodromy x_1)).toFun x_2
Tactic: ext : 3
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
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 := ⋯ }
have refine : ∀ (γ₀ γ₁ : Path e₀ e₁),
  Eq.{u_2 + 1} (α :=
      Path.Homotopic.Quotient (X := X) (({ toFun := p, continuous_toFun := sorry : C(E, X) } : (a : E) → X) e₀ : X)
        (({ toFun := p, continuous_toFun := sorry : C(E, X) } : (a : E) → X) e₁ : X))
      ((fun (γ : Path.Homotopic.Quotient e₀ e₁) ↦ γ.map { toFun := p, continuous_toFun := sorry : C(E, X) }) ⟦γ₀⟧)
      ((fun (γ : Path.Homotopic.Quotient e₀ e₁) ↦ γ.map { toFun := p, continuous_toFun := sorry : C(E, X) }) ⟦γ₁⟧) →
    Eq (α := Path.Homotopic.Quotient e₀ e₁) ⟦γ₀⟧ ⟦γ₁⟧
Tactic: refine Quotient.ind₂ fun γ₀ γ₁ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
e₀ e₁ : E
γ₀ γ₁ : Path e₀ e₁
⊢ Path.Homotopic.Quotient.mk (γ₀.map ⋯) = Path.Homotopic.Quotient.mk (γ₁.map ⋯) →
    Path.Homotopic.Quotient.mk γ₀ = Path.Homotopic.Quotient.mk γ₁
have rw : (γ₀.map sorry).Homotopic (γ₁.map sorry) → Path.Homotopic.Quotient.mk γ₀ = Path.Homotopic.Quotient.mk γ₁
Tactic: rw [Path.Homotopic.Quotient.eq]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
e₀ e₁ : E
γ₀ γ₁ : Path e₀ e₁
⊢ (γ₀.map ⋯).Homotopic (γ₁.map ⋯) → Path.Homotopic.Quotient.mk γ₀ = Path.Homotopic.Quotient.mk γ₁
have rw : (γ₀.map sorry).Homotopic (γ₁.map sorry) → γ₀.Homotopic γ₁
Tactic: rw [Path.Homotopic.Quotient.eq]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
e₀ e₁ : E
γ₀ γ₁ : Path e₀ e₁
⊢ Path.Homotopic.Quotient.mk (γ₀.map ⋯) = Path.Homotopic.Quotient.mk (γ₁.map ⋯) →
    Path.Homotopic.Quotient.mk γ₀ = Path.Homotopic.Quotient.mk γ₁
have iterate : (γ₀.map sorry).Homotopic (γ₁.map sorry) → γ₀.Homotopic γ₁
Tactic: iterate 2 rw [Path.Homotopic.Quotient.eq]
-- 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 : 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)
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 : 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)
⊢ ∃! 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 : 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 (α := E) ((Γ : (a : (↑I : Type)) → E) 1 : E) ((Γ' : (a : (↑I : Type)) → E) 1 : E)
have h : Γ = cov.liftPath (f.comp pγ.toContinuousMap) e₀ sorry
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])
-- 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 : 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₀ ⋯
⊢ Eq (α := E) ((Γ : (a : (↑I : Type)) → E) 1 : E) ((Γ' : (a : (↑I : Type)) → E) 1 : E)
have h₁ : Γ' = cov.liftPath (f.comp pγ'.toContinuousMap) e₀ sorry
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])
-- 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 : 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' := ⋯ }
⊢ Γ = cov.liftPath (f.comp pγ.toContinuousMap) e₀ ⋯
have h : Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp pγ.toContinuousMap) : (a : (↑I : Type)) → X) ∧
  (Γ : (a : (↑I : Type)) → E) 0 = e₀
Tactic: rw [eq_liftPath_iff']