awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
n : ℤ
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙ Equivalence.functor (opShiftFunctorEquivalence C n))
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))
    (NatTrans.app (Iso.hom (Equivalence.counitIso (opShiftFunctorEquivalence C n)))
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))
    (Functor.map (shiftFunctor Cᵒᵖ n) (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n))) X))

Tactic:
(opShiftFunctorEquivalence C n).counit_app_functor X

Premises used: CategoryTheory.Functor.op, CategoryTheory.shiftFunctor, Int.add.match_1, Int.add, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence, Int.neg, CategoryTheory.Equivalence.counit_app_functor
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
n m : ℤ
hnm : autoParam (n + m = 0) shiftFunctorCompIsoId_op_hom_app._auto_1
⊢ m + n = 0

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
n m : ℤ
hnm : n + m = 0
⊢ m + n = 0

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
n m : ℤ
hnm : n + m = 0
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n ⋙ shiftFunctor Cᵒᵖ m) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X)
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId Cᵒᵖ n m hnm)) X)
    (Functor.map (shiftFunctor Cᵒᵖ m) (NatTrans.app (Iso.hom (shiftFunctorOpIso C n m hnm)) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorOpIso C m n ⋯))
          (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) (Opposite.unop X))) ≫
        Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C m n ⋯)) (Opposite.unop X)))

Tactic:
simp [shiftFunctorCompIsoId, shiftFunctorZero_op_hom_app X,
    shiftFunctorAdd'_op_inv_app X n m 0 hnm m n 0 hnm (by lia) (add_zero 0)]

Premises used: CategoryTheory.Pretriangulated.shiftFunctorAdd'_op_inv_app, CategoryTheory.Pretriangulated.shiftFunctorZero_op_hom_app, CategoryTheory.shiftFunctorCompIsoId, add_zero, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
n m : ℤ
hnm : autoParam (n + m = 0) shiftFunctorCompIsoId_op_inv_app._auto_1
⊢ m + n = 0

Tactic:
omega
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
n m : ℤ
hnm : n + m = 0
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n ⋙ shiftFunctor Cᵒᵖ m) X)
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId Cᵒᵖ n m hnm)) X)
    (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C m n ⋯)) (Opposite.unop X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorOpIso C m n ⋯))
          (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) (Opposite.unop X))) ≫
        Functor.map (shiftFunctor Cᵒᵖ m) (NatTrans.app (Iso.inv (shiftFunctorOpIso C n m hnm)) X))

Tactic:
simp [shiftFunctorCompIsoId, shiftFunctorZero_op_inv_app X,
    shiftFunctorAdd'_op_hom_app X n m 0 hnm m n 0 hnm (by lia) (add_zero 0)]

Premises used: CategoryTheory.Pretriangulated.shiftFunctorZero_op_inv_app, CategoryTheory.Pretriangulated.shiftFunctorAdd'_op_hom_app, CategoryTheory.shiftFunctorCompIsoId, add_zero, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : C
m n : ℤ
hmn : m + n = 0
⊢ m = -n

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : C
n : ℤ
hmn : -n + n = 0
⊢ n + -n = 0

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
n : ℤ
X Y : Cᵒᵖ
f : Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (Opposite.unop X)) ⟶ Y
⊢ Eq (α := X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) Y)
    ((opShiftFunctorEquivalenceSymmHomEquiv :
          (a : Opposite.op ((shiftFunctor C n).obj (Opposite.unop X)) ⟶ Y) → X ⟶ (shiftFunctor Cᵒᵖ n).obj Y)
        f :
      X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) Y)
    (CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1}
          (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙ Equivalence.functor (opShiftFunctorEquivalence C n)) X)
        (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C n))) X)
        (Functor.map (shiftFunctor Cᵒᵖ n) f) :
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) Y)

Tactic:
rfl

