awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
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
inr₃₇ : c ≤ x → x ≤ a → ¬x ≤ b → ¬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

Tactic:
tauto
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
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]]
mpr : (∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]) → Monotone f ∨ Antitone f
⊢ Monotone f ∨ Antitone f ↔ ∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]

Tactic:
constructor
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : Monotone f
a b c : α
mp : c ∈ Icc (min a b) (max a b) → f c ∈ Icc (f (min a b)) (f (max a b))
⊢ c ∈ [[a, b]] → f c ∈ [[f a, f b]]

Tactic:
simp_rw [← Icc_min_max, ← hf.map_min, ← hf.map_max]

Premises used: Set.Icc_min_max, Monotone.map_max, Monotone.map_min
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : Antitone f
a b c : α
mp : c ∈ Icc (min a b) (max a b) → f c ∈ Icc (f (max a b)) (f (min a b))
⊢ c ∈ [[a, b]] → f c ∈ [[f a, f b]]

Tactic:
simp_rw [← Icc_min_max, ← hf.map_min, ← hf.map_max]

Premises used: Set.Icc_min_max, Antitone.map_max, Antitone.map_min
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : Monotone f
a b c : α
⊢ c ∈ Icc (min a b) (max a b) → f c ∈ Icc (f (min a b)) (f (max a b))

Tactic:
fun hc => ⟨hf hc.1, hf hc.2⟩

Premises used: Set.Mem, setOf, Set.Icc, And.right, And.left, And.intro
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : Antitone f
a b c : α
⊢ c ∈ Icc (min a b) (max a b) → f c ∈ Icc (f (max a b)) (f (min a b))

Tactic:
fun hc => ⟨hf hc.2, hf hc.1⟩

Premises used: Set.Mem, setOf, Set.Icc, And.right, And.left, And.intro
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : Monotone f
a b c : α
⊢ c ∈ Icc (min a b) (max a b) → f c ∈ Icc (f (min a b)) (f (max a b))

Tactic:
exacts [fun hc => ⟨hf hc.1, hf hc.2⟩, fun hc => ⟨hf hc.2, hf hc.1⟩]
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
mpr : ¬Monotone f ∧ ¬Antitone f → ∃ (a : α) (b : α), ∃ c ∈ [[a, b]], f c ∉ [[f a, f b]]
⊢ (∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]) → Monotone f ∨ Antitone f

Tactic:
contrapose!
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
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]]
⊢ ¬Monotone f ∧ ¬Antitone f → ∃ (a : α) (b : α), ∃ c ∈ [[a, b]], f c ∉ [[f a, f b]]

Tactic:
rw [not_monotone_not_antitone_iff_exists_le_le]

Premises used: not_monotone_not_antitone_iff_exists_le_le
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
a b c : α
hab : a ≤ b
hbc : b ≤ c
hfab : f a < f b
hfcb : f c < f b
⊢ ∃ (a : α) (b : α), ∃ c ∈ [[a, b]], f c ∉ [[f a, f b]]

Tactic:
⟨a, c, b, Icc_subset_uIcc ⟨hab, hbc⟩, fun h => h.2.not_gt <| max_lt hfab hfcb⟩

Premises used: Set.Icc_subset_uIcc, max_lt, And.right, LE.le.not_gt, And.intro, Exists.intro
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
a b c : α
hab : a ≤ b
hbc : b ≤ c
hfab : f a < f b
hfcb : f c < f b
⊢ ∃ (a : α) (b : α), ∃ c ∈ [[a, b]], f c ∉ [[f a, f b]]

Tactic:
exact ⟨a, c, b, Icc_subset_uIcc ⟨hab, hbc⟩, fun h => h.2.not_gt <| max_lt hfab hfcb⟩
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
a b c : α
hab : a ≤ b
hbc : b ≤ c
hfba : f b < f a
hfbc : f b < f c
⊢ ∃ (a : α) (b : α), ∃ c ∈ [[a, b]], f c ∉ [[f a, f b]]

Tactic:
⟨a, c, b, Icc_subset_uIcc ⟨hab, hbc⟩, fun h => h.1.not_gt <| lt_min hfba hfbc⟩

Premises used: Set.Icc_subset_uIcc, lt_min, LE.le.not_gt, And.left, And.intro, Exists.intro
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
a b c : α
hab : a ≤ b
hbc : b ≤ c
hfba : f b < f a
hfbc : f b < f c
⊢ ∃ (a : α) (b : α), ∃ c ∈ [[a, b]], f c ∉ [[f a, f b]]

