awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : (Functor.{v₁, v₂, u₁, u₂} C D)ᵒᵖ
f : F ⟶ G
e_f :
  (NatIso.ofComponents (fun (x : C) ↦ Iso.refl ((unop G).obj x)) ⋯).hom ≫ f.unop =
    { app := fun (X : C) ↦ f.unop.op.unop.app X, naturality := ⋯ } ≫
      (NatIso.ofComponents (fun (x : C) ↦ Iso.refl ((unop F).obj x)) ⋯).hom
⊢ ((NatIso.ofComponents (fun (x : C) ↦ Iso.refl ((unop G).obj x)) ⋯).hom ≫ f.unop).op =
    Quiver.Hom.op
      ({ app := fun (X : C) ↦ f.unop.op.unop.app X, naturality := ⋯ } ≫
        (NatIso.ofComponents (fun (x : C) ↦ Iso.refl ((unop F).obj x)) ⋯).hom)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D)ᵒᵖ
η : F ⟶ G
dsimp :
  η ≫ (unop G).rightOpLeftOpIso.hom.op =
    (unop F).rightOpLeftOpIso.hom.op ≫ (NatTrans.leftOp (NatTrans.rightOp η.unop)).op
⊢ Eq (α :=
    obj (𝟭 (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D)ᵒᵖ) F ⟶
      obj
        (comp (D := Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ)
          { obj := fun (F : (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D)ᵒᵖ) ↦ (unop F).rightOp,
            map := fun {X Y : (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D)ᵒᵖ} (η : X ⟶ Y) ↦ NatTrans.rightOp η.unop, map_id := ⋯,
            map_comp := ⋯ }
          { obj := fun (F : Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ) ↦ op F.leftOp,
            map := fun {X Y : Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ} (η : X ⟶ Y) ↦ (NatTrans.leftOp η).op, map_id := ⋯,
            map_comp := ⋯ })
        G)
    (map (𝟭 (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D)ᵒᵖ) η ≫
      Iso.hom ((fun (F : (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D)ᵒᵖ) ↦ (unop F).rightOpLeftOpIso.op) G))
    (Iso.hom ((fun (F : (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D)ᵒᵖ) ↦ (unop F).rightOpLeftOpIso.op) F) ≫
      map
        (comp (D := Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ)
          { obj := fun (F : (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D)ᵒᵖ) ↦ (unop F).rightOp,
            map := fun {X Y : (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D)ᵒᵖ} (η : X ⟶ Y) ↦ NatTrans.rightOp η.unop, map_id := ⋯,
            map_comp := ⋯ : (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D)ᵒᵖ ⥤ Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ }
          { obj := fun (F : Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ) ↦ op F.leftOp,
            map := fun {X Y : Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ} (η : X ⟶ Y) ↦ (NatTrans.leftOp η).op, map_id := ⋯,
            map_comp := ⋯ : Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ ⥤ (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D)ᵒᵖ })
        η)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D)ᵒᵖ
η : F ⟶ G
⊢ η = η.unop.op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D)ᵒᵖ
η : F ⟶ G
rw :
  ((unop G).rightOpLeftOpIso.hom ≫ η.unop).op =
    (NatTrans.leftOp (NatTrans.rightOp η.unop.op.unop) ≫ (unop F).rightOpLeftOpIso.hom).op
⊢ η ≫ (unop G).rightOpLeftOpIso.hom.op =
    (unop F).rightOpLeftOpIso.hom.op ≫ (NatTrans.leftOp (NatTrans.rightOp η.unop)).op

Tactic:
rw [show η = η.unop.op by simp, ← op_comp, ← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D)ᵒᵖ
η : F ⟶ G
e_f :
  (unop G).rightOpLeftOpIso.hom ≫ η.unop =
    NatTrans.leftOp (NatTrans.rightOp η.unop.op.unop) ≫ (unop F).rightOpLeftOpIso.hom
⊢ ((unop G).rightOpLeftOpIso.hom ≫ η.unop).op =
    (NatTrans.leftOp (NatTrans.rightOp η.unop.op.unop) ≫ (unop F).rightOpLeftOpIso.hom).op

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.PEmpty
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
α : Type u_1
inst_2 : IsEmpty α
⊢ IsEmpty.{u_1 + 1} (Discrete α)

Tactic:
Function.isEmpty Discrete.as

