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 : 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
inr₁₈ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬b ≤ x → c ≤ x
inr₁₉ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬x ≤ c → c ≤ x
inr₂₀ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬b ≤ x → c ≤ x
inr₂₁ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬x ≤ c → c ≤ x
inr₂₂ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬b ≤ x → x ≤ b
inr₂₃ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬x ≤ c → x ≤ b
inr₂₄ : a ≤ x → x ≤ c → ¬a ≤ x → ¬x ≤ a → ¬b ≤ x → x ≤ b
inr₂₅ : a ≤ x → x ≤ c → ¬a ≤ x → ¬x ≤ a → ¬x ≤ c → x ≤ b
inr₂₆ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬b ≤ x → x ≤ b
inr₂₇ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬x ≤ c → x ≤ b
inr₂₈ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬b ≤ x → x ≤ b
inr₂₉ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬x ≤ c → x ≤ b
inr₃₀ : c ≤ x → x ≤ a → ¬a ≤ x → ¬b ≤ x → ¬b ≤ 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 → ¬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
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
inr₁₈ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬b ≤ x → c ≤ x
inr₁₉ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬x ≤ c → c ≤ x
inr₂₀ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬b ≤ x → c ≤ x
inr₂₁ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬x ≤ c → c ≤ x
inr₂₂ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬b ≤ x → x ≤ b
inr₂₃ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬x ≤ c → x ≤ b
inr₂₄ : a ≤ x → x ≤ c → ¬a ≤ x → ¬x ≤ a → ¬b ≤ x → x ≤ b
inr₂₅ : a ≤ x → x ≤ c → ¬a ≤ x → ¬x ≤ a → ¬x ≤ c → x ≤ b
inr₂₆ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬b ≤ x → x ≤ b
inr₂₇ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬x ≤ c → x ≤ b
inr₂₈ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬b ≤ x → x ≤ b
inr₂₉ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬x ≤ c → x ≤ b
inr₃₀ : c ≤ x → x ≤ a → ¬a ≤ x → ¬b ≤ x → ¬b ≤ x → x ≤ b
inr₃₁ : c ≤ x → x ≤ a → ¬a ≤ x → ¬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 ≤ a → ¬b ≤ 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
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
inr₁₈ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬b ≤ x → c ≤ x
inr₁₉ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬x ≤ c → c ≤ x
inr₂₀ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬b ≤ x → c ≤ x
inr₂₁ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬x ≤ c → c ≤ x
inr₂₂ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬b ≤ x → x ≤ b
inr₂₃ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬x ≤ c → x ≤ b
inr₂₄ : a ≤ x → x ≤ c → ¬a ≤ x → ¬x ≤ a → ¬b ≤ x → x ≤ b
inr₂₅ : a ≤ x → x ≤ c → ¬a ≤ x → ¬x ≤ a → ¬x ≤ c → x ≤ b
inr₂₆ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬b ≤ x → x ≤ b
inr₂₇ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬x ≤ c → x ≤ b
inr₂₈ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬b ≤ x → x ≤ b
inr₂₉ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬x ≤ c → x ≤ b
inr₃₀ : c ≤ x → x ≤ a → ¬a ≤ x → ¬b ≤ x → ¬b ≤ x → x ≤ b
inr₃₁ : c ≤ x → x ≤ a → ¬a ≤ x → ¬b ≤ x → ¬x ≤ c → x ≤ b
inr₃₂ : c ≤ x → x ≤ a → ¬a ≤ x → ¬x ≤ a → ¬b ≤ 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 ≤ a → ¬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
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
inr₁₈ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬b ≤ x → c ≤ x
inr₁₉ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬x ≤ c → c ≤ x
inr₂₀ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬b ≤ x → c ≤ x
inr₂₁ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬x ≤ c → c ≤ x
inr₂₂ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬b ≤ x → x ≤ b
inr₂₃ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬x ≤ c → x ≤ b
inr₂₄ : a ≤ x → x ≤ c → ¬a ≤ x → ¬x ≤ a → ¬b ≤ x → x ≤ b
inr₂₅ : a ≤ x → x ≤ c → ¬a ≤ x → ¬x ≤ a → ¬x ≤ c → x ≤ b
inr₂₆ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬b ≤ x → x ≤ b
inr₂₇ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬x ≤ c → x ≤ b
inr₂₈ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬b ≤ x → x ≤ b
inr₂₉ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬x ≤ c → x ≤ b
inr₃₀ : c ≤ x → x ≤ a → ¬a ≤ x → ¬b ≤ x → ¬b ≤ x → x ≤ b
inr₃₁ : c ≤ x → x ≤ a → ¬a ≤ x → ¬b ≤ x → ¬x ≤ c → x ≤ b
inr₃₂ : c ≤ x → x ≤ a → ¬a ≤ x → ¬x ≤ a → ¬b ≤ x → x ≤ b
inr₃₃ : c ≤ x → x ≤ a → ¬a ≤ x → ¬x ≤ a → ¬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 → ¬x ≤ b → ¬b ≤ x → ¬b ≤ 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
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
inr₁₈ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬b ≤ x → c ≤ x
inr₁₉ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬x ≤ c → c ≤ x
inr₂₀ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬b ≤ x → c ≤ x
inr₂₁ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬x ≤ c → c ≤ x
inr₂₂ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬b ≤ x → x ≤ b
inr₂₃ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬x ≤ c → x ≤ b
inr₂₄ : a ≤ x → x ≤ c → ¬a ≤ x → ¬x ≤ a → ¬b ≤ x → x ≤ b
inr₂₅ : a ≤ x → x ≤ c → ¬a ≤ x → ¬x ≤ a → ¬x ≤ c → x ≤ b
inr₂₆ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬b ≤ x → x ≤ b
inr₂₇ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬x ≤ c → x ≤ b
inr₂₈ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬b ≤ x → x ≤ b
inr₂₉ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬x ≤ c → x ≤ b
inr₃₀ : c ≤ x → x ≤ a → ¬a ≤ x → ¬b ≤ x → ¬b ≤ x → x ≤ b
inr₃₁ : c ≤ x → x ≤ a → ¬a ≤ x → ¬b ≤ x → ¬x ≤ c → x ≤ b
inr₃₂ : c ≤ x → x ≤ a → ¬a ≤ x → ¬x ≤ a → ¬b ≤ x → x ≤ b
inr₃₃ : c ≤ x → x ≤ a → ¬a ≤ x → ¬x ≤ a → ¬x ≤ c → x ≤ b
inr₃₄ : c ≤ x → x ≤ a → ¬x ≤ b → ¬b ≤ x → ¬b ≤ 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 → ¬x ≤ b → ¬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
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
inr₁₈ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬b ≤ x → c ≤ x
inr₁₉ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬x ≤ c → c ≤ x
inr₂₀ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬b ≤ x → c ≤ x
inr₂₁ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬x ≤ c → c ≤ x
inr₂₂ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬b ≤ x → x ≤ b
inr₂₃ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬x ≤ c → x ≤ b
inr₂₄ : a ≤ x → x ≤ c → ¬a ≤ x → ¬x ≤ a → ¬b ≤ x → x ≤ b
inr₂₅ : a ≤ x → x ≤ c → ¬a ≤ x → ¬x ≤ a → ¬x ≤ c → x ≤ b
inr₂₆ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬b ≤ x → x ≤ b
inr₂₇ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬x ≤ c → x ≤ b
inr₂₈ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬b ≤ x → x ≤ b
inr₂₉ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬x ≤ c → x ≤ b
inr₃₀ : c ≤ x → x ≤ a → ¬a ≤ x → ¬b ≤ x → ¬b ≤ x → x ≤ b
inr₃₁ : c ≤ x → x ≤ a → ¬a ≤ x → ¬b ≤ x → ¬x ≤ c → x ≤ b
inr₃₂ : c ≤ x → x ≤ a → ¬a ≤ x → ¬x ≤ a → ¬b ≤ x → x ≤ b
inr₃₃ : c ≤ x → x ≤ a → ¬a ≤ x → ¬x ≤ a → ¬x ≤ c → x ≤ b
inr₃₄ : c ≤ x → x ≤ a → ¬x ≤ b → ¬b ≤ x → ¬b ≤ x → x ≤ b
inr₃₅ : c ≤ x → x ≤ a → ¬x ≤ b → ¬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 → ¬x ≤ b → ¬x ≤ a → ¬b ≤ 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
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
inr₁₈ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬b ≤ x → c ≤ x
inr₁₉ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬x ≤ c → c ≤ x
inr₂₀ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬b ≤ x → c ≤ x
inr₂₁ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬x ≤ c → c ≤ x
inr₂₂ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬b ≤ x → x ≤ b
inr₂₃ : a ≤ x → x ≤ c → ¬a ≤ x → ¬b ≤ x → ¬x ≤ c → x ≤ b
inr₂₄ : a ≤ x → x ≤ c → ¬a ≤ x → ¬x ≤ a → ¬b ≤ x → x ≤ b
inr₂₅ : a ≤ x → x ≤ c → ¬a ≤ x → ¬x ≤ a → ¬x ≤ c → x ≤ b
inr₂₆ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬b ≤ x → x ≤ b
inr₂₇ : a ≤ x → x ≤ c → ¬x ≤ b → ¬b ≤ x → ¬x ≤ c → x ≤ b
inr₂₈ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬b ≤ x → x ≤ b
inr₂₉ : a ≤ x → x ≤ c → ¬x ≤ b → ¬x ≤ a → ¬x ≤ c → x ≤ b
inr₃₀ : c ≤ x → x ≤ a → ¬a ≤ x → ¬b ≤ x → ¬b ≤ x → x ≤ b
inr₃₁ : c ≤ x → x ≤ a → ¬a ≤ x → ¬b ≤ x → ¬x ≤ c → x ≤ b
inr₃₂ : c ≤ x → x ≤ a → ¬a ≤ x → ¬x ≤ a → ¬b ≤ x → x ≤ b
inr₃₃ : c ≤ x → x ≤ a → ¬a ≤ x → ¬x ≤ a → ¬x ≤ c → x ≤ b
inr₃₄ : c ≤ x → x ≤ a → ¬x ≤ b → ¬b ≤ x → ¬b ≤ x → x ≤ b
inr₃₅ : c ≤ x → x ≤ a → ¬x ≤ b → ¬b ≤ x → ¬x ≤ c → x ≤ b
inr₃₆ : c ≤ x → x ≤ a → ¬x ≤ b → ¬x ≤ a → ¬b ≤ 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 → ¬x ≤ b → ¬x ≤ a → ¬x ≤ c → x ≤ b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
⊢ Monotone f ∨ Antitone f ↔ ∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]
have mp : Monotone f ∨ Antitone f → ∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
mp : Monotone f ∨ Antitone f → ∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]
⊢ Monotone f ∨ Antitone f ↔ ∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]
have mpr : (∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]) → Monotone f ∨ Antitone f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : Monotone f
a b c : α
⊢ c ∈ [[a, b]] → f c ∈ [[f a, f b]]
have mp : c ∈ Icc (min a b) (max a b) → f c ∈ Icc (f (min a b)) (f (max a b))
Tactic: simp_rw [← Icc_min_max, ← hf.map_min, ← hf.map_max]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : Antitone f
a b c : α
⊢ c ∈ [[a, b]] → f c ∈ [[f a, f b]]
have mp : c ∈ Icc (min a b) (max a b) → f c ∈ Icc (f (max a b)) (f (min a b))
Tactic: simp_rw [← Icc_min_max, ← hf.map_min, ← hf.map_max]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
⊢ (∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]) → Monotone f ∨ Antitone f
have mpr : ¬Monotone f ∧ ¬Antitone f → ∃ (a : α) (b : α), ∃ c ∈ [[a, b]], f c ∉ [[f a, f b]]
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
⊢ ¬Monotone f ∧ ¬Antitone f → ∃ (a : α) (b : α), ∃ c ∈ [[a, b]], f c ∉ [[f a, f b]]
have mpr : (∃ (a : α) (b : α) (c : α), a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)) →
  ∃ (a : α) (b : α), ∃ c ∈ [[a, b]], f c ∉ [[f a, f b]]
