-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
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
mp₂₂ : ¬v = w → v = t → w = s → ¬t = w → s = w
mp₂₃ : ¬v = w → v = t → w = s → ¬s = v → s = w
mp₂₄ : ¬v = w → v = t → w = s → ¬t = w → s = w
mp₂₅ : ¬v = w → v = t → w = s → ¬s = v → s = w
mp₂₆ : ¬v = w → v = t → w = s → ¬t = w → s = w
mp₂₇ : ¬v = w → v = t → w = s → ¬s = v → t = v
mp₂₈ : ¬v = w → v = t → w = s → ¬t = w → t = v
mp₂₉ : ¬v = w → v = t → w = s → ¬s = v → t = v
mp₃₀ : ¬v = w → v = t → w = s → ¬t = w → t = v
mp₃₁ : ¬v = w → v = t → w = s → ¬s = v → t = v
mp₃₂ : ¬v = w → v = t → w = s → ¬t = w → t = v
mpr₉ : ¬v = w → s = v → t = w → ¬v = s → v = t
mpr₁₀ : ¬v = w → s = v → t = w → ¬w = t → v = t
mpr₁₁ : ¬v = w → s = v → t = w → ¬v = s → v = t
mpr₁₂ : ¬v = w → s = v → t = w → ¬w = t → v = t
mpr₁₃ : ¬v = w → s = v → t = w → ¬v = s → v = t
mpr₁₄ : ¬v = w → s = v → t = w → ¬w = t → v = t
mpr₁₅ : ¬v = w → s = v → t = w → ¬v = s → w = s
mpr₁₆ : ¬v = w → s = v → t = w → ¬w = t → w = s
mpr₁₇ : ¬v = w → s = v → t = w → ¬v = s → w = s
mpr₁₈ : ¬v = w → s = v → t = w → ¬w = t → w = s
mpr₁₉ : ¬v = w → s = v → t = w → ¬v = s → w = s
mpr₂₀ : ¬v = w → s = v → t = w → ¬w = t → w = s
mpr₂₁ : ¬v = w → s = w → t = v → ¬v = s → v = t
mpr₂₂ : ¬v = w → s = w → t = v → ¬w = t → v = t
mpr₂₃ : ¬v = w → s = w → t = v → ¬v = s → v = t
mpr₂₄ : ¬v = w → s = w → t = v → ¬w = t → v = t
mpr₂₅ : ¬v = w → s = w → t = v → ¬v = s → v = t
mpr₂₆ : ¬v = w → s = w → t = v → ¬w = t → v = t
mpr₂₇ : ¬v = w → s = w → t = v → ¬v = s → w = s
mpr₂₈ : ¬v = w → s = w → t = v → ¬w = t → w = s
mpr₂₉ : ¬v = w → s = w → t = v → ¬v = s → w = s
mpr₃₀ : ¬v = w → s = w → t = v → ¬w = t → w = s
mpr₃₁ : ¬v = w → s = w → t = v → ¬v = s → w = s
mpr₃₂ : ¬v = w → s = w → t = v → ¬w = t → w = s
mp₃₃ mp₃₄ mp₃₅ : ¬v = w → v = s → w = t → ¬s = v → s = w
mp₃₆ mp₃₇ mp₃₈ : ¬v = w → v = s → w = t → ¬t = w → s = w
mp₃₉ mp₄₀ mp₄₁ : ¬v = w → v = s → w = t → ¬s = v → t = v
mp₄₂ mp₄₃ mp₄₄ : ¬v = w → v = s → w = t → ¬t = w → t = v
mp₄₅ mp₄₆ mp₄₇ : ¬v = w → v = t → w = s → ¬s = v → s = w
mp₄₈ mp₄₉ mp₅₀ : ¬v = w → v = t → w = s → ¬t = w → s = w
mp₅₁ mp₅₂ mp₅₃ : ¬v = w → v = t → w = s → ¬s = v → t = v
mp₅₄ mp₅₅ mp₅₆ : ¬v = w → v = t → w = s → ¬t = w → t = v
mpr₃₃ mpr₃₄ mpr₃₅ : ¬v = w → s = v → t = w → ¬v = s → v = t
mpr₃₆ mpr₃₇ mpr₃₈ : ¬v = w → s = v → t = w → ¬w = t → v = t
mpr₃₉ mpr₄₀ mpr₄₁ : ¬v = w → s = v → t = w → ¬v = s → w = s
mpr₄₂ mpr₄₃ mpr₄₄ : ¬v = w → s = v → t = w → ¬w = t → w = s
mpr₄₅ mpr₄₆ mpr₄₇ : ¬v = w → s = w → t = v → ¬v = s → v = t
mpr₄₈ mpr₄₉ mpr₅₀ : ¬v = w → s = w → t = v → ¬w = t → v = t
mpr₅₁ mpr₅₂ mpr₅₃ : ¬v = w → s = w → t = v → ¬v = s → w = s
mpr₅₄ mpr₅₅ mpr₅₆ : ¬v = w → s = w → t = v → ¬w = t → w = s
mp₅₇ mp₅₈ : ¬v = w → v = s → w = t → ¬s = v → s = w
mp₅₉ mp₆₀ : ¬v = w → v = s → w = t → ¬t = w → s = w
mp₆₁ mp₆₂ : ¬v = w → v = s → w = t → ¬s = v → t = v
mp₆₃ mp₆₄ : ¬v = w → v = s → w = t → ¬t = w → t = v
mp₆₅ mp₆₆ : ¬v = w → v = t → w = s → ¬s = v → s = w
mp₆₇ mp₆₈ : ¬v = w → v = t → w = s → ¬t = w → s = w
mp₆₉ mp₇₀ : ¬v = w → v = t → w = s → ¬s = v → t = v
mp₇₁ mp₇₂ : ¬v = w → v = t → w = s → ¬t = w → t = v
mpr₅₇ mpr₅₈ : ¬v = w → s = v → t = w → ¬v = s → v = t
mpr₅₉ mpr₆₀ : ¬v = w → s = v → t = w → ¬w = t → v = t
mpr₆₁ mpr₆₂ : ¬v = w → s = v → t = w → ¬v = s → w = s
mpr₆₃ mpr₆₄ : ¬v = w → s = v → t = w → ¬w = t → w = s
mpr₆₅ mpr₆₆ : ¬v = w → s = w → t = v → ¬v = s → v = t
mpr₆₇ mpr₆₈ : ¬v = w → s = w → t = v → ¬w = t → v = t
mpr₆₉ mpr₇₀ : ¬v = w → s = w → t = v → ¬v = s → w = s
mpr₇₁ mpr₇₂ : ¬v = w → s = w → t = v → ¬w = t → w = s
⊢ ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)

Tactic:
tauto