Premises used: Function.isEmpty, CategoryTheory.Discrete.as
-- Module: Mathlib.CategoryTheory.PEmpty
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{w, v, w, u} (Discrete PEmpty.{w + 1}) C
⊢ F = G

Tactic:
Functor.ext (fun x => x.as.elim) fun x _ _ => x.as.elim

Premises used: CategoryTheory.Functor.ext, PEmpty.elim, CategoryTheory.Discrete.as
-- Module: Mathlib.CategoryTheory.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w} C (Discrete PUnit.{w + 1})
X : C
⊢ F.obj X = G.obj X

Tactic:
simp only [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
mp :
  Nonempty (Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})) →
    Nonempty C ∧ ∀ (x y : C), Nonempty.{max 1 (v + 1)} (Unique (x ⟶ y))
mpr :
  (Nonempty C ∧ ∀ (x y : C), Nonempty.{max 1 (v + 1)} (Unique (x ⟶ y))) →
    Nonempty (Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1}))
⊢ Nonempty (Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})) ↔
    Nonempty C ∧ ∀ (x y : C), Nonempty.{max 1 (v + 1)} (Unique (x ⟶ y))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
h : Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})
⊢ Nonempty C ∧ ∀ (x y : C), Nonempty.{max 1 (v + 1)} (Unique (x ⟶ y))

Tactic:
⟨⟨h.inverse.obj ⟨⟨⟩⟩⟩, fun x y => Nonempty.intro ?_⟩

Premises used: Nonempty.intro, CategoryTheory.Discrete.mk, And.intro, PUnit.unit, CategoryTheory.Functor.obj, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
h : Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})
mp : (x y : C) → Unique (x ⟶ y)
⊢ Nonempty C ∧ ∀ (x y : C), Nonempty.{max 1 (v + 1)} (Unique (x ⟶ y))

Tactic:
refine ⟨⟨h.inverse.obj ⟨⟨⟩⟩⟩, fun x y => Nonempty.intro ?_⟩
-- Module: Mathlib.CategoryTheory.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
h : Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})
x y : C
⊢ x ⟶ h.inverse.obj { as := PUnit.unit }

Tactic:
convert! h.unit.app x

Premises used: CategoryTheory.Equivalence.unit, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
h : Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})
x y : C
have : (hx : x ⟶ h.inverse.obj { as := PUnit.unit }) → x ⟶ y
⊢ x ⟶ y

Tactic:
have hx : x ⟶ h.inverse.obj ⟨⟨⟩⟩ := by convert! h.unit.app x
-- Module: Mathlib.CategoryTheory.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
h : Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})
x y : C
hx : x ⟶ h.inverse.obj { as := PUnit.unit }
⊢ h.inverse.obj { as := PUnit.unit : Discrete PUnit.{w + 1} } ⟶ y

Tactic:
convert! h.unitInv.app y

Premises used: CategoryTheory.Equivalence.unitInv, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
h : Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})
x y : C
hx : x ⟶ h.inverse.obj { as := PUnit.unit }
have : (hy : h.inverse.obj { as := PUnit.unit : Discrete PUnit.{w + 1} } ⟶ y) → x ⟶ y
⊢ x ⟶ y

Tactic:
have hy : h.inverse.obj ⟨⟨⟩⟩ ⟶ y := by convert! h.unitInv.app y
-- Module: Mathlib.CategoryTheory.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
h : Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})
x y : C
hx : x ⟶ h.inverse.obj { as := PUnit.unit }
hy : h.inverse.obj { as := PUnit.unit : Discrete PUnit.{w + 1} } ⟶ y
⊢ x ⟶ y

Tactic:
exact hx ≫ hy
-- Module: Mathlib.CategoryTheory.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
h : Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})
x y : C
f : x ⟶ y :=
  have hx : x ⟶ h.inverse.obj { as := PUnit.unit } := Eq.mpr ⋯ (h.unit.app x);
  have hy : h.inverse.obj { as := PUnit.unit : Discrete PUnit.{w + 1} } ⟶ y := Eq.mpr ⋯ (h.unitInv.app y);
  hx ≫ hy
mp : Subsingleton.{v + 1} (x ⟶ y)
⊢ Unique (x ⟶ y)

Tactic:
suffices sub : Subsingleton (x ⟶ y) from uniqueOfSubsingleton f
-- Module: Mathlib.CategoryTheory.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
h : Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})
x y : C
f : x ⟶ y :=
  have hx : x ⟶ h.inverse.obj { as := PUnit.unit } := Eq.mpr ⋯ (h.unit.app x);
  have hy : h.inverse.obj { as := PUnit.unit : Discrete PUnit.{w + 1} } ⟶ y := Eq.mpr ⋯ (h.unitInv.app y);
  hx ≫ hy
