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
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
x y z : X
e : E
hpe : x = p e
γ : Path x y
γ' : Path y z
x_1 : (↑I : Type)
⊢ (p ∘
        (⇑(↑({ toContinuousMap := cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯, source' := ⋯, target' := ⋯ :
                      Path e ((cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯ : (a : (↑I : Type)) → E) 1) }.trans
                  {
                    toContinuousMap :=
                      cov.liftPath (↑γ' : C((↑I : Type), X))
                        ((cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯ : (a : (↑I : Type)) → E) 1) ⋯,
                    source' := ⋯, target' := ⋯ :
                    Path ((cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯ : (a : (↑I : Type)) → E) 1)
                      ((cov.liftPath (↑γ' : C((↑I : Type), X))
                            ((cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯ : (a : (↑I : Type)) → E) 1) ⋯).toFun
                        1) }) :
              C((↑I : Type), E)) :
          (a : (↑I : Type)) → E))
      x_1 =
    ((↑(γ.trans γ') : C((↑I : Type), X)) : (a : (↑I : Type)) → X) x_1
have simp : p
    (if h : (↑x_1 : ℝ) ≤ 1 / 2 then
      ({ toContinuousMap := cov.liftPath (↑γ : C((↑I : Type), X)) e sorry, source' := sorry, target' := sorry :
            Path e ((cov.liftPath (↑γ : C((↑I : Type), X)) e sorry : (a : (↑I : Type)) → E) 1) } :
          (a : (↑I : Type)) → E)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ)) sorry)
    else
      ({
            toContinuousMap :=
              cov.liftPath (↑γ' : C((↑I : Type), X))
                ((cov.liftPath (↑γ : C((↑I : Type), X)) e sorry : (a : (↑I : Type)) → E) 1) sorry,
            source' := sorry, target' := sorry :
            Path ((cov.liftPath (↑γ : C((↑I : Type), X)) e sorry : (a : (↑I : Type)) → E) 1)
              ((cov.liftPath (↑γ' : C((↑I : Type), X))
                    ((cov.liftPath (↑γ : C((↑I : Type), X)) e sorry : (a : (↑I : Type)) → E) 1) sorry).toFun
                1) } :
          (a : (↑I : Type)) → E)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ) - 1) sorry)) =
  if h : (↑x_1 : ℝ) ≤ 1 / 2 then (γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ)) sorry)
  else (γ' : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ) - 1) sorry)
Tactic: simp only [ContinuousMap.coe_coe, Function.comp_apply, Path.trans_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
x y z : X
e : E
hpe : x = p e
γ : Path x y
γ' : Path y z
x_1 : (↑I : Type)
⊢ p
      (if h : (↑x_1 : ℝ) ≤ 1 / 2 then
        ({ toContinuousMap := cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯, source' := ⋯, target' := ⋯ :
              Path e ((cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯ : (a : (↑I : Type)) → E) 1) } :
            (a : (↑I : Type)) → E)
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ)) ⋯)
      else
        ({
              toContinuousMap :=
                cov.liftPath (↑γ' : C((↑I : Type), X))
                  ((cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯ : (a : (↑I : Type)) → E) 1) ⋯,
              source' := ⋯, target' := ⋯ :
              Path ((cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯ : (a : (↑I : Type)) → E) 1)
                ((cov.liftPath (↑γ' : C((↑I : Type), X))
                      ((cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯ : (a : (↑I : Type)) → E) 1) ⋯).toFun
                  1) } :
            (a : (↑I : Type)) → E)
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ) - 1) ⋯)) =
    if h : (↑x_1 : ℝ) ≤ 1 / 2 then
      (γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ)) ⋯)
    else (γ' : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ) - 1) ⋯)
have pos : ∀ (h : (↑x_1 : ℝ) ≤ 1 / 2),
  p
      (({ toContinuousMap := cov.liftPath (↑γ : C((↑I : Type), X)) e sorry, source' := sorry, target' := sorry :
            Path e ((cov.liftPath (↑γ : C((↑I : Type), X)) e sorry : (a : (↑I : Type)) → E) 1) } :
          (a : (↑I : Type)) → E)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ)) sorry)) =
    (γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ)) sorry)
