awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Union (goal)
Goal:
X : Type u_1
inst : LinearOrder X
a : ℕ → X
N : ℕ
ih : Ico (a 0) (a N) ⊆ ⋃ i ∈ Finset.range N, Ico (a i) (a (i + 1))
⊢ Ico (a 0) (a (N + 1)) ⊆ ⋃ i ∈ Finset.range (N + 1), Ico (a i) (a (i + 1))
have _ : Ico (a 0) (a N) ∪ Ico (a N) (a (N + 1)) ⊆ ⋃ i ∈ Finset.range (N + 1), Ico (a i) (a (i + 1))
Tactic: calc
    _ ⊆ Ico (a 0) (a N) ∪ Ico (a N) (a (N + 1)) := Ico_subset_Ico_union_Ico
    _ ⊆ _ := by simpa [Finset.range_add_one] using
                  union_subset_union_right (Ico (a N) (a (N + 1))) ih
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Union (goal)
Goal:
X : Type u_1
inst : LinearOrder X
N : ℕ
a : ℕ → X
⊢ Ico (a 0) (a N) ⊆ ⋃ i ∈ Finset.range N, Ico (a i) (a (i + 1))
have zero : Ico (a 0) (a 0) ⊆ ⋃ i ∈ Finset.range 0, Ico (a i) (a (i + 1))
Tactic: induction N with
  | zero => simp
  | succ N ih => calc
    _ ⊆ Ico (a 0) (a N) ∪ Ico (a N) (a (N + 1)) := Ico_subset_Ico_union_Ico
    _ ⊆ _ := by simpa [Finset.range_add_one] using
                  union_subset_union_right (Ico (a N) (a (N + 1))) ih
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Union (goal)
Goal:
X : Type u_1
inst : LinearOrder X
N : ℕ
a : ℕ → X
zero : Ico (a 0) (a 0) ⊆ ⋃ i ∈ Finset.range 0, Ico (a i) (a (i + 1))
⊢ Ico (a 0) (a N) ⊆ ⋃ i ∈ Finset.range N, Ico (a i) (a (i + 1))
have succ : ∀ (N : ℕ) (ih : Ico (a 0) (a N) ⊆ ⋃ i ∈ Finset.range N, Ico (a i) (a (i + 1))),
  Ico (a 0) (a (N + 1)) ⊆ ⋃ i ∈ Finset.range (N + 1), Ico (a i) (a (i + 1))