⊢ ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
h : Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})
x y : C
f : x ⟶ y :=
  have hx : x ⟶ h.inverse.obj { as := PUnit.unit } := Eq.mpr ⋯ (h.unit.app x);
  have hy : h.inverse.obj { as := PUnit.unit : Discrete PUnit.{w + 1} } ⟶ y := Eq.mpr ⋯ (h.unitInv.app y);
  hx ≫ hy
⊢ ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y

Tactic:
have : ∀ z, z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y := by
      simp
-- Module: Mathlib.CategoryTheory.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
h : Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})
x y : C
f : x ⟶ y :=
  have hx : x ⟶ h.inverse.obj { as := PUnit.unit } := Eq.mpr ⋯ (h.unit.app x);
  have hy : h.inverse.obj { as := PUnit.unit : Discrete PUnit.{w + 1} } ⟶ y := Eq.mpr ⋯ (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
mp : ∀ (a b : x ⟶ y), a = b
⊢ Subsingleton.{v + 1} (x ⟶ y)

Tactic:
apply Subsingleton.intro

Premises used: Subsingleton.intro
-- Module: Mathlib.CategoryTheory.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
h : Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})
x y : C
f : x ⟶ y :=
  have hx : x ⟶ h.inverse.obj { as := PUnit.unit } := Eq.mpr ⋯ (h.unit.app x);
  have hy : h.inverse.obj { as := PUnit.unit : Discrete PUnit.{w + 1} } ⟶ y := Eq.mpr ⋯ (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
a b : x ⟶ y
mp :
  h.unit.app x ≫ (h.functor ⋙ h.inverse).map a ≫ h.unitInv.app y =
    h.unit.app x ≫ (h.functor ⋙ h.inverse).map b ≫ h.unitInv.app y
⊢ a = b

Tactic:
rw [this a, this b]
-- Module: Mathlib.CategoryTheory.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
h : Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})
x y : C
f : x ⟶ y :=
  have hx : x ⟶ h.inverse.obj { as := PUnit.unit } := Eq.mpr ⋯ (h.unit.app x);
  have hy : h.inverse.obj { as := PUnit.unit : Discrete PUnit.{w + 1} } ⟶ y := Eq.mpr ⋯ (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
a b : x ⟶ y
mp :
  h.unit.app x ≫ h.inverse.map (h.functor.map a) ≫ h.unitInv.app y =
    h.unit.app x ≫ h.inverse.map (h.functor.map b) ≫ h.unitInv.app y
⊢ h.unit.app x ≫ (h.functor ⋙ h.inverse).map a ≫ h.unitInv.app y =
    h.unit.app x ≫ (h.functor ⋙ h.inverse).map b ≫ h.unitInv.app y

Tactic:
simp only [Functor.comp_map]

Premises used: CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
h : Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})
x y : C
f : x ⟶ y :=
  have hx : x ⟶ h.inverse.obj { as := PUnit.unit } := Eq.mpr ⋯ (h.unit.app x);
  have hy : h.inverse.obj { as := PUnit.unit : Discrete PUnit.{w + 1} } ⟶ y := Eq.mpr ⋯ (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
a b : x ⟶ y
mp : h.functor.map a = h.functor.map b
⊢ h.unit.app x ≫ h.inverse.map (h.functor.map a) ≫ h.unitInv.app y =
    h.unit.app x ≫ h.inverse.map (h.functor.map b) ≫ h.unitInv.app y

Tactic:
congr 3
-- Module: Mathlib.CategoryTheory.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
h : Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})
x y : C
f : x ⟶ y :=
  have hx : x ⟶ h.inverse.obj { as := PUnit.unit } := Eq.mpr ⋯ (h.unit.app x);
  have hy : h.inverse.obj { as := PUnit.unit : Discrete PUnit.{w + 1} } ⟶ y := Eq.mpr ⋯ (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
a b : x ⟶ y
mp : ULift.down.{w, 0} (h.functor.map a) = ULift.down.{w, 0} (h.functor.map b)
⊢ h.functor.map a = h.functor.map b

Tactic:
apply ULift.ext

Premises used: ULift.ext
-- Module: Mathlib.CategoryTheory.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
h : Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})
x y : C
f : x ⟶ y :=
  have hx : x ⟶ h.inverse.obj { as := PUnit.unit } := Eq.mpr ⋯ (h.unit.app x);
  have hy : h.inverse.obj { as := PUnit.unit : Discrete PUnit.{w + 1} } ⟶ y := Eq.mpr ⋯ (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
a b : x ⟶ y
⊢ ULift.down.{w, 0} (h.functor.map a) = ULift.down.{w, 0} (h.functor.map b)

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ (x y : C), Nonempty.{max 1 (v + 1)} (Unique (x ⟶ y))
p : C
mpr : ∀ (this : (x y : C) → Unique (x ⟶ y)), Nonempty (Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1}))
⊢ Nonempty (Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1}))

