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)
a : A
⊢ Eq.{u_1 + 1} (α := E) ((cov.liftHomotopy H f H_0 : (a : (↑I : Type) × A) → E) (0, a) : E) ((f : (a : A) → E) a : E)

Tactic:
cov.liftPath_zero ..

Premises used: IsCoveringMap.liftPath_zero
-- 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)
H' : (↑I : Type) × A → E
⊢ H' = (⇑(cov.liftHomotopy H f H_0) : (a : (↑I : Type) × A) → E) ↔
    (∀ (a : A), Continuous[_, inst] fun (x : (↑I : Type)) ↦ H' (x, a)) ∧
      p ∘ H' = (⇑H : (a : (↑I : Type) × A) → X) ∧ ∀ (a : A), H' (0, a) = (f : (a : A) → E) a

Tactic:
⟨?_, fun ⟨H'_cont, H'_lifts, H'_0⟩ ↦ funext fun ⟨t, a⟩ ↦ ?_⟩

Premises used: _private.0.IsLocalHomeomorph.continuous_lift.match_1, IsCoveringMap.liftHomotopy, funext, Iff.intro, _private.0.IsCoveringMap.eq_liftHomotopy_iff.match_1, Eq, DFunLike.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)
H' : (↑I : Type) × A → E
refine_1 :
  H' = (⇑(cov.liftHomotopy H f H_0) : (a : (↑I : Type) × A) → E) →
    (∀ (a : A), Continuous[_, inst] fun (x : (↑I : Type)) ↦ H' (x, a)) ∧
      p ∘ H' = (⇑H : (a : (↑I : Type) × A) → X) ∧ ∀ (a : A), H' (0, a) = (f : (a : A) → E) a
refine_2 :
  ((∀ (a : A), Continuous[_, inst] fun (x : (↑I : Type)) ↦ H' (x, a)) ∧
      p ∘ H' = (⇑H : (a : (↑I : Type) × A) → X) ∧ ∀ (a : A), H' (0, a) = (f : (a : A) → E) a) →
    ∀ (H'_cont : ∀ (a : A), Continuous[_, inst] fun (x : (↑I : Type)) ↦ H' (x, a))
      (H'_lifts : p ∘ H' = (⇑H : (a : (↑I : Type) × A) → X)) (H'_0 : ∀ (a : A), H' (0, a) = (f : (a : A) → E) a)
      (x : (↑I : Type) × A) (t : (↑I : Type)) (a : A),
      H' (t, a) = (cov.liftHomotopy H f H_0 : (a : (↑I : Type) × A) → E) (t, a)
⊢ H' = (⇑(cov.liftHomotopy H f H_0) : (a : (↑I : Type) × A) → E) ↔
    (∀ (a : A), Continuous[_, inst] fun (x : (↑I : Type)) ↦ H' (x, a)) ∧
      p ∘ H' = (⇑H : (a : (↑I : Type) × A) → X) ∧ ∀ (a : A), H' (0, a) = (f : (a : A) → E) a

Tactic:
refine ⟨?_, fun ⟨H'_cont, H'_lifts, H'_0⟩ ↦ funext fun ⟨t, 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)
⊢ (∀ (a : A),
      Continuous[_, inst] fun (x : (↑I : Type)) ↦ (cov.liftHomotopy H f H_0 : (a : (↑I : Type) × A) → E) (x, a)) ∧
    Eq (α := (↑I : Type) × A → X) (p ∘ (⇑(cov.liftHomotopy H f H_0) : (a : (↑I : Type) × A) → E))
        (⇑H : (a : (↑I : Type) × A) → X) ∧
      ∀ (a : A),
        Eq.{u_1 + 1} (α := E) ((cov.liftHomotopy H f H_0 : (a : (↑I : Type) × A) → E) (0, a) : E)
          ((f : (a : A) → E) a : E)

Tactic:
⟨fun a ↦ ?_, cov.liftHomotopy_lifts H f H_0, cov.liftHomotopy_zero H f H_0⟩

Premises used: IsCoveringMap.liftHomotopy_zero, And.intro, 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)
refine_1 :
  ∀ (a : A), Continuous[_, inst] fun (x : (↑I : Type)) ↦ (cov.liftHomotopy H f H_0 : (a : (↑I : Type) × A) → E) (x, a)
⊢ (∀ (a : A),
      Continuous[_, inst] fun (x : (↑I : Type)) ↦ (cov.liftHomotopy H f H_0 : (a : (↑I : Type) × A) → E) (x, a)) ∧
    Eq (α := (↑I : Type) × A → X) (p ∘ (⇑(cov.liftHomotopy H f H_0) : (a : (↑I : Type) × A) → E))
        (⇑H : (a : (↑I : Type) × A) → X) ∧
      ∀ (a : A),
        Eq.{u_1 + 1} (α := E) ((cov.liftHomotopy H f H_0 : (a : (↑I : Type) × A) → E) (0, a) : E)
          ((f : (a : A) → E) a : E)

Tactic:
refine ⟨fun a ↦ ?_, cov.liftHomotopy_lifts H f H_0, cov.liftHomotopy_zero H f H_0⟩
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
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)
a : A
refine_1 :
  Continuous[_, inst] fun (x : (↑I : Type)) ↦
    (cov.liftPath (H.comp (ContinuousMap.prodMk (ContinuousMap.id (↑I : Type)) (ContinuousMap.const (↑I : Type) a)))
          ((f : (a : A) → E) a) ⋯ :
        (a : (↑I : Type)) → E)
      x
⊢ Continuous[_, inst] fun (x : (↑I : Type)) ↦ (cov.liftHomotopy H f H_0 : (a : (↑I : Type) × A) → E) (x, a)

Tactic:
simp_rw [liftHomotopy_apply]

Premises used: IsCoveringMap.liftHomotopy_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)
a : A
⊢ Continuous[_, inst] fun (x : (↑I : Type)) ↦
    (cov.liftPath (H.comp (ContinuousMap.prodMk (ContinuousMap.id (↑I : Type)) (ContinuousMap.const (↑I : Type) a)))
          ((f : (a : A) → E) a) ⋯ :
        (a : (↑I : Type)) → E)
      x

