awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
mp : ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mpr : a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mp₁ mp₂ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mp₃ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ c
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
have mp₄ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
mp : ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mpr : a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mp₁ mp₂ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mp₃ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ c
mp₄ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ b
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
have mpr₁ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
mp : ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mpr : a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mp₁ mp₂ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mp₃ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ c
mp₄ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ b
mpr₁ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
have mpr₂ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
mp : ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mpr : a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mp₁ mp₂ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mp₃ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ c
mp₄ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ b
mpr₁ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₂ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₃ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₄ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₅ : a ≤ b → a ≤ c → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mpr₆ : ¬a ≤ c → ¬a ≤ b → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
have mp₅ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
mp : ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mpr : a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mp₁ mp₂ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mp₃ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ c
mp₄ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ b
mpr₁ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₂ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₃ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₄ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₅ : a ≤ b → a ≤ c → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mpr₆ : ¬a ≤ c → ¬a ≤ b → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mp₅ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
have mp₆ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
mp : ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mpr : a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mp₁ mp₂ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mp₃ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ c
mp₄ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ b
mpr₁ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₂ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₃ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₄ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₅ : a ≤ b → a ≤ c → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mpr₆ : ¬a ≤ c → ¬a ≤ b → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mp₅ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₆ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
have mp₇ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
mp : ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mpr : a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mp₁ mp₂ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mp₃ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ c
mp₄ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ b
mpr₁ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₂ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₃ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₄ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₅ : a ≤ b → a ≤ c → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mpr₆ : ¬a ≤ c → ¬a ≤ b → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mp₅ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₆ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
mp₇ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
have mp₈ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ c → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
mp : ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mpr : a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mp₁ mp₂ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mp₃ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ c
mp₄ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ b
mpr₁ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₂ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₃ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₄ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₅ : a ≤ b → a ≤ c → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mpr₆ : ¬a ≤ c → ¬a ≤ b → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mp₅ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₆ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
mp₇ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
mp₈ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ c → False
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
have mp₉ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ b → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
mp : ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mpr : a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mp₁ mp₂ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mp₃ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ c
mp₄ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ b
mpr₁ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₂ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₃ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₄ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₅ : a ≤ b → a ≤ c → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mpr₆ : ¬a ≤ c → ¬a ≤ b → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mp₅ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₆ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
mp₇ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
mp₈ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ c → False
mp₉ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ b → False
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
have mp₁₀ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ c → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
mp : ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mpr : a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mp₁ mp₂ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mp₃ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ c
mp₄ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ b
mpr₁ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₂ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₃ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₄ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₅ : a ≤ b → a ≤ c → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mpr₆ : ¬a ≤ c → ¬a ≤ b → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mp₅ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₆ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
mp₇ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
mp₈ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ c → False
mp₉ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₀ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ c → False
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
have mp₁₁ : a ≤ c → ¬a ≤ c → ¬a ≤ b → ¬a ≤ b → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
mp : ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mpr : a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mp₁ mp₂ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mp₃ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ c
mp₄ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ b
mpr₁ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₂ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₃ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₄ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₅ : a ≤ b → a ≤ c → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mpr₆ : ¬a ≤ c → ¬a ≤ b → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mp₅ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₆ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
mp₇ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
mp₈ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ c → False
mp₉ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₀ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ c → False
mp₁₁ : a ≤ c → ¬a ≤ c → ¬a ≤ b → ¬a ≤ b → False
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
have mp₁₂ : a ≤ c → ¬a ≤ c → ¬a ≤ b → ¬a ≤ c → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
mp : ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mpr : a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mp₁ mp₂ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mp₃ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ c
mp₄ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ b
mpr₁ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₂ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₃ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₄ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₅ : a ≤ b → a ≤ c → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mpr₆ : ¬a ≤ c → ¬a ≤ b → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mp₅ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₆ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
mp₇ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
mp₈ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ c → False
mp₉ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₀ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ c → False
mp₁₁ : a ≤ c → ¬a ≤ c → ¬a ≤ b → ¬a ≤ b → False
mp₁₂ : a ≤ c → ¬a ≤ c → ¬a ≤ b → ¬a ≤ c → False
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
have mp₁₃ : a ≤ b → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
mp : ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mpr : a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mp₁ mp₂ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mp₃ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ c
mp₄ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ b
mpr₁ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₂ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₃ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₄ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₅ : a ≤ b → a ≤ c → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mpr₆ : ¬a ≤ c → ¬a ≤ b → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mp₅ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₆ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
mp₇ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
mp₈ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ c → False
mp₉ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₀ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ c → False
mp₁₁ : a ≤ c → ¬a ≤ c → ¬a ≤ b → ¬a ≤ b → False
mp₁₂ : a ≤ c → ¬a ≤ c → ¬a ≤ b → ¬a ≤ c → False
mp₁₃ : a ≤ b → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
have mp₁₄ : a ≤ b → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
mp : ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mpr : a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mp₁ mp₂ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mp₃ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ c
mp₄ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ b
mpr₁ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₂ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₃ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₄ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₅ : a ≤ b → a ≤ c → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mpr₆ : ¬a ≤ c → ¬a ≤ b → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mp₅ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₆ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
mp₇ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
mp₈ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ c → False
mp₉ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₀ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ c → False
mp₁₁ : a ≤ c → ¬a ≤ c → ¬a ≤ b → ¬a ≤ b → False
mp₁₂ : a ≤ c → ¬a ≤ c → ¬a ≤ b → ¬a ≤ c → False
mp₁₃ : a ≤ b → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₄ : a ≤ b → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
have mp₁₅ : a ≤ b → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
mp : ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mpr : a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mp₁ mp₂ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mp₃ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ c
mp₄ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ b
mpr₁ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₂ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₃ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₄ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₅ : a ≤ b → a ≤ c → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mpr₆ : ¬a ≤ c → ¬a ≤ b → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mp₅ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₆ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
mp₇ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
mp₈ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ c → False
mp₉ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₀ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ c → False
mp₁₁ : a ≤ c → ¬a ≤ c → ¬a ≤ b → ¬a ≤ b → False
mp₁₂ : a ≤ c → ¬a ≤ c → ¬a ≤ b → ¬a ≤ c → False
mp₁₃ : a ≤ b → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₄ : a ≤ b → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
mp₁₅ : a ≤ b → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
have mp₁₆ : a ≤ b → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ c → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
mp : ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mpr : a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mp₁ mp₂ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mp₃ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ c
mp₄ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ b
mpr₁ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₂ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₃ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₄ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₅ : a ≤ b → a ≤ c → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mpr₆ : ¬a ≤ c → ¬a ≤ b → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mp₅ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₆ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
mp₇ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
mp₈ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ c → False
mp₉ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₀ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ c → False
mp₁₁ : a ≤ c → ¬a ≤ c → ¬a ≤ b → ¬a ≤ b → False
mp₁₂ : a ≤ c → ¬a ≤ c → ¬a ≤ b → ¬a ≤ c → False
mp₁₃ : a ≤ b → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₄ : a ≤ b → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
mp₁₅ : a ≤ b → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
mp₁₆ : a ≤ b → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ c → False
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
have mp₁₇ : a ≤ b → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ b → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
mp : ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mpr : a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mp₁ mp₂ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mp₃ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ c
mp₄ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ b
mpr₁ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₂ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₃ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₄ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₅ : a ≤ b → a ≤ c → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mpr₆ : ¬a ≤ c → ¬a ≤ b → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mp₅ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₆ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
mp₇ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
mp₈ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ c → False
mp₉ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₀ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ c → False
mp₁₁ : a ≤ c → ¬a ≤ c → ¬a ≤ b → ¬a ≤ b → False
mp₁₂ : a ≤ c → ¬a ≤ c → ¬a ≤ b → ¬a ≤ c → False
mp₁₃ : a ≤ b → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₄ : a ≤ b → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
mp₁₅ : a ≤ b → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
mp₁₆ : a ≤ b → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ c → False
mp₁₇ : a ≤ b → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ b → False
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
have mp₁₈ : a ≤ b → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ c → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
mp : ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mpr : a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mp₁ mp₂ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mp₃ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ c
mp₄ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ b
mpr₁ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₂ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₃ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₄ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₅ : a ≤ b → a ≤ c → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mpr₆ : ¬a ≤ c → ¬a ≤ b → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mp₅ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₆ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
mp₇ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
mp₈ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ c → False
mp₉ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₀ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ c → False
mp₁₁ : a ≤ c → ¬a ≤ c → ¬a ≤ b → ¬a ≤ b → False
mp₁₂ : a ≤ c → ¬a ≤ c → ¬a ≤ b → ¬a ≤ c → False
mp₁₃ : a ≤ b → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₄ : a ≤ b → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
mp₁₅ : a ≤ b → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
mp₁₆ : a ≤ b → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ c → False
mp₁₇ : a ≤ b → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₈ : a ≤ b → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ c → False
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
have mp₁₉ : a ≤ b → ¬a ≤ c → ¬a ≤ b → ¬a ≤ b → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
mp : ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mpr : a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mp₁ mp₂ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mp₃ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ c
mp₄ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ b
mpr₁ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₂ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₃ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₄ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₅ : a ≤ b → a ≤ c → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mpr₆ : ¬a ≤ c → ¬a ≤ b → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mp₅ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₆ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
mp₇ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
mp₈ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ c → False
mp₉ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₀ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ c → False
mp₁₁ : a ≤ c → ¬a ≤ c → ¬a ≤ b → ¬a ≤ b → False
mp₁₂ : a ≤ c → ¬a ≤ c → ¬a ≤ b → ¬a ≤ c → False
mp₁₃ : a ≤ b → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₄ : a ≤ b → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
mp₁₅ : a ≤ b → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
mp₁₆ : a ≤ b → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ c → False
mp₁₇ : a ≤ b → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₈ : a ≤ b → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ c → False
mp₁₉ : a ≤ b → ¬a ≤ c → ¬a ≤ b → ¬a ≤ b → False
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
have mp₂₀ : a ≤ b → ¬a ≤ c → ¬a ≤ b → ¬a ≤ c → False
Tactic: tauto