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
u : U
h :
  ∀ (v : Symmetrify U) (f : u ⟶ v),
    ((⇑(Quiver.symmetrifyStar (φ.obj u)) :
            (a : Star (Symmetrify.of.obj (φ.obj u))) → Star (φ.obj u) ⊕ Costar (φ.obj u)) ∘
          φ.symmetrify.star u)
        (Sigma.mk (β := fun (v : Symmetrify U) ↦ u ⟶ v) v (Sum.inl f)) =
      Function.comp (α := Star.{u, u_1} (obj.{u, u, u_1, u_1} Symmetrify.of u)) (Sum.map (φ.star u) (φ.costar u))
        (⇑(Quiver.symmetrifyStar u) : (a : Star (Symmetrify.of.obj u)) → Star u ⊕ Costar u)
        (Sigma.mk (β := fun (v : Symmetrify U) ↦ u ⟶ v) v (Sum.inl f))
⊢ (⇑(Quiver.symmetrifyStar (φ.obj u)) : (a : Star (Symmetrify.of.obj (φ.obj u))) → Star (φ.obj u) ⊕ Costar (φ.obj u)) ∘
      φ.symmetrify.star u =
    Sum.map (φ.star u) (φ.costar u) ∘
      (⇑(Quiver.symmetrifyStar u) : (a : Star (Symmetrify.of.obj u)) → Star u ⊕ Costar u)
have h₁ : ∀ (v : Symmetrify U) (g : v ⟶ u),
  ((⇑(Quiver.symmetrifyStar (φ.obj u)) : (a : Star (Symmetrify.of.obj (φ.obj u))) → Star (φ.obj u) ⊕ Costar (φ.obj u)) ∘
        φ.symmetrify.star u)
      (Sigma.mk (β := fun (v : Symmetrify U) ↦ u ⟶ v) v (Sum.inr g)) =
    Function.comp (α := Star.{u, u_1} (obj.{u, u, u_1, u_1} Symmetrify.of u)) (Sum.map (φ.star u) (φ.costar u))
      (⇑(Quiver.symmetrifyStar u) : (a : Star (Symmetrify.of.obj u)) → Star u ⊕ Costar u)
      (Sigma.mk (β := fun (v : Symmetrify U) ↦ u ⟶ v) v (Sum.inr g))
Tactic: ext ⟨v, f | g⟩
-- 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
u : U
⊢ φ.symmetrify.costar u =
    (⇑(Equiv.symm (symmetrifyCostar (φ.obj u))) :
        (a : Costar (φ.obj u) ⊕ Star (φ.obj u)) → Costar (Symmetrify.of.obj (φ.obj u))) ∘
      Sum.map (φ.costar u) (φ.star u) ∘ (⇑(symmetrifyCostar u) : (a : Costar (Symmetrify.of.obj u)) → Costar u ⊕ Star u)
have rw : (⇑(symmetrifyCostar (φ.obj u)) : (a : Costar (Symmetrify.of.obj (φ.obj u))) → Costar (φ.obj u) ⊕ Star (φ.obj u)) ∘
    φ.symmetrify.costar u =
  Sum.map (φ.costar u) (φ.star u) ∘ (⇑(symmetrifyCostar u) : (a : Costar (Symmetrify.of.obj u)) → Costar u ⊕ Star u)
Tactic: rw [Equiv.eq_symm_comp (e := Quiver.symmetrifyCostar (φ.obj u))]
-- 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
u : U
⊢ (⇑(symmetrifyCostar (φ.obj u)) : (a : Costar (Symmetrify.of.obj (φ.obj u))) → Costar (φ.obj u) ⊕ Star (φ.obj u)) ∘
      φ.symmetrify.costar u =
    Sum.map (φ.costar u) (φ.star u) ∘ (⇑(symmetrifyCostar u) : (a : Costar (Symmetrify.of.obj u)) → Costar u ⊕ Star u)
have h : ∀ (v : Symmetrify U) (f : v ⟶ u),
  ((⇑(symmetrifyCostar (φ.obj u)) : (a : Costar (Symmetrify.of.obj (φ.obj u))) → Costar (φ.obj u) ⊕ Star (φ.obj u)) ∘
        φ.symmetrify.costar u)
      (Sigma.mk (β := fun (u_1 : Symmetrify U) ↦ u_1 ⟶ u) v (Sum.inl f)) =
    Function.comp (α := Costar.{u, u_1} (obj.{u, u, u_1, u_1} Symmetrify.of u)) (Sum.map (φ.costar u) (φ.star u))
      (⇑(symmetrifyCostar u) : (a : Costar (Symmetrify.of.obj u)) → Costar u ⊕ Star u)
      (Sigma.mk (β := fun (u_1 : Symmetrify U) ↦ u_1 ⟶ u) v (Sum.inl f))
