awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
⊢ Eq.{v_1 + 1} (α :=
    Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X) ⟶
      Opposite.unop
        (Functor.obj.{v_1, v_1, u_1, u_1}
          (Equivalence.functor (opShiftFunctorEquivalence C 0) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C 0))
          X))
    (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 0))) X))
    (Quiver.Hom.unop
      (Quiver.Hom.op
          (Functor.map (shiftFunctor C (A := ℤ) 0)
            (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X))) ≫
        Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X))))
have a : Eq.{v_1 + 1} (α :=
  Opposite.unop X ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
      (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
  (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 0 0 sorry)) (Opposite.unop X) ≫
      Functor.map (shiftFunctor C (A := ℤ) 0) (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 sorry)) X)) :
    Opposite.unop X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
  (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X) ≫
      Functor.map (shiftFunctor C (A := ℤ) 0) (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X)) :
    Opposite.unop X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
Tactic: dsimp [opShiftFunctorEquivalence]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
⊢ Eq.{v_1 + 1} (α :=
    Opposite.unop X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 0 0 ⋯)) (Opposite.unop X) ≫
        Functor.map (shiftFunctor C (A := ℤ) 0)
          (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X)) :
      Opposite.unop X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
    (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X) ≫
        Functor.map (shiftFunctor C (A := ℤ) 0) (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X)) :
      Opposite.unop X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
have a : Eq.{v_1 + 1} (α :=
  Opposite.unop X ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
      (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
  (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 0 0 sorry)) (Opposite.unop X) ≫
      Functor.map (shiftFunctor C (A := ℤ) 0) (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 sorry)) X)) :
    Opposite.unop X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
  (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X) ≫
      Functor.map (shiftFunctor C (A := ℤ) 0)
        (Quiver.Hom.unop
          (NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 sorry)) X ≫
            Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X)))) :
    Opposite.unop X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
