-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Covering (goal)
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ x₁ y₁ : U
p₁ : Path.{u, u_1} u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar.{u, u_1} u⦄,
    Eq (α := PathStar.{v, u_2} (φ.obj u))
        ((fun (p : PathStar.{u, u_1} u) ↦
            Sigma.mk (β := fun (v : V) ↦ Path.{v, u_2} (φ.obj u) v)
              (φ.obj (p.fst (β := fun (v : U) ↦ Path.{u, u_1} u v)))
              (φ.mapPath (p.snd (β := fun (v : U) ↦ Path.{u, u_1} u v))))
          (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁))
        ((fun (p : PathStar.{u, u_1} u) ↦
            Sigma.mk (β := fun (v : V) ↦ Path.{v, u_2} (φ.obj u) v)
              (φ.obj (p.fst (β := fun (v : U) ↦ Path.{u, u_1} u v)))
              (φ.mapPath (p.snd (β := fun (v : U) ↦ Path.{u, u_1} u v))))
          a₂) →
      Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁ = a₂
y₂ : U
p₂ : Path.{u, u_1} u y₂
cons :
  Eq (α := PathStar.{v, u_2} (φ.obj u))
      ((fun (p : PathStar.{u, u_1} u) ↦
          Sigma.mk (β := fun (v : V) ↦ Path.{v, u_2} (φ.obj u) v) (φ.obj (p.fst (β := fun (v : U) ↦ Path.{u, u_1} u v)))
            (φ.mapPath (p.snd (β := fun (v : U) ↦ Path.{u, u_1} u v))))
        (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) y₁ (p₁.cons e₁)))
      ((fun (p : PathStar.{u, u_1} u) ↦
          Sigma.mk (β := fun (v : V) ↦ Path.{v, u_2} (φ.obj u) v) (φ.obj (p.fst (β := fun (v : U) ↦ Path.{u, u_1} u v)))
            (φ.mapPath (p.snd (β := fun (v : U) ↦ Path.{u, u_1} u v))))
        (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) u Path.nil)) →
    Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) y₁ (p₁.cons e₁) =
      Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) u Path.nil
⊢ Eq (α := PathStar.{v, u_2} (φ.obj u))
      ((fun (p : PathStar.{u, u_1} u) ↦
          Sigma.mk (β := fun (v : V) ↦ Path.{v, u_2} (φ.obj u) v) (φ.obj (p.fst (β := fun (v : U) ↦ Path.{u, u_1} u v)))
            (φ.mapPath (p.snd (β := fun (v : U) ↦ Path.{u, u_1} u v))))
        (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) y₁ (p₁.cons e₁)))
      ((fun (p : PathStar.{u, u_1} u) ↦
          Sigma.mk (β := fun (v : V) ↦ Path.{v, u_2} (φ.obj u) v) (φ.obj (p.fst (β := fun (v : U) ↦ Path.{u, u_1} u v)))
            (φ.mapPath (p.snd (β := fun (v : U) ↦ Path.{u, u_1} u v))))
        (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) y₂ p₂)) →
    Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) y₁ (p₁.cons e₁) =
      Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) y₂ p₂
have cons₁ : ∀ {b : U} (p₂ : Path.{u, u_1} u b) (e₂ : b ⟶ y₂),
  Eq (α := PathStar.{v, u_2} (φ.obj u))
      ((fun (p : PathStar.{u, u_1} u) ↦
          Sigma.mk (β := fun (v : V) ↦ Path.{v, u_2} (φ.obj u) v) (φ.obj (p.fst (β := fun (v : U) ↦ Path.{u, u_1} u v)))
            (φ.mapPath (p.snd (β := fun (v : U) ↦ Path.{u, u_1} u v))))
        (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) y₁ (p₁.cons e₁)))
      ((fun (p : PathStar.{u, u_1} u) ↦
          Sigma.mk (β := fun (v : V) ↦ Path.{v, u_2} (φ.obj u) v) (φ.obj (p.fst (β := fun (v : U) ↦ Path.{u, u_1} u v)))
            (φ.mapPath (p.snd (β := fun (v : U) ↦ Path.{u, u_1} u v))))
        (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) y₂ (p₂.cons e₂))) →
    Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) y₁ (p₁.cons e₁) =
      Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) y₂ (p₂.cons e₂)
Tactic: rcases p₂ with - | ⟨p₂, e₂⟩
Cleared hypotheses: p₂