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
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)
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)
⊢ ∀ (x : A), (cov.liftHomotopy (↑F : C((↑I : Type) × A, X)) f₀' F_0).toFun (1, x) = (f₁' : (a : A) → E) x

Tactic:
simp_rw [toFun_eq_coe, ← curry_apply]

Premises used: ContinuousMap.curry_apply, ContinuousMap.toFun_eq_coe
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
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)

Tactic:
congr_fun (cov.eq_of_comp_eq
        (ContinuousMap.continuous _) f₁'.continuous ?_ a <| (rel 1 a ha).trans he)

Premises used: ContinuousMap.continuous, congr_fun, OfNat.ofNat, IsCoveringMap.eq_of_comp_eq, 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
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)
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))
⊢ ∀ (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:
refine congr_fun (cov.eq_of_comp_eq
        (ContinuousMap.continuous _) f₁'.continuous ?_ a <| (rel 1 a ha).trans he)

Premises used: ContinuousMap.continuous, congr_fun, IsCoveringMap.eq_of_comp_eq
-- 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
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)
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
⊢ 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:
ext a
-- 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
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
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
⊢ (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:
rw [h₁, Function.comp_apply, curry_apply]

Premises used: ContinuousMap.curry_apply, Function.comp_apply
-- 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
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 : (a : (↑I : Type) × A) → E) (1, a)) = (f₁ : (a : A) → X) a

Tactic:
(congr_fun (cov.liftHomotopy_lifts F f₀' _) (1, a)).trans (F.apply_one a)

Premises used: Prod.mk, congr_fun, OfNat.ofNat, Eq.trans, IsCoveringMap.liftHomotopy_lifts
-- 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
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 : (a : (↑I : Type) × A) → E) (1, a)) = (f₁ : (a : A) → X) a

Tactic:
exact (congr_fun (cov.liftHomotopy_lifts F f₀' _) (1, a)).trans (F.apply_one a)

Premises used: Prod.mk, congr_fun, OfNat.ofNat, Eq.trans, IsCoveringMap.liftHomotopy_lifts
-- 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 : PreconnectedSpace A
f₀ f₁ : C(A, E)
S : Set A
he : ∃ a ∈ S, Eq.{u_1 + 1} (α := E) ((f₀ : (a : A) → E) a : E) ((f₁ : (a : A) → E) a : E)
⊢ f₀.HomotopicRel f₁ S ↔
    ({ toFun := p, continuous_toFun := ⋯ : C(E, X) }.comp f₀).HomotopicRel
      ({ toFun := p, continuous_toFun := ⋯ : C(E, X) }.comp f₁) S

Tactic:
⟨fun ⟨F⟩ ↦ ⟨F.compContinuousMap _⟩, fun ⟨F⟩ ↦ ⟨cov.liftHomotopyRel F he rfl rfl⟩⟩

Premises used: ContinuousMap.HomotopyRel.compContinuousMap, ContinuousMap.mk, ContinuousMap.HomotopicRel, ContinuousMap.comp, _private.0.IsCoveringMap.homotopicRel_iff_comp.match_2, Nonempty.intro, IsCoveringMap.liftHomotopyRel, _private.0.IsCoveringMap.homotopicRel_iff_comp.match_1, Iff.intro, IsCoveringMap.continuous, rfl
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ₀ γ₁ : C((↑I : Type), X)
h : γ₀.HomotopicRel γ₁ {0, 1}
e : E
h₀ : (γ₀ : (a : (↑I : Type)) → X) 0 = p e
h₁ : (γ₁ : (a : (↑I : Type)) → X) 0 = p e
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)
⊢ 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
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ₀ γ₁ : C((↑I : Type), X)
e : E
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) 0 : E)
    ((cov.liftPath γ₁ e h₁ : (a : (↑I : Type)) → E) 0 : E)

Tactic:
simp_rw [liftPath_zero]

Premises used: IsCoveringMap.liftPath_zero
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ₀ γ₁ : C((↑I : Type), X)
e : E
h₀ : (γ₀ : (a : (↑I : Type)) → X) 0 = p e
h₁ : (γ₁ : (a : (↑I : Type)) → X) 0 = p e
H : γ₀.HomotopyRel γ₁ {0, 1}
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)
⊢ 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 ..)
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ₀ γ₁ : C((↑I : Type), X)
e : E
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)
rw₁ rw₂ :
  Eq (α := E) ((this : (a : (↑I : Type) × (↑I : Type)) → E) (0, 1) : E)
    ((this : (a : (↑I : Type) × (↑I : Type)) → E) (0, 1) : E)
⊢ Eq (α := E) ((cov.liftPath γ₀ e h₀ : (a : (↑I : Type)) → E) 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)]