Tactic:
haveI := fun x y => (h x y).some
-- Module: Mathlib.CategoryTheory.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ (x y : C), Nonempty.{max 1 (v + 1)} (Unique (x ⟶ y))
p : C
this : (x y : C) → Unique (x ⟶ y)
⊢ Iso (C := Discrete PUnit.{w + 1} ⥤ Discrete PUnit.{w + 1})
    (Functor.comp.{w, v, w, w, u, w} (Functor.obj (Functor.const (Discrete PUnit.{w + 1})) p)
      (Functor.obj (Functor.const C) { as := PUnit.unit : Discrete PUnit.{w + 1} }))
    (𝟭 (Discrete PUnit.{w + 1}))

Tactic:
apply Functor.punitExt

Premises used: CategoryTheory.Functor.punitExt
-- Module: Mathlib.CategoryTheory.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ (x y : C), Nonempty.{max 1 (v + 1)} (Unique (x ⟶ y))
p : C
this : (x y : C) → Unique (x ⟶ y)
mpr :
  Iso (C := Functor.{v, v, u, u} C C) (𝟭 C)
    (Functor.obj (Functor.const C) { as := PUnit.unit : Discrete PUnit.{w + 1} } ⋙
      Functor.obj (Functor.const (Discrete PUnit.{w + 1})) p)
⊢ Nonempty (Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1}))

Tactic:
refine
      Nonempty.intro
        (CategoryTheory.Equivalence.mk ((Functor.const _).obj ⟨⟨⟩⟩)
          ((@Functor.const <| Discrete PUnit).obj p) ?_ (by apply Functor.punitExt))

Premises used: Nonempty.intro, PUnit, CategoryTheory.Functor.const, CategoryTheory.Equivalence.mk, CategoryTheory.Functor.obj, CategoryTheory.Discrete
-- Module: Mathlib.CategoryTheory.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ (x y : C), Nonempty.{max 1 (v + 1)} (Unique (x ⟶ y))
p : C
this : (x y : C) → Unique (x ⟶ y)
⊢ Iso (C := Functor.{v, v, u, u} C C) (𝟭 C)
    (Functor.obj (Functor.const C) { as := PUnit.unit : Discrete PUnit.{w + 1} } ⋙
      Functor.obj (Functor.const (Discrete PUnit.{w + 1})) p)

Tactic:
exact
      NatIso.ofComponents fun _ =>
        { hom := default
          inv := default }

Premises used: Inhabited.default, CategoryTheory.Iso.mk, CategoryTheory.NatIso.ofComponents
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
a : Paths V
P : {b : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 a)
comp : ∀ {u v : V} (p : a ⟶ Prefunctor.obj (of V) u) (q : u ⟶ v), P p → P (p ≫ Prefunctor.map (of V) q)
b : Paths V
⊢ P Quiver.Path.nil

Tactic:
id

Premises used: CategoryTheory.Paths
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
a : Paths V
P : {b : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 a)
comp : ∀ {u v : V} (p : a ⟶ Prefunctor.obj (of V) u) (q : u ⟶ v), P p → P (p ≫ Prefunctor.map (of V) q)
b : Paths V
⊢ P Quiver.Path.nil

Tactic:
exact id
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
a : Paths V
P : {b : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 a)
comp : ∀ {u v : V} (p : a ⟶ Prefunctor.obj (of V) u) (q : u ⟶ v), P p → P (p ≫ Prefunctor.map (of V) q)
b b_1 c : Paths V
a_1 : Quiver.Path.{v₁, u₁} a b_1
w : b_1 ⟶ c
h : P a_1
⊢ P (a_1.cons w)

Tactic:
comp _ w h

