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
u v : U
p : Path.{u, u_1} u v
⊢ φ.pathStar u (PathStar.mk p) = PathStar.mk (φ.mapPath p)

Tactic:
rfl

Premises used: Prefunctor.pathStar, 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), Injective (φ.star u)
u v₁ y₂ : U
p₂ : Path.{u, u_1} u y₂
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) u Path.nil))
      ((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)) →
    Eq (α := PathStar.{u, u_1} u) (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) u Path.nil)
nil₁ :
  ∀ {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) u Path.nil))
        ((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) u Path.nil =
        Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) y₂ (p₂.cons e₂)
⊢ 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))
      ((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) u Path.nil = Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) y₂ p₂

Tactic:
rcases p₂ with - | ⟨p₂, 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₁ : U
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))
    ((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))
⊢ Eq (α := PathStar.{u, u_1} u) (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) u Path.nil)

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), Injective (φ.star u)
u v₁ y₂ b : U
p₂ : Path.{u, u_1} u b
e₂ : b ⟶ y₂
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))
    ((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₂)))
⊢ φ.obj u = φ.obj y₂ ∧
    HEq (α := Path.{v, u_2} (φ.obj u) (φ.obj u)) (φ.mapPath Path.nil) ((φ.mapPath p₂).cons (φ.map e₂))

Tactic:
simp only [mapPath_cons, Sigma.mk.inj_iff] at h

Premises used: Sigma.mk.inj_iff, Prefunctor.mapPath_cons
-- 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₁ y₂ b : U
p₂ : Path.{u, u_1} u b
e₂ : b ⟶ y₂
h :
  φ.obj u = φ.obj y₂ ∧
    HEq (α := Path.{v, u_2} (φ.obj u) (φ.obj u)) (φ.mapPath Path.nil) ((φ.mapPath p₂).cons (φ.map e₂))
nil : False
⊢ 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₂)

Tactic:
exfalso
-- 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₁ y₂ b : U
p₂ : Path.{u, u_1} u b
e₂ : b ⟶ y₂
h :
  φ.obj u = φ.obj y₂ ∧
    HEq (α := Path.{v, u_2} (φ.obj u) (φ.obj u)) (φ.mapPath Path.nil) ((φ.mapPath p₂).cons (φ.map e₂))
⊢ φ.obj u = φ.obj y₂

Tactic:
obtain ⟨h, h'⟩ := 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₁ y₂ b : U
p₂ : Path.{u, u_1} u b
e₂ : b ⟶ y₂
h :
  φ.obj u = φ.obj y₂ ∧
    HEq (α := Path.{v, u_2} (φ.obj u) (φ.obj u)) (φ.mapPath Path.nil) ((φ.mapPath p₂).cons (φ.map e₂))
h₁ : φ.obj u = φ.obj y₂
⊢ HEq (α := Path.{v, u_2} (φ.obj u) (φ.obj u)) (φ.mapPath Path.nil) ((φ.mapPath p₂).cons (φ.map e₂))

Tactic:
obtain ⟨h, h'⟩ := 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₁ y₂ b : U
p₂ : Path.{u, u_1} u b
e₂ : b ⟶ y₂
h : φ.obj u = φ.obj y₂
h' : HEq (α := Path.{v, u_2} (φ.obj u) (φ.obj u)) (φ.mapPath Path.nil) ((φ.mapPath p₂).cons (φ.map e₂))
⊢ φ.mapPath Path.nil = (Path.cast ⋯ ⋯ (φ.mapPath p₂)).cons (Hom.cast ⋯ ⋯ (φ.map e₂))

Tactic:
rw [← Path.eq_cast_iff_heq rfl h.symm, Path.cast_cons] at h'

Premises used: Quiver.Path.eq_cast_iff_heq, Quiver.Path.cast_cons, Eq.symm, 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), Injective (φ.star u)
u v₁ y₂ b : U
p₂ : Path.{u, u_1} u b
e₂ : b ⟶ y₂
h : φ.obj u = φ.obj y₂
h' : φ.mapPath Path.nil = (Path.cast ⋯ ⋯ (φ.mapPath p₂)).cons (Hom.cast ⋯ ⋯ (φ.map e₂))
⊢ False

Tactic:
(Path.nil_ne_cons _ _) h'

Premises used: Quiver.Path.nil_ne_cons
-- 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₁ y₂ b : U
p₂ : Path.{u, u_1} u b
e₂ : b ⟶ y₂
h : φ.obj u = φ.obj y₂
h' : φ.mapPath Path.nil = (Path.cast ⋯ ⋯ (φ.mapPath p₂)).cons (Hom.cast ⋯ ⋯ (φ.map e₂))
⊢ False

Tactic:
exact (Path.nil_ne_cons _ _) h'