Tactic:
exact ⟨a, c, b, Icc_subset_uIcc ⟨hab, hbc⟩, fun h => h.1.not_gt <| lt_min hfba hfbc⟩
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
s : Set α
⊢ MonotoneOn f s ∨ AntitoneOn f s ↔ ∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, c ∈ [[a, b]] → f c ∈ [[f a, f b]]

Tactic:
simp [monotoneOn_iff_monotone, antitoneOn_iff_antitone, monotone_or_antitone_iff_uIcc,
    mem_uIcc]

Premises used: Set.antitoneOn_iff_antitone, Set.monotoneOn_iff_monotone, Set.monotone_or_antitone_iff_uIcc, Set.mem_uIcc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
⊢ Ι a b = Ioc a b

Tactic:
simp [uIoc, h]

Premises used: Set.uIoc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : b ≤ a
⊢ Ι a b = Ioc b a

Tactic:
simp [uIoc, h]

Premises used: Set.uIoc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
inl : a ≤ b → Ι a b = Ioc a b ∪ Ioc b a
inr : b ≤ a → Ι a b = Ioc a b ∪ Ioc b a
⊢ Ι a b = Ioc a b ∪ Ioc b a

Tactic:
cases le_total a b

Premises used: le_total
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
⊢ Ι a b = Ioc a b ∪ Ioc b a

Tactic:
simp [uIoc, *]

Premises used: Set.uIoc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : b ≤ a
⊢ Ι a b = Ioc a b ∪ Ioc b a

Tactic:
simp [uIoc, *]

Premises used: Set.uIoc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
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
rw₃ rw₄ : b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b
⊢ a ∈ Ι b c ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b

Tactic:
rw [uIoc_eq_union, mem_union, mem_Ioc, mem_Ioc]

Premises used: Set.mem_union, Set.mem_Ioc, Set.uIoc_eq_union
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
simp : ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
⊢ a ∉ Ι b c ↔ a ≤ b ∧ a ≤ c ∨ c < a ∧ b < a

Tactic:
simp only [uIoc_eq_union, mem_union, mem_Ioc, ← not_le]

Premises used: Set.mem_union, not_le, Set.mem_Ioc, Set.uIoc_eq_union
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
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
mp₂₀ : a ≤ b → ¬a ≤ c → ¬a ≤ b → ¬a ≤ c → False
mpr₇ : a ≤ b → a ≤ c → ¬a ≤ b → a ≤ c → False
mpr₈ : a ≤ b → a ≤ c → ¬a ≤ c → a ≤ b → False
mpr₉ : ¬a ≤ c → ¬a ≤ b → ¬a ≤ b → a ≤ c → False
mpr₁₀ : ¬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

Tactic:
tauto
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ a ∈ Ι a b ↔ b < a

Tactic:
simp [mem_uIoc]

Premises used: Set.mem_uIoc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ b ∈ Ι a b ↔ a < b

Tactic:
simp [mem_uIoc]

Premises used: Set.mem_uIoc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
P : α → Prop
⊢ (∀ x ∈ Ι a b, P x) ↔ (∀ x ∈ Ioc a b, P x) ∧ ∀ x ∈ Ioc b a, P x

Tactic:
simp only [uIoc_eq_union, mem_union, or_imp, forall_and]

Premises used: Set.mem_union, or_imp, Set.uIoc_eq_union, forall_and
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
h : [[a, b]] ⊆ [[c, d]]
⊢ Ι a b ⊆ Ι c d

Tactic:
Ioc_subset_Ioc (uIcc_subset_uIcc_iff_le.1 h).1 (uIcc_subset_uIcc_iff_le.1 h).2

Premises used: Set.uIoc, Set.uIcc_subset_uIcc_iff_le, And.right, Set.Ioc_subset_Ioc, And.left, Iff.mp
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Ι a b = Ι b a

Tactic:
simp only [uIoc, min_comm a b, max_comm a b]

Premises used: min_comm, Set.uIoc, max_comm
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Ioc a b ⊆ Ι a b

Tactic:
Ioc_subset_Ioc (min_le_left _ _) (le_max_right _ _)

Premises used: le_max_right, Set.uIoc, min_le_left, Set.Ioc_subset_Ioc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Ioc a b ⊆ Ι b a

Tactic:
Ioc_subset_Ioc (min_le_right _ _) (le_max_left _ _)

Premises used: Set.uIoc, Set.Ioc_subset_Ioc, min_le_right, le_max_left
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Ι a b ⊆ [[a, b]]

Tactic:
Ioc_subset_Icc_self

