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 x : α
h2 : x ≤ b
inl : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₁ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₂ : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₃ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₄ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₅ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₆ inl₇ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₈ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → c ≤ x
inl₉ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → x ≤ b
inl₁₀ inl₁₁ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₁₂ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → c ≤ x
inl₁₃ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → x ≤ b
inl₁₄ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬b ≤ x → c ≤ x
inl₁₅ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬x ≤ c → c ≤ x
inl₁₆ : a ≤ x → x ≤ c → ¬a ≤ x → ¬x ≤ a → ¬b ≤ x → c ≤ x
inl₁₇ : a ≤ x → x ≤ c → ¬a ≤ x → ¬x ≤ a → ¬x ≤ c → c ≤ x
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
have inl₁₈ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬b ≤ x → c ≤ x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c x : α
h2 : x ≤ b
inl : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₁ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₂ : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₃ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₄ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₅ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₆ inl₇ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₈ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → c ≤ x
inl₉ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → x ≤ b
inl₁₀ inl₁₁ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₁₂ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → c ≤ x
inl₁₃ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → x ≤ b
inl₁₄ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬b ≤ x → c ≤ x
inl₁₅ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬x ≤ c → c ≤ x
inl₁₆ : a ≤ x → x ≤ c → ¬a ≤ x → ¬x ≤ a → ¬b ≤ x → c ≤ x
inl₁₇ : a ≤ x → x ≤ c → ¬a ≤ x → ¬x ≤ a → ¬x ≤ c → c ≤ x
inl₁₈ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬b ≤ x → c ≤ x
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
have inl₁₉ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬x ≤ c → c ≤ x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c x : α
h2 : x ≤ b
inl : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₁ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₂ : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₃ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₄ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₅ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₆ inl₇ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₈ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → c ≤ x
inl₉ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → x ≤ b
inl₁₀ inl₁₁ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₁₂ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → c ≤ x
inl₁₃ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → x ≤ b
inl₁₄ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬b ≤ x → c ≤ x
inl₁₅ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬x ≤ c → c ≤ x
inl₁₆ : a ≤ x → x ≤ c → ¬a ≤ x → ¬x ≤ a → ¬b ≤ x → c ≤ x
inl₁₇ : a ≤ x → x ≤ c → ¬a ≤ x → ¬x ≤ a → ¬x ≤ c → c ≤ x
inl₁₈ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬b ≤ x → c ≤ x
inl₁₉ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬x ≤ c → c ≤ x
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
have inl₂₀ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬b ≤ x → c ≤ x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c x : α
h2 : x ≤ b
inl : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₁ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₂ : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₃ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₄ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₅ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₆ inl₇ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₈ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → c ≤ x
inl₉ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → x ≤ b
inl₁₀ inl₁₁ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inl₁₂ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → c ≤ x
inl₁₃ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → x ≤ b
inl₁₄ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬b ≤ x → c ≤ x
inl₁₅ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬x ≤ c → c ≤ x
inl₁₆ : a ≤ x → x ≤ c → ¬a ≤ x → ¬x ≤ a → ¬b ≤ x → c ≤ x
inl₁₇ : a ≤ x → x ≤ c → ¬a ≤ x → ¬x ≤ a → ¬x ≤ c → c ≤ x
inl₁₈ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬b ≤ x → c ≤ x
inl₁₉ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬x ≤ c → c ≤ x
inl₂₀ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬b ≤ x → c ≤ x
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
have inl₂₁ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬x ≤ c → c ≤ x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c x : α
h2 : b ≤ x
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
have inr : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c x : α
h2 : b ≤ x
inr : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
have inr₁ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c x : α
h2 : b ≤ x
inr : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₁ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₂ : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₃ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
have inr₄ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c x : α
h2 : b ≤ x
inr : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₁ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₂ : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₃ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₄ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
have inr₅ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c x : α
h2 : b ≤ x
inr : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₁ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₂ : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₃ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₄ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₅ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
have inr₆ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c x : α
h2 : b ≤ x
inr : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₁ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₂ : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₃ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₄ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₅ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₆ inr₇ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
have inr₈ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → c ≤ x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c x : α
h2 : b ≤ x
inr : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₁ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₂ : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₃ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₄ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₅ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₆ inr₇ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₈ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → c ≤ x
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
have inr₉ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → x ≤ b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c x : α
h2 : b ≤ x
inr : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₁ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₂ : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₃ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₄ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₅ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₆ inr₇ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₈ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → c ≤ x
inr₉ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → x ≤ b
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
have inr₁₀ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c x : α
h2 : b ≤ x
inr : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₁ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₂ : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₃ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₄ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₅ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₆ inr₇ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₈ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → c ≤ x
inr₉ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → x ≤ b
inr₁₀ inr₁₁ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
have inr₁₂ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → c ≤ x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c x : α
h2 : b ≤ x
inr : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₁ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₂ : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₃ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₄ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₅ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₆ inr₇ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₈ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → c ≤ x
inr₉ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → x ≤ b
inr₁₀ inr₁₁ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₁₂ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → c ≤ x
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
have inr₁₃ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → x ≤ b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c x : α
h2 : b ≤ x
inr : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₁ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₂ : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₃ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₄ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₅ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₆ inr₇ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₈ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → c ≤ x
inr₉ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → x ≤ b
inr₁₀ inr₁₁ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₁₂ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → c ≤ x
inr₁₃ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → x ≤ b
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
have inr₁₄ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬b ≤ x → c ≤ x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c x : α
h2 : b ≤ x
inr : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₁ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₂ : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₃ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₄ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₅ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₆ inr₇ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₈ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → c ≤ x
inr₉ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → x ≤ b
inr₁₀ inr₁₁ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₁₂ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → c ≤ x
inr₁₃ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → x ≤ b
inr₁₄ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬b ≤ x → c ≤ x
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
have inr₁₅ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬x ≤ c → c ≤ x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c x : α
h2 : b ≤ x
inr : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₁ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₂ : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₃ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₄ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₅ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₆ inr₇ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₈ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → c ≤ x
inr₉ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → x ≤ b
inr₁₀ inr₁₁ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₁₂ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → c ≤ x
inr₁₃ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → x ≤ b
inr₁₄ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬b ≤ x → c ≤ x
inr₁₅ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬x ≤ c → c ≤ x
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
have inr₁₆ : a ≤ x → x ≤ c → ¬a ≤ x → ¬x ≤ a → ¬b ≤ x → c ≤ x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c x : α
h2 : b ≤ x
inr : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₁ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₂ : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₃ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₄ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₅ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₆ inr₇ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₈ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → c ≤ x
inr₉ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → x ≤ b
inr₁₀ inr₁₁ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₁₂ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → c ≤ x
inr₁₃ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → x ≤ b
inr₁₄ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬b ≤ x → c ≤ x
inr₁₅ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬x ≤ c → c ≤ x
inr₁₆ : a ≤ x → x ≤ c → ¬a ≤ x → ¬x ≤ a → ¬b ≤ x → c ≤ x
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
have inr₁₇ : a ≤ x → x ≤ c → ¬a ≤ x → ¬x ≤ a → ¬x ≤ c → c ≤ x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c x : α
h2 : b ≤ x
inr : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₁ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₂ : a ≤ x → x ≤ c → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₃ : c ≤ x → x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₄ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₅ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₆ inr₇ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₈ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → c ≤ x
inr₉ : a ≤ x → x ≤ c → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → x ≤ b
inr₁₀ inr₁₁ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
inr₁₂ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → c ≤ x
inr₁₃ : c ≤ x → x ≤ a → ¬(a ≤ x ∧ x ≤ b) → ¬(b ≤ x ∧ x ≤ a) → ¬(b ≤ x ∧ x ≤ c) → x ≤ b
inr₁₄ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬b ≤ x → c ≤ x
inr₁₅ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬x ≤ c → c ≤ x
inr₁₆ : a ≤ x → x ≤ c → ¬a ≤ x → ¬x ≤ a → ¬b ≤ x → c ≤ x
inr₁₇ : a ≤ x → x ≤ c → ¬a ≤ x → ¬x ≤ a → ¬x ≤ c → c ≤ x
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
have inr₁₈ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬b ≤ x → c ≤ x
Tactic: tauto