Premises used: Quiver.Path.nil_ne_cons
-- 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 :
  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))
⊢ φ.obj y₁ = φ.obj u ∧
    HEq ((φ.mapPath p₁).cons (φ.map e₁)) (β := Path.{v, u_2} (φ.obj u) (φ.obj u)) (φ.mapPath Path.nil)

Tactic:
simp only [mapPath_cons, Sigma.mk.inj_iff] at h

Premises used: Sigma.mk.inj_iff, Prefunctor.mapPath_cons
-- 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 :
  φ.obj y₁ = φ.obj u ∧
    HEq ((φ.mapPath p₁).cons (φ.map e₁)) (β := Path.{v, u_2} (φ.obj u) (φ.obj u)) (φ.mapPath Path.nil)
cons : False
⊢ 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

Tactic:
exfalso
-- 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 :
  φ.obj y₁ = φ.obj u ∧
    HEq ((φ.mapPath p₁).cons (φ.map e₁)) (β := Path.{v, u_2} (φ.obj u) (φ.obj u)) (φ.mapPath Path.nil)
⊢ φ.obj y₁ = φ.obj u

Tactic:
obtain ⟨h, h'⟩ := 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₂
h :
  φ.obj y₁ = φ.obj u ∧
    HEq ((φ.mapPath p₁).cons (φ.map e₁)) (β := Path.{v, u_2} (φ.obj u) (φ.obj u)) (φ.mapPath Path.nil)
h₁ : φ.obj y₁ = φ.obj u
⊢ HEq ((φ.mapPath p₁).cons (φ.map e₁)) (β := Path.{v, u_2} (φ.obj u) (φ.obj u)) (φ.mapPath Path.nil)

Tactic:
obtain ⟨h, h'⟩ := 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₂
h : φ.obj y₁ = φ.obj u
h' : HEq ((φ.mapPath p₁).cons (φ.map e₁)) (β := Path.{v, u_2} (φ.obj u) (φ.obj u)) (φ.mapPath Path.nil)
⊢ (Path.cast ⋯ ⋯ (φ.mapPath p₁)).cons (Hom.cast ⋯ h (φ.map e₁)) = φ.mapPath Path.nil

Tactic:
rw [← Path.cast_eq_iff_heq rfl h, Path.cast_cons] at h'

Premises used: Quiver.Path.cast_cons, Quiver.Path.cast_eq_iff_heq, 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), 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 : φ.obj y₁ = φ.obj u
h' : (Path.cast ⋯ ⋯ (φ.mapPath p₁)).cons (Hom.cast ⋯ h (φ.map e₁)) = φ.mapPath Path.nil
⊢ False

Tactic:
(Path.cons_ne_nil _ _) h'

Premises used: Quiver.Path.cons_ne_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), 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 : φ.obj y₁ = φ.obj u
h' : (Path.cast ⋯ ⋯ (φ.mapPath p₁)).cons (Hom.cast ⋯ h (φ.map e₁)) = φ.mapPath Path.nil
⊢ False

Tactic:
exact (Path.cons_ne_nil _ _) h'

Premises used: Quiver.Path.cons_ne_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), 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 :
  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₂)))
⊢ φ.obj y₁ = φ.obj y₂ ∧ (φ.mapPath p₁).cons (φ.map e₁) ≍ (φ.mapPath p₂).cons (φ.map e₂)

Tactic:
simp only [mapPath_cons, Sigma.mk.inj_iff] at h

Premises used: Sigma.mk.inj_iff, Prefunctor.mapPath_cons
-- 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 : φ.obj y₁ = φ.obj y₂ ∧ (φ.mapPath p₁).cons (φ.map e₁) ≍ (φ.mapPath p₂).cons (φ.map e₂)
⊢ φ.obj y₁ = φ.obj y₂

Tactic:
obtain ⟨hφy, h'⟩ := 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 : φ.obj y₁ = φ.obj y₂ ∧ (φ.mapPath p₁).cons (φ.map e₁) ≍ (φ.mapPath p₂).cons (φ.map e₂)
hφy : φ.obj y₁ = φ.obj y₂
⊢ (φ.mapPath p₁).cons (φ.map e₁) ≍ (φ.mapPath p₂).cons (φ.map e₂)

Tactic:
obtain ⟨hφy, h'⟩ := 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 (φ.map e₁) ≍ (φ.mapPath p₂).cons (φ.map e₂)
⊢ (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)

Tactic:
rw [← Path.cast_eq_iff_heq rfl hφy, Path.cast_cons, Path.cast_rfl_rfl] at h'

Premises used: Quiver.Path.cast_cons, Quiver.Path.cast_eq_iff_heq, Quiver.Path.cast_rfl_rfl, rfl