Tactic: ext ⟨v, f | g⟩
-- 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
u : U
h :
  ∀ (v : Symmetrify U) (f : v ⟶ u),
    ((⇑(symmetrifyCostar (φ.obj u)) : (a : Costar (Symmetrify.of.obj (φ.obj u))) → Costar (φ.obj u) ⊕ Star (φ.obj u)) ∘
          φ.symmetrify.costar u)
        (Sigma.mk (β := fun (u_1 : Symmetrify U) ↦ u_1 ⟶ u) v (Sum.inl f)) =
      Function.comp (α := Costar.{u, u_1} (obj.{u, u, u_1, u_1} Symmetrify.of u)) (Sum.map (φ.costar u) (φ.star u))
        (⇑(symmetrifyCostar u) : (a : Costar (Symmetrify.of.obj u)) → Costar u ⊕ Star u)
        (Sigma.mk (β := fun (u_1 : Symmetrify U) ↦ u_1 ⟶ u) v (Sum.inl f))
⊢ (⇑(symmetrifyCostar (φ.obj u)) : (a : Costar (Symmetrify.of.obj (φ.obj u))) → Costar (φ.obj u) ⊕ Star (φ.obj u)) ∘
      φ.symmetrify.costar u =
    Sum.map (φ.costar u) (φ.star u) ∘ (⇑(symmetrifyCostar u) : (a : Costar (Symmetrify.of.obj u)) → Costar u ⊕ Star u)
have h₁ : ∀ (v : Symmetrify U) (g : u ⟶ v),
  ((⇑(symmetrifyCostar (φ.obj u)) : (a : Costar (Symmetrify.of.obj (φ.obj u))) → Costar (φ.obj u) ⊕ Star (φ.obj u)) ∘
        φ.symmetrify.costar u)
      (Sigma.mk (β := fun (u_1 : Symmetrify U) ↦ u_1 ⟶ u) v (Sum.inr g)) =
    Function.comp (α := Costar.{u, u_1} (obj.{u, u, u_1, u_1} Symmetrify.of u)) (Sum.map (φ.costar u) (φ.star u))
      (⇑(symmetrifyCostar u) : (a : Costar (Symmetrify.of.obj u)) → Costar u ⊕ Star u)
      (Sigma.mk (β := fun (u_1 : Symmetrify U) ↦ u_1 ⟶ u) v (Sum.inr g))
Tactic: ext ⟨v, f | g⟩
-- 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φ : φ.IsCovering
⊢ φ.symmetrify.IsCovering
have refine_1 : ∀ (u : Symmetrify U), Bijective (φ.symmetrify.star u)
Tactic: refine ⟨fun u => ?_, fun u => ?_⟩
-- 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φ : φ.IsCovering
refine_1 : ∀ (u : Symmetrify U), Bijective (φ.symmetrify.star u)
⊢ φ.symmetrify.IsCovering
have refine_2 : ∀ (u : Symmetrify U), Bijective (φ.symmetrify.costar u)
Tactic: refine ⟨fun u => ?_, fun u => ?_⟩
-- 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₁ y₂ : U
p₂ : Path.{u, u_1} u y₂
⊢ 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))))
        (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) y₂ p₂)) →
    Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) u Path.nil = Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) y₂ p₂
have nil : 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))))
      (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) u Path.nil)) →
  Eq (α := PathStar.{u, u_1} u) (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) u Path.nil)
    (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) u Path.nil)
Tactic: rcases p₂ with - | ⟨p₂, e₂⟩
Cleared hypotheses: y₂, 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₁ y₂ : U
p₂ : Path.{u, u_1} u y₂
nil :
  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))))
        (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) u Path.nil)) →
    Eq (α := PathStar.{u, u_1} u) (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) u Path.nil)
      (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) u Path.nil)
⊢ 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))))
        (Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) y₂ p₂)) →
    Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) u Path.nil = Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) y₂ p₂
have nil₁ : ∀ {b : U} (p₂ : Path.{u, u_1} u b) (e₂ : b ⟶ y₂),
  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))))
        (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) u Path.nil =
      Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) y₂ (p₂.cons e₂)
Tactic: rcases p₂ with - | ⟨p₂, e₂⟩
Cleared hypotheses: p₂
-- 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₁ y₂ b : U
p₂ : Path.{u, u_1} u b
e₂ : b ⟶ 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) 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))))
      (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) u Path.nil =
    Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) y₂ (p₂.cons e₂)