Premises used: CategoryTheory.Paths, Quiver.Hom.toPath, Quiver.Path.comp
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
a : Paths V
P : {b : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 a)
comp : ∀ {u v : V} (p : a ⟶ Prefunctor.obj (of V) u) (q : u ⟶ v), P p → P (p ≫ Prefunctor.map (of V) q)
b b_1 c : Paths V
a_1 : Quiver.Path.{v₁, u₁} a b_1
w : b_1 ⟶ c
h : P a_1
⊢ P (a_1.cons w)

Tactic:
exact comp _ w h
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
a : Paths V
P : {b : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 a)
comp : ∀ {u v : V} (p : a ⟶ Prefunctor.obj (of V) u) (q : u ⟶ v), P p → P (p ≫ Prefunctor.map (of V) q)
b : Paths V
f : a ⟶ b
nil : P Quiver.Path.nil
cons : ∀ {b c : Paths V} (a_1 : Quiver.Path.{v₁, u₁} a b) (w : b ⟶ c) (h : P a_1), P (a_1.cons w)
⊢ P f

Tactic:
induction f with
  | nil => exact id
  | cons _ w h => exact comp _ w h
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : Prefunctor.obj (of V) v ⟶ b) (q : u ⟶ v), P p → P (Prefunctor.map (of V) q ≫ p)
a : Paths V
f : a ⟶ b
generalize : ∀ (k : ℕ) (h : Quiver.Path.length f = k), P f
⊢ P f

Tactic:
generalize h : f.length = k

Premises used: Quiver.Path.length
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : Prefunctor.obj (of V) v ⟶ b) (q : u ⟶ v), P p → P (Prefunctor.map (of V) q ≫ p)
h : Quiver.Path.length.{u₁, v₁} (V := V) (a := b) Quiver.Path.nil = 0
⊢ P Quiver.Path.nil

Tactic:
id

Premises used: CategoryTheory.Paths
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : Prefunctor.obj (of V) v ⟶ b) (q : u ⟶ v), P p → P (Prefunctor.map (of V) q ≫ p)
h : Quiver.Path.length.{u₁, v₁} (V := V) (a := b) Quiver.Path.nil = 0
⊢ P Quiver.Path.nil

Tactic:
exact id
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : Prefunctor.obj (of V) v ⟶ b) (q : u ⟶ v), P p → P (Prefunctor.map (of V) q ≫ p)
a b_1 : Paths V
a_1 : Quiver.Path.{v₁, u₁} a b_1
a_2 : b_1 ⟶ b
h : (a_1.cons a_2).length = 0
⊢ P (a_1.cons a_2)

Tactic:
simp at h
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : Prefunctor.obj (of V) v ⟶ b) (q : u ⟶ v), P p → P (Prefunctor.map (of V) q ≫ p)
a : Paths V
f : a ⟶ b
h : Quiver.Path.length f = 0
zero : ∀ (h : Quiver.Path.length.{u₁, v₁} (V := V) (a := b) Quiver.Path.nil = 0), P Quiver.Path.nil
zero₁ :
  ∀ {b_1 : Paths V} (a_1 : Quiver.Path.{v₁, u₁} a b_1) (a_2 : b_1 ⟶ b) (h : (a_1.cons a_2).length = 0), P (a_1.cons a_2)
⊢ P f

Tactic:
cases f with
    | nil => exact id
    | cons _ _ => simp at h
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : Prefunctor.obj (of V) v ⟶ b) (q : u ⟶ v), P p → P (Prefunctor.map (of V) q ≫ p)
k : ℕ
h' : ∀ {a : Paths V} (f : a ⟶ b) (h : Quiver.Path.length f = k), P f
a : Paths V
f : a ⟶ b
h : Quiver.Path.length f = k + 1
succ :
  ∀ (c : V) (f : a ⟶ c) (q : Quiver.Path.{v₁, u₁} c b) (hq : q.length = k) (h : (f.toPath.comp q).length = k + 1),
    P (f.toPath.comp q)
⊢ P f

Tactic:
obtain ⟨c, f, q, hq, rfl⟩ := f.eq_toPath_comp_of_length_eq_succ h

Premises used: Quiver.Path.eq_toPath_comp_of_length_eq_succ, rfl
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : Prefunctor.obj (of V) v ⟶ b) (q : u ⟶ v), P p → P (Prefunctor.map (of V) q ≫ p)
k : ℕ
h' : ∀ {a : Paths V} (f : a ⟶ b) (h : Quiver.Path.length f = k), P f
a : Paths V
c : V
f : a ⟶ c
q : Quiver.Path.{v₁, u₁} c b
hq : q.length = k
h : (f.toPath.comp q).length = k + 1
⊢ P (f.toPath.comp q)

