-- 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
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
⊢ ¬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 = s
Tactic: tauto