Tactic: rw [shiftFunctorZero_op_hom_app, unop_comp, Quiver.Hom.unop_op, Functor.map_comp,
    shiftFunctorCompIsoId_zero_zero_inv_app, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
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) ≫ f.unop)
have 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))))
Tactic: rw [← opShiftFunctorEquivalenceSymmHomEquiv_left_inv]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Basic (goal)
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''
⊢ homOfEq (homOfEq f hX hY) hX' hY' = homOfEq f ⋯ ⋯
have subst : homOfEq (homOfEq f sorry sorry) sorry sorry = homOfEq f sorry sorry
Tactic: subst hX hY hX' hY'
Cleared hypotheses: X', Y', hX, hY, X'', Y'', hX', hY'
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Basic (hypothesis)
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
⊢ f = g
have h₁ : homOfEq f sorry sorry = homOfEq g sorry sorry
Tactic: subst hX hY
Cleared hypotheses: X', Y', hX, hY, h
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Basic (goal)
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'
⊢ f ≍ f'
have subst : ∀ {f' : X ⟶ Y} (e : homOfEq f sorry sorry = f'), f ≍ f'
Tactic: subst hX hY
Cleared hypotheses: X', Y', hX, hY, f', e
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Basic (hypothesis)
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'
have e₁ : f = f'
Tactic: rw [Quiver.homOfEq_rfl] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Basic (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
X Y : V
f f' : X ⟶ Y
e : f = f'
⊢ f ≍ f'
have rw : f' ≍ f'
Tactic: rw [e]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Basic (goal)
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'
⊢ homOfEq f hX hY = g ↔ f = homOfEq g ⋯ ⋯
have subst : ∀ (g : X ⟶ Y), homOfEq f sorry sorry = g ↔ f = homOfEq g sorry sorry
Tactic: subst hX hY
Cleared hypotheses: X', Y', g, hX, hY
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Basic (goal)
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
⊢ f = homOfEq g hX hY ↔ homOfEq f ⋯ ⋯ = g
have subst : ∀ (f : X' ⟶ Y'), f = homOfEq g sorry sorry ↔ homOfEq f sorry sorry = g
Tactic: subst hX hY
Cleared hypotheses: X, Y, f, hX, hY
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Basic (goal)
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'
⊢ homOfEq f hX hY ≍ g ↔ f ≍ g
have refl : ∀ (g : X ⟶ Y'), homOfEq f sorry hY ≍ g ↔ f ≍ g
Tactic: cases hX
Cleared hypotheses: X', g, hX
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Basic (goal)
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'
⊢ homOfEq f ⋯ hY ≍ g ↔ f ≍ g
have refl : ∀ (g : X ⟶ Y), homOfEq f sorry sorry ≍ g ↔ f ≍ g
Tactic: cases hY
Cleared hypotheses: Y', hY, g
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Basic (goal)
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
⊢ f ≍ homOfEq g hX hY ↔ f ≍ g
have refl : ∀ (g : X ⟶ Y'), f ≍ homOfEq g sorry hY ↔ f ≍ g
Tactic: cases hX
Cleared hypotheses: X', g, hX
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Basic (goal)
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'
⊢ f ≍ homOfEq g ⋯ hY ↔ f ≍ g
have refl : ∀ (g : X ⟶ Y), f ≍ homOfEq g sorry sorry ↔ f ≍ g
Tactic: cases hY
Cleared hypotheses: Y', hY, g
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).IsTrail ↔ p.IsTrail
have subst_vars : ∀ (p : G.Walk u' v'), (p.copy sorry sorry).IsTrail ↔ p.IsTrail
Tactic: subst_vars
Cleared hypotheses: u, v, p, hu, hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).IsPath ↔ p.IsPath
have subst_vars : ∀ (p : G.Walk u' v'), (p.copy sorry sorry).IsPath ↔ p.IsPath
Tactic: subst_vars
Cleared hypotheses: u, v, p, hu, hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u u' : V
p : G.Walk u u
hu : u = u'
⊢ (p.copy hu hu).IsCircuit ↔ p.IsCircuit
have subst_vars : ∀ (p : G.Walk u' u'), (p.copy sorry sorry).IsCircuit ↔ p.IsCircuit
Tactic: subst_vars
Cleared hypotheses: u, p, hu
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u u' : V
p : G.Walk u u
hu : u = u'
⊢ (p.copy hu hu).IsCycle ↔ p.IsCycle
have subst_vars : ∀ (p : G.Walk u' u'), (p.copy sorry sorry).IsCycle ↔ p.IsCycle
Tactic: subst_vars
Cleared hypotheses: u, p, hu
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.IsTrail ↔ p.IsTrail
have mp : p.reverse.IsTrail → p.IsTrail
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
mp : p.reverse.IsTrail → p.IsTrail
⊢ p.reverse.IsTrail ↔ p.IsTrail
have mpr : p.IsTrail → p.reverse.IsTrail
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.reverse.IsTrail
⊢ p.IsTrail
have h₁ : p = p.reverse.reverse
Tactic: convert! h.reverse _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.reverse.IsTrail
⊢ p = p.reverse.reverse
have h₁ : p = p
Tactic: rw [reverse_reverse]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.reverse.IsTrail
⊢ p = p.reverse.reverse
have h₁ : p = p
Tactic: try rw [reverse_reverse]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
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.IsTrail
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
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
⊢ q.IsTrail
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
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
⊢ w.length ≤ G.edgeFinset.card
have this : edges.card = w.length
Tactic: have : edges.card = w.length := length_edges _ ▸ List.toFinset_card_of_nodup h.edges_nodup
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
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
⊢ w.length ≤ G.edgeFinset.card
have rw : edges.card ≤ G.edgeFinset.card
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u)
u v : V
w : G.Walk u v
h_1 : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this : edges.card = w.length
e : Sym2 V
h : e ∈ edges
⊢ e ∈ G.edgeFinset
have refine : e ∈ G.edgeSet
Tactic: refine mem_edgeFinset.mpr ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u)
u v : V
w : G.Walk u v
h_1 : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this : edges.card = w.length
e : Sym2 V
h : e ∈ edges
⊢ e ∈ G.edgeSet
have a : e ∈ w.edges
Tactic: apply w.edges_subset_edgeSet
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
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
⊢ edges.card ≤ G.edgeFinset.card
have this₁ : edges ⊆ G.edgeFinset
Tactic: have : edges ⊆ G.edgeFinset := by
    intro e h
    refine mem_edgeFinset.mpr ?_
    apply w.edges_subset_edgeSet
    simpa [edges] using h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u)
