awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hpq' : (p.append q).support.Nodup
⊢ p.support.Disjoint q.tail.support
have hpq'₁ : (p.support ++ q.support.tail).Nodup
Tactic: rw [support_append] at hpq'
Cleared hypotheses: hpq'
-- 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
hpq : (p.append q).IsPath
hq : ¬q.Nil
hpq' : (p.support ++ q.support.tail).Nodup
⊢ p.support.Disjoint q.tail.support
have rw : p.support.Disjoint q.support.tail
Tactic: rw [support_tail_of_not_nil q hq]
-- 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
x : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x ∈ q.support
⊢ False
have hq : ¬q.Nil
Tactic: have hq : ¬q.Nil := by
    intro hq
    simp [nil_iff_support_eq.mp hq, hyv] at hy
-- 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
hpq : (p.append q).IsPath
x : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x ∈ q.support
hq : ¬q.Nil
⊢ x ∈ q.tail.support
have rw : x ∈ q.support.tail
Tactic: rw [support_tail_of_not_nil q hq]
-- 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
x : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x ∈ q.support
hq : ¬q.Nil
⊢ x ∈ q.support.tail
have hy₁ : x = v ∨ x ∈ q.support.tail
Tactic: rw [mem_support_iff] at hy
Cleared hypotheses: hy, hq
-- 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
x : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x ∈ q.support
hq : ¬q.Nil
⊢ False
have hx' : x ∈ q.tail.support
Tactic: have hx' : x ∈ q.tail.support := by
    rw [support_tail_of_not_nil q hq]
    rw [mem_support_iff] at hy
    exact hy.resolve_left hyv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