Tactic: rw [not_monotone_not_antitone_iff_exists_le_le]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Ι a b = Ioc a b ∪ Ioc b a
have inl : a ≤ b → Ι a b = Ioc a b ∪ Ioc b a
Tactic: cases le_total a b
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
inl : a ≤ b → Ι a b = Ioc a b ∪ Ioc b a
⊢ Ι a b = Ioc a b ∪ Ioc b a
have inr : b ≤ a → Ι a b = Ioc a b ∪ Ioc b a
Tactic: cases le_total a b
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ a ∈ Ι b c ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b
have rw : a ∈ Ioc b c ∪ Ioc c b ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b
Tactic: rw [uIoc_eq_union, mem_union, mem_Ioc, mem_Ioc]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
rw : a ∈ Ioc b c ∪ Ioc c b ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b
⊢ a ∈ Ι b c ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b
have rw₁ : a ∈ Ioc b c ∨ a ∈ Ioc c b ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b
Tactic: rw [uIoc_eq_union, mem_union, mem_Ioc, mem_Ioc]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
rw : a ∈ Ioc b c ∪ Ioc c b ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b
rw₁ : a ∈ Ioc b c ∨ a ∈ Ioc c b ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b
⊢ a ∈ Ι b c ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b
have rw₂ : b < a ∧ a ≤ c ∨ a ∈ Ioc c b ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b
Tactic: rw [uIoc_eq_union, mem_union, mem_Ioc, mem_Ioc]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
rw : a ∈ Ioc b c ∪ Ioc c b ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b
rw₁ : a ∈ Ioc b c ∨ a ∈ Ioc c b ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b
rw₂ : b < a ∧ a ≤ c ∨ a ∈ Ioc c b ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b
⊢ a ∈ Ι b c ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b
have rw₃ : b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b
Tactic: rw [uIoc_eq_union, mem_union, mem_Ioc, mem_Ioc]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ a ∉ Ι b c ↔ a ≤ b ∧ a ≤ c ∨ c < a ∧ b < a
have simp : ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
Tactic: simp only [uIoc_eq_union, mem_union, mem_Ioc, ← not_le]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b 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 ≤ 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
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
have mpr : a ≤ b ∧ a ≤ c ∨ ¬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)
⊢ ¬(¬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 ≤ 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
⊢ ¬(¬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 ≤ c
Tactic: tauto