awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Covering (goal)
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
p₁ : Path.{u, u_1} u v₁
⊢ ∀ ⦃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) v₁ 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) v₁ p₁ = a₂
have 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))))
        (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))))
        a₂) →
    Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) u Path.nil = a₂
Tactic: induction p₁ with
  | nil =>
    rintro ⟨y₂, p₂⟩
    rcases p₂ with - | ⟨p₂, e₂⟩
    · intro; rfl -- Porting note: goal not present in lean3.
    · intro h
      simp only [mapPath_cons, Sigma.mk.inj_iff] at h
      exfalso
      obtain ⟨h, h'⟩ := h
      rw [← Path.eq_cast_iff_heq rfl h.symm, Path.cast_cons] at h'
      exact (Path.nil_ne_cons _ _) h'
  | cons p₁ e₁ ih =>
    rename_i x₁ y₁
    rintro ⟨y₂, p₂⟩
    rcases p₂ with - | ⟨p₂, e₂⟩
    · intro h
      simp only [mapPath_cons, Sigma.mk.inj_iff] at h
      exfalso
      obtain ⟨h, h'⟩ := h
      rw [← Path.cast_eq_iff_heq rfl h, Path.cast_cons] at h'
      exact (Path.cons_ne_nil _ _) h'
    · rename_i x₂
      intro h
      simp only [mapPath_cons, Sigma.mk.inj_iff] at h
      obtain ⟨hφy, h'⟩ := h
      rw [← Path.cast_eq_iff_heq rfl hφy, Path.cast_cons, Path.cast_rfl_rfl] at h'
      have hφx := Path.obj_eq_of_cons_eq_cons h'
      have hφp := Path.heq_of_cons_eq_cons h'
      have hφe := HEq.trans (Hom.cast_heq rfl hφy _).symm (Path.hom_heq_of_cons_eq_cons h')
      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⟩
      cases ih h_path_star
      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⟩
      cases hφ x₁ h_star
      rfl
Cleared hypotheses: p₁
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Covering (goal)
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
⊢ ∃ (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)
have 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)
Tactic: use ⟨u, Path.nil⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Covering (goal)
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'
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨⟨u', q'⟩, h⟩ := ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Covering (goal)
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'
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨rfl, rfl⟩ := h
Cleared hypotheses: b, p', ev, h
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Covering (goal)
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
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨⟨u'', eu⟩, k⟩ := hφ u' ⟨_, ev⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Covering (hypothesis)
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
⊢ ∃ (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)
have k₁ : φ.obj u'' = c ∧ φ.map eu ≍ ev
Tactic: simp only [star_apply, Sigma.mk.inj_iff] at k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Covering (goal)
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
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨rfl, k⟩ := k
Cleared hypotheses: c, ev, k
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Covering (hypothesis)
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
⊢ ∃ (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)
have k₁ : φ.map eu = ev
Tactic: simp only [heq_eq_eq] at k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Covering (goal)
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
⊢ ∃ (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)
have 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))
Tactic: subst k
Cleared hypotheses: ev, k
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Covering (goal)
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''
⊢ ∃ (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))
have 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))
Tactic: use ⟨_, q'.cons eu⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Covering (goal)
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
⊢ ∃ (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
have 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: 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]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Covering (goal)
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)
⊢ ∃ (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
have 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)
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]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Covering (goal)
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
⊢ φ.costar u =
    (⇑(starEquivCostar (φ.obj u)) : (a : Star (φ.obj u)) → Costar (φ.obj u)) ∘
      φ.star u ∘ (⇑(Equiv.symm (starEquivCostar u)) : (a : Costar u) → Star u)
have 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))
Tactic: ext ⟨v, f⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Covering (goal)
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))
⊢ φ.costar u =
    (⇑(starEquivCostar (φ.obj u)) : (a : Star (φ.obj u)) → Costar (φ.obj u)) ∘
      φ.star u ∘ (⇑(Equiv.symm (starEquivCostar u)) : (a : Costar u) → Star u)
have 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)
Tactic: ext ⟨v, f⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Covering (goal)
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
⊢ Bijective (φ.costar u) ↔ Bijective (φ.star u)
have 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)
Tactic: rw [Prefunctor.costar_conj_star φ, EquivLike.comp_bijective, EquivLike.bijective_comp]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Covering (goal)
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)
⊢ Bijective (φ.costar u) ↔ Bijective (φ.star u)
have rw₁ : Bijective (α := Costar.{u, u_1} u) (φ.star u ∘ (⇑(Equiv.symm (starEquivCostar u)) : (a : Costar u) → Star u)) ↔
  Bijective (φ.star u)
Tactic: rw [Prefunctor.costar_conj_star φ, EquivLike.comp_bijective, EquivLike.bijective_comp]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Covering (goal)
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)
⊢ Bijective (φ.costar u) ↔ Bijective (φ.star u)
have rw₂ : Bijective (φ.star u) ↔ Bijective (φ.star u)
Tactic: rw [Prefunctor.costar_conj_star φ, EquivLike.comp_bijective, EquivLike.bijective_comp]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Decomposition (goal)
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
⊢ ∃ (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₂)
have 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₂)
Tactic: obtain rfl := eq_of_length_zero p h_len
Cleared hypotheses: b, p, hb_in_S, h_len