awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
γ_0 : (γ : (a : (↑I : Type)) → X) 0 = p e
Γ : C((↑I : Type), E)
simp_rw :
  Eq (α := (a : (↑I : Type)) → E) (⇑Γ : (a : (↑I : Type)) → E) (⇑(cov.liftPath γ e γ_0) : (a : (↑I : Type)) → E) ↔
    Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑γ : (a : (↑I : Type)) → X) ∧
      (Γ : (a : (↑I : Type)) → E) 0 = e
simp_rw₁ :
  Continuous[_, inst] (⇑Γ : (a : (↑I : Type)) → E) ∧
      Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑γ : (a : (↑I : Type)) → X) ∧
        (Γ : (a : (↑I : Type)) → E) 0 = e ↔
    Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑γ : (a : (↑I : Type)) → X) ∧
      (Γ : (a : (↑I : Type)) → E) 0 = e
⊢ Γ = cov.liftPath γ e γ_0 ↔
    Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑γ : (a : (↑I : Type)) → X) ∧
      (Γ : (a : (↑I : Type)) → E) 0 = e

Tactic:
simp_rw [← DFunLike.coe_fn_eq, eq_liftPath_iff, and_iff_right (ContinuousMap.continuous _)]

Premises used: ContinuousMap.continuous, and_iff_right, DFunLike.coe_fn_eq, IsCoveringMap.eq_liftPath_iff
-- 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
e : E
x : X
hpe : x = p e
⊢ cov.liftPath (ContinuousMap.const (↑I : Type) x) e hpe = ContinuousMap.const (↑I : Type) e

Tactic:
.symm <| (cov.eq_liftPath_iff' _).mpr ⟨funext fun _ ↦ hpe.symm, rfl⟩

Premises used: Iff.mpr, IsCoveringMap.eq_liftPath_iff', funext, And.intro, Eq.symm, rfl
-- 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
γ_1 : C((↑I : Type), X)
e_1 : E
γ_0 : (γ_1 : (a : (↑I : Type)) → X) 0 = p e_1
x y z : X
e : E
hpe : x = p e
γ : Path x y
γ' : Path y z
Γ : C((↑I : Type), E) := cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯
⊢ ((↑(γ.trans γ') : C((↑I : Type), X)) : (a : (↑I : Type)) → X) 0 = p e

Tactic:
simpa
-- 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
γ_1 : C((↑I : Type), X)
e_1 : E
γ_0 : (γ_1 : (a : (↑I : Type)) → X) 0 = p e_1
x y z : X
e : E
hpe : x = p e
γ : Path x y
γ' : Path y z
Γ : C((↑I : Type), E) := cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯
⊢ ((↑γ' : C((↑I : Type), X)) : (a : (↑I : Type)) → X) 0 = p ((Γ : (a : (↑I : Type)) → E) 1)

Tactic:
simpa using (congr_fun (cov.liftPath_lifts γ ..) 1).symm

Premises used: toContinuousMap, IsCoveringMap.liftPath_lifts, congr_fun, OfNat.ofNat, Eq.symm
-- 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
e : E
hpe : x = p e
γ : Path x y
γ' : Path y z
⊢ ((↑({ 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)
      0 =
    e

Tactic:
simp
-- 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
e : E
hpe : x = p e
γ : Path x y
γ' : Path y z
refine :
  ∀ (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
⊢ cov.liftPath (↑(γ.trans γ') : C((↑I : Type), X)) e ⋯ =
    (↑({ 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))

Tactic:
refine .symm <| (cov.eq_liftPath_iff' _).mpr ⟨funext fun _ ↦ ?_, by simp⟩

Premises used: Iff.mpr, IsCoveringMap.eq_liftPath_iff', funext, And.intro
-- 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
e : E
hpe : x = p e
γ : Path x y
γ' : Path y z
x_1 : (↑I : Type)
simp :
  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) ⋯)
⊢ (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

Tactic:
simp only [ContinuousMap.coe_coe, Function.comp_apply, Path.trans_apply]

Premises used: Path.trans_apply, ContinuousMap.coe_coe, Function.comp_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 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 : ℝ)) ⋯)
neg :
  ∀ (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) ⋯)
⊢ 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) ⋯)

Tactic:
split_ifs
-- 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
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)) 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 : ℝ)) ⋯)

Tactic:
congr_fun (cov.liftPath_lifts γ e (γ.source.trans hpe)) _

Premises used: toContinuousMap, IsCoveringMap.liftPath_lifts, Path.source, congr_fun, 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 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)) 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 : ℝ)) ⋯)