Premises used: Set.uIoc, Set.Ioc_subset_Icc_self, Set.uIcc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
simp_rw : b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b → a < b ∧ b ≤ c ∨ c < b ∧ b ≤ a → a = b
⊢ a ∈ Ι b c → b ∈ Ι a c → a = b

Tactic:
simp_rw [mem_uIoc]

Premises used: Set.mem_uIoc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : b < a
right : a ≤ c
left_1 : a < b
right_1 : b ≤ c
inl : a ≤ b
inl₁ : b ≤ a
⊢ a = b

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : b < a
right : a ≤ c
left_1 : c < b
right_1 : b ≤ a
inl : a ≤ b
inl₁ : b ≤ a
⊢ a = b

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : c < a
right : a ≤ b
left_1 : a < b
right_1 : b ≤ c
inr : a ≤ b
inr₁ : b ≤ a
⊢ a = b

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : c < a
right : a ≤ b
left_1 : c < b
right_1 : b ≤ a
inr : a ≤ b
inr₁ : b ≤ a
⊢ a = b

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : b < a
right : a ≤ c
left_1 : a < b
right_1 : b ≤ c
⊢ a ≤ b

Tactic:
le_of_lt ‹_›

Premises used: le_of_lt
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : b < a
right : a ≤ c
left_1 : a < b
right_1 : b ≤ c
⊢ a ≤ b

Tactic:
exact le_of_lt ‹_›

Premises used: le_of_lt
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : b < a
right : a ≤ c
left_1 : a < b
right_1 : b ≤ c
⊢ a ≤ b

Tactic:
first | assumption | exact le_of_lt ‹_› | exact le_trans ‹_› (le_of_lt ‹_›)

Premises used: le_of_lt, le_trans
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : b < a
right : a ≤ c
left_1 : a < b
right_1 : b ≤ c
⊢ b ≤ a

Tactic:
le_of_lt ‹_›

Premises used: le_of_lt
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : b < a
right : a ≤ c
left_1 : a < b
right_1 : b ≤ c
⊢ b ≤ a

Tactic:
exact le_of_lt ‹_›

Premises used: le_of_lt
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : b < a
right : a ≤ c
left_1 : a < b
right_1 : b ≤ c
⊢ b ≤ a

Tactic:
first | assumption | exact le_of_lt ‹_› | exact le_trans ‹_› (le_of_lt ‹_›)

Premises used: le_of_lt, le_trans
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : b < a
right : a ≤ c
left_1 : c < b
right_1 : b ≤ a
⊢ a ≤ b

Tactic:
le_of_lt ‹_›

Premises used: le_of_lt
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : b < a
right : a ≤ c
left_1 : c < b
right_1 : b ≤ a
⊢ a ≤ b

Tactic:
le_trans ‹_› (le_of_lt ‹_›)

Premises used: le_of_lt, le_trans
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : b < a
right : a ≤ c
left_1 : c < b
right_1 : b ≤ a
⊢ a ≤ b

Tactic:
exact le_trans ‹_› (le_of_lt ‹_›)

Premises used: le_of_lt, le_trans
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : b < a
right : a ≤ c
left_1 : c < b
right_1 : b ≤ a
⊢ a ≤ b

Tactic:
first | assumption | exact le_of_lt ‹_› | exact le_trans ‹_› (le_of_lt ‹_›)

Premises used: le_of_lt, le_trans
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : b < a
right : a ≤ c
left_1 : c < b
right_1 : b ≤ a
⊢ b ≤ a

Tactic:
assumption
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : b < a
right : a ≤ c
left_1 : c < b
right_1 : b ≤ a
⊢ b ≤ a

Tactic:
first | assumption | exact le_of_lt ‹_› | exact le_trans ‹_› (le_of_lt ‹_›)

Premises used: le_of_lt, le_trans
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : c < a
right : a ≤ b
left_1 : a < b
right_1 : b ≤ c
⊢ a ≤ b

Tactic:
assumption
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : c < a
right : a ≤ b
left_1 : a < b
right_1 : b ≤ c
⊢ a ≤ b

Tactic:
first | assumption | exact le_of_lt ‹_› | exact le_trans ‹_› (le_of_lt ‹_›)

Premises used: le_of_lt, le_trans
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : c < a
right : a ≤ b
left_1 : a < b
right_1 : b ≤ c
⊢ b ≤ a

Tactic:
le_of_lt ‹_›

Premises used: le_of_lt
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : c < a
right : a ≤ b
left_1 : a < b
right_1 : b ≤ c
⊢ b ≤ a