have h₁ : φ.obj u = φ.obj y₂ ∧ HEq (α := Path.{v, u_2} (φ.obj u) (φ.obj u)) (φ.mapPath Path.nil) ((φ.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 (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₁ y₂ b : U
p₂ : Path.{u, u_1} u b
e₂ : b ⟶ y₂
h :
  φ.obj u = φ.obj y₂ ∧
    HEq (α := Path.{v, u_2} (φ.obj u) (φ.obj u)) (φ.mapPath Path.nil) ((φ.mapPath p₂).cons (φ.map e₂))
⊢ Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) u Path.nil =
    Sigma.mk (β := fun (v : U) ↦ Path.{u, u_1} u v) y₂ (p₂.cons e₂)
have nil : False
Tactic: exfalso
-- 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₁ y₂ b : U
p₂ : Path.{u, u_1} u b
e₂ : b ⟶ y₂
h :
  φ.obj u = φ.obj y₂ ∧
    HEq (α := Path.{v, u_2} (φ.obj u) (φ.obj u)) (φ.mapPath Path.nil) ((φ.mapPath p₂).cons (φ.map e₂))
⊢ False
have h₁ : φ.obj u = φ.obj y₂
Tactic: obtain ⟨h, 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₁ y₂ b : U
p₂ : Path.{u, u_1} u b
e₂ : b ⟶ y₂
h :
  φ.obj u = φ.obj y₂ ∧
    HEq (α := Path.{v, u_2} (φ.obj u) (φ.obj u)) (φ.mapPath Path.nil) ((φ.mapPath p₂).cons (φ.map e₂))
h₁ : φ.obj u = φ.obj y₂
⊢ False
have h' : HEq (α := Path.{v, u_2} (φ.obj u) (φ.obj u)) (φ.mapPath Path.nil) ((φ.mapPath p₂).cons (φ.map e₂))
Tactic: obtain ⟨h, 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₁ y₂ b : U
p₂ : Path.{u, u_1} u b
e₂ : b ⟶ y₂
h : φ.obj u = φ.obj y₂
h' : HEq (α := Path.{v, u_2} (φ.obj u) (φ.obj u)) (φ.mapPath Path.nil) ((φ.mapPath p₂).cons (φ.map e₂))
⊢ False
have h'₁ : φ.mapPath Path.nil = (Path.cast sorry sorry (φ.mapPath p₂)).cons (Hom.cast sorry sorry (φ.map e₂))
Tactic: rw [← Path.eq_cast_iff_heq rfl h.symm, Path.cast_cons] at h'
Cleared hypotheses: 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₂ : U
p₂ : Path.{u, u_1} u y₂
⊢ 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₂)) →
    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₂
have cons : 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) u Path.nil)) →
  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) u Path.nil
Tactic: rcases p₂ with - | ⟨p₂, e₂⟩
Cleared hypotheses: y₂, p₂
-- 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₂
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) u Path.nil))
⊢ 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) u Path.nil
have h₁ : φ.obj y₁ = φ.obj u ∧ HEq ((φ.mapPath p₁).cons (φ.map e₁)) (β := Path.{v, u_2} (φ.obj u) (φ.obj u)) (φ.mapPath Path.nil)
Tactic: simp only [mapPath_cons, Sigma.mk.inj_iff] at h
Cleared hypotheses: 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₂
h :
  φ.obj y₁ = φ.obj u ∧
    HEq ((φ.mapPath p₁).cons (φ.map e₁)) (β := Path.{v, u_2} (φ.obj u) (φ.obj u)) (φ.mapPath Path.nil)
⊢ 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) u Path.nil
have cons : False
Tactic: exfalso
-- 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₂
h :
  φ.obj y₁ = φ.obj u ∧
    HEq ((φ.mapPath p₁).cons (φ.map e₁)) (β := Path.{v, u_2} (φ.obj u) (φ.obj u)) (φ.mapPath Path.nil)
⊢ False
have h₁ : φ.obj y₁ = φ.obj u
Tactic: obtain ⟨h, 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₂
h :
  φ.obj y₁ = φ.obj u ∧
    HEq ((φ.mapPath p₁).cons (φ.map e₁)) (β := Path.{v, u_2} (φ.obj u) (φ.obj u)) (φ.mapPath Path.nil)
h₁ : φ.obj y₁ = φ.obj u
⊢ False
have h' : HEq ((φ.mapPath p₁).cons (φ.map e₁)) (β := Path.{v, u_2} (φ.obj u) (φ.obj u)) (φ.mapPath Path.nil)
Tactic: obtain ⟨h, 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₂
h : φ.obj y₁ = φ.obj u
h' : HEq ((φ.mapPath p₁).cons (φ.map e₁)) (β := Path.{v, u_2} (φ.obj u) (φ.obj u)) (φ.mapPath Path.nil)
⊢ False
have h'₁ : (Path.cast sorry sorry (φ.mapPath p₁)).cons (Hom.cast sorry h (φ.map e₁)) = φ.mapPath Path.nil
Tactic: rw [← Path.cast_eq_iff_heq rfl h, Path.cast_cons] at h'
Cleared hypotheses: h'