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), Surjective (φ.star u)
u : U
v b c : V
p' : Path.{v, u_2} (φ.obj u) b
ev : b ⟶ c
ih :
  ∃ (a : PathStar.{u, u_1} 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) b p'
cons :
  ∀ (u' : U) (q' : Path.{u, u_1} u u')
    (h :
      (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' q') =
        Sigma.mk (β := fun (v : V) ↦ Path.{v, u_2} (φ.obj u) v) b p'),
    ∃ (a : PathStar.{u, u_1} 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) c (p'.cons ev)
⊢ ∃ (a : PathStar.{u, u_1} 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) c (p'.cons ev)

Tactic:
obtain ⟨⟨u', q'⟩, h⟩ := ih
-- 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 b c : V
p' : Path.{v, u_2} (φ.obj u) b
ev : b ⟶ c
u' : U
q' : Path.{u, u_1} u u'
h :
  Sigma.mk (β := fun (v : V) ↦ Path.{v, u_2} (φ.obj u) v) (φ.obj u') (φ.mapPath q') =
    Sigma.mk (β := fun (v : V) ↦ Path.{v, u_2} (φ.obj u) v) b p'
cons :
  ∀ (ev : φ.obj u' ⟶ c),
    ∃ (a : PathStar.{u, u_1} 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) c ((φ.mapPath q').cons ev)
⊢ ∃ (a : PathStar.{u, u_1} 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) c (p'.cons ev)

Tactic:
obtain ⟨rfl, rfl⟩ := h

Premises used: 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 c : V
u' : U
q' : Path.{u, u_1} u u'
ev : φ.obj u' ⟶ c
cons :
  ∀ (u'' : U) (eu : u' ⟶ u'')
    (k : φ.star u' (Sigma.mk (β := fun (v : U) ↦ u' ⟶ v) u'' eu) = Sigma.mk (β := fun (v : V) ↦ φ.obj u' ⟶ v) c ev),
    ∃ (a : PathStar.{u, u_1} 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) c ((φ.mapPath q').cons ev)
⊢ ∃ (a : PathStar.{u, u_1} 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) c ((φ.mapPath q').cons ev)

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

Premises used: Sigma.mk
-- 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 c : V
u' : U
q' : Path.{u, u_1} u u'
ev : φ.obj u' ⟶ c
u'' : U
eu : u' ⟶ u''
k : φ.star u' (Sigma.mk (β := fun (v : U) ↦ u' ⟶ v) u'' eu) = Sigma.mk (β := fun (v : V) ↦ φ.obj u' ⟶ v) c ev
⊢ φ.obj u'' = c ∧ φ.map eu ≍ ev

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

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), Surjective (φ.star u)
u : U
v c : V
u' : U
q' : Path.{u, u_1} u u'
ev : φ.obj u' ⟶ c
u'' : U
eu : u' ⟶ u''
k : φ.obj u'' = c ∧ φ.map eu ≍ ev
cons :
  ∀ (ev : φ.obj u' ⟶ φ.obj u'') (k : φ.map eu ≍ ev),
    ∃ (a : PathStar.{u, u_1} 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'') ((φ.mapPath q').cons ev)
⊢ ∃ (a : PathStar.{u, u_1} 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) c ((φ.mapPath q').cons ev)

Tactic:
obtain ⟨rfl, k⟩ := k

Premises used: 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
u' : U
q' : Path.{u, u_1} u u'
u'' : U
eu : u' ⟶ u''
ev : φ.obj u' ⟶ φ.obj u''
k : φ.map eu ≍ ev
⊢ φ.map eu = ev

Tactic:
simp only [heq_eq_eq] at k

Premises used: heq_eq_eq
-- 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
u' : U
q' : Path.{u, u_1} u u'
u'' : U
eu : u' ⟶ u''
ev : φ.obj u' ⟶ φ.obj u''
k : φ.map eu = ev
cons :
  ∃ (a : PathStar.{u, u_1} 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'') ((φ.mapPath q').cons (φ.map eu))
⊢ ∃ (a : PathStar.{u, u_1} 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'') ((φ.mapPath q').cons ev)

Tactic:
subst k
-- 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
u' : U
q' : Path.{u, u_1} u u'
u'' : U
eu : u' ⟶ u''
h :
  (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'' (q'.cons eu)) =
    Sigma.mk (β := fun (v : V) ↦ Path.{v, u_2} (φ.obj u) v) (φ.obj u'') ((φ.mapPath q').cons (φ.map eu))
⊢ ∃ (a : PathStar.{u, u_1} 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'') ((φ.mapPath q').cons (φ.map eu))

Tactic:
use ⟨_, q'.cons eu⟩
-- 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
u' : U
q' : Path.{u, u_1} u u'
u'' : U
eu : u' ⟶ 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'' (q'.cons eu)) =
    Sigma.mk (β := fun (v : V) ↦ Path.{v, u_2} (φ.obj u) v) (φ.obj u'') ((φ.mapPath q').cons (φ.map eu))

Tactic:
simp only [Prefunctor.mapPath_cons]

Premises used: 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), Surjective (φ.star u)
u : U
v : V
p : Path.{v, u_2} (φ.obj u) v
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)
cons :
  ∀ {b c : V} (p' : Path.{v, u_2} (φ.obj u) b) (ev : b ⟶ c)
    (ih :
      ∃ (a : PathStar.{u, u_1} 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) b p'),
    ∃ (a : PathStar.{u, u_1} 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) c (p'.cons ev)
⊢ ∃ (a : PathStar.{u, u_1} 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) v p

Tactic:
induction p with
  | nil =>
    use ⟨u, Path.nil⟩
    simp only [Prefunctor.mapPath_nil]
  | 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
    -- Porting note: was `obtain ⟨rfl, rfl⟩ := k`
    obtain ⟨rfl, k⟩ := k
    simp only [heq_eq_eq] at k
    subst k
    use ⟨_, q'.cons eu⟩
    simp only [Prefunctor.mapPath_cons]

Premises used: heq_eq_eq, Prefunctor.mapPath_nil, Prefunctor.star_apply, Sigma.mk.inj_iff, Prefunctor.mapPath_cons, 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), Bijective (φ.star u)
u : U
⊢ Bijective (φ.pathStar u)

Tactic:
⟨φ.pathStar_injective (fun u => (hφ u).1) _, φ.pathStar_surjective (fun u => (hφ u).2) _⟩

Premises used: Prefunctor.pathStar_surjective, Prefunctor.pathStar_injective, And.right, And.left, And.intro, Function.Bijective
-- 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φ : φ.IsCovering
u : U
⊢ Bijective (φ.pathStar u)

Tactic:
φ.pathStar_bijective hφ.1 u

Premises used: Prefunctor.IsCovering.star_bijective, Prefunctor.pathStar_bijective
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type ?u.14854
inst_1 : Quiver.{v, ?u.14854} V
φ : Prefunctor.{u, v, u_1, ?u.14854} U V
W : Type ?u.14880
inst_2 : Quiver.{w, ?u.14880} W
ψ : Prefunctor.{v, w, ?u.14854, ?u.14880} V W
inst_3 : HasInvolutiveReverse.{u, u_1} U
inst_4 : HasInvolutiveReverse.{v, ?u.14854} V
u : U
e : Star.{u, u_1} u
⊢ (fun (e : Costar.{u, u_1} u) ↦
        Sigma.mk (β := fun (v : U) ↦ u ⟶ v) (e.fst (β := fun (u_1 : U) ↦ u_1 ⟶ u))
          (reverse (e.snd (β := fun (u_1 : U) ↦ u_1 ⟶ u))))
      ((fun (e : Star.{u, u_1} u) ↦
          (Sigma.mk (β := fun (u_1 : U) ↦ u_1 ⟶ u) (e.fst (β := fun (v : U) ↦ u ⟶ v))
              (reverse (e.snd (β := fun (v : U) ↦ u ⟶ v))) :
            (u_1 : U) × (u_1 ⟶ u)))
        e) =
    e

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type ?u.14854
inst_1 : Quiver.{v, ?u.14854} V
φ : Prefunctor.{u, v, u_1, ?u.14854} U V
W : Type ?u.14880
inst_2 : Quiver.{w, ?u.14880} W
ψ : Prefunctor.{v, w, ?u.14854, ?u.14880} V W
inst_3 : HasInvolutiveReverse.{u, u_1} U
inst_4 : HasInvolutiveReverse.{v, ?u.14854} V
u : U
e : Costar.{u, u_1} u
⊢ (fun (e : Star.{u, u_1} u) ↦
        (Sigma.mk (β := fun (u_1 : U) ↦ u_1 ⟶ u) (e.fst (β := fun (v : U) ↦ u ⟶ v))
            (reverse (e.snd (β := fun (v : U) ↦ u ⟶ v))) :
          (u_1 : U) × (u_1 ⟶ u)))
      ((fun (e : Costar.{u, u_1} u) ↦
          Sigma.mk (β := fun (v : U) ↦ u ⟶ v) (e.fst (β := fun (u_1 : U) ↦ u_1 ⟶ u))
            (reverse (e.snd (β := fun (u_1 : U) ↦ u_1 ⟶ u))))
        e) =
    e

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
inst_1 : HasInvolutiveReverse.{u, u_1} U
u v : U
e : u ⟶ v
⊢ (starEquivCostar u : (a : Star u) → Costar u) (Star.mk e) = Costar.mk (reverse e)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
inst_1 : HasInvolutiveReverse.{u, u_1} U
u v : U
e : u ⟶ v
⊢ (Equiv.symm (starEquivCostar v) : (a : Costar v) → Star v) (Costar.mk e) = Star.mk (reverse e)

Tactic:
rfl

Premises used: 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
inst_2 : HasInvolutiveReverse.{u, u_1} U
inst_3 : HasInvolutiveReverse.{v, u_2} V
inst_4 : φ.MapReverse
u : U
h :
  ∀ (v : U) (f : v ⟶ u),
    (φ.costar u (Sigma.mk (β := fun (u_1 : U) ↦ u_1 ⟶ u) v f)).fst (β := fun (u_1 : V) ↦ u_1 ⟶ φ.obj u) =
      Sigma.fst (β := fun (u_1 : V) ↦ u_1 ⟶ φ.obj u)
        (Function.comp (α := Costar.{u, u_1} u) (⇑(starEquivCostar (φ.obj u)) : (a : Star (φ.obj u)) → Costar (φ.obj u))
          (φ.star u ∘ (⇑(Equiv.symm (starEquivCostar u)) : (a : Costar u) → Star u))
          (Sigma.mk (β := fun (u_1 : U) ↦ u_1 ⟶ u) v f))
h₁ :
  ∀ (v : U) (f : v ⟶ u),
    HEq ((φ.costar u (Sigma.mk (β := fun (u_1 : U) ↦ u_1 ⟶ u) v f)).snd (β := fun (u_1 : V) ↦ u_1 ⟶ φ.obj u)) (β :=
      Sigma.fst (β := fun (u_1 : V) ↦ u_1 ⟶ φ.obj u)
          (Function.comp (α := Costar.{u, u_1} u)
            (⇑(starEquivCostar (φ.obj u)) : (a : Star (φ.obj u)) → Costar (φ.obj u))
            (φ.star u ∘ (⇑(Equiv.symm (starEquivCostar u)) : (a : Costar u) → Star u))
            (Sigma.mk (β := fun (u_1 : U) ↦ u_1 ⟶ u) v f)) ⟶
        φ.obj u)
      (Sigma.snd (β := fun (u_1 : V) ↦ u_1 ⟶ φ.obj u)
          (Function.comp (α := Costar.{u, u_1} u)
            (⇑(starEquivCostar (φ.obj u)) : (a : Star (φ.obj u)) → Costar (φ.obj u))
            (φ.star u ∘ (⇑(Equiv.symm (starEquivCostar u)) : (a : Costar u) → Star u))
            (Sigma.mk (β := fun (u_1 : U) ↦ u_1 ⟶ u) v f)) :
        Sigma.fst (β := fun (u_1 : V) ↦ u_1 ⟶ φ.obj u)
            (Function.comp (α := Costar.{u, u_1} u)
              (⇑(starEquivCostar (φ.obj u)) : (a : Star (φ.obj u)) → Costar (φ.obj u))
              (φ.star u ∘ (⇑(Equiv.symm (starEquivCostar u)) : (a : Costar u) → Star u))
              (Sigma.mk (β := fun (u_1 : U) ↦ u_1 ⟶ u) v f)) ⟶
          φ.obj u)
⊢ φ.costar u =
    (⇑(starEquivCostar (φ.obj u)) : (a : Star (φ.obj u)) → Costar (φ.obj u)) ∘
      φ.star u ∘ (⇑(Equiv.symm (starEquivCostar u)) : (a : Costar u) → Star u)

Tactic:
ext ⟨v, f⟩
-- 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
inst_2 : HasInvolutiveReverse.{u, u_1} U
inst_3 : HasInvolutiveReverse.{v, u_2} V
inst_4 : φ.MapReverse
u v : U
f : v ⟶ u
⊢ (φ.costar u (Sigma.mk (β := fun (u_1 : U) ↦ u_1 ⟶ u) v f)).fst (β := fun (u_1 : V) ↦ u_1 ⟶ φ.obj u) =
    Sigma.fst (β := fun (u_1 : V) ↦ u_1 ⟶ φ.obj u)
      (Function.comp (α := Costar.{u, u_1} u) (⇑(starEquivCostar (φ.obj u)) : (a : Star (φ.obj u)) → Costar (φ.obj u))
        (φ.star u ∘ (⇑(Equiv.symm (starEquivCostar u)) : (a : Costar u) → Star u))
        (Sigma.mk (β := fun (u_1 : U) ↦ u_1 ⟶ u) v f))

Tactic:
simp
-- 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
inst_2 : HasInvolutiveReverse.{u, u_1} U
inst_3 : HasInvolutiveReverse.{v, u_2} V
inst_4 : φ.MapReverse
u v : U
f : v ⟶ u
⊢ HEq ((φ.costar u (Sigma.mk (β := fun (u_1 : U) ↦ u_1 ⟶ u) v f)).snd (β := fun (u_1 : V) ↦ u_1 ⟶ φ.obj u)) (β :=
    Sigma.fst (β := fun (u_1 : V) ↦ u_1 ⟶ φ.obj u)
        (Function.comp (α := Costar.{u, u_1} u) (⇑(starEquivCostar (φ.obj u)) : (a : Star (φ.obj u)) → Costar (φ.obj u))
          (φ.star u ∘ (⇑(Equiv.symm (starEquivCostar u)) : (a : Costar u) → Star u))
          (Sigma.mk (β := fun (u_1 : U) ↦ u_1 ⟶ u) v f)) ⟶
      φ.obj u)
    (Sigma.snd (β := fun (u_1 : V) ↦ u_1 ⟶ φ.obj u)
        (Function.comp (α := Costar.{u, u_1} u) (⇑(starEquivCostar (φ.obj u)) : (a : Star (φ.obj u)) → Costar (φ.obj u))
          (φ.star u ∘ (⇑(Equiv.symm (starEquivCostar u)) : (a : Costar u) → Star u))
          (Sigma.mk (β := fun (u_1 : U) ↦ u_1 ⟶ u) v f)) :
      Sigma.fst (β := fun (u_1 : V) ↦ u_1 ⟶ φ.obj u)
          (Function.comp (α := Costar.{u, u_1} u)
            (⇑(starEquivCostar (φ.obj u)) : (a : Star (φ.obj u)) → Costar (φ.obj u))
            (φ.star u ∘ (⇑(Equiv.symm (starEquivCostar u)) : (a : Costar u) → Star u))
            (Sigma.mk (β := fun (u_1 : U) ↦ u_1 ⟶ u) v f)) ⟶
        φ.obj u)

Tactic:
simp
-- 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
inst_2 : HasInvolutiveReverse.{u, u_1} U
inst_3 : HasInvolutiveReverse.{v, u_2} V
inst_4 : φ.MapReverse
u : U
rw :
  Bijective (α := Costar.{u, u_1} u) (β := Costar.{v, u_2} (φ.obj u))
      ((⇑(starEquivCostar (φ.obj u)) : (a : Star (φ.obj u)) → Costar (φ.obj u)) ∘
        φ.star u ∘ (⇑(Equiv.symm (starEquivCostar u)) : (a : Costar u) → Star u)) ↔
    Bijective (φ.star u)
rw₁ :
  Bijective (α := Costar.{u, u_1} u) (φ.star u ∘ (⇑(Equiv.symm (starEquivCostar u)) : (a : Costar u) → Star u)) ↔
    Bijective (φ.star u)
rw₂ rw₃ : Bijective (φ.star u) ↔ Bijective (φ.star u)
⊢ Bijective (φ.costar u) ↔ Bijective (φ.star u)

Tactic:
rw [Prefunctor.costar_conj_star φ, EquivLike.comp_bijective, EquivLike.bijective_comp]

Premises used: EquivLike.comp_bijective, Prefunctor.costar_conj_star, EquivLike.bijective_comp
-- 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
inst_2 : HasInvolutiveReverse.{u, u_1} U
inst_3 : HasInvolutiveReverse.{v, u_2} V
inst_4 : φ.MapReverse
h : ∀ (u : U), Bijective (φ.star u)
⊢ φ.IsCovering

Tactic:
⟨h, fun u => (φ.bijective_costar_iff_bijective_star u).2 (h u)⟩

Premises used: Iff.mpr, Prefunctor.IsCovering.mk, Prefunctor.bijective_costar_iff_bijective_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
inst_2 : HasInvolutiveReverse.{u, u_1} U
inst_3 : HasInvolutiveReverse.{v, u_2} V
inst_4 : φ.MapReverse
h : ∀ (u : U), Bijective (φ.costar u)
⊢ φ.IsCovering

Tactic:
⟨fun u => (φ.bijective_costar_iff_bijective_star u).1 (h u), h⟩

Premises used: Iff.mp, Prefunctor.IsCovering.mk, Prefunctor.bijective_costar_iff_bijective_star
-- Module: Mathlib.Combinatorics.Quiver.Path.Decomposition
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
h_len : p.length = 0
zero :
  ∀ (p : Path.{u_2, u_1} a a) (hb_in_S : a ∈ S) (h_len : p.length = 0),
    ∃ (u : V),
      ¬u ∈ S ∧
        ∃ (v : V),
          v ∈ S ∧
            ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v a), p = p₁.comp (e.toPath.comp p₂)
⊢ ∃ (u : V),
    ¬u ∈ S ∧
      ∃ (v : V),
        v ∈ S ∧
          ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)

Tactic:
obtain rfl := eq_of_length_zero p h_len

Premises used: Quiver.Path.eq_of_length_zero, rfl
-- Module: Mathlib.Combinatorics.Quiver.Path.Decomposition
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a : V
S : Set V
ha_not_in_S : ¬a ∈ S
p : Path.{u_2, u_1} a a
hb_in_S : a ∈ S
h_len : p.length = 0
⊢ ∃ (u : V),
    ¬u ∈ S ∧
      ∃ (v : V),
        v ∈ S ∧
          ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v a), p = p₁.comp (e.toPath.comp p₂)

Tactic:
(ha_not_in_S hb_in_S).elim

Premises used: False.elim
-- Module: Mathlib.Combinatorics.Quiver.Path.Decomposition
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a : V
S : Set V
ha_not_in_S : ¬a ∈ S
p : Path.{u_2, u_1} a a
hb_in_S : a ∈ S
h_len : p.length = 0
⊢ ∃ (u : V),
    ¬u ∈ S ∧
      ∃ (v : V),
        v ∈ S ∧
          ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v a), p = p₁.comp (e.toPath.comp p₂)

Tactic:
exact (ha_not_in_S hb_in_S).elim

Premises used: False.elim
-- Module: Mathlib.Combinatorics.Quiver.Path.Decomposition
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
n : ℕ
ih :
  ∀ {a b : V} (p : Path.{u_2, u_1} a b) (S : Set V) (ha_not_in_S : ¬a ∈ S) (hb_in_S : b ∈ S) (h_len : p.length = n),
    ∃ (u : V),
      ¬u ∈ S ∧
        ∃ (v : V),
          v ∈ S ∧
            ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
a b : V
p : Path.{u_2, u_1} a b
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
h_len : p.length = n + 1
⊢ 0 < p.length

Tactic:
simp [h_len]
-- Module: Mathlib.Combinatorics.Quiver.Path.Decomposition
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
n : ℕ
ih :
  ∀ {a b : V} (p : Path.{u_2, u_1} a b) (S : Set V) (ha_not_in_S : ¬a ∈ S) (hb_in_S : b ∈ S) (h_len : p.length = n),
    ∃ (u : V),
      ¬u ∈ S ∧
        ∃ (v : V),
          v ∈ S ∧
            ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
a b : V
p : Path.{u_2, u_1} a b
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
h_len : p.length = n + 1
⊢ 0 < p.length

Tactic:
have h_pos : 0 < p.length := by simp [h_len]