Tactic:
le_trans ‹_› (le_of_lt ‹_›)

Premises used: le_of_lt, le_trans
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : c < a
right : a ≤ b
left_1 : a < b
right_1 : b ≤ c
⊢ b ≤ a

Tactic:
exact le_trans ‹_› (le_of_lt ‹_›)

Premises used: le_of_lt, le_trans
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : c < a
right : a ≤ b
left_1 : a < b
right_1 : b ≤ c
⊢ b ≤ a

Tactic:
first | assumption | exact le_of_lt ‹_› | exact le_trans ‹_› (le_of_lt ‹_›)

Premises used: le_of_lt, le_trans
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : c < a
right : a ≤ b
left_1 : c < b
right_1 : b ≤ a
⊢ a ≤ b

Tactic:
assumption
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : c < a
right : a ≤ b
left_1 : c < b
right_1 : b ≤ a
⊢ a ≤ b

Tactic:
first | assumption | exact le_of_lt ‹_› | exact le_trans ‹_› (le_of_lt ‹_›)

Premises used: le_of_lt, le_trans
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : c < a
right : a ≤ b
left_1 : c < b
right_1 : b ≤ a
⊢ b ≤ a

Tactic:
assumption
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : c < a
right : a ≤ b
left_1 : c < b
right_1 : b ≤ a
⊢ b ≤ a

Tactic:
first | assumption | exact le_of_lt ‹_› | exact le_trans ‹_› (le_of_lt ‹_›)

Premises used: le_of_lt, le_trans
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ b ∈ Ι a c → c ∈ Ι a b → b = c

Tactic:
simpa only [uIoc_comm a] using eq_of_mem_uIoc_of_mem_uIoc

Premises used: Set.uIoc_comm, Set.eq_of_mem_uIoc_of_mem_uIoc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
ha : a ≤ c
hb : b ≤ c
⊢ a ∉ Ι b c → b ∉ Ι a c → a = b

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h : Eq.{u_1 + 1} (α := Set α) ((fun (b : α) ↦ Ι b a) b) ((fun (b : α) ↦ Ι b a) c)
⊢ ∀ (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

Premises used: Set.ext_iff
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) b) x ↔ Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) c) x
inl : ∀ (ha : b ≤ a), b = c
inr : ∀ (ha : a < b), b = c
⊢ b = c

Tactic:
obtain ha | ha := le_or_gt b a

Premises used: le_or_gt
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) b) x ↔ Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) c) x
ha : b ≤ a
⊢ b ∉ (fun (b : α) ↦ Ι b a) b ↔ b ∉ (fun (b : α) ↦ Ι b a) c

Tactic:
have hb := (h b).not
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) b) x ↔ Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) c) x
ha : b ≤ a
hb : b ∉ (fun (b : α) ↦ Ι b a) b ↔ b ∉ (fun (b : α) ↦ Ι b a) c
⊢ b ≤ c

Tactic:
simp only [ha, left_mem_uIoc, true_iff, notMem_uIoc, ← not_le,
      and_true, not_true, false_and, not_false_iff, or_false] at hb

Premises used: not_le, and_true, false_and, true_iff, Set.left_mem_uIoc, not_true, or_false, not_false_iff, Set.notMem_uIoc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) b) x ↔ Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) c) x
ha : b ≤ a
hb : b ≤ c
⊢ b = c

Tactic:
hb.eq_of_not_lt fun hc => ?_

Premises used: LE.le.eq_of_not_lt
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) b) x ↔ Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) c) x
ha : b ≤ a
hb : b ≤ c
inl : ∀ (hc : b < c), False
⊢ b = c

Tactic:
refine hb.eq_of_not_lt fun hc => ?_

Premises used: LE.le.eq_of_not_lt
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) b) x ↔ Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) c) x
ha : b ≤ a
hb : b ≤ c
hc : b < c
⊢ False

Tactic:
simpa [ha, and_iff_right hc, ← @not_le _ _ _ a, iff_not_self, -not_le] using h c

Premises used: not_le, iff_not_self, and_iff_right
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) b) x ↔ Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) c) x
ha : a < b
⊢ b = c

Tactic:
eq_of_mem_uIoc_of_mem_uIoc ((h _).1 <| left_mem_uIoc.2 ha)
        ((h _).2 <| left_mem_uIoc.2 <| ha.trans_le ?_)

Premises used: Iff.mpr, Set.left_mem_uIoc, LT.lt.trans_le, Iff.mp, Set.eq_of_mem_uIoc_of_mem_uIoc