awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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), 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₂)))
⊢ 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) y₂ (p₂.cons e₂)
have h₁ : φ.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
Cleared hypotheses: h
-- 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), 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₂)
⊢ 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) y₂ (p₂.cons e₂)
have hφy : φ.obj y₁ = φ.obj y₂
Tactic: obtain ⟨hφy, h'⟩ := h
Cleared hypotheses: h
-- 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), 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₂
⊢ 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) y₂ (p₂.cons e₂)
have h' : (φ.mapPath p₁).cons (φ.map e₁) ≍ (φ.mapPath p₂).cons (φ.map e₂)
Tactic: obtain ⟨hφy, h'⟩ := h
Cleared hypotheses: h
-- 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), 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₂)
⊢ 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) y₂ (p₂.cons e₂)
have h'₁ : (φ.mapPath p₁).cons (Hom.cast sorry 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'
Cleared hypotheses: h'
-- 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), 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 (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)
⊢ 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) y₂ (p₂.cons e₂)
have hφx : φ.obj x₁ = φ.obj x₂
Tactic: have hφx := Path.obj_eq_of_cons_eq_cons h'
-- 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), 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 (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
⊢ 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) y₂ (p₂.cons e₂)
have hφp : φ.mapPath p₁ ≍ φ.mapPath p₂
Tactic: have hφp := Path.heq_of_cons_eq_cons h'
-- 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), 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 (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : φ.mapPath p₁ ≍ φ.mapPath p₂
⊢ 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) y₂ (p₂.cons e₂)
have hφe : φ.map e₁ ≍ φ.map e₂
Tactic: have hφe := HEq.trans (Hom.cast_heq rfl hφy _).symm (Path.hom_heq_of_cons_eq_cons 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), 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 (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : φ.mapPath p₁ ≍ φ.mapPath p₂
hφe : φ.map e₁ ≍ φ.map e₂
⊢ φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁) =
    φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₂ p₂)
have simp : φ.obj x₁ = φ.obj x₂ ∧ φ.mapPath p₁ ≍ φ.mapPath p₂
Tactic: simp only [Prefunctor.pathStar_apply, Sigma.mk.inj_iff]
-- 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), 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 (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : φ.mapPath p₁ ≍ φ.mapPath p₂
hφe : φ.map e₁ ≍ φ.map e₂
⊢ 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) y₂ (p₂.cons e₂)
have h_path_star : φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁) =
  φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₂ p₂)
Tactic: 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⟩
-- 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₁ 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 (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : φ.mapPath p₁ ≍ φ.mapPath p₂
hφe : φ.map e₁ ≍ φ.map e₂
h_path_star :
  φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁) =
    φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₂ p₂)
⊢ 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) y₂ (p₂.cons e₂)
have cons : ∀ (e₂ : x₁ ⟶ y₂) (hφx : φ.obj x₁ = φ.obj x₁) (hφe : φ.map e₁ ≍ φ.map e₂)
  (h' : (φ.mapPath p₁).cons (Hom.cast sorry hφy (φ.map e₁)) = (φ.mapPath p₁).cons (φ.map e₂))
  (hφp : φ.mapPath p₁ ≍ φ.mapPath p₁)
  (h_path_star :
    φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁) =
      φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁)),
  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) y₂ (p₁.cons e₂)
Tactic: cases ih h_path_star
Cleared hypotheses: x₂, p₂, e₂, h', hφx, hφp, hφe, h_path_star
-- 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₁ 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₂ : U
hφy : φ.obj y₁ = φ.obj y₂
e₂ : x₁ ⟶ y₂
hφx : φ.obj x₁ = φ.obj x₁
hφe : φ.map e₁ ≍ φ.map e₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₁).cons (φ.map e₂)
hφp : φ.mapPath p₁ ≍ φ.mapPath p₁
h_path_star :
  φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁) =
    φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁)
⊢ φ.star x₁ (Sigma.mk (β := fun (v : U) ↦ x₁ ⟶ v) y₁ e₁) = φ.star x₁ (Sigma.mk (β := fun (v : U) ↦ x₁ ⟶ v) y₂ e₂)
have simp : φ.obj y₁ = φ.obj y₂ ∧ φ.map e₁ ≍ φ.map e₂
Tactic: simp only [Prefunctor.star_apply, Sigma.mk.inj_iff]
-- 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), 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₂ : U
hφy : φ.obj y₁ = φ.obj y₂
e₂ : x₁ ⟶ y₂
hφx : φ.obj x₁ = φ.obj x₁
hφe : φ.map e₁ ≍ φ.map e₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₁).cons (φ.map e₂)
hφp : φ.mapPath p₁ ≍ φ.mapPath p₁
h_path_star :
  φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁) =
    φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁)
⊢ 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) y₂ (p₁.cons e₂)
have h_star : φ.star x₁ (Sigma.mk (β := fun (v : U) ↦ x₁ ⟶ v) y₁ e₁) = φ.star x₁ (Sigma.mk (β := fun (v : U) ↦ x₁ ⟶ v) y₂ 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⟩
-- 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₁ 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₂ : U
hφy : φ.obj y₁ = φ.obj y₂
e₂ : x₁ ⟶ y₂
hφx : φ.obj x₁ = φ.obj x₁
hφe : φ.map e₁ ≍ φ.map e₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₁).cons (φ.map e₂)
hφp : φ.mapPath p₁ ≍ φ.mapPath p₁
h_path_star :
  φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁) =
    φ.pathStar u (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) x₁ p₁)
h_star : φ.star x₁ (Sigma.mk (β := fun (v : U) ↦ x₁ ⟶ v) y₁ e₁) = φ.star x₁ (Sigma.mk (β := fun (v : U) ↦ x₁ ⟶ v) y₂ e₂)
⊢ 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) y₂ (p₁.cons e₂)
have cons : ∀ (hφy : φ.obj y₁ = φ.obj y₁) (hφe : φ.map e₁ ≍ φ.map e₁)
  (h' : (φ.mapPath p₁).cons (Hom.cast sorry hφy (φ.map e₁)) = (φ.mapPath p₁).cons (φ.map e₁))
  (h_star :
    φ.star x₁ (Sigma.mk (β := fun (v : U) ↦ x₁ ⟶ v) y₁ e₁) = φ.star x₁ (Sigma.mk (β := fun (v : U) ↦ x₁ ⟶ v) y₁ e₁)),
  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) y₁ (p₁.cons e₁)
Tactic: cases hφ x₁ h_star
Cleared hypotheses: y₂, hφy, e₂, hφe, h', h_star