Tactic:
exact congr_fun (cov.liftPath_lifts γ e (γ.source.trans hpe)) _

Premises used: toContinuousMap, IsCoveringMap.liftPath_lifts, Path.source, congr_fun, 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 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) ⋯)

Tactic:
congr_fun (cov.liftPath_lifts γ' _ ?_) _

Premises used: toContinuousMap, IsCoveringMap.liftPath_lifts, congr_fun
-- 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
e : E
hpe : x = p e
γ : Path x y
γ' : Path y z
x_1 : (↑I : Type)
h : ¬(↑x_1 : ℝ) ≤ 1 / 2
neg :
  ((↑γ' : C((↑I : Type), X)) : (a : (↑I : Type)) → X) 0 =
    p ((cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯ : (a : (↑I : Type)) → E) 1)
⊢ 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) ⋯)

Tactic:
refine congr_fun (cov.liftPath_lifts γ' _ ?_) _

Premises used: toContinuousMap, IsCoveringMap.liftPath_lifts, congr_fun
-- 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
e : E
hpe : x = p e
γ : Path x y
γ' : Path y z
x_1 : (↑I : Type)
h : ¬(↑x_1 : ℝ) ≤ 1 / 2
⊢ ((↑γ' : C((↑I : Type), X)) : (a : (↑I : Type)) → X) 0 =
    p ((cov.liftPath (↑γ : C((↑I : Type), X)) e ⋯ : (a : (↑I : Type)) → E) 1)

Tactic:
simpa using (congr_fun (cov.liftPath_lifts γ ..) 1).symm

Premises used: toContinuousMap, IsCoveringMap.liftPath_lifts, congr_fun, OfNat.ofNat, Eq.symm
-- 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 :
  ∀ (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) ⋯ :
              (a : (↑I : Type)) → E)
            ta.1)
        (t, a) =
      (H : (a : (↑I : Type) × A) → X) (t, 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)

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)
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) ⋯ :
            (a : (↑I : Type)) → E)
          ta.1)
      (t, a) =
    (H : (a : (↑I : Type) × A) → X) (t, a)

Tactic:
congr_fun (cov.liftPath_lifts ..) t

Premises used: IsCoveringMap.liftPath_lifts, 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)
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) ⋯ :
            (a : (↑I : Type)) → E)
          ta.1)
      (t, a) =
    (H : (a : (↑I : Type) × A) → X) (t, a)

Tactic:
exact congr_fun (cov.liftPath_lifts ..) t

Premises used: IsCoveringMap.liftPath_lifts, 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)
⊢ Continuous[inst_2, inst] (⇑f : (a : A) → E)

Tactic:
f.continuous

Premises used: ContinuousMap.continuous
-- 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 :
  ∀ (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) ⋯ :
            (a : (↑I : Type)) → E)
          (0, a).1 :
        E)
      ((f : (a : A) → E) a : E)
⊢ 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

Tactic:
convert! f.continuous with a

Premises used: ContinuousMap.continuous
-- 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 (α := 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) ⋯ :
          (a : (↑I : Type)) → E)
        (0, a).1 :
      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)
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) ⋯ :
          (a : (↑I : Type)) → E)
        (0, a).1 :
      E)
    ((f : (a : A) → E) a : E)

Tactic:
exact 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)
a : A
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) ⋯ :
        (a : (↑I : Type)) → E)
      x
⊢ 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

Tactic:
dsimp only
-- 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
⊢ (H.comp (ContinuousMap.prodMk (ContinuousMap.id (↑I : Type)) (ContinuousMap.const (↑I : Type) a)) :
        (a : (↑I : Type)) → X)
      0 =
    p ((f : (a : A) → E) a)

Tactic:
simp [*]
-- 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 (γ_0 := by simp [*])).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)
⊢ Eq (α := (↑I : Type) × A → X) (p ∘ (⇑(cov.liftHomotopy H f H_0) : (a : (↑I : Type) × A) → E))
    (⇑H : (a : (↑I : Type) × A) → X)

Tactic:
funext fun ⟨t, _⟩ ↦ congr_fun (cov.liftPath_lifts ..) t

Premises used: _private.0.IsLocalHomeomorph.continuous_lift.match_1, IsCoveringMap.liftHomotopy, ContinuousMap.comp, Function.comp, Set.Elem, Prod.mk, funext, ContinuousMap.id, IsCoveringMap.liftPath_lifts, ContinuousMap.prodMk, ContinuousMap.const, congr_fun, IsCoveringMap.liftHomotopy._proof_4, Eq, Prod.snd, DFunLike.coe, unitInterval