Premises used: Quiver.Hom.op, rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
n : ℤ
X Y : Cᵒᵖ
f : Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (Opposite.unop X)) ⟶ Y
⊢ CategoryStruct.comp (Y :=
      Opposite.unop
        (Functor.obj.{v_1, v_1, u_1, u_1}
          (Equivalence.functor (opShiftFunctorEquivalence C n) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C n))
          Y))
      (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n))) Y))
      (Functor.map (shiftFunctor C n)
        (Quiver.Hom.unop
          ((opShiftFunctorEquivalenceSymmHomEquiv :
              (a : Opposite.op ((shiftFunctor C n).obj (Opposite.unop X)) ⟶ Y) → X ⟶ (shiftFunctor Cᵒᵖ n).obj Y)
            f))) =
    f.unop

Tactic:
Quiver.Hom.op_inj (opShiftFunctorEquivalenceSymmHomEquiv.left_inv f)

Premises used: CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv, Quiver.Hom.op_inj, Equiv.left_inv
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
n : ℤ
X Y : Cᵒᵖ
f : Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (Opposite.unop X)) ⟶ Y
rw :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) Y)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (Opposite.unop X))
    (Functor.map (shiftFunctor C n)
      (Quiver.Hom.unop
        ((opShiftFunctorEquivalenceSymmHomEquiv :
            (a : Opposite.op ((shiftFunctor C n).obj (Opposite.unop X)) ⟶ Y) → X ⟶ (shiftFunctor Cᵒᵖ n).obj Y)
          f)))
    (Quiver.Hom.unop (NatTrans.app (Iso.hom (Equivalence.unitIso (opShiftFunctorEquivalence C n))) Y) ≫
      CategoryStruct.comp (Y :=
        Opposite.unop
          (Functor.obj.{v_1, v_1, u_1, u_1}
            (Equivalence.functor (opShiftFunctorEquivalence C n) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C n))
            Y))
        (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n))) Y))
        (Functor.map (shiftFunctor C n)
          (Quiver.Hom.unop
            ((opShiftFunctorEquivalenceSymmHomEquiv :
                (a : Opposite.op ((shiftFunctor C n).obj (Opposite.unop X)) ⟶ Y) → X ⟶ (shiftFunctor Cᵒᵖ n).obj Y)
              f))))
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) Y)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (Opposite.unop X))
    (Functor.map (shiftFunctor C n)
      (Quiver.Hom.unop
        ((opShiftFunctorEquivalenceSymmHomEquiv :
            (a : Opposite.op ((shiftFunctor C n).obj (Opposite.unop X)) ⟶ Y) → X ⟶ (shiftFunctor Cᵒᵖ n).obj Y)
          f)))
    (Quiver.Hom.unop (NatTrans.app (Iso.hom (Equivalence.unitIso (opShiftFunctorEquivalence C n))) Y) ≫ f.unop)

Tactic:
rw [← opShiftFunctorEquivalenceSymmHomEquiv_left_inv]

Premises used: CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_left_inv
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
n : ℤ
X Y : Cᵒᵖ
f : Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (Opposite.unop X)) ⟶ Y
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) Y)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (Opposite.unop X))
    (Functor.map (shiftFunctor C n)
      (Quiver.Hom.unop
        ((opShiftFunctorEquivalenceSymmHomEquiv :
            (a : Opposite.op ((shiftFunctor C n).obj (Opposite.unop X)) ⟶ Y) → X ⟶ (shiftFunctor Cᵒᵖ n).obj Y)
          f)))
    (Quiver.Hom.unop (NatTrans.app (Iso.hom (Equivalence.unitIso (opShiftFunctorEquivalence C n))) Y) ≫
      CategoryStruct.comp (Y :=
        Opposite.unop
          (Functor.obj.{v_1, v_1, u_1, u_1}
            (Equivalence.functor (opShiftFunctorEquivalence C n) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C n))
            Y))
        (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n))) Y))
        (Functor.map (shiftFunctor C n)
          (Quiver.Hom.unop
            ((opShiftFunctorEquivalenceSymmHomEquiv :
                (a : Opposite.op ((shiftFunctor C n).obj (Opposite.unop X)) ⟶ Y) → X ⟶ (shiftFunctor Cᵒᵖ n).obj Y)
              f))))

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.Basic
Goal:
V : Type u
a b : Empty V
⊢ (a ⟶ b) = PEmpty

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Quiver.Basic
Goal:
V : Type u
inst : Quiver.{u_1, u} V
⊢ ∀ (_ : ∀ (a b : V), Subsingleton.{u_1 + 1} (a ⟶ b)) (a b : V), Subsingleton.{u_1 + 1} (b ⟶ a)