Tactic:
comp _ _ (h' _ hq)

Premises used: Quiver.Hom.toPath
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : Prefunctor.obj (of V) v ⟶ b) (q : u ⟶ v), P p → P (Prefunctor.map (of V) q ≫ p)
k : ℕ
h' : ∀ {a : Paths V} (f : a ⟶ b) (h : Quiver.Path.length f = k), P f
a : Paths V
c : V
f : a ⟶ c
q : Quiver.Path.{v₁, u₁} c b
hq : q.length = k
h : (f.toPath.comp q).length = k + 1
⊢ P (f.toPath.comp q)

Tactic:
exact comp _ _ (h' _ hq)
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : Prefunctor.obj (of V) v ⟶ b) (q : u ⟶ v), P p → P (Prefunctor.map (of V) q ≫ p)
a : Paths V
f : a ⟶ b
k : ℕ
h : Quiver.Path.length f = k
zero : ∀ {a : Paths V} (f : a ⟶ b) (h : Quiver.Path.length f = 0), P f
succ :
  ∀ (k : ℕ) (h' : ∀ {a : Paths V} (f : a ⟶ b) (h : Quiver.Path.length f = k), P f) {a : Paths V} (f : a ⟶ b)
    (h : Quiver.Path.length f = k + 1), P f
⊢ P f

Tactic:
induction k generalizing f a with
  | zero => cases f with
    | nil => exact id
    | cons _ _ => simp at h
  | succ k h' =>
    obtain ⟨c, f, q, hq, rfl⟩ := f.eq_toPath_comp_of_length_eq_succ h
    exact comp _ _ (h' _ hq)

Premises used: rfl
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
P : {a b : Paths V} → (a ⟶ b) → Prop
id : ∀ {v : V}, P (𝟙 (Prefunctor.obj (of V) v))
comp :
  ∀ {u v w : V} (p : Prefunctor.obj (of V) u ⟶ Prefunctor.obj (of V) v) (q : v ⟶ w),
    P p → P (p ≫ Prefunctor.map (of V) q)
⊢ ∀ {a b : Paths V} (f : a ⟶ b), P f

Tactic:
fun {_} ↦ induction_fixed_source _ id comp

Premises used: CategoryTheory.Paths.induction_fixed_source
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
P : {a b : Paths V} → (a ⟶ b) → Prop
id : ∀ {v : V}, P (𝟙 (Prefunctor.obj (of V) v))
comp :
  ∀ {u v w : V} (p : u ⟶ v) (q : Prefunctor.obj (of V) v ⟶ Prefunctor.obj (of V) w),
    P q → P (Prefunctor.map (of V) p ≫ q)
a b : Paths V
revert : ∀ {a : Paths V} (f : a ⟶ b), P f
⊢ ∀ (f : a ⟶ b), P f

Tactic:
revert a
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
P : {a b : Paths V} → (a ⟶ b) → Prop
id : ∀ {v : V}, P (𝟙 (Prefunctor.obj (of V) v))
comp :
  ∀ {u v w : V} (p : u ⟶ v) (q : Prefunctor.obj (of V) v ⟶ Prefunctor.obj (of V) w),
    P q → P (Prefunctor.map (of V) p ≫ q)
b a : Paths V
⊢ ∀ (f : a ⟶ b), P f

Tactic:
induction_fixed_target (P := fun f ↦ P f) id (fun _ _ ↦ comp _ _)

Premises used: CategoryTheory.Paths.induction_fixed_target
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
P : {a b : Paths V} → (a ⟶ b) → Prop
id : ∀ {v : V}, P (𝟙 (Prefunctor.obj (of V) v))
comp :
  ∀ {u v w : V} (p : u ⟶ v) (q : Prefunctor.obj (of V) v ⟶ Prefunctor.obj (of V) w),
    P q → P (Prefunctor.map (of V) p ≫ q)
b : Paths V
⊢ ∀ {a : Paths V} (f : a ⟶ b), P f

Tactic:
exact induction_fixed_target (P := fun f ↦ P f) id (fun _ _ ↦ comp _ _)

Premises used: CategoryTheory.Paths.induction_fixed_target