u v : V
w : G.Walk u v
h : w.IsTrail
let let₁ let₂ : w.length ≤ G.edgeFinset.card
⊢ w.length ≤ G.edgeFinset.card
have let₃ : let edges := w.edges.toFinset;
∀ (this : edges.card = w.length), w.length ≤ G.edgeFinset.card
Tactic: classical
  let edges := w.edges.toFinset
  have : edges.card = w.length := length_edges _ ▸ List.toFinset_card_of_nodup h.edges_nodup
  rw [← this]
  have : edges ⊆ G.edgeFinset := by
    intro e h
    refine mem_edgeFinset.mpr ?_
    apply w.edges_subset_edgeSet
    simpa [edges] using h
  exact Finset.card_le_card this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u)
u v : V
w : G.Walk u v
h : w.IsTrail
let let₁ let₂ : w.length ≤ G.edgeFinset.card
let₃ :
  let edges := w.edges.toFinset;
  ∀ (this : edges.card = w.length), w.length ≤ G.edgeFinset.card
⊢ w.length ≤ G.edgeFinset.card
have let₄ : let edges := w.edges.toFinset;
∀ (this : edges.card = w.length), edges.card ≤ G.edgeFinset.card
Tactic: classical
  let edges := w.edges.toFinset
  have : edges.card = w.length := length_edges _ ▸ List.toFinset_card_of_nodup h.edges_nodup
  rw [← this]
  have : edges ⊆ G.edgeFinset := by
    intro e h
    refine mem_edgeFinset.mpr ?_
    apply w.edges_subset_edgeSet
    simpa [edges] using h
  exact Finset.card_le_card this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u)
u v : V
w : G.Walk u v
h : w.IsTrail
let let₁ let₂ : w.length ≤ G.edgeFinset.card
let₃ :
  let edges := w.edges.toFinset;
  ∀ (this : edges.card = w.length), w.length ≤ G.edgeFinset.card
let₄ :
  let edges := w.edges.toFinset;
  ∀ (this : edges.card = w.length), edges.card ≤ G.edgeFinset.card
⊢ w.length ≤ G.edgeFinset.card
have let₅ : let edges := w.edges.toFinset;
∀ (this : edges.card = w.length) (this : edges ⊆ G.edgeFinset), edges.card ≤ G.edgeFinset.card
Tactic: classical
  let edges := w.edges.toFinset
  have : edges.card = w.length := length_edges _ ▸ List.toFinset_card_of_nodup h.edges_nodup
  rw [← this]
  have : edges ⊆ G.edgeFinset := by
    intro e h
    refine mem_edgeFinset.mpr ?_
    apply w.edges_subset_edgeSet
    simpa [edges] using h
  exact Finset.card_le_card this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ IsPath.{u} (V := V) (G := G) (u := u) Walk.nil