Premises used: ContinuousMap.HomotopyRel.eq_fst, OfNat.ofNat, Or.inr, rfl, ContinuousMap.HomotopyRel.eq_snd
-- 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
x y : E
γ : Path.Homotopic.Quotient x y
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 := ⋯ : 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)
⊢ (↑(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)

Tactic:
obtain ⟨γ⟩ := γ
-- 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
x y : E
γ_1 : Path.Homotopic.Quotient x y
γ : 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 := ⋯ : 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)

Tactic:
(DFunLike.congr_fun ((cov.eq_liftPath_iff' _).mpr ⟨rfl, γ.source⟩).symm 1).trans γ.target

Premises used: Iff.mpr, DFunLike.congr_fun, IsCoveringMap.eq_liftPath_iff', And.intro, Path.source, Path.target, 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
x y : E
γ_1 : Path.Homotopic.Quotient x y
γ : 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 := ⋯ : 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)

Tactic:
exact (DFunLike.congr_fun ((cov.eq_liftPath_iff' _).mpr ⟨rfl, γ.source⟩).symm 1).trans γ.target

Premises used: Iff.mpr, DFunLike.congr_fun, IsCoveringMap.eq_liftPath_iff', And.intro, Path.source, Path.target, 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
x : X
⊢ cov.monodromy (Path.Homotopic.Quotient.refl x) = id

Tactic:
funext fun e ↦ Subtype.ext <| DFunLike.congr_fun (cov.liftPath_const e.2.symm) 1

Premises used: DFunLike.congr_fun, IsCoveringMap.liftPath_const, funext, OfNat.ofNat, Eq.symm, Subtype.property, Subtype.ext
-- 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
x y z : X
γ : Path.Homotopic.Quotient x y
γ' : Path.Homotopic.Quotient y z
e : (↑(p ⁻¹' {x}) : Type u_1)
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)
⊢ cov.monodromy (γ.trans γ') e = cov.monodromy γ' (cov.monodromy γ e)

Tactic:
obtain ⟨γ⟩ := γ
-- 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
x y z : X
γ_1 : Path.Homotopic.Quotient x y
γ' : Path.Homotopic.Quotient y z
e : (↑(p ⁻¹' {x}) : Type u_1)
γ : Path x y
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)
⊢ 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 ⟨γ'⟩ := γ'
-- 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
x y z : X
γ_1 : Path.Homotopic.Quotient x y
γ'_1 : Path.Homotopic.Quotient y z
e : (↑(p ⁻¹' {x}) : Type u_1)
γ : Path x y
γ' : 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:
Subtype.ext ((DFunLike.congr_fun (cov.liftPath_trans e.2.symm ..) 1).trans (Path.target _))

Premises used: DFunLike.congr_fun, Path.target, OfNat.ofNat, Eq.symm, Eq.trans, Subtype.property, Subtype.ext, IsCoveringMap.liftPath_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
x y z : X
γ_1 : Path.Homotopic.Quotient x y
γ'_1 : Path.Homotopic.Quotient y z
e : (↑(p ⁻¹' {x}) : Type u_1)
γ : Path x y
γ' : 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:
exact Subtype.ext ((DFunLike.congr_fun (cov.liftPath_trans e.2.symm ..) 1).trans (Path.target _))

Premises used: Subtype.ext
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
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
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
⊢ ↾cov.monodromy (𝟙 x) = 𝟙 (↑(p ⁻¹' {x.as}) : Type u_1)

Tactic:
ext x : 3
-- 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
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 : FundamentalGroupoid X
x : (↑(p ⁻¹' {x_1.as}) : Type u_1)
⊢ TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (↾cov.monodromy (𝟙 x_1))) x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (↑(p ⁻¹' {x_1.as}) : Type u_1))).toFun x

Tactic:
simpa using congr_fun cov.monodromy_refl x

Premises used: IsCoveringMap.monodromy_refl, congr_fun
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
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
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
⊢ ↾cov.monodromy (x ≫ x_1) = ↾cov.monodromy x ≫ ↾cov.monodromy x_1

Tactic:
ext : 3
-- 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
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
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:
simpa using cov.monodromy_trans_apply _ _ _

Premises used: IsCoveringMap.monodromy_trans_apply
-- 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
x y : X
γ : Path.Homotopic.Quotient x y
⊢ Function.Bijective (cov.monodromy γ)

Tactic:
(isIso_iff_bijective _).mp (cov.monodromyFunctor.map_isIso _)

Premises used: Set.Mem, CategoryTheory.isIso_iff_bijective, IsCoveringMap.monodromyFunctor, IsCoveringMap.monodromy, Iff.mp, CategoryTheory.Functor.map_isIso