Tactic:
(cov.liftPath _ _ <| H_0 a).2

Premises used: IsCoveringMap.liftPath, ContinuousMap.continuous_toFun
-- 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)
a : A
⊢ Continuous[_, inst] fun (x : (↑I : Type)) ↦
    (cov.liftPath (H.comp (ContinuousMap.prodMk (ContinuousMap.id (↑I : Type)) (ContinuousMap.const (↑I : Type) a)))
          ((f : (a : A) → E) a) ⋯ :
        (a : (↑I : Type)) → E)
      x

Tactic:
exact (cov.liftPath _ _ <| H_0 a).2

Premises used: IsCoveringMap.liftPath, ContinuousMap.continuous_toFun
-- 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)
H' : (↑I : Type) × A → E
h :
  (∀ (a : A), Continuous[_, inst] fun (x : (↑I : Type)) ↦ H' (x, a)) ∧
    p ∘ H' = (⇑H : (a : (↑I : Type) × A) → X) ∧ ∀ (a : A), H' (0, a) = (f : (a : A) → E) a
H'_cont : ∀ (a : A), Continuous[_, inst] fun (x : (↑I : Type)) ↦ H' (x, a)
H'_lifts : p ∘ H' = (⇑H : (a : (↑I : Type) × A) → X)
H'_0 : ∀ (a : A), H' (0, a) = (f : (a : A) → E) a
x : (↑I : Type) × A
t : (↑I : Type)
a : A
apply :
  Eq (α := (↑I : Type) → X) (p ∘ fun (x : (↑I : Type)) ↦ H' (x, a))
    (⇑(H.comp (ContinuousMap.prodMk (ContinuousMap.id (↑I : Type)) (ContinuousMap.const (↑I : Type) (t, a).2))) :
      (a : (↑I : Type)) → X)
⊢ H' (t, a) = (cov.liftHomotopy H f H_0 : (a : (↑I : Type) × A) → E) (t, a)

Tactic:
apply congr_fun ((cov.eq_liftPath_iff _).mpr ⟨H'_cont a, _, H'_0 a⟩) t

Premises used: Iff.mpr, And.intro, congr_fun, IsCoveringMap.eq_liftPath_iff
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
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)
H' : (↑I : Type) × A → E
h_1 :
  (∀ (a : A), Continuous[_, inst] fun (x : (↑I : Type)) ↦ H' (x, a)) ∧
    p ∘ H' = (⇑H : (a : (↑I : Type) × A) → X) ∧ ∀ (a : A), H' (0, a) = (f : (a : A) → E) a
H'_cont : ∀ (a : A), Continuous[_, inst] fun (x : (↑I : Type)) ↦ H' (x, a)
H'_lifts : p ∘ H' = (⇑H : (a : (↑I : Type) × A) → X)
H'_0 : ∀ (a : A), H' (0, a) = (f : (a : A) → E) a
x : (↑I : Type) × A
t : (↑I : Type)
a : A
h :
  ∀ (t_1 : ℝ) (a_1 : t_1 ∈ I),
    (p ∘ fun (x : (↑I : Type)) ↦ H' (x, a)) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t_1 a_1) =
      (H.comp (ContinuousMap.prodMk (ContinuousMap.id (↑I : Type)) (ContinuousMap.const (↑I : Type) (t, a).2)) :
          (a : (↑I : Type)) → X)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t_1 a_1)
⊢ Eq (α := (↑I : Type) → X) (p ∘ fun (x : (↑I : Type)) ↦ H' (x, a))
    (⇑(H.comp (ContinuousMap.prodMk (ContinuousMap.id (↑I : Type)) (ContinuousMap.const (↑I : Type) (t, a).2))) :
      (a : (↑I : Type)) → X)

Tactic:
ext ⟨t, 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)
H' : (↑I : Type) × A → E
h :
  (∀ (a : A), Continuous[_, inst] fun (x : (↑I : Type)) ↦ H' (x, a)) ∧
    p ∘ H' = (⇑H : (a : (↑I : Type) × A) → X) ∧ ∀ (a : A), H' (0, a) = (f : (a : A) → E) a
H'_cont : ∀ (a : A), Continuous[_, inst] fun (x : (↑I : Type)) ↦ H' (x, a)
H'_lifts : p ∘ H' = (⇑H : (a : (↑I : Type) × A) → X)
H'_0 : ∀ (a : A), H' (0, a) = (f : (a : A) → E) a
x : (↑I : Type) × A
t_1 : (↑I : Type)
a_1 : A
t : ℝ
a : t ∈ I
⊢ (p ∘ fun (x : (↑I : Type)) ↦ H' (x, a_1)) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t a) =
    (H.comp (ContinuousMap.prodMk (ContinuousMap.id (↑I : Type)) (ContinuousMap.const (↑I : Type) (t_1, a_1).2)) :
        (a : (↑I : Type)) → X)
      (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t a)

Tactic:
congr_fun H'_lifts _

Premises used: 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)
H' : (↑I : Type) × A → E
h :
  (∀ (a : A), Continuous[_, inst] fun (x : (↑I : Type)) ↦ H' (x, a)) ∧
    p ∘ H' = (⇑H : (a : (↑I : Type) × A) → X) ∧ ∀ (a : A), H' (0, a) = (f : (a : A) → E) a
H'_cont : ∀ (a : A), Continuous[_, inst] fun (x : (↑I : Type)) ↦ H' (x, a)
H'_lifts : p ∘ H' = (⇑H : (a : (↑I : Type) × A) → X)
H'_0 : ∀ (a : A), H' (0, a) = (f : (a : A) → E) a
x : (↑I : Type) × A
t_1 : (↑I : Type)
a_1 : A
t : ℝ
a : t ∈ I
⊢ (p ∘ fun (x : (↑I : Type)) ↦ H' (x, a_1)) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t a) =
    (H.comp (ContinuousMap.prodMk (ContinuousMap.id (↑I : Type)) (ContinuousMap.const (↑I : Type) (t_1, a_1).2)) :
        (a : (↑I : Type)) → X)
      (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t a)

Tactic:
exact congr_fun H'_lifts _

Premises used: 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)
H' : ContinuousMap.{u_3, u_1} ((↑I : Type) × A) E
simp_rw :
  ((∀ (a : A), Continuous[_, inst] fun (x : (↑I : Type)) ↦ (H' : (a : (↑I : Type) × A) → E) (x, a)) ∧
      Eq (α := (↑I : Type) × A → X) (p ∘ (⇑H' : (a : (↑I : Type) × A) → E)) (⇑H : (a : (↑I : Type) × A) → X) ∧
        ∀ (a : A), Eq.{u_1 + 1} (α := E) ((H' : (a : (↑I : Type) × A) → E) (0, a) : E) ((f : (a : A) → E) a : E)) ↔
    Eq (α := (↑I : Type) × A → X) (p ∘ (⇑H' : (a : (↑I : Type) × A) → E)) (⇑H : (a : (↑I : Type) × A) → X) ∧
      ∀ (a : A), Eq.{u_1 + 1} (α := E) ((H' : (a : (↑I : Type) × A) → E) (0, a) : E) ((f : (a : A) → E) a : E)
⊢ H' = cov.liftHomotopy H f H_0 ↔
    Eq (α := (↑I : Type) × A → X) (p ∘ (⇑H' : (a : (↑I : Type) × A) → E)) (⇑H : (a : (↑I : Type) × A) → X) ∧
      ∀ (a : A), Eq.{u_1 + 1} (α := E) ((H' : (a : (↑I : Type) × A) → E) (0, a) : E) ((f : (a : A) → E) a : E)

Tactic:
simp_rw [← DFunLike.coe_fn_eq, eq_liftHomotopy_iff]

Premises used: DFunLike.coe_fn_eq, IsCoveringMap.eq_liftHomotopy_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
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)
H' : ContinuousMap.{u_3, u_1} ((↑I : Type) × A) E
⊢ ((∀ (a : A), Continuous[_, inst] fun (x : (↑I : Type)) ↦ (H' : (a : (↑I : Type) × A) → E) (x, a)) ∧
      Eq (α := (↑I : Type) × A → X) (p ∘ (⇑H' : (a : (↑I : Type) × A) → E)) (⇑H : (a : (↑I : Type) × A) → X) ∧
        ∀ (a : A), Eq.{u_1 + 1} (α := E) ((H' : (a : (↑I : Type) × A) → E) (0, a) : E) ((f : (a : A) → E) a : E)) ↔
    Eq (α := (↑I : Type) × A → X) (p ∘ (⇑H' : (a : (↑I : Type) × A) → E)) (⇑H : (a : (↑I : Type) × A) → X) ∧
      ∀ (a : A), Eq.{u_1 + 1} (α := E) ((H' : (a : (↑I : Type) × A) → E) (0, a) : E) ((f : (a : A) → E) a : E)

Tactic:
and_iff_right fun a ↦ H'.2.comp (.prodMk_left a)

Premises used: Continuous.comp, and_iff_right, ContinuousMap.continuous_toFun, Continuous.prodMk_left
-- 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)
H' : ContinuousMap.{u_3, u_1} ((↑I : Type) × A) E
⊢ ((∀ (a : A), Continuous[_, inst] fun (x : (↑I : Type)) ↦ (H' : (a : (↑I : Type) × A) → E) (x, a)) ∧
      Eq (α := (↑I : Type) × A → X) (p ∘ (⇑H' : (a : (↑I : Type) × A) → E)) (⇑H : (a : (↑I : Type) × A) → X) ∧
        ∀ (a : A), Eq.{u_1 + 1} (α := E) ((H' : (a : (↑I : Type) × A) → E) (0, a) : E) ((f : (a : A) → E) a : E)) ↔
    Eq (α := (↑I : Type) × A → X) (p ∘ (⇑H' : (a : (↑I : Type) × A) → E)) (⇑H : (a : (↑I : Type) × A) → X) ∧
      ∀ (a : A), Eq.{u_1 + 1} (α := E) ((H' : (a : (↑I : Type) × A) → E) (0, a) : E) ((f : (a : A) → E) a : E)

Tactic:
exact and_iff_right fun a ↦ H'.2.comp (.prodMk_left a)

Premises used: Continuous.comp, and_iff_right, ContinuousMap.continuous_toFun, Continuous.prodMk_left
-- 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)
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)
t : (↑I : Type)
a : A
ha : a ∈ S
rw :
  Eq (α := E)
    ((cov.liftPath
            (comp (↑F : C((↑I : Type) × A, X)) (prodMk (ContinuousMap.id (↑I : Type)) (const (↑I : Type) (t, a).2)))
            ((f₀' : (a : A) → E) (t, a).2) ⋯ :
          (a : (↑I : Type)) → E)
        0 :
      E)
    ((f₀' : (a : A) → E) a : E)
rw₁ :
  ∀ (a_1 a' : (↑I : Type)),
    p
        ((cov.liftPath
              (comp (↑F : C((↑I : Type) × A, X)) (prodMk (ContinuousMap.id (↑I : Type)) (const (↑I : Type) (t, a).2)))
              ((f₀' : (a : A) → E) (t, a).2) ⋯ :
            (a : (↑I : Type)) → E)
          a_1) =
      p
        ((cov.liftPath
              (comp (↑F : C((↑I : Type) × A, X)) (prodMk (ContinuousMap.id (↑I : Type)) (const (↑I : Type) (t, a).2)))
              ((f₀' : (a : A) → E) (t, a).2) ⋯ :
            (a : (↑I : Type)) → E)
          a')
⊢ 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)

Tactic:
rw [liftHomotopy_apply, cov.const_of_comp (ContinuousMap.continuous _) _ t 0]

Premises used: ContinuousMap.continuous, IsCoveringMap.liftHomotopy_apply, OfNat.ofNat, IsCoveringMap.const_of_comp
-- 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)
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)
t : (↑I : Type)
a : A
ha : a ∈ S
⊢ Eq (α := E)
    ((cov.liftPath
            (comp (↑F : C((↑I : Type) × A, X)) (prodMk (ContinuousMap.id (↑I : Type)) (const (↑I : Type) (t, a).2)))
            ((f₀' : (a : A) → E) (t, a).2) ⋯ :
          (a : (↑I : Type)) → E)
        0 :
      E)
    ((f₀' : (a : A) → E) a : E)

Tactic:
apply cov.liftPath_zero

Premises used: IsCoveringMap.liftPath_zero
-- 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)
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)
t_1 : (↑I : Type)
a : A
ha : a ∈ S
t t' : (↑I : Type)
simp_rw :
  Eq (α := X)
    ((comp (↑F : C((↑I : Type) × A, X)) (prodMk (ContinuousMap.id (↑I : Type)) (const (↑I : Type) a)) :
          (a : (↑I : Type)) → X)
        t :
      X)
    ((comp (↑F : C((↑I : Type) × A, X)) (prodMk (ContinuousMap.id (↑I : Type)) (const (↑I : Type) a)) :
          (a : (↑I : Type)) → X)
        t' :
      X)
⊢ p
      ((cov.liftPath
            (comp (↑F : C((↑I : Type) × A, X)) (prodMk (ContinuousMap.id (↑I : Type)) (const (↑I : Type) (t_1, a).2)))
            ((f₀' : (a : A) → E) (t_1, a).2) ⋯ :
          (a : (↑I : Type)) → E)
        t) =
    p
      ((cov.liftPath
            (comp (↑F : C((↑I : Type) × A, X)) (prodMk (ContinuousMap.id (↑I : Type)) (const (↑I : Type) (t_1, a).2)))
            ((f₀' : (a : A) → E) (t_1, a).2) ⋯ :
          (a : (↑I : Type)) → E)
        t')

Tactic:
simp_rw [← p.comp_apply, cov.liftPath_lifts]

Premises used: IsCoveringMap.liftPath_lifts, 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)
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)
t_1 : (↑I : Type)
a : A
ha : a ∈ S
t t' : (↑I : Type)
⊢ Eq (α := X)
    ((comp (↑F : C((↑I : Type) × A, X)) (prodMk (ContinuousMap.id (↑I : Type)) (const (↑I : Type) a)) :
          (a : (↑I : Type)) → X)
        t :
      X)
    ((comp (↑F : C((↑I : Type) × A, X)) (prodMk (ContinuousMap.id (↑I : Type)) (const (↑I : Type) a)) :
          (a : (↑I : Type)) → X)
        t' :
      X)

Tactic:
(F.prop t a ha).trans (F.prop t' a ha).symm

Premises used: ContinuousMap.HomotopyWith.prop, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
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)
t_1 : (↑I : Type)
a : A
ha : a ∈ S
t t' : (↑I : Type)
⊢ Eq (α := X)
    ((comp (↑F : C((↑I : Type) × A, X)) (prodMk (ContinuousMap.id (↑I : Type)) (const (↑I : Type) a)) :
          (a : (↑I : Type)) → X)
        t :
      X)
    ((comp (↑F : C((↑I : Type) × A, X)) (prodMk (ContinuousMap.id (↑I : Type)) (const (↑I : Type) a)) :
          (a : (↑I : Type)) → X)
        t' :
      X)

Tactic:
exact (F.prop t a ha).trans (F.prop t' a ha).symm

Premises used: ContinuousMap.HomotopyWith.prop, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
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)
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
⊢ ∀ (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