Tactic:
fun inst a b ↦ inst b a
-- Module: Mathlib.Combinatorics.Quiver.Basic
Goal:
V : Type u
inst : Quiver.{u_1, u} V
⊢ ∀ (_ : ∀ (a b : V), Subsingleton.{u_1 + 1} (b ⟶ a)) (a b : V), Subsingleton.{u_1 + 1} (a ⟶ b)

Tactic:
fun inst a b ↦ inst b a
-- Module: Mathlib.Combinatorics.Quiver.Basic
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
X Y X' Y' : V
f : X ⟶ Y
hX : X = X'
hY : Y = Y'
subst : X ⟶ Y
⊢ X' ⟶ Y'

Tactic:
subst hX hY
-- Module: Mathlib.Combinatorics.Quiver.Basic
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
X Y : V
f : X ⟶ Y
⊢ X ⟶ Y

Tactic:
exact f
-- Module: Mathlib.Combinatorics.Quiver.Basic
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
X Y X' Y' : V
f : X ⟶ Y
hX : X = X'
hY : Y = Y'
X'' Y'' : V
hX' : X' = X''
hY' : Y' = Y''
subst : homOfEq (homOfEq f ⋯ ⋯) ⋯ ⋯ = homOfEq f ⋯ ⋯
⊢ homOfEq (homOfEq f hX hY) hX' hY' = homOfEq f ⋯ ⋯

Tactic:
subst hX hY hX' hY'
-- Module: Mathlib.Combinatorics.Quiver.Basic
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
X Y : V
f : X ⟶ Y
⊢ homOfEq (homOfEq f ⋯ ⋯) ⋯ ⋯ = homOfEq f ⋯ ⋯

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Basic
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
X Y X' Y' : V
hX : X = X'
hY : Y = Y'
f g : X ⟶ Y
h : homOfEq f hX hY = homOfEq g hX hY
⊢ homOfEq f ⋯ ⋯ = homOfEq g ⋯ ⋯

Tactic:
subst hX hY
-- Module: Mathlib.Combinatorics.Quiver.Basic
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
X Y : V
f g : X ⟶ Y
h : homOfEq f ⋯ ⋯ = homOfEq g ⋯ ⋯
⊢ f = g

Tactic:
h

Premises used: Quiver.homOfEq
-- Module: Mathlib.Combinatorics.Quiver.Basic
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
X Y : V
f g : X ⟶ Y
h : homOfEq f ⋯ ⋯ = homOfEq g ⋯ ⋯
⊢ f = g

Tactic:
exact h
-- Module: Mathlib.Combinatorics.Quiver.Basic
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
X Y : V
f : X ⟶ Y
⊢ homOfEq f ⋯ ⋯ = f

Tactic:
rfl

Premises used: Quiver.homOfEq, rfl
-- Module: Mathlib.Combinatorics.Quiver.Basic
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
X Y X' Y' : V
hX : X = X'
hY : Y = Y'
f : X ⟶ Y
f' : X' ⟶ Y'
e : homOfEq f hX hY = f'
subst : ∀ {f' : X ⟶ Y} (e : homOfEq f ⋯ ⋯ = f'), f ≍ f'
⊢ f ≍ f'

Tactic:
subst hX hY
-- Module: Mathlib.Combinatorics.Quiver.Basic
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
X Y : V
f f' : X ⟶ Y
e : homOfEq f ⋯ ⋯ = f'
⊢ f = f'

Tactic:
rw [Quiver.homOfEq_rfl] at e

Premises used: Quiver.homOfEq_rfl
-- Module: Mathlib.Combinatorics.Quiver.Basic
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
X Y : V
f f' : X ⟶ Y
e : f = f'
rw rw₁ : f' ≍ f'
⊢ f ≍ f'

