awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s t v w : V
rw : Adj (fromEdgeSet {s(s, t)}) v w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
rw₁ : Membership.mem (γ := Set (Sym2 V)) {s(s, t)} s(v, w) ∧ v ≠ w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
⊢ (edge s t).Adj v w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
have rw₂ : s(v, w) = s(s, t) ∧ v ≠ w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
Tactic: rw [edge, fromEdgeSet_adj, Set.mem_singleton_iff, Sym2.eq_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s t v w : V
rw : Adj (fromEdgeSet {s(s, t)}) v w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
rw₁ : Membership.mem (γ := Set (Sym2 V)) {s(s, t)} s(v, w) ∧ v ≠ w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
rw₂ : s(v, w) = s(s, t) ∧ v ≠ w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
⊢ (edge s t).Adj v w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
have rw₃ : (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
Tactic: rw [edge, fromEdgeSet_adj, Set.mem_singleton_iff, Sym2.eq_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s t v w : V
⊢ (edge s t).Adj v w ↔ s(s, t) = s(v, w) ∧ v ≠ w
have simp : ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
Tactic: simp only [edge_adj, ne_eq, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk,
    and_congr_left_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s t v w : V
tauto tauto₁ : ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
⊢ ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
have mp : ¬v = w → v = s ∧ w = t ∨ v = t ∧ w = s → s = v ∧ t = w ∨ s = w ∧ t = v
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s t v w : V
tauto tauto₁ : ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
mp : ¬v = w → v = s ∧ w = t ∨ v = t ∧ w = s → s = v ∧ t = w ∨ s = w ∧ t = v
⊢ ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
have mpr : ¬v = w → s = v ∧ t = w ∨ s = w ∧ t = v → v = s ∧ w = t ∨ v = t ∧ w = s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s t v w : V
tauto tauto₁ : ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
mp : ¬v = w → v = s ∧ w = t ∨ v = t ∧ w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mpr : ¬v = w → s = v ∧ t = w ∨ s = w ∧ t = v → v = s ∧ w = t ∨ v = t ∧ w = s
⊢ ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
have mp₁ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s t v w : V
tauto tauto₁ : ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
mp : ¬v = w → v = s ∧ w = t ∨ v = t ∧ w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mpr : ¬v = w → s = v ∧ t = w ∨ s = w ∧ t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mp₁ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
⊢ ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
have mp₂ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s t v w : V
tauto tauto₁ : ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
mp : ¬v = w → v = s ∧ w = t ∨ v = t ∧ w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mpr : ¬v = w → s = v ∧ t = w ∨ s = w ∧ t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mp₁ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₂ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₃ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₄ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
⊢ ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
have mp₅ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → s = w
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s t v w : V
tauto tauto₁ : ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
mp : ¬v = w → v = s ∧ w = t ∨ v = t ∧ w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mpr : ¬v = w → s = v ∧ t = w ∨ s = w ∧ t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mp₁ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₂ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₃ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₄ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₅ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → s = w
⊢ ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
have mp₆ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → t = v
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s t v w : V
tauto tauto₁ : ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
mp : ¬v = w → v = s ∧ w = t ∨ v = t ∧ w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mpr : ¬v = w → s = v ∧ t = w ∨ s = w ∧ t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mp₁ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₂ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₃ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₄ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₅ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → s = w
mp₆ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → t = v
⊢ ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
have mp₇ : ¬v = w → v = t → w = s → ¬(s = v ∧ t = w) → s = w
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s t v w : V
tauto tauto₁ : ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
mp : ¬v = w → v = s ∧ w = t ∨ v = t ∧ w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mpr : ¬v = w → s = v ∧ t = w ∨ s = w ∧ t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mp₁ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₂ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₃ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₄ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₅ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → s = w
mp₆ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → t = v
mp₇ : ¬v = w → v = t → w = s → ¬(s = v ∧ t = w) → s = w
⊢ ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
have mp₈ : ¬v = w → v = t → w = s → ¬(s = v ∧ t = w) → t = v
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s t v w : V
tauto tauto₁ : ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
mp : ¬v = w → v = s ∧ w = t ∨ v = t ∧ w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mpr : ¬v = w → s = v ∧ t = w ∨ s = w ∧ t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mp₁ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₂ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₃ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₄ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₅ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → s = w
mp₆ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → t = v
mp₇ : ¬v = w → v = t → w = s → ¬(s = v ∧ t = w) → s = w
mp₈ : ¬v = w → v = t → w = s → ¬(s = v ∧ t = w) → t = v
⊢ ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
have mpr₁ : ¬v = w → s = v → t = w → v = s ∧ w = t ∨ v = t ∧ w = s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s t v w : V
tauto tauto₁ : ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
mp : ¬v = w → v = s ∧ w = t ∨ v = t ∧ w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mpr : ¬v = w → s = v ∧ t = w ∨ s = w ∧ t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mp₁ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₂ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₃ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₄ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₅ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → s = w
mp₆ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → t = v
mp₇ : ¬v = w → v = t → w = s → ¬(s = v ∧ t = w) → s = w
mp₈ : ¬v = w → v = t → w = s → ¬(s = v ∧ t = w) → t = v
mpr₁ : ¬v = w → s = v → t = w → v = s ∧ w = t ∨ v = t ∧ w = s
⊢ ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
have mpr₂ : ¬v = w → s = w → t = v → v = s ∧ w = t ∨ v = t ∧ w = s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s t v w : V
tauto tauto₁ : ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
mp : ¬v = w → v = s ∧ w = t ∨ v = t ∧ w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mpr : ¬v = w → s = v ∧ t = w ∨ s = w ∧ t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mp₁ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₂ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₃ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₄ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₅ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → s = w
mp₆ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → t = v
mp₇ : ¬v = w → v = t → w = s → ¬(s = v ∧ t = w) → s = w
mp₈ : ¬v = w → v = t → w = s → ¬(s = v ∧ t = w) → t = v
mpr₁ : ¬v = w → s = v → t = w → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₂ : ¬v = w → s = w → t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₃ : ¬v = w → s = v → t = w → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₄ : ¬v = w → s = w → t = v → v = s ∧ w = t ∨ v = t ∧ w = s
⊢ ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
have mpr₅ : ¬v = w → s = v → t = w → ¬(v = s ∧ w = t) → v = t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s t v w : V
tauto tauto₁ : ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
mp : ¬v = w → v = s ∧ w = t ∨ v = t ∧ w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mpr : ¬v = w → s = v ∧ t = w ∨ s = w ∧ t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mp₁ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₂ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₃ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₄ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₅ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → s = w
mp₆ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → t = v
mp₇ : ¬v = w → v = t → w = s → ¬(s = v ∧ t = w) → s = w
mp₈ : ¬v = w → v = t → w = s → ¬(s = v ∧ t = w) → t = v
mpr₁ : ¬v = w → s = v → t = w → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₂ : ¬v = w → s = w → t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₃ : ¬v = w → s = v → t = w → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₄ : ¬v = w → s = w → t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₅ : ¬v = w → s = v → t = w → ¬(v = s ∧ w = t) → v = t
⊢ ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
have mpr₆ : ¬v = w → s = v → t = w → ¬(v = s ∧ w = t) → w = s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s t v w : V
tauto tauto₁ : ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
mp : ¬v = w → v = s ∧ w = t ∨ v = t ∧ w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mpr : ¬v = w → s = v ∧ t = w ∨ s = w ∧ t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mp₁ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₂ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₃ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₄ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₅ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → s = w
mp₆ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → t = v
mp₇ : ¬v = w → v = t → w = s → ¬(s = v ∧ t = w) → s = w
mp₈ : ¬v = w → v = t → w = s → ¬(s = v ∧ t = w) → t = v
mpr₁ : ¬v = w → s = v → t = w → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₂ : ¬v = w → s = w → t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₃ : ¬v = w → s = v → t = w → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₄ : ¬v = w → s = w → t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₅ : ¬v = w → s = v → t = w → ¬(v = s ∧ w = t) → v = t
mpr₆ : ¬v = w → s = v → t = w → ¬(v = s ∧ w = t) → w = s
⊢ ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
have mpr₇ : ¬v = w → s = w → t = v → ¬(v = s ∧ w = t) → v = t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s t v w : V
tauto tauto₁ : ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
mp : ¬v = w → v = s ∧ w = t ∨ v = t ∧ w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mpr : ¬v = w → s = v ∧ t = w ∨ s = w ∧ t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mp₁ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₂ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₃ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₄ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₅ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → s = w
mp₆ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → t = v
mp₇ : ¬v = w → v = t → w = s → ¬(s = v ∧ t = w) → s = w
mp₈ : ¬v = w → v = t → w = s → ¬(s = v ∧ t = w) → t = v
mpr₁ : ¬v = w → s = v → t = w → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₂ : ¬v = w → s = w → t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₃ : ¬v = w → s = v → t = w → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₄ : ¬v = w → s = w → t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₅ : ¬v = w → s = v → t = w → ¬(v = s ∧ w = t) → v = t
mpr₆ : ¬v = w → s = v → t = w → ¬(v = s ∧ w = t) → w = s
mpr₇ : ¬v = w → s = w → t = v → ¬(v = s ∧ w = t) → v = t
⊢ ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
have mpr₈ : ¬v = w → s = w → t = v → ¬(v = s ∧ w = t) → w = s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s t v w : V
tauto tauto₁ : ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
mp : ¬v = w → v = s ∧ w = t ∨ v = t ∧ w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mpr : ¬v = w → s = v ∧ t = w ∨ s = w ∧ t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mp₁ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₂ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₃ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₄ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₅ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → s = w
mp₆ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → t = v
mp₇ : ¬v = w → v = t → w = s → ¬(s = v ∧ t = w) → s = w
mp₈ : ¬v = w → v = t → w = s → ¬(s = v ∧ t = w) → t = v
mpr₁ : ¬v = w → s = v → t = w → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₂ : ¬v = w → s = w → t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₃ : ¬v = w → s = v → t = w → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₄ : ¬v = w → s = w → t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₅ : ¬v = w → s = v → t = w → ¬(v = s ∧ w = t) → v = t
mpr₆ : ¬v = w → s = v → t = w → ¬(v = s ∧ w = t) → w = s
mpr₇ : ¬v = w → s = w → t = v → ¬(v = s ∧ w = t) → v = t
mpr₈ : ¬v = w → s = w → t = v → ¬(v = s ∧ w = t) → w = s
⊢ ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
have mp₉ : ¬v = w → v = s → w = t → ¬s = v → s = w
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s t v w : V
tauto tauto₁ : ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
mp : ¬v = w → v = s ∧ w = t ∨ v = t ∧ w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mpr : ¬v = w → s = v ∧ t = w ∨ s = w ∧ t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mp₁ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₂ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₃ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₄ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₅ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → s = w
mp₆ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → t = v
mp₇ : ¬v = w → v = t → w = s → ¬(s = v ∧ t = w) → s = w
mp₈ : ¬v = w → v = t → w = s → ¬(s = v ∧ t = w) → t = v
mpr₁ : ¬v = w → s = v → t = w → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₂ : ¬v = w → s = w → t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₃ : ¬v = w → s = v → t = w → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₄ : ¬v = w → s = w → t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₅ : ¬v = w → s = v → t = w → ¬(v = s ∧ w = t) → v = t
mpr₆ : ¬v = w → s = v → t = w → ¬(v = s ∧ w = t) → w = s
mpr₇ : ¬v = w → s = w → t = v → ¬(v = s ∧ w = t) → v = t
mpr₈ : ¬v = w → s = w → t = v → ¬(v = s ∧ w = t) → w = s
mp₉ : ¬v = w → v = s → w = t → ¬s = v → s = w
⊢ ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
have mp₁₀ : ¬v = w → v = s → w = t → ¬t = w → s = w
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s t v w : V
tauto tauto₁ : ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
mp : ¬v = w → v = s ∧ w = t ∨ v = t ∧ w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mpr : ¬v = w → s = v ∧ t = w ∨ s = w ∧ t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mp₁ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₂ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₃ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₄ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₅ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → s = w
mp₆ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → t = v
mp₇ : ¬v = w → v = t → w = s → ¬(s = v ∧ t = w) → s = w
mp₈ : ¬v = w → v = t → w = s → ¬(s = v ∧ t = w) → t = v
mpr₁ : ¬v = w → s = v → t = w → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₂ : ¬v = w → s = w → t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₃ : ¬v = w → s = v → t = w → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₄ : ¬v = w → s = w → t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₅ : ¬v = w → s = v → t = w → ¬(v = s ∧ w = t) → v = t
mpr₆ : ¬v = w → s = v → t = w → ¬(v = s ∧ w = t) → w = s
mpr₇ : ¬v = w → s = w → t = v → ¬(v = s ∧ w = t) → v = t
mpr₈ : ¬v = w → s = w → t = v → ¬(v = s ∧ w = t) → w = s
mp₉ : ¬v = w → v = s → w = t → ¬s = v → s = w
mp₁₀ : ¬v = w → v = s → w = t → ¬t = w → s = w
mp₁₁ : ¬v = w → v = s → w = t → ¬s = v → s = w
mp₁₂ : ¬v = w → v = s → w = t → ¬t = w → s = w
mp₁₃ : ¬v = w → v = s → w = t → ¬s = v → s = w
mp₁₄ : ¬v = w → v = s → w = t → ¬t = w → s = w
⊢ ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
have mp₁₅ : ¬v = w → v = s → w = t → ¬s = v → t = v
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s t v w : V
tauto tauto₁ : ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
mp : ¬v = w → v = s ∧ w = t ∨ v = t ∧ w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mpr : ¬v = w → s = v ∧ t = w ∨ s = w ∧ t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mp₁ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₂ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₃ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₄ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₅ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → s = w
mp₆ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → t = v
mp₇ : ¬v = w → v = t → w = s → ¬(s = v ∧ t = w) → s = w
mp₈ : ¬v = w → v = t → w = s → ¬(s = v ∧ t = w) → t = v
mpr₁ : ¬v = w → s = v → t = w → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₂ : ¬v = w → s = w → t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₃ : ¬v = w → s = v → t = w → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₄ : ¬v = w → s = w → t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₅ : ¬v = w → s = v → t = w → ¬(v = s ∧ w = t) → v = t
mpr₆ : ¬v = w → s = v → t = w → ¬(v = s ∧ w = t) → w = s
mpr₇ : ¬v = w → s = w → t = v → ¬(v = s ∧ w = t) → v = t
mpr₈ : ¬v = w → s = w → t = v → ¬(v = s ∧ w = t) → w = s
mp₉ : ¬v = w → v = s → w = t → ¬s = v → s = w
mp₁₀ : ¬v = w → v = s → w = t → ¬t = w → s = w
mp₁₁ : ¬v = w → v = s → w = t → ¬s = v → s = w
mp₁₂ : ¬v = w → v = s → w = t → ¬t = w → s = w
mp₁₃ : ¬v = w → v = s → w = t → ¬s = v → s = w
mp₁₄ : ¬v = w → v = s → w = t → ¬t = w → s = w
mp₁₅ : ¬v = w → v = s → w = t → ¬s = v → t = v
⊢ ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
have mp₁₆ : ¬v = w → v = s → w = t → ¬t = w → t = v
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s t v w : V
tauto tauto₁ : ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
mp : ¬v = w → v = s ∧ w = t ∨ v = t ∧ w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mpr : ¬v = w → s = v ∧ t = w ∨ s = w ∧ t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mp₁ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₂ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₃ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₄ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₅ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → s = w
mp₆ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → t = v
mp₇ : ¬v = w → v = t → w = s → ¬(s = v ∧ t = w) → s = w
mp₈ : ¬v = w → v = t → w = s → ¬(s = v ∧ t = w) → t = v
mpr₁ : ¬v = w → s = v → t = w → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₂ : ¬v = w → s = w → t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₃ : ¬v = w → s = v → t = w → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₄ : ¬v = w → s = w → t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₅ : ¬v = w → s = v → t = w → ¬(v = s ∧ w = t) → v = t
mpr₆ : ¬v = w → s = v → t = w → ¬(v = s ∧ w = t) → w = s
mpr₇ : ¬v = w → s = w → t = v → ¬(v = s ∧ w = t) → v = t
mpr₈ : ¬v = w → s = w → t = v → ¬(v = s ∧ w = t) → w = s
mp₉ : ¬v = w → v = s → w = t → ¬s = v → s = w
mp₁₀ : ¬v = w → v = s → w = t → ¬t = w → s = w
mp₁₁ : ¬v = w → v = s → w = t → ¬s = v → s = w
mp₁₂ : ¬v = w → v = s → w = t → ¬t = w → s = w
mp₁₃ : ¬v = w → v = s → w = t → ¬s = v → s = w
mp₁₄ : ¬v = w → v = s → w = t → ¬t = w → s = w
mp₁₅ : ¬v = w → v = s → w = t → ¬s = v → t = v
mp₁₆ : ¬v = w → v = s → w = t → ¬t = w → t = v
mp₁₇ : ¬v = w → v = s → w = t → ¬s = v → t = v
mp₁₈ : ¬v = w → v = s → w = t → ¬t = w → t = v
mp₁₉ : ¬v = w → v = s → w = t → ¬s = v → t = v
mp₂₀ : ¬v = w → v = s → w = t → ¬t = w → t = v
⊢ ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
have mp₂₁ : ¬v = w → v = t → w = s → ¬s = v → s = w
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s t v w : V
tauto tauto₁ : ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
mp : ¬v = w → v = s ∧ w = t ∨ v = t ∧ w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mpr : ¬v = w → s = v ∧ t = w ∨ s = w ∧ t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mp₁ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₂ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₃ : ¬v = w → v = s → w = t → s = v ∧ t = w ∨ s = w ∧ t = v
mp₄ : ¬v = w → v = t → w = s → s = v ∧ t = w ∨ s = w ∧ t = v
mp₅ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → s = w
mp₆ : ¬v = w → v = s → w = t → ¬(s = v ∧ t = w) → t = v
mp₇ : ¬v = w → v = t → w = s → ¬(s = v ∧ t = w) → s = w
mp₈ : ¬v = w → v = t → w = s → ¬(s = v ∧ t = w) → t = v
mpr₁ : ¬v = w → s = v → t = w → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₂ : ¬v = w → s = w → t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₃ : ¬v = w → s = v → t = w → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₄ : ¬v = w → s = w → t = v → v = s ∧ w = t ∨ v = t ∧ w = s
mpr₅ : ¬v = w → s = v → t = w → ¬(v = s ∧ w = t) → v = t
mpr₆ : ¬v = w → s = v → t = w → ¬(v = s ∧ w = t) → w = s
mpr₇ : ¬v = w → s = w → t = v → ¬(v = s ∧ w = t) → v = t
mpr₈ : ¬v = w → s = w → t = v → ¬(v = s ∧ w = t) → w = s
mp₉ : ¬v = w → v = s → w = t → ¬s = v → s = w
mp₁₀ : ¬v = w → v = s → w = t → ¬t = w → s = w
mp₁₁ : ¬v = w → v = s → w = t → ¬s = v → s = w
mp₁₂ : ¬v = w → v = s → w = t → ¬t = w → s = w
mp₁₃ : ¬v = w → v = s → w = t → ¬s = v → s = w
mp₁₄ : ¬v = w → v = s → w = t → ¬t = w → s = w
mp₁₅ : ¬v = w → v = s → w = t → ¬s = v → t = v
mp₁₆ : ¬v = w → v = s → w = t → ¬t = w → t = v
mp₁₇ : ¬v = w → v = s → w = t → ¬s = v → t = v
mp₁₈ : ¬v = w → v = s → w = t → ¬t = w → t = v
mp₁₉ : ¬v = w → v = s → w = t → ¬s = v → t = v
mp₂₀ : ¬v = w → v = s → w = t → ¬t = w → t = v
mp₂₁ : ¬v = w → v = t → w = s → ¬s = v → s = w
⊢ ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
have mp₂₂ : ¬v = w → v = t → w = s → ¬t = w → s = w
Tactic: tauto