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

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

Tactic:
simp only [Prefunctor.mapPath_nil, eq_self_iff_true, heq_iff_eq, and_self_iff]

Result:
no goals

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

Tactic:
induction p with
| nil =>
  use ⟨u, Path.nil⟩
  simp only [Prefunctor.mapPath_nil, eq_self_iff_true, heq_iff_eq, and_self_iff]
| cons p' ev ih =>
  obtain ⟨⟨u', q'⟩, h⟩ := ih
  simp only at h
  obtain ⟨rfl, rfl⟩ := h
  obtain ⟨⟨u'', eu⟩, k⟩ := hφ u' ⟨_, ev⟩
  simp only [star_apply, Sigma.mk.inj_iff] at k
  obtain ⟨rfl, k⟩ := k
  simp only [heq_eq_eq] at k
  subst k
  use ⟨_, q'.cons eu⟩
  simp only [Prefunctor.mapPath_cons, eq_self_iff_true, heq_iff_eq, and_self_iff]

Result:
no goals

Proof state:
case mk.cons.intro.mk.refl.intro.mk.intro
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v : V
u' : U
q' : Path u u'
u'' : U
eu : u' ⟶ u''
ev : φ.obj u' ⟶ φ.obj u''
k : HEq (φ.map eu) ev
⊢ ∃ a, (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨φ.obj u'', (φ.mapPath q').cons ev⟩

Tactic:
simp only [heq_eq_eq] at k

Result:
case mk.cons.intro.mk.refl.intro.mk.intro
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v : V
u' : U
q' : Path u u'
u'' : U
eu : u' ⟶ u''
ev : φ.obj u' ⟶ φ.obj u''
k : φ.map eu = ev
⊢ ∃ a, (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨φ.obj u'', (φ.mapPath q').cons ev⟩

Proof state:
case mk.cons.intro.mk.refl.intro.mk.intro
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v : V
u' : U
q' : Path u u'
u'' : U
eu : u' ⟶ u''
ev : φ.obj u' ⟶ φ.obj u''
k : φ.map eu = ev
⊢ ∃ a, (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨φ.obj u'', (φ.mapPath q').cons ev⟩

Tactic:
subst k

Result:
case mk.cons.intro.mk.refl.intro.mk.intro
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v : V
u' : U
q' : Path u u'
u'' : U
eu : u' ⟶ u''
⊢ ∃ a, (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨φ.obj u'', (φ.mapPath q').cons (φ.map eu)⟩

Proof state:
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
⊢ Surjective fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩

Tactic:
rintro ⟨v, p⟩

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

Proof state:
case mk.cons.intro.mk.refl.intro.mk
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v c✝ : V
u' : U
q' : Path u u'
ev : φ.obj u' ⟶ c✝
u'' : U
eu : u' ⟶ u''
k : φ.obj u'' = c✝ ∧ HEq (φ.map eu) ev
⊢ ∃ a, (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨c✝, (φ.mapPath q').cons ev⟩

Tactic:
obtain ⟨rfl, k⟩ := k

Result:
case mk.cons.intro.mk.refl.intro.mk.intro
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v : V
u' : U
q' : Path u u'
u'' : U
eu : u' ⟶ u''
ev : φ.obj u' ⟶ φ.obj u''
k : HEq (φ.map eu) ev
⊢ ∃ a, (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨φ.obj u'', (φ.mapPath q').cons ev⟩

Proof state:
case mk.cons.intro.mk.refl.intro.mk.intro
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v : V
u' : U
q' : Path u u'
u'' : U
eu : u' ⟶ u''
⊢ ∃ a, (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨φ.obj u'', (φ.mapPath q').cons (φ.map eu)⟩

Tactic:
use ⟨_, q'.cons eu⟩

Result:
case h
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v : V
u' : U
q' : Path u u'
u'' : U
eu : u' ⟶ u''
⊢ (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨u'', q'.cons eu⟩ = ⟨φ.obj u'', (φ.mapPath q').cons (φ.map eu)⟩

Proof state:
case mk.cons.intro.mk
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v b✝ c✝ : V
p' : Path (φ.obj u) b✝
ev : b✝ ⟶ c✝
u' : U
q' : Path u u'
h : ⟨φ.obj u', φ.mapPath q'⟩ = ⟨b✝, p'⟩
⊢ ∃ a, (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨c✝, p'.cons ev⟩

Tactic:
obtain ⟨rfl, rfl⟩ := h

Result:
case mk.cons.intro.mk.refl
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v c✝ : V
u' : U
q' : Path u u'
ev : φ.obj u' ⟶ c✝
⊢ ∃ a, (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨c✝, (φ.mapPath q').cons ev⟩

Proof state:
case mk.cons.intro.mk
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v b✝ c✝ : V
p' : Path (φ.obj u) b✝
ev : b✝ ⟶ c✝
u' : U
q' : Path u u'
h : (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨u', q'⟩ = ⟨b✝, p'⟩
⊢ ∃ a, (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨c✝, p'.cons ev⟩

Tactic:
simp only at h

Result:
case mk.cons.intro.mk
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v b✝ c✝ : V
p' : Path (φ.obj u) b✝
ev : b✝ ⟶ c✝
u' : U
q' : Path u u'
h : ⟨φ.obj u', φ.mapPath q'⟩ = ⟨b✝, p'⟩
⊢ ∃ a, (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨c✝, p'.cons ev⟩

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

Tactic:
use ⟨u, Path.nil⟩

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

Proof state:
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
⊢ Surjective (φ.pathStar u)

Tactic:
dsimp (config := { unfoldPartialApp := true }) [Prefunctor.pathStar, Quiver.PathStar.mk]

Result:
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
⊢ Surjective fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩

Proof state:
case h
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v : V
u' : U
q' : Path u u'
u'' : U
eu : u' ⟶ u''
⊢ (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨u'', q'.cons eu⟩ = ⟨φ.obj u'', (φ.mapPath q').cons (φ.map eu)⟩

Tactic:
simp only [Prefunctor.mapPath_cons, eq_self_iff_true, heq_iff_eq, and_self_iff]

Result:
no goals

Proof state:
case mk.cons.intro.mk.refl
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v c✝ : V
u' : U
q' : Path u u'
ev : φ.obj u' ⟶ c✝
⊢ ∃ a, (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨c✝, (φ.mapPath q').cons ev⟩

Tactic:
obtain ⟨⟨u'', eu⟩, k⟩ := hφ u' ⟨_, ev⟩

Result:
case mk.cons.intro.mk.refl.intro.mk
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v c✝ : V
u' : U
q' : Path u u'
ev : φ.obj u' ⟶ c✝
u'' : U
eu : u' ⟶ u''
k : φ.star u' ⟨u'', eu⟩ = ⟨c✝, ev⟩
⊢ ∃ a, (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨c✝, (φ.mapPath q').cons ev⟩