Tactic:
rw [e]
-- Module: Mathlib.Combinatorics.Quiver.Basic
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
X Y X' Y' : V
f : X ⟶ Y
g : X' ⟶ Y'
hX : X = X'
hY : Y = Y'
subst : ∀ (g : X ⟶ Y), homOfEq f ⋯ ⋯ = g ↔ f = homOfEq g ⋯ ⋯
⊢ homOfEq f hX hY = g ↔ f = homOfEq g ⋯ ⋯

Tactic:
subst hX hY
-- Module: Mathlib.Combinatorics.Quiver.Basic
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
X Y : V
f g : X ⟶ Y
⊢ homOfEq f ⋯ ⋯ = g ↔ f = homOfEq g ⋯ ⋯

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.Basic
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
X Y X' Y' : V
f : X ⟶ Y
g : X' ⟶ Y'
hX : X' = X
hY : Y' = Y
subst : ∀ (f : X' ⟶ Y'), f = homOfEq g ⋯ ⋯ ↔ homOfEq f ⋯ ⋯ = g
⊢ f = homOfEq g hX hY ↔ homOfEq f ⋯ ⋯ = g

Tactic:
subst hX hY
-- Module: Mathlib.Combinatorics.Quiver.Basic
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
X' Y' : V
g f : X' ⟶ Y'
⊢ f = homOfEq g ⋯ ⋯ ↔ homOfEq f ⋯ ⋯ = g

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.Basic
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
X Y X' Y' : V
hX : X = X'
hY : Y = Y'
f : X ⟶ Y
⊢ homOfEq f hX hY ≍ f

Tactic:
(heq_of_homOfEq_ext hX hY rfl).symm

Premises used: HEq.symm, rfl, Quiver.heq_of_homOfEq_ext
-- Module: Mathlib.Combinatorics.Quiver.Basic
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
X Y X' Y' : V
f : X ⟶ Y
g : X' ⟶ Y'
hX : X = X'
hY : Y = Y'
refl : ∀ (g : X ⟶ Y'), homOfEq f ⋯ hY ≍ g ↔ f ≍ g
⊢ homOfEq f hX hY ≍ g ↔ f ≍ g

Tactic:
cases hX
-- Module: Mathlib.Combinatorics.Quiver.Basic
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
X Y Y' : V
f : X ⟶ Y
hY : Y = Y'
g : X ⟶ Y'
refl : ∀ (g : X ⟶ Y), homOfEq f ⋯ ⋯ ≍ g ↔ f ≍ g
⊢ homOfEq f ⋯ hY ≍ g ↔ f ≍ g

Tactic:
cases hY
-- Module: Mathlib.Combinatorics.Quiver.Basic
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
X Y : V
f g : X ⟶ Y
⊢ homOfEq f ⋯ ⋯ ≍ g ↔ f ≍ g

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Basic
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
X Y X' Y' : V
f : X ⟶ Y
g : X' ⟶ Y'
hX : X' = X
hY : Y' = Y
refl : ∀ (g : X ⟶ Y'), f ≍ homOfEq g ⋯ hY ↔ f ≍ g
⊢ f ≍ homOfEq g hX hY ↔ f ≍ g

Tactic:
cases hX
-- Module: Mathlib.Combinatorics.Quiver.Basic
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
X Y Y' : V
f : X ⟶ Y
hY : Y' = Y
g : X ⟶ Y'
refl : ∀ (g : X ⟶ Y), f ≍ homOfEq g ⋯ ⋯ ↔ f ≍ g
⊢ f ≍ homOfEq g ⋯ hY ↔ f ≍ g

Tactic:
cases hY
-- Module: Mathlib.Combinatorics.Quiver.Basic
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
X Y : V
f g : X ⟶ Y
⊢ f ≍ homOfEq g ⋯ ⋯ ↔ f ≍ g

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
subst_vars : ∀ (p : G.Walk u' v'), (p.copy ⋯ ⋯).IsTrail ↔ p.IsTrail
⊢ (p.copy hu hv).IsTrail ↔ p.IsTrail

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).IsTrail ↔ p.IsTrail

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.support.Nodup
⊢ p.IsPath

Tactic:
⟨⟨edges_nodup_of_support_nodup h⟩, h⟩

Premises used: SimpleGraph.Walk.edges_nodup_of_support_nodup, SimpleGraph.Walk.IsTrail.mk, SimpleGraph.Walk.IsPath.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.IsPath ↔ p.support.Nodup

Tactic:
⟨IsPath.support_nodup, IsPath.mk'⟩

Premises used: Iff.intro, SimpleGraph.Walk.IsPath.support_nodup, SimpleGraph.Walk.IsPath.mk'
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.IsPath ↔ Injective.{1, u + 1} (β := V) fun (x : Fin p.support.length) ↦ p.support.get x

Tactic:
p.isPath_def.trans List.nodup_iff_injective_get

Premises used: SimpleGraph.Walk.isPath_def, Iff.trans, List.nodup_iff_injective_get
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
subst_vars : ∀ (p : G.Walk u' v'), (p.copy ⋯ ⋯).IsPath ↔ p.IsPath
⊢ (p.copy hu hv).IsPath ↔ p.IsPath

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).IsPath ↔ p.IsPath

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u u' : V
p : G.Walk u u
hu : u = u'
subst_vars : ∀ (p : G.Walk u' u'), (p.copy ⋯ ⋯).IsCircuit ↔ p.IsCircuit
⊢ (p.copy hu hu).IsCircuit ↔ p.IsCircuit

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u' : V
p : G.Walk u' u'
⊢ (p.copy ⋯ ⋯).IsCircuit ↔ p.IsCircuit

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
hp : p.IsCircuit
⊢ ¬p.Nil