Tactic: induction N with
  | zero => simp
  | succ N ih => calc
    _ ⊆ Ico (a 0) (a N) ∪ Ico (a N) (a (N + 1)) := Ico_subset_Ico_union_Ico
    _ ⊆ _ := by simpa [Finset.range_add_one] using
                  union_subset_union_right (Ico (a N) (a (N + 1))) ih
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : Lattice α
a b : α
h : a ≤ b
⊢ [[a, b]] = Icc a b
have rw : Icc (a ⊓ b) (a ⊔ b) = Icc a b
Tactic: rw [uIcc, inf_eq_left.2 h, sup_eq_right.2 h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : Lattice α
a b : α
h : a ≤ b
rw : Icc (a ⊓ b) (a ⊔ b) = Icc a b
⊢ [[a, b]] = Icc a b
have rw₁ : Icc a (a ⊔ b) = Icc a b
Tactic: rw [uIcc, inf_eq_left.2 h, sup_eq_right.2 h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : Lattice α
a b : α
h : a ≤ b
rw : Icc (a ⊓ b) (a ⊔ b) = Icc a b
rw₁ : Icc a (a ⊔ b) = Icc a b
⊢ [[a, b]] = Icc a b
have rw₂ : Icc a b = Icc a b
Tactic: rw [uIcc, inf_eq_left.2 h, sup_eq_right.2 h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : Lattice α
a b : α
h : b ≤ a
⊢ [[a, b]] = Icc b a
have rw : Icc (a ⊓ b) (a ⊔ b) = Icc b a
Tactic: rw [uIcc, inf_eq_right.2 h, sup_eq_left.2 h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : Lattice α
a b : α
h : b ≤ a
rw : Icc (a ⊓ b) (a ⊔ b) = Icc b a
⊢ [[a, b]] = Icc b a
have rw₁ : Icc b (a ⊔ b) = Icc b a
Tactic: rw [uIcc, inf_eq_right.2 h, sup_eq_left.2 h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : Lattice α
a b : α
h : b ≤ a
rw : Icc (a ⊓ b) (a ⊔ b) = Icc b a
rw₁ : Icc b (a ⊔ b) = Icc b a
⊢ [[a, b]] = Icc b a
have rw₂ : Icc b a = Icc b a
Tactic: rw [uIcc, inf_eq_right.2 h, sup_eq_left.2 h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : Lattice α
a b : α
⊢ [[a, b]] = [[b, a]]
have simp_rw : Icc (a ⊓ b) (a ⊔ b) = Icc (b ⊓ a) (b ⊔ a)
Tactic: simp_rw [uIcc, inf_comm, sup_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : Lattice α
a b : α
simp_rw : Icc (a ⊓ b) (a ⊔ b) = Icc (b ⊓ a) (b ⊔ a)
⊢ [[a, b]] = [[b, a]]
have simp_rw₁ : Icc (a ⊓ b) (a ⊔ b) = Icc (a ⊓ b) (b ⊔ a)
Tactic: simp_rw [uIcc, inf_comm, sup_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (hypothesis)
Goal:
α : Type u_1
inst : DistribLattice α
a b c : α
h : Eq.{u_1 + 1} (α := Set α) ((fun (b : α) ↦ [[b, a]]) b) ((fun (b : α) ↦ [[b, a]]) c)
⊢ b = c
have h₁ : ∀ (x : α),
  Membership.mem (γ := Set α) ((fun (b : α) ↦ [[b, a]]) b) x ↔
    Membership.mem (γ := Set α) ((fun (b : α) ↦ [[b, a]]) c) x
Tactic: rw [Set.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ MapsTo f [[a, b]] [[f a, f b]]
have rw : MapsTo f (Icc (min a b) (max a b)) (Icc (f (min a b)) (f (max a b)))
Tactic: rw [uIcc, uIcc, ← hf.map_sup, ← hf.map_inf]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
rw : MapsTo f (Icc (min a b) (max a b)) (Icc (f (min a b)) (f (max a b)))
⊢ MapsTo f [[a, b]] [[f a, f b]]
have hx : a ∈ [[a, b]]
Tactic: rw [uIcc, uIcc, ← hf.map_sup, ← hf.map_inf]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
rw : MapsTo f (Icc (min a b) (max a b)) (Icc (f (min a b)) (f (max a b)))
hx : a ∈ [[a, b]]
⊢ MapsTo f [[a, b]] [[f a, f b]]
have hy : b ∈ [[a, b]]
Tactic: rw [uIcc, uIcc, ← hf.map_sup, ← hf.map_inf]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ MapsTo f [[a, b]] [[f a, f b]]
have rw : MapsTo f (Icc (min a b) (max a b)) (Icc (f (max a b)) (f (min a b)))
Tactic: rw [uIcc, uIcc, ← hf.map_sup, ← hf.map_inf]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
rw : MapsTo f (Icc (min a b) (max a b)) (Icc (f (max a b)) (f (min a b)))
⊢ MapsTo f [[a, b]] [[f a, f b]]
have hx : a ∈ [[a, b]]
Tactic: rw [uIcc, uIcc, ← hf.map_sup, ← hf.map_inf]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
rw : MapsTo f (Icc (min a b) (max a b)) (Icc (f (max a b)) (f (min a b)))
hx : a ∈ [[a, b]]
⊢ MapsTo f [[a, b]] [[f a, f b]]
have hy : b ∈ [[a, b]]
Tactic: rw [uIcc, uIcc, ← hf.map_sup, ← hf.map_inf]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ [[a, b]] = Icc a b ∪ Icc b a
have rw : [[a, b]] = Icc (min a b) (max a b)
Tactic: rw [Icc_union_Icc', max_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
rw : [[a, b]] = Icc (min a b) (max a b)
⊢ [[a, b]] = Icc a b ∪ Icc b a
have h₁ : b ≤ b
Tactic: rw [Icc_union_Icc', max_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
rw : [[a, b]] = Icc (min a b) (max a b)
h₁ : b ≤ b
⊢ [[a, b]] = Icc a b ∪ Icc b a
have h₂ : a ≤ a
Tactic: rw [Icc_union_Icc', max_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c x : α
⊢ x ∈ [[a, c]] → x ∈ [[a, b]] ∪ [[b, c]]
have simp : a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
Tactic: simp only [mem_uIcc, mem_union]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b 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 : ∀ (h2 : 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
Tactic: rcases le_total x b with h2 | h2
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c x : α
inl : ∀ (h2 : 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
⊢ 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 : ∀ (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
Tactic: rcases le_total x b with h2 | h2
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c x : α
h2 : 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 inl : 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 : x ≤ b
inl : 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 inl₁ : 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 : 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
⊢ 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 → ¬(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 : 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
⊢ 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₅ : 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 : 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
⊢ 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 → ¬(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 : 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
⊢ 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 → ¬(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 : 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
⊢ 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 → ¬(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 : 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
⊢ 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₁₀ : 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 : 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
⊢ 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₁₂ : 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 : 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
⊢ 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₁₃ : 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 : 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
⊢ 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 → ¬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 : 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
⊢ 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 → ¬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 : 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
⊢ 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 → ¬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 : 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
⊢ 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 → ¬a ≤ x → ¬x ≤ a → ¬x ≤ c → c ≤ x
Tactic: tauto