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
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
⊢ ¬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 = 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
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
⊢ ¬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 → 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
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
⊢ ¬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 → 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
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
⊢ ¬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 → ¬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
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
⊢ ¬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 = 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
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
⊢ ¬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 → ¬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
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
⊢ ¬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 → 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
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
⊢ ¬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 → ¬w = t → v = t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s t : V
⊢ edge s t = edge t s
have rw : fromEdgeSet {s(s, t)} = edge t s
Tactic: rw [edge, edge, Sym2.eq_swap]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s t : V
rw : fromEdgeSet {s(s, t)} = edge t s
⊢ edge s t = edge t s
have rw₁ : Eq (α := SimpleGraph V) (fromEdgeSet {s(s, t)}) (fromEdgeSet {s(t, s)})
Tactic: rw [edge, edge, Sym2.eq_swap]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s t : V
rw : fromEdgeSet {s(s, t)} = edge t s
rw₁ : Eq (α := SimpleGraph V) (fromEdgeSet {s(s, t)}) (fromEdgeSet {s(t, s)})
⊢ edge s t = edge t s
have rw₂ : Eq (α := SimpleGraph V) (fromEdgeSet {s(t, s)}) (fromEdgeSet {s(t, s)})
Tactic: rw [edge, edge, Sym2.eq_swap]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
x x_1 : V
⊢ Decidable ((edge s t).Adj x x_1)
have rw : Decidable ((x = s ∧ x_1 = t ∨ x = t ∧ x_1 = s) ∧ x ≠ x_1)
Tactic: rw [edge_adj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s : V
⊢ edge s s = ⊥
have Adj : ∀ (x x_1 : V), (edge s s).Adj x x_1 ↔ Adj ⊥ x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s x x_1 : V
⊢ (edge s s).Adj x x_1 ↔ Adj ⊥ x x_1
have Adj : (x = s ∧ x_1 = s ∨ x = s ∧ x_1 = s) ∧ x ≠ x_1 ↔ Adj ⊥ x x_1
Tactic: rw [edge_adj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
⊢ edge v w ≤ G ↔ v = w ∨ G.Adj v w
have inl : ∀ (h : v = w), edge v w ≤ G ↔ v = w ∨ G.Adj v w
Tactic: obtain h | h := eq_or_ne v w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
inl : ∀ (h : v = w), edge v w ≤ G ↔ v = w ∨ G.Adj v w
⊢ edge v w ≤ G ↔ v = w ∨ G.Adj v w
have inr : ∀ (h : v ≠ w), edge v w ≤ G ↔ v = w ∨ G.Adj v w
Tactic: obtain h | h := eq_or_ne v w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : v ≠ w
⊢ edge v w ≤ G ↔ v = w ∨ G.Adj v w
have inr : ∀ (hadj : v = w ∨ G.Adj v w) (v' w' : V) (hvw' : (edge v w).Adj v' w'), G.Adj v' w'
Tactic: refine ⟨fun h ↦ .inr <| h (by simp_all [edge_adj]), fun hadj v' w' hvw' ↦ ?_⟩