Tactic:
(hp.ne_nil ·.eq_nil)

Premises used: SimpleGraph.Walk.Nil.eq_nil, SimpleGraph.Walk.IsCircuit.ne_nil, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.IsCycle ↔ p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup

Tactic:
Iff.intro (fun h => ⟨h.1.1, h.1.2, h.2⟩) fun h => ⟨⟨h.1, h.2.1⟩, h.2.2⟩

Premises used: SimpleGraph.Walk.IsCircuit.mk, SimpleGraph.Walk.IsCircuit.isTrail, SimpleGraph.Walk.IsCircuit.ne_nil, And.right, And.left, And.intro, Iff.intro, SimpleGraph.Walk.IsCycle.support_nodup, SimpleGraph.Walk.IsCycle.isCircuit, SimpleGraph.Walk.IsCycle.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u u' : V
p : G.Walk u u
hu : u = u'
subst_vars : ∀ (p : G.Walk u' u'), (p.copy ⋯ ⋯).IsCycle ↔ p.IsCycle
⊢ (p.copy hu hu).IsCycle ↔ p.IsCycle

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u' : V
p : G.Walk u' u'
⊢ (p.copy ⋯ ⋯).IsCycle ↔ p.IsCycle

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
hp : p.IsCycle
⊢ ¬p.Nil

Tactic:
(hp.ne_nil ·.eq_nil)

Premises used: SimpleGraph.Walk.Nil.eq_nil, SimpleGraph.Walk.IsCircuit.ne_nil, SimpleGraph.Walk.IsCycle.isCircuit, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ List.Nodup.{u} (α := Sym2 V) (edges (G := G) (u := u) Walk.nil)

Tactic:
simp [edges]

Premises used: SimpleGraph.Walk.edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h p).IsTrail → p.IsTrail

Tactic:
simp [isTrail_def]

Premises used: SimpleGraph.Walk.isTrail_def
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h p).IsTrail ↔ p.IsTrail ∧ s(u, v) ∉ p.edges

Tactic:
simp [isTrail_def, and_comm]

Premises used: SimpleGraph.Walk.isTrail_def, and_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u u' v : V
w : G.Walk u' v
hw : w.IsTrail
hu : G.Adj u u'
hu' : s(u, u') ∉ w.edges
⊢ (cons hu w).IsTrail

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.IsTrail
⊢ p.reverse.IsTrail

