awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Quiver.Covering
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₂ x₂ : U
p₂ : Path.{u, u_1} u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)
⊢ φ.obj x₁ = φ.obj x₂

Tactic:
have hφx := Path.obj_eq_of_cons_eq_cons h'
-- Module: Mathlib.Combinatorics.Quiver.Covering
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₂ x₂ : U
p₂ : Path.{u, u_1} u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
⊢ φ.mapPath p₁ ≍ φ.mapPath p₂

Tactic:
have hφp := Path.heq_of_cons_eq_cons h'
-- Module: Mathlib.Combinatorics.Quiver.Covering
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₂ x₂ : U
p₂ : Path.{u, u_1} u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : φ.mapPath p₁ ≍ φ.mapPath p₂
⊢ φ.map e₁ ≍ φ.map e₂

Tactic:
have hφe := HEq.trans (Hom.cast_heq rfl hφy _).symm (Path.hom_heq_of_cons_eq_cons h')
-- Module: Mathlib.Combinatorics.Quiver.Covering
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₂ x₂ : U
p₂ : Path.{u, u_1} u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : φ.mapPath p₁ ≍ φ.mapPath p₂
hφe : φ.map e₁ ≍ φ.map e₂
simp : φ.obj x₁ = φ.obj x₂ ∧ φ.mapPath p₁ ≍ φ.mapPath p₂
⊢ φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁) =
    φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₂ p₂)

Tactic:
simp only [Prefunctor.pathStar_apply, Sigma.mk.inj_iff]

Premises used: Prefunctor.pathStar_apply, Sigma.mk.inj_iff
-- Module: Mathlib.Combinatorics.Quiver.Covering
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₂ x₂ : U
p₂ : Path.{u, u_1} u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : φ.mapPath p₁ ≍ φ.mapPath p₂
hφe : φ.map e₁ ≍ φ.map e₂
⊢ φ.obj x₁ = φ.obj x₂ ∧ φ.mapPath p₁ ≍ φ.mapPath p₂

Tactic:
⟨hφx, hφp⟩

Premises used: And.intro
-- Module: Mathlib.Combinatorics.Quiver.Covering
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₂ x₂ : U
p₂ : Path.{u, u_1} u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : φ.mapPath p₁ ≍ φ.mapPath p₂
hφe : φ.map e₁ ≍ φ.map e₂
⊢ φ.obj x₁ = φ.obj x₂ ∧ φ.mapPath p₁ ≍ φ.mapPath p₂

Tactic:
exact ⟨hφx, hφp⟩
-- Module: Mathlib.Combinatorics.Quiver.Covering
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₂ x₂ : U
p₂ : Path.{u, u_1} u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : φ.mapPath p₁ ≍ φ.mapPath p₂
hφe : φ.map e₁ ≍ φ.map e₂
⊢ φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁) =
    φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₂ p₂)

Tactic:
have h_path_star : φ.pathStar u ⟨x₁, p₁⟩ = φ.pathStar u ⟨x₂, p₂⟩ := by
        simp only [Prefunctor.pathStar_apply, Sigma.mk.inj_iff]; exact ⟨hφx, hφp⟩
-- Module: Mathlib.Combinatorics.Quiver.Covering
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₂ x₂ : U
p₂ : Path.{u, u_1} u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : φ.mapPath p₁ ≍ φ.mapPath p₂
hφe : φ.map e₁ ≍ φ.map e₂
h_path_star :
  φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁) =
    φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₂ p₂)
cons :
  ∀ (e₂ : x₁ ⟶ y₂) (hφx : φ.obj x₁ = φ.obj x₁) (hφe : φ.map e₁ ≍ φ.map e₂)
    (h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₁).cons (φ.map e₂))
    (hφp : φ.mapPath p₁ ≍ φ.mapPath p₁)
    (h_path_star :
      φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁) =
        φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ 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₁.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:
cases ih h_path_star
-- Module: Mathlib.Combinatorics.Quiver.Covering
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
hφy : φ.obj y₁ = φ.obj y₂
e₂ : x₁ ⟶ y₂
hφx : φ.obj x₁ = φ.obj x₁
hφe : φ.map e₁ ≍ φ.map e₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₁).cons (φ.map e₂)
hφp : φ.mapPath p₁ ≍ φ.mapPath p₁
h_path_star :
  φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁) =
    φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁)
simp : φ.obj y₁ = φ.obj y₂ ∧ φ.map e₁ ≍ φ.map e₂
⊢ φ.star x₁ (Sigma.mk (β := fun (v : U) ↦ x₁ ⟶ v) y₁ e₁) = φ.star x₁ (Sigma.mk (β := fun (v : U) ↦ x₁ ⟶ v) y₂ e₂)

Tactic:
simp only [Prefunctor.star_apply, Sigma.mk.inj_iff]