Tactic: split_ifs
-- 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
e : E
hpe : x = p e
γ : Path x y
γ' : Path y z
x_1 : (↑I : Type)
pos :
  ∀ (h : (↑x_1 : ℝ) ≤ 1 / 2),
    p
        (({ toContinuousMap := cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯, source' := ⋯, target' := ⋯ :
              Path e ((cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯ : (a : (↑I : Type)) → E) 1) } :
            (a : (↑I : Type)) → E)
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ)) ⋯)) =
      (γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ)) ⋯)
⊢ p
      (if h : (↑x_1 : ℝ) ≤ 1 / 2 then
        ({ toContinuousMap := cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯, source' := ⋯, target' := ⋯ :
              Path e ((cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯ : (a : (↑I : Type)) → E) 1) } :
            (a : (↑I : Type)) → E)
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ)) ⋯)
      else
        ({
              toContinuousMap :=
                cov.liftPath (↑γ' : C((↑I : Type), X))
                  ((cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯ : (a : (↑I : Type)) → E) 1) ⋯,
              source' := ⋯, target' := ⋯ :
              Path ((cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯ : (a : (↑I : Type)) → E) 1)
                ((cov.liftPath (↑γ' : C((↑I : Type), X))
                      ((cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯ : (a : (↑I : Type)) → E) 1) ⋯).toFun
                  1) } :
            (a : (↑I : Type)) → E)
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ) - 1) ⋯)) =
    if h : (↑x_1 : ℝ) ≤ 1 / 2 then
      (γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ)) ⋯)
    else (γ' : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ) - 1) ⋯)
have neg : ∀ (h : ¬(↑x_1 : ℝ) ≤ 1 / 2),
  p
      (({
            toContinuousMap :=
              cov.liftPath (↑γ' : C((↑I : Type), X))
                ((cov.liftPath (↑γ : C((↑I : Type), X)) e sorry : (a : (↑I : Type)) → E) 1) sorry,
            source' := sorry, target' := sorry :
            Path ((cov.liftPath (↑γ : C((↑I : Type), X)) e sorry : (a : (↑I : Type)) → E) 1)
              ((cov.liftPath (↑γ' : C((↑I : Type), X))
                    ((cov.liftPath (↑γ : C((↑I : Type), X)) e sorry : (a : (↑I : Type)) → E) 1) sorry).toFun
                1) } :
          (a : (↑I : Type)) → E)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ) - 1) sorry)) =
    (γ' : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ) - 1) sorry)
Tactic: split_ifs
-- 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
e : E
hpe : x = p e
γ : Path x y
γ' : Path y z
x_1 : (↑I : Type)
h : ¬(↑x_1 : ℝ) ≤ 1 / 2
⊢ p
      (({
            toContinuousMap :=
              cov.liftPath (↑γ' : C((↑I : Type), X))
                ((cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯ : (a : (↑I : Type)) → E) 1) ⋯,
            source' := ⋯, target' := ⋯ :
            Path ((cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯ : (a : (↑I : Type)) → E) 1)
              ((cov.liftPath (↑γ' : C((↑I : Type), X))
                    ((cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯ : (a : (↑I : Type)) → E) 1) ⋯).toFun
                1) } :
          (a : (↑I : Type)) → E)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ) - 1) ⋯)) =
    (γ' : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x_1 : ℝ) - 1) ⋯)
have neg : ((↑γ' : C((↑I : Type), X)) : (a : (↑I : Type)) → X) 0 =
  p ((cov.liftPath (↑γ : C((↑I : Type), X)) e sorry : (a : (↑I : Type)) → E) 1)
Tactic: refine congr_fun (cov.liftPath_lifts γ' _ ?_) _
-- 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)
⊢ Eq (α := (↑I : Type) × A → X)
    (p ∘ fun (ta : (↑I : Type) × A) ↦
      (cov.liftPath
            (H.comp (ContinuousMap.prodMk (ContinuousMap.id (↑I : Type)) (ContinuousMap.const (↑I : Type) ta.2)))
            ((f : (a : A) → E) ta.2) ⋯ :
          (a : (↑I : Type)) → E)
        ta.1)
    (⇑H : (a : (↑I : Type) × A) → X)
have h : ∀ (t : (↑I : Type)) (a : A),
  (p ∘ fun (ta : (↑I : Type) × A) ↦
        (cov.liftPath
              (H.comp (ContinuousMap.prodMk (ContinuousMap.id (↑I : Type)) (ContinuousMap.const (↑I : Type) ta.2)))
              ((f : (a : A) → E) ta.2) sorry :
            (a : (↑I : Type)) → E)
          ta.1)
      (t, a) =
    (H : (a : (↑I : Type) × A) → X) (t, a)
Tactic: ext ⟨t, 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)
⊢ Continuous[inst_2, inst] fun (x : A) ↦
    (cov.liftPath
          (H.comp (ContinuousMap.prodMk (ContinuousMap.id (↑I : Type)) (ContinuousMap.const (↑I : Type) (0, x).2)))
          ((f : (a : A) → E) (0, x).2) ⋯ :
        (a : (↑I : Type)) → E)
      (0, x).1
have h : ∀ (a : A),
  Eq (α := E)
    ((cov.liftPath
            (H.comp (ContinuousMap.prodMk (ContinuousMap.id (↑I : Type)) (ContinuousMap.const (↑I : Type) (0, a).2)))
            ((f : (a : A) → E) (0, a).2) sorry :
          (a : (↑I : Type)) → E)
        (0, a).1 :
      E)
    ((f : (a : A) → E) a : E)
Tactic: convert! f.continuous with 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)
a : A
⊢ Continuous[_, inst] fun (x : (↑I : Type)) ↦
    (cov.liftPath
          (H.comp (ContinuousMap.prodMk (ContinuousMap.id (↑I : Type)) (ContinuousMap.const (↑I : Type) (x, a).2)))
          ((f : (a : A) → E) (x, a).2) ⋯ :
        (a : (↑I : Type)) → E)
      (x, a).1
have dsimp : 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) sorry :
      (a : (↑I : Type)) → E)
    x