have isTrail : IsTrail.{u} (V := V) (G := G) (u := u) Walk.nil
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u : V
isTrail : IsTrail.{u} (V := V) (G := G) (u := u) Walk.nil
⊢ IsPath.{u} (V := V) (G := G) (u := u) Walk.nil
have support_nodup : List.Nodup.{u} (α := V) (support (G := G) (u := u) Walk.nil)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h p).IsPath ↔ p.IsPath ∧ u ∉ p.support
have mp : (cons h p).IsPath → p.IsPath ∧ u ∉ p.support
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
mp : (cons h p).IsPath → p.IsPath ∧ u ∉ p.support
⊢ (cons h p).IsPath ↔ p.IsPath ∧ u ∉ p.support
have mpr : p.IsPath ∧ u ∉ p.support → (cons h p).IsPath
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.IsPath ↔ p = nil
have nil : IsPath.{u} (V := V) (G := G) (u := u) nil ↔ Eq.{u + 1} (α := G.Walk u u) nil nil
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
nil : IsPath.{u} (V := V) (G := G) (u := u) Walk.nil ↔ Eq.{u + 1} (α := G.Walk u u) Walk.nil Walk.nil
⊢ p.IsPath ↔ p = Walk.nil
have cons : ∀ {v : V} (h : G.Adj u v) (p : G.Walk v u), (cons h p).IsPath ↔ cons h p = Walk.nil
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.IsPath ↔ p.IsPath
have mp : p.reverse.IsPath → p.IsPath
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
mp : p.reverse.IsPath → p.IsPath
⊢ p.reverse.IsPath ↔ p.IsPath
have mpr : p.IsPath → p.reverse.IsPath
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.reverse.IsPath
⊢ p.IsPath
have h₁ : p = p.reverse.reverse
Tactic: convert! h.reverse
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
⊢ (p.append q).IsPath → p.IsPath
have simp : (p.support ++ q.support.tail).Nodup → p.support.Nodup
Tactic: simp only [isPath_def, support_append]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
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).IsPath
⊢ q.IsPath
have rw : ∀ (h : (p.append q).reverse.IsPath), q.reverse.IsPath
Tactic: rw [← isPath_reverse_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
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).reverse.IsPath
⊢ q.reverse.IsPath
have h₁ : (q.reverse.append p.reverse).IsPath
Tactic: rw [reverse_append] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h : p₁.IsSubwalk p₂
h₂ : p₂.IsTrail
⊢ p₁.IsTrail
have obtain : ∀ (w_1 : G.Walk v' v) (w_2 : G.Walk w w') (h : p₂ = (w_1.append p₁).append w_2), p₁.IsTrail
Tactic: obtain ⟨_, _, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h₂ : p₂.IsTrail
w_1 : G.Walk v' v
w_2 : G.Walk w w'
h : p₂ = (w_1.append p₁).append w_2
⊢ p₁.IsTrail
have h₃ : ((w_1.append p₁).append w_2).IsTrail
Tactic: rw [h] at h₂
Cleared hypotheses: h₂, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h : p₁.IsSubwalk p₂
h₂ : p₂.IsPath
⊢ p₁.IsPath
have obtain : ∀ (w_1 : G.Walk v' v) (w_2 : G.Walk w w') (h : p₂ = (w_1.append p₁).append w_2), p₁.IsPath
Tactic: obtain ⟨_, _, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h₂ : p₂.IsPath
w_1 : G.Walk v' v
w_2 : G.Walk w w'
h : p₂ = (w_1.append p₁).append w_2
⊢ p₁.IsPath
have h₃ : ((w_1.append p₁).append w_2).IsPath
Tactic: rw [h] at h₂
Cleared hypotheses: h₂, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ (p.concat h).IsPath ↔ p.IsPath ∧ w ∉ p.support
have rw : (cons sorry p.reverse).IsPath ↔ p.reverse.IsPath ∧ w ∉ p.reverse.support
Tactic: rw [← (p.concat h).isPath_reverse_iff, ← p.isPath_reverse_iff, reverse_concat, ← List.mem_reverse,
    ← support_reverse]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
⊢ w ∈ p.support ↔ ∃ (q : G.Walk u w) (r : G.Walk w v), q.IsPath ∧ r.IsPath ∧ p = q.append r
have refine : ∀ (hw : w ∈ p.support), ∃ (q : G.Walk u w) (r : G.Walk w v), q.IsPath ∧ r.IsPath ∧ p = q.append r
Tactic: refine ⟨fun hw ↦ ?_, fun ⟨q, r, hq, hr, hqr⟩ ↦ p.mem_support_iff_exists_append.mpr ⟨q, r, hqr⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
⊢ ∃ (q : G.Walk u w) (r : G.Walk w v), q.IsPath ∧ r.IsPath ∧ p = q.append r
have obtain : ∀ (q : G.Walk u w) (r : G.Walk w v) (hqr : p = q.append r),
  ∃ (q : G.Walk u w) (r : G.Walk w v), q.IsPath ∧ r.IsPath ∧ p = q.append r
Tactic: obtain ⟨q, r, hqr⟩ := p.mem_support_iff_exists_append.mp hw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
q : G.Walk u w
r : G.Walk w v
hqr : p = q.append r
⊢ ∃ (q : G.Walk u w) (r : G.Walk w v), q.IsPath ∧ r.IsPath ∧ p = q.append r
have this : (q.append r).IsPath
Tactic: have : (q.append r).IsPath := hqr ▸ hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
hq : ¬q.Nil
⊢ p.support.Disjoint q.tail.support
have hpq' : (p.append q).support.Nodup
Tactic: have hpq' := hpq.support_nodup