hp : p.IsCycle
⊢ 3 ≤ p.length
have hp₁ : p.IsTrail
Tactic: have ⟨⟨hp, hp'⟩, _⟩ := hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
hp : p.IsCycle
hp₁ : p.IsTrail
⊢ 3 ≤ p.length
have hp' : p ≠ nil
Tactic: have ⟨⟨hp, hp'⟩, _⟩ := hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
hp : p.IsCycle
hp₁ : p.IsTrail
hp' : p ≠ nil
⊢ 3 ≤ p.length
have support_nodup : p.support.tail.Nodup
Tactic: have ⟨⟨hp, hp'⟩, _⟩ := hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : G.Adj v u
hc : (cons h p).IsCycle
⊢ ¬p.Nil
have this : 3 ≤ p.length + 1
Tactic: have := Walk.length_cons _ _ ▸ Walk.IsCycle.three_le_length hc
-- 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 : G.Adj v u
hc : (cons h p).IsCycle
this : 3 ≤ p.length + 1
⊢ ¬p.Nil
have rw : 0 < p.length
Tactic: rw [Walk.not_nil_iff_lt_length]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
⊢ (cons h p).IsCycle ↔ p.IsPath ∧ s(u, v) ∉ p.edges
have simp : (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
Tactic: simp only [Walk.isCycle_def, Walk.isPath_def, Walk.isTrail_def, edges_cons, List.nodup_cons,
    support_cons, List.tail_cons]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
⊢ (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
have this : p.support.Nodup → p.edges.Nodup
Tactic: have : p.support.Nodup → p.edges.Nodup := edges_nodup_of_support_nodup
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
this : p.support.Nodup → p.edges.Nodup
⊢ (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
have inl : ∀ (this : ¬p.support.Nodup),
  (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
this : p.support.Nodup → p.edges.Nodup
inl :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
⊢ (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
have inr : ∀ (this : p.edges.Nodup),
  (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
this : p.support.Nodup → p.edges.Nodup
inl :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₁ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₁ :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
⊢ (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
have inl₂ : ∀ (this : ¬p.support.Nodup),
  (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
this : p.support.Nodup → p.edges.Nodup
inl :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₁ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₁ :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₂ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
⊢ (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
have inl₃ : ∀ (this : ¬p.support.Nodup),
  p.support.Nodup ∧ s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
this : p.support.Nodup → p.edges.Nodup
inl :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₁ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₁ :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₂ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₃ :
  ∀ (this : ¬p.support.Nodup),
    p.support.Nodup ∧ s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
⊢ (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
have inr₂ : ∀ (this : p.edges.Nodup),
  (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
this : p.support.Nodup → p.edges.Nodup
inl :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₁ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₁ :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₂ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₃ :
  ∀ (this : ¬p.support.Nodup),
    p.support.Nodup ∧ s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inr₂ :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
⊢ (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
have inr₃ : ∀ (this : p.edges.Nodup),
  p.support.Nodup ∧ s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
this : p.support.Nodup → p.edges.Nodup
inl :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₁ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₁ :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₂ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₃ :
  ∀ (this : ¬p.support.Nodup),
    p.support.Nodup ∧ s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inr₂ :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₃ :
  ∀ (this : p.edges.Nodup),
    p.support.Nodup ∧ s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
⊢ (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
have inl₄ : ∀ (this : ¬p.support.Nodup),
  s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
this : p.support.Nodup → p.edges.Nodup
inl :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₁ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₁ :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₂ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₃ :
  ∀ (this : ¬p.support.Nodup),
    p.support.Nodup ∧ s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inr₂ :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₃ :
  ∀ (this : p.edges.Nodup),
    p.support.Nodup ∧ s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inl₄ :
  ∀ (this : ¬p.support.Nodup),
    s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
⊢ (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
have inl₅ : ∀ (this : ¬p.support.Nodup),
  p.support.Nodup → s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
this : p.support.Nodup → p.edges.Nodup
inl :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₁ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₁ :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₂ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₃ :
  ∀ (this : ¬p.support.Nodup),
    p.support.Nodup ∧ s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inr₂ :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₃ :
  ∀ (this : p.edges.Nodup),
    p.support.Nodup ∧ s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inl₄ :
  ∀ (this : ¬p.support.Nodup),
    s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₅ :
  ∀ (this : ¬p.support.Nodup),
    p.support.Nodup → s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
⊢ (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
have inr₄ : ∀ (this : p.edges.Nodup),
  s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
this : p.support.Nodup → p.edges.Nodup
inl :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₁ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₁ :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₂ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₃ :
  ∀ (this : ¬p.support.Nodup),
    p.support.Nodup ∧ s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inr₂ :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₃ :
  ∀ (this : p.edges.Nodup),
    p.support.Nodup ∧ s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inl₄ :
  ∀ (this : ¬p.support.Nodup),
    s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₅ :
  ∀ (this : ¬p.support.Nodup),
    p.support.Nodup → s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inr₄ inr₅ :
  ∀ (this : p.edges.Nodup),
    s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
⊢ (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
have inr₆ : ∀ (this : p.edges.Nodup), s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
this : p.support.Nodup → p.edges.Nodup
inl :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₁ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₁ :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₂ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₃ :
  ∀ (this : ¬p.support.Nodup),
    p.support.Nodup ∧ s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inr₂ :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₃ :
  ∀ (this : p.edges.Nodup),
    p.support.Nodup ∧ s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inl₄ :
  ∀ (this : ¬p.support.Nodup),
    s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₅ :
  ∀ (this : ¬p.support.Nodup),
    p.support.Nodup → s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inr₄ inr₅ :
  ∀ (this : p.edges.Nodup),
    s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₆ : ∀ (this : p.edges.Nodup), s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup
⊢ (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
have inr₇ : ∀ (this : p.edges.Nodup), s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → s(u, v) ∉ p.edges
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
this : p.support.Nodup → p.edges.Nodup
inl :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₁ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₁ :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₂ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₃ :
  ∀ (this : ¬p.support.Nodup),
    p.support.Nodup ∧ s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inr₂ :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₃ :
  ∀ (this : p.edges.Nodup),
    p.support.Nodup ∧ s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inl₄ :
  ∀ (this : ¬p.support.Nodup),
    s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₅ :
  ∀ (this : ¬p.support.Nodup),
    p.support.Nodup → s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inr₄ inr₅ :
  ∀ (this : p.edges.Nodup),
    s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₆ : ∀ (this : p.edges.Nodup), s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup
inr₇ :
  ∀ (this : p.edges.Nodup), s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → s(u, v) ∉ p.edges
⊢ (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
have inr₈ : ∀ (this : p.edges.Nodup),
  p.support.Nodup → s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
Tactic: tauto
Cleared hypotheses: this