Tactic: dsimp only
-- 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)
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
have 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
Tactic: refine ⟨?_, fun ⟨H'_cont, H'_lifts, H'_0⟩ ↦ funext fun ⟨t, 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)
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
⊢ 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
have 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)
Tactic: refine ⟨?_, fun ⟨H'_cont, H'_lifts, H'_0⟩ ↦ funext fun ⟨t, 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)
⊢ (∀ (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)
have refine_1 : ∀ (a : A), Continuous[_, inst] fun (x : (↑I : Type)) ↦ (cov.liftHomotopy H f H_0 : (a : (↑I : Type) × A) → E) (x, a)
Tactic: refine ⟨fun a ↦ ?_, cov.liftHomotopy_lifts H f H_0, cov.liftHomotopy_zero H f H_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
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)
have 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) sorry :
      (a : (↑I : Type)) → E)
    x
Tactic: simp_rw [liftHomotopy_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)
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
⊢ H' (t, a) = (cov.liftHomotopy H f H_0 : (a : (↑I : Type) × A) → E) (t, a)
have 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)
Tactic: apply congr_fun ((cov.eq_liftPath_iff _).mpr ⟨H'_cont a, _, H'_0 a⟩) t
-- 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)
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
⊢ 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)
have 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)
Tactic: ext ⟨t, 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)
H' : ContinuousMap.{u_3, u_1} ((↑I : Type) × 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)
have 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)
Tactic: simp_rw [← DFunLike.coe_fn_eq, eq_liftHomotopy_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
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.{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)
have 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) sorry :
        (a : (↑I : Type)) → E)
      0 :
    E)
  ((f₀' : (a : A) → E) a : E)
Tactic: rw [liftHomotopy_apply, cov.const_of_comp (ContinuousMap.continuous _) _ t 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
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)
⊢ 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)
have 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) sorry :
          (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) sorry :
          (a : (↑I : Type)) → E)
        a')
Tactic: rw [liftHomotopy_apply, cov.const_of_comp (ContinuousMap.continuous _) _ t 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
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)
⊢ 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')
have 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)
Tactic: simp_rw [← p.comp_apply, cov.liftPath_lifts]