Premises used: Prefunctor.star_apply, Sigma.mk.inj_iff
-- Module: Mathlib.Combinatorics.Quiver.Covering
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
hφy : φ.obj y₁ = φ.obj y₂
e₂ : x₁ ⟶ y₂
hφx : φ.obj x₁ = φ.obj x₁
hφe : φ.map e₁ ≍ φ.map e₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₁).cons (φ.map e₂)
hφp : φ.mapPath p₁ ≍ φ.mapPath p₁
h_path_star :
  φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁) =
    φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁)
⊢ φ.obj y₁ = φ.obj y₂ ∧ φ.map e₁ ≍ φ.map e₂

Tactic:
⟨hφy, hφe⟩

Premises used: And.intro
-- Module: Mathlib.Combinatorics.Quiver.Covering
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
hφy : φ.obj y₁ = φ.obj y₂
e₂ : x₁ ⟶ y₂
hφx : φ.obj x₁ = φ.obj x₁
hφe : φ.map e₁ ≍ φ.map e₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₁).cons (φ.map e₂)
hφp : φ.mapPath p₁ ≍ φ.mapPath p₁
h_path_star :
  φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁) =
    φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁)
⊢ φ.obj y₁ = φ.obj y₂ ∧ φ.map e₁ ≍ φ.map e₂

Tactic:
exact ⟨hφy, hφe⟩
-- Module: Mathlib.Combinatorics.Quiver.Covering
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
hφy : φ.obj y₁ = φ.obj y₂
e₂ : x₁ ⟶ y₂
hφx : φ.obj x₁ = φ.obj x₁
hφe : φ.map e₁ ≍ φ.map e₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₁).cons (φ.map e₂)
hφp : φ.mapPath p₁ ≍ φ.mapPath p₁
h_path_star :
  φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁) =
    φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁)
⊢ φ.star x₁ (Sigma.mk (β := fun (v : U) ↦ x₁ ⟶ v) y₁ e₁) = φ.star x₁ (Sigma.mk (β := fun (v : U) ↦ x₁ ⟶ v) y₂ e₂)

Tactic:
have h_star : φ.star x₁ ⟨y₁, e₁⟩ = φ.star x₁ ⟨y₂, e₂⟩ := by
        simp only [Prefunctor.star_apply, Sigma.mk.inj_iff]; exact ⟨hφy, hφe⟩
-- Module: Mathlib.Combinatorics.Quiver.Covering
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
hφy : φ.obj y₁ = φ.obj y₂
e₂ : x₁ ⟶ y₂
hφx : φ.obj x₁ = φ.obj x₁
hφe : φ.map e₁ ≍ φ.map e₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₁).cons (φ.map e₂)
hφp : φ.mapPath p₁ ≍ φ.mapPath p₁
h_path_star :
  φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁) =
    φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁)
h_star : φ.star x₁ (Sigma.mk (β := fun (v : U) ↦ x₁ ⟶ v) y₁ e₁) = φ.star x₁ (Sigma.mk (β := fun (v : U) ↦ x₁ ⟶ v) y₂ e₂)
cons :
  ∀ (hφy : φ.obj y₁ = φ.obj y₁) (hφe : φ.map e₁ ≍ φ.map e₁)
    (h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₁).cons (φ.map e₁))
    (h_star :
      φ.star x₁ (Sigma.mk (β := fun (v : U) ↦ x₁ ⟶ v) y₁ e₁) = φ.star x₁ (Sigma.mk (β := fun (v : U) ↦ x₁ ⟶ v) y₁ 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₁)
⊢ 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:
cases hφ x₁ h_star
-- Module: Mathlib.Combinatorics.Quiver.Covering
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₂
hφx : φ.obj x₁ = φ.obj x₁
hφp : φ.mapPath p₁ ≍ φ.mapPath p₁
h_path_star :
  φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁) =
    φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁)
hφy : φ.obj y₁ = φ.obj y₁
hφe : φ.map e₁ ≍ φ.map e₁
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₁).cons (φ.map e₁)
h_star : φ.star x₁ (Sigma.mk (β := fun (v : U) ↦ x₁ ⟶ v) y₁ e₁) = φ.star x₁ (Sigma.mk (β := fun (v : U) ↦ x₁ ⟶ v) y₁ 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:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Covering
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), Surjective (φ.star u)
u : U
v : V
h :
  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) u Path.nil))
    (Sigma.mk (β := fun (v : V) ↦ Path.{v, u_2} (φ.obj u) v) (φ.obj u) Path.nil)
⊢ ∃ (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))))
        a)
      (Sigma.mk (β := fun (v : V) ↦ Path.{v, u_2} (φ.obj u) v) (φ.obj u) Path.nil)

Tactic:
use ⟨u, Path.nil⟩
-- Module: Mathlib.Combinatorics.Quiver.Covering
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), Surjective (φ.star u)
u : U
v : V
⊢ 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) u Path.nil))
    (Sigma.mk (β := fun (v : V) ↦ Path.{v, u_2} (φ.obj u) v) (φ.obj u) Path.nil)

Tactic:
simp only [Prefunctor.mapPath_nil]

Premises used: Prefunctor.mapPath_nil