-- Mathlib/Combinatorics/Quiver/Covering.lean
theorem Prefunctor.pathStar_injective (hφ : ∀ u, Injective (φ.star u)) (u : U) :
    Injective (φ.pathStar u)

Proof state:
case mk.cons.mk.cons.intro.refl
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨x₁, p₁⟩ = (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨x₁, p₁⟩ = a₂
y₂ : U
hφy : φ.obj y₁ = φ.obj y₂
e₂ : x₁ ⟶ y₂
hφx : φ.obj x₁ = φ.obj x₁
hφe : HEq (φ.map e₁) (φ.map e₂)
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₁).cons (φ.map e₂)
hφp : HEq (φ.mapPath p₁) (φ.mapPath p₁)
h_path_star : φ.pathStar u ⟨x₁, p₁⟩ = φ.pathStar u ⟨x₁, p₁⟩
⊢ ⟨y₁, p₁.cons e₁⟩ = ⟨y₂, p₁.cons 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⟩

Result:
case mk.cons.mk.cons.intro.refl
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨x₁, p₁⟩ = (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨x₁, p₁⟩ = a₂
y₂ : U
hφy : φ.obj y₁ = φ.obj y₂
e₂ : x₁ ⟶ y₂
hφx : φ.obj x₁ = φ.obj x₁
hφe : HEq (φ.map e₁) (φ.map e₂)
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₁).cons (φ.map e₂)
hφp : HEq (φ.mapPath p₁) (φ.mapPath p₁)
h_path_star : φ.pathStar u ⟨x₁, p₁⟩ = φ.pathStar u ⟨x₁, p₁⟩
h_star : φ.star x₁ ⟨y₁, e₁⟩ = φ.star x₁ ⟨y₂, e₂⟩
⊢ ⟨y₁, p₁.cons e₁⟩ = ⟨y₂, p₁.cons e₂⟩

Proof state:
case mk.cons.mk.cons.intro
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨x₁, p₁⟩ = (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨x₁, p₁⟩ = a₂
y₂ x₂ : U
p₂ : Path 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 : HEq (φ.mapPath p₁) (φ.mapPath p₂)
hφe : HEq (φ.map e₁) (φ.map e₂)
h_path_star : φ.pathStar u ⟨x₁, p₁⟩ = φ.pathStar u ⟨x₂, p₂⟩
⊢ ⟨y₁, p₁.cons e₁⟩ = ⟨y₂, p₂.cons e₂⟩

Tactic:
cases ih h_path_star

Result:
case mk.cons.mk.cons.intro.refl
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨x₁, p₁⟩ = (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨x₁, p₁⟩ = a₂
y₂ : U
hφy : φ.obj y₁ = φ.obj y₂
e₂ : x₁ ⟶ y₂
hφx : φ.obj x₁ = φ.obj x₁
hφe : HEq (φ.map e₁) (φ.map e₂)
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₁).cons (φ.map e₂)
hφp : HEq (φ.mapPath p₁) (φ.mapPath p₁)
h_path_star : φ.pathStar u ⟨x₁, p₁⟩ = φ.pathStar u ⟨x₁, p₁⟩
⊢ ⟨y₁, p₁.cons e₁⟩ = ⟨y₂, p₁.cons e₂⟩

Proof state:
case mk.cons.mk.cons.intro.refl.refl
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨x₁, p₁⟩ = (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨x₁, p₁⟩ = a₂
hφx : φ.obj x₁ = φ.obj x₁
hφp : HEq (φ.mapPath p₁) (φ.mapPath p₁)
h_path_star : φ.pathStar u ⟨x₁, p₁⟩ = φ.pathStar u ⟨x₁, p₁⟩
hφy : φ.obj y₁ = φ.obj y₁
hφe : HEq (φ.map e₁) (φ.map e₁)
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₁).cons (φ.map e₁)
h_star : φ.star x₁ ⟨y₁, e₁⟩ = φ.star x₁ ⟨y₁, e₁⟩
⊢ ⟨y₁, p₁.cons e₁⟩ = ⟨y₁, p₁.cons e₁⟩

Tactic:
rfl

Result:
no goals

Proof state:
case mk.nil.mk.nil
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ : U
a✝ : (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨u, Path.nil⟩ = (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨u, Path.nil⟩
⊢ ⟨u, Path.nil⟩ = ⟨u, Path.nil⟩

Tactic:
rfl

Result:
no goals

Proof state:
case mk.nil.mk
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ y₂ : U
p₂ : Path u y₂
⊢ (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨u, Path.nil⟩ = (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨y₂, p₂⟩ →
    ⟨u, Path.nil⟩ = ⟨y₂, p₂⟩

Tactic:
rcases p₂ with - | ⟨p₂, e₂⟩

Result:
case mk.nil.mk.nil
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ : U
⊢ (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨u, Path.nil⟩ = (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨u, Path.nil⟩ →
    ⟨u, Path.nil⟩ = ⟨u, Path.nil⟩

case mk.nil.mk.cons
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ y₂ b✝ : U
p₂ : Path u b✝
e₂ : b✝ ⟶ y₂
⊢ (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨u, Path.nil⟩ = (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨y₂, p₂.cons e₂⟩ →
    ⟨u, Path.nil⟩ = ⟨y₂, p₂.cons e₂⟩

Proof state:
case mk.cons.mk.cons.intro
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨x₁, p₁⟩ = (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨x₁, p₁⟩ = a₂
y₂ x₂ : U
p₂ : Path 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 : HEq (φ.mapPath p₁) (φ.mapPath p₂)
⊢ ⟨y₁, p₁.cons e₁⟩ = ⟨y₂, p₂.cons e₂⟩

Tactic:
have hφe := HEq.trans (Hom.cast_heq rfl hφy _).symm (Path.hom_heq_of_cons_eq_cons h')

Result:
case mk.cons.mk.cons.intro
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨x₁, p₁⟩ = (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨x₁, p₁⟩ = a₂
y₂ x₂ : U
p₂ : Path 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 : HEq (φ.mapPath p₁) (φ.mapPath p₂)
hφe : HEq (φ.map e₁) (φ.map e₂)
⊢ ⟨y₁, p₁.cons e₁⟩ = ⟨y₂, p₂.cons e₂⟩

Proof state:
case mk.nil.mk.cons.intro
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ y₂ b✝ : U
p₂ : Path 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'

Result:
no goals

Proof state:
case mk.nil.mk.cons.intro
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ y₂ b✝ : U
p₂ : Path u b✝
e₂ : b✝ ⟶ y₂
h : φ.obj u = φ.obj y₂
h' : HEq (φ.mapPath Path.nil) ((φ.mapPath p₂).cons (φ.map e₂))
⊢ False

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

Result:
case mk.nil.mk.cons.intro
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ y₂ b✝ : U
p₂ : Path u b✝
e₂ : b✝ ⟶ y₂
h : φ.obj u = φ.obj y₂
h' : φ.mapPath Path.nil = (Path.cast ⋯ ⋯ (φ.mapPath p₂)).cons (Hom.cast ⋯ ⋯ (φ.map e₂))
⊢ False