Tactic:
simpa [isTrail_def] using h

Premises used: SimpleGraph.Walk.isTrail_def
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
mp : p.reverse.IsTrail → p.IsTrail
mpr : p.IsTrail → p.reverse.IsTrail
⊢ p.reverse.IsTrail ↔ p.IsTrail

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.reverse.IsTrail
⊢ p.reverse.reverse.IsTrail

Tactic:
h.reverse _

Premises used: SimpleGraph.Walk.IsTrail.reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.reverse.IsTrail
h₁ : p = p.reverse.reverse
⊢ p.IsTrail

Tactic:
convert! h.reverse _

Premises used: SimpleGraph.Walk.IsTrail.reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.reverse.IsTrail
h₁ h₂ : p = p
⊢ p = p.reverse.reverse

Tactic:
rw [reverse_reverse]

Premises used: SimpleGraph.Walk.reverse_reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.reverse.IsTrail
h₁ h₂ : p = p
⊢ p = p.reverse.reverse

Tactic:
try rw [reverse_reverse]

Premises used: SimpleGraph.Walk.reverse_reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.IsTrail
⊢ p.reverse.IsTrail

Tactic:
h.reverse _

Premises used: SimpleGraph.Walk.IsTrail.reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.IsTrail
⊢ p.reverse.IsTrail

Tactic:
convert! h.reverse _

Premises used: SimpleGraph.Walk.IsTrail.reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : (p.append q).IsTrail
⊢ p.edges.Nodup ∧ q.edges.Nodup ∧ ∀ a ∈ p.edges, ∀ b ∈ q.edges, a ≠ b

Tactic:
rw [isTrail_def, edges_append, List.nodup_append] at h

Premises used: SimpleGraph.Walk.isTrail_def, List.nodup_append, SimpleGraph.Walk.edges_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : p.edges.Nodup ∧ q.edges.Nodup ∧ ∀ a ∈ p.edges, ∀ b ∈ q.edges, a ≠ b
⊢ p.IsTrail

Tactic:
⟨h.1⟩

Premises used: SimpleGraph.Walk.IsTrail.mk, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : p.edges.Nodup ∧ q.edges.Nodup ∧ ∀ a ∈ p.edges, ∀ b ∈ q.edges, a ≠ b
⊢ p.IsTrail

Tactic:
exact ⟨h.1⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : p.edges.Nodup ∧ q.edges.Nodup ∧ ∀ a ∈ p.edges, ∀ b ∈ q.edges, a ≠ b
⊢ q.IsTrail

Tactic:
⟨h.2.1⟩

Premises used: SimpleGraph.Walk.IsTrail.mk, And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : p.edges.Nodup ∧ q.edges.Nodup ∧ ∀ a ∈ p.edges, ∀ b ∈ q.edges, a ≠ b
⊢ q.IsTrail

Tactic:
exact ⟨h.2.1⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsTrail
e : Sym2 V
⊢ List.count e p.edges ≤ 1

Tactic:
List.nodup_iff_count_le_one.mp h.edges_nodup e

Premises used: SimpleGraph.Walk.IsTrail.edges_nodup, Iff.mp, List.nodup_iff_count_le_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsTrail
e : Sym2 V
he : e ∈ p.edges
⊢ List.count e p.edges = 1

Tactic:
List.count_eq_one_of_mem h.edges_nodup he

Premises used: SimpleGraph.Walk.IsTrail.edges_nodup, List.count_eq_one_of_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u)
u v : V
w : G.Walk u v
h : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
⊢ edges.card = w.length

Tactic:
have : edges.card = w.length := length_edges _ ▸ List.toFinset_card_of_nodup h.edges_nodup
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u)
u v : V
w : G.Walk u v
h : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this : edges.card = w.length
rw : edges.card ≤ G.edgeFinset.card
⊢ w.length ≤ G.edgeFinset.card

Tactic:
rw [← this]