awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Set.Union
Goal:
X : Type u_1
inst : LinearOrder X
a : ℕ → X
N : ℕ
ih : Ioc (a 0) (a N) ⊆ ⋃ i ∈ Finset.range N, Ioc (a i) (a (i + 1))
⊢ Ioc (a 0) (a (N + 1)) ⊆ Ioc (a 0) (a N) ∪ Ioc (a N) (a (N + 1))

Tactic:
Ioc_subset_Ioc_union_Ioc

Premises used: Set.Ioc_subset_Ioc_union_Ioc
-- Module: Mathlib.Order.Interval.Set.Union
Goal:
X : Type u_1
inst : LinearOrder X
a : ℕ → X
N : ℕ
ih : Ioc (a 0) (a N) ⊆ ⋃ i ∈ Finset.range N, Ioc (a i) (a (i + 1))
⊢ Ioc (a 0) (a N) ∪ Ioc (a N) (a (N + 1)) ⊆ ⋃ i ∈ Finset.range (N + 1), Ioc (a i) (a (i + 1))

Tactic:
simpa [Finset.range_add_one] using
                  union_subset_union_right (Ioc (a N) (a (N + 1))) ih

Premises used: Set.Ioc, Set.union_subset_union_right, Finset.range_add_one, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Order.Interval.Set.Union
Goal:
X : Type u_1
inst : LinearOrder X
a : ℕ → X
N : ℕ
ih : Ioc (a 0) (a N) ⊆ ⋃ i ∈ Finset.range N, Ioc (a i) (a (i + 1))
_ : Ioc (a 0) (a N) ∪ Ioc (a N) (a (N + 1)) ⊆ ⋃ i ∈ Finset.range (N + 1), Ioc (a i) (a (i + 1))
⊢ Ioc (a 0) (a (N + 1)) ⊆ ⋃ i ∈ Finset.range (N + 1), Ioc (a i) (a (i + 1))

Tactic:
calc
    _ ⊆ Ioc (a 0) (a N) ∪ Ioc (a N) (a (N + 1)) := Ioc_subset_Ioc_union_Ioc
    _ ⊆ _ := by simpa [Finset.range_add_one] using
                  union_subset_union_right (Ioc (a N) (a (N + 1))) ih

Premises used: Set.Ioc, Set.Ioc_subset_Ioc_union_Ioc, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Order.Interval.Set.Union
Goal:
X : Type u_1
inst : LinearOrder X
N : ℕ
a : ℕ → X
zero : Ioc (a 0) (a 0) ⊆ ⋃ i ∈ Finset.range 0, Ioc (a i) (a (i + 1))
succ :
  ∀ (N : ℕ) (ih : Ioc (a 0) (a N) ⊆ ⋃ i ∈ Finset.range N, Ioc (a i) (a (i + 1))),
    Ioc (a 0) (a (N + 1)) ⊆ ⋃ i ∈ Finset.range (N + 1), Ioc (a i) (a (i + 1))
⊢ Ioc (a 0) (a N) ⊆ ⋃ i ∈ Finset.range N, Ioc (a i) (a (i + 1))

Tactic:
induction N with
  | zero => simp
  | succ N ih => calc
    _ ⊆ Ioc (a 0) (a N) ∪ Ioc (a N) (a (N + 1)) := Ioc_subset_Ioc_union_Ioc
    _ ⊆ _ := by simpa [Finset.range_add_one] using
                  union_subset_union_right (Ioc (a N) (a (N + 1))) ih

Premises used: Set.Ioc, Set.Ioc_subset_Ioc_union_Ioc, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Order.Interval.Set.Union
Goal:
X : Type u_1
inst : LinearOrder X
a : ℕ → X
⊢ Ico (a 0) (a 0) ⊆ ⋃ i ∈ Finset.range 0, Ico (a i) (a (i + 1))

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.Union
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)) ⊆ Ico (a 0) (a N) ∪ Ico (a N) (a (N + 1))

Tactic:
Ico_subset_Ico_union_Ico

Premises used: Set.Ico_subset_Ico_union_Ico
-- Module: Mathlib.Order.Interval.Set.Union
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) ∪ Ico (a N) (a (N + 1)) ⊆ ⋃ i ∈ Finset.range (N + 1), Ico (a i) (a (i + 1))

Tactic:
simpa [Finset.range_add_one] using
                  union_subset_union_right (Ico (a N) (a (N + 1))) ih

Premises used: Set.union_subset_union_right, Finset.range_add_one, Set.Ico, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Order.Interval.Set.Union
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) ∪ Ico (a N) (a (N + 1)) ⊆ ⋃ i ∈ Finset.range (N + 1), Ico (a i) (a (i + 1))
⊢ Ico (a 0) (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

Premises used: Set.Ico_subset_Ico_union_Ico, Set.Ico, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Order.Interval.Set.Union
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))
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))
⊢ Ico (a 0) (a N) ⊆ ⋃ i ∈ Finset.range N, 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

Premises used: Set.Ico_subset_Ico_union_Ico, Set.Ico, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : Lattice α
a b : α
⊢ Eq (α := Set αᵒᵈ) ([[(toDual : (a : α) → αᵒᵈ) a, (toDual : (a : α) → αᵒᵈ) b]] : Set αᵒᵈ)
    ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' [[a, b]] : Set αᵒᵈ)

Tactic:
Icc_toDual (α := α)

Premises used: Set.Icc_toDual, Set.uIcc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : Lattice α
a b : αᵒᵈ
⊢ Eq (α := Set α) ([[(ofDual : (a : αᵒᵈ) → α) a, (ofDual : (a : αᵒᵈ) → α) b]] : Set α)
    ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' [[a, b]] : Set α)

Tactic:
Icc_ofDual

Premises used: Set.Icc_ofDual, Set.uIcc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
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
rw₂ rw₃ : Icc a b = Icc a b
⊢ [[a, b]] = Icc a b

Tactic:
rw [uIcc, inf_eq_left.2 h, sup_eq_right.2 h]

Premises used: Iff.mpr, sup_eq_right, inf_eq_left, Set.uIcc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
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
rw₂ rw₃ : Icc b a = Icc b a
⊢ [[a, b]] = Icc b a

Tactic:
rw [uIcc, inf_eq_right.2 h, sup_eq_left.2 h]

Premises used: Iff.mpr, sup_eq_left, inf_eq_right, Set.uIcc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : Lattice α
a b : α
simp_rw : Icc (a ⊓ b) (a ⊔ b) = Icc (b ⊓ a) (b ⊔ a)
simp_rw₁ : Icc (a ⊓ b) (a ⊔ b) = Icc (a ⊓ b) (b ⊔ a)
⊢ [[a, b]] = [[b, a]]

Tactic:
simp_rw [uIcc, inf_comm, sup_comm]

Premises used: inf_comm, sup_comm, Set.uIcc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : Lattice α
a b : α
h : a < b
⊢ [[a, b]] = Icc a b

Tactic:
uIcc_of_le h.le

Premises used: Set.uIcc_of_le, LT.lt.le
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : Lattice α
a b : α
h : b < a
⊢ [[a, b]] = Icc b a

Tactic:
uIcc_of_ge h.le

Premises used: Set.uIcc_of_ge, LT.lt.le
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : Lattice α
a : α
⊢ [[a, a]] = {a}

Tactic:
simp [uIcc]

Premises used: Set.uIcc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : Lattice α
a b : α
⊢ [[a, b]].Nonempty

Tactic:
nonempty_Icc.2 inf_le_sup

Premises used: Iff.mpr, Set.nonempty_Icc, inf_le_sup, Set.uIcc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : Lattice α
a b : α
⊢ Icc a b ⊆ [[a, b]]

Tactic:
Icc_subset_Icc inf_le_left le_sup_right

Premises used: le_sup_right, Set.Icc_subset_Icc, inf_le_left, Set.uIcc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : Lattice α
a b : α
⊢ Icc b a ⊆ [[a, b]]

Tactic:
Icc_subset_Icc inf_le_right le_sup_left

Premises used: le_sup_left, inf_le_right, Set.Icc_subset_Icc, Set.uIcc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : Lattice α
a b : α
⊢ a ∈ [[a, b]]

Tactic:
⟨inf_le_left, le_sup_left⟩

Premises used: le_sup_left, Set.Mem, setOf, Set.Icc, And.intro, inf_le_left, Set.uIcc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : Lattice α
a b : α
⊢ b ∈ [[a, b]]

Tactic:
⟨inf_le_right, le_sup_right⟩

Premises used: Set.Mem, setOf, inf_le_right, le_sup_right, Set.Icc, And.intro, Set.uIcc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : Lattice α
a b x : α
ha : a ≤ x
hb : x ≤ b
⊢ x ∈ [[a, b]]

Tactic:
Icc_subset_uIcc ⟨ha, hb⟩

Premises used: Set.Icc_subset_uIcc, And.intro
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : Lattice α
a b x : α
hb : b ≤ x
ha : x ≤ a
⊢ x ∈ [[a, b]]

Tactic:
Icc_subset_uIcc' ⟨hb, ha⟩

Premises used: And.intro, Set.Icc_subset_uIcc'
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : Lattice α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ ∈ [[a₂, b₂]]
h₂ : b₁ ∈ [[a₂, b₂]]
⊢ [[a₁, b₁]] ⊆ [[a₂, b₂]]

Tactic:
Icc_subset_Icc (le_inf h₁.1 h₂.1) (sup_le h₁.2 h₂.2)

Premises used: le_inf, And.right, And.left, Set.Icc_subset_Icc, sup_le, Set.uIcc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : Lattice α
a₁ a₂ b₁ b₂ : α
ha : a₁ ∈ Icc a₂ b₂
hb : b₁ ∈ Icc a₂ b₂
⊢ [[a₁, b₁]] ⊆ Icc a₂ b₂

Tactic:
Icc_subset_Icc (le_inf ha.1 hb.1) (sup_le ha.2 hb.2)

Premises used: le_inf, And.right, And.left, Set.Icc_subset_Icc, sup_le, Set.uIcc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : Lattice α
a₁ a₂ b₁ b₂ : α
⊢ [[a₁, b₁]] ⊆ [[a₂, b₂]] ↔ a₁ ∈ [[a₂, b₂]] ∧ b₁ ∈ [[a₂, b₂]]

Tactic:
Iff.intro (fun h => ⟨h left_mem_uIcc, h right_mem_uIcc⟩) fun h =>
    uIcc_subset_uIcc h.1 h.2

Premises used: Set.right_mem_uIcc, Set.left_mem_uIcc, And.right, And.left, And.intro, Iff.intro, Set.uIcc_subset_uIcc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : Lattice α
a₁ a₂ b₁ b₂ : α
⊢ [[a₁, b₁]] ⊆ [[a₂, b₂]] ↔ a₂ ⊓ b₂ ≤ a₁ ⊓ b₁ ∧ a₁ ⊔ b₁ ≤ a₂ ⊔ b₂

Tactic:
Icc_subset_Icc_iff inf_le_sup

Premises used: Set.Icc_subset_Icc_iff, inf_le_sup, Set.uIcc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : Lattice α
a b x : α
h : x ∈ [[a, b]]
⊢ [[x, b]] ⊆ [[a, b]]

Tactic:
uIcc_subset_uIcc h right_mem_uIcc

Premises used: Set.right_mem_uIcc, Set.uIcc_subset_uIcc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : Lattice α
a b x : α
h : x ∈ [[a, b]]
⊢ [[a, x]] ⊆ [[a, b]]

Tactic:
uIcc_subset_uIcc left_mem_uIcc h

Premises used: Set.left_mem_uIcc, Set.uIcc_subset_uIcc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : Lattice α
s : Set α
⊢ BddBelow s ∧ BddAbove s ↔ ∃ (a : α) (b : α), s ⊆ [[a, b]]

Tactic:
bddBelow_bddAbove_iff_subset_Icc.trans
    ⟨fun ⟨a, b, h⟩ => ⟨a, b, fun _ hx => Icc_subset_uIcc (h hx)⟩, fun ⟨_, _, h⟩ => ⟨_, _, h⟩⟩

Premises used: bddBelow_bddAbove_iff_subset_Icc, Set.Icc_subset_uIcc, Exists, HasSubset.Subset, _private.0.Set.bdd_below_bdd_above_iff_subset_uIcc.match_1, Set.Icc, Max.max, Iff.intro, Exists.intro, Iff.trans, _private.0.Set.bdd_below_bdd_above_iff_subset_uIcc.match_2, Set.uIcc, Min.min
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
β : Type u_2
inst : Lattice α
inst_1 : Lattice β
a₁ a₂ : α
b₁ b₂ : β
⊢ [[a₁, a₂]] ×ˢ [[b₁, b₂]] = [[(a₁, b₁), (a₂, b₂)]]

Tactic:
Icc_prod_Icc _ _ _ _

Premises used: Set.Icc_prod_Icc, Set.uIcc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
β : Type u_2
inst : Lattice α
inst_1 : Lattice β
a b : α × β
⊢ [[a, b]] = [[a.1, b.1]] ×ˢ [[a.2, b.2]]

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : DistribLattice α
a b c : α
ha : a ∈ [[b, c]]
hb : b ∈ [[a, c]]
⊢ a = b

Tactic:
eq_of_inf_eq_sup_eq (inf_congr_right ha.1 hb.1) <| sup_congr_right ha.2 hb.2

Premises used: eq_of_inf_eq_sup_eq, inf_congr_right, And.right, And.left, sup_congr_right
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : DistribLattice α
a b c : α
⊢ b ∈ [[a, c]] → c ∈ [[a, b]] → b = c

Tactic:
simpa only [uIcc_comm a] using eq_of_mem_uIcc_of_mem_uIcc

Premises used: Set.uIcc_comm, Set.eq_of_mem_uIcc_of_mem_uIcc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
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)
⊢ ∀ (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 : DistribLattice α
a b c : α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) ((fun (b : α) ↦ [[b, a]]) b) x ↔
      Membership.mem (γ := Set α) ((fun (b : α) ↦ [[b, a]]) c) x
⊢ b = c

Tactic:
eq_of_mem_uIcc_of_mem_uIcc ((h _).1 left_mem_uIcc) ((h _).2 left_mem_uIcc)

Premises used: Iff.mpr, Set.eq_of_mem_uIcc_of_mem_uIcc, Set.left_mem_uIcc, Iff.mp
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : DistribLattice α
a b c : α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) ((fun (b : α) ↦ [[b, a]]) b) x ↔
      Membership.mem (γ := Set α) ((fun (b : α) ↦ [[b, a]]) c) x
⊢ b = c

Tactic:
exact eq_of_mem_uIcc_of_mem_uIcc ((h _).1 left_mem_uIcc) ((h _).2 left_mem_uIcc)

Premises used: Iff.mpr, Set.eq_of_mem_uIcc_of_mem_uIcc, Set.left_mem_uIcc, Iff.mp
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : DistribLattice α
a : α
⊢ Injective (uIcc a)

Tactic:
simpa only [uIcc_comm] using uIcc_injective_right a

Premises used: Set.uIcc_comm, Set.uIcc_injective_right
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
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]]
hy : b ∈ [[a, b]]
hx₁ : a ∈ [[a, b]]
hy₁ : b ∈ [[a, b]]
⊢ MapsTo f [[a, b]] [[f a, f b]]

Tactic:
rw [uIcc, uIcc, ← hf.map_sup, ← hf.map_inf]

Premises used: MonotoneOn.map_inf, MonotoneOn.map_sup, Set.uIcc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ MapsTo f (Icc (min a b) (max a b)) (Icc (f (min a b)) (f (max a b)))

Tactic:
apply_rules [left_mem_uIcc, right_mem_uIcc, hf.mapsTo_Icc]

Premises used: Set.right_mem_uIcc, Set.left_mem_uIcc, MonotoneOn.mapsTo_Icc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

Tactic:
apply_rules [left_mem_uIcc, right_mem_uIcc, hf.mapsTo_Icc]

Premises used: Set.right_mem_uIcc, Set.left_mem_uIcc, MonotoneOn.mapsTo_Icc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ b ∈ [[a, b]]

Tactic:
apply_rules [left_mem_uIcc, right_mem_uIcc, hf.mapsTo_Icc]

Premises used: Set.right_mem_uIcc, Set.left_mem_uIcc, MonotoneOn.mapsTo_Icc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
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]]
hy : b ∈ [[a, b]]
hx₁ : a ∈ [[a, b]]
hy₁ : b ∈ [[a, b]]
⊢ MapsTo f [[a, b]] [[f a, f b]]

Tactic:
rw [uIcc, uIcc, ← hf.map_sup, ← hf.map_inf]

Premises used: AntitoneOn.map_inf, AntitoneOn.map_sup, Set.uIcc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ MapsTo f (Icc (min a b) (max a b)) (Icc (f (max a b)) (f (min a b)))

Tactic:
apply_rules [left_mem_uIcc, right_mem_uIcc, hf.mapsTo_Icc]

Premises used: Set.right_mem_uIcc, Set.left_mem_uIcc, AntitoneOn.mapsTo_Icc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

Tactic:
apply_rules [left_mem_uIcc, right_mem_uIcc, hf.mapsTo_Icc]

Premises used: Set.right_mem_uIcc, Set.left_mem_uIcc, AntitoneOn.mapsTo_Icc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ b ∈ [[a, b]]

Tactic:
apply_rules [left_mem_uIcc, right_mem_uIcc, hf.mapsTo_Icc]

Premises used: Set.right_mem_uIcc, Set.left_mem_uIcc, AntitoneOn.mapsTo_Icc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Lattice β
f : α → β
a b : α
hf : Monotone f
⊢ MapsTo f [[a, b]] [[f a, f b]]

Tactic:
(hf.monotoneOn _).mapsTo_uIcc

Premises used: MonotoneOn.mapsTo_uIcc, Monotone.monotoneOn
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Lattice β
f : α → β
a b : α
hf : Antitone f
⊢ MapsTo f [[a, b]] [[f a, f b]]

Tactic:
(hf.antitoneOn _).mapsTo_uIcc

Premises used: Antitone.antitoneOn, AntitoneOn.mapsTo_uIcc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ f '' [[a, b]] ⊆ [[f a, f b]]

Tactic:
hf.mapsTo_uIcc.image_subset

Premises used: MonotoneOn.mapsTo_uIcc, Set.MapsTo.image_subset
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ f '' [[a, b]] ⊆ [[f a, f b]]

Tactic:
hf.mapsTo_uIcc.image_subset

Premises used: AntitoneOn.mapsTo_uIcc, Set.MapsTo.image_subset
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Lattice β
f : α → β
a b : α
hf : Monotone f
⊢ f '' [[a, b]] ⊆ [[f a, f b]]

Tactic:
(hf.monotoneOn _).image_uIcc_subset

Premises used: Monotone.monotoneOn, MonotoneOn.image_uIcc_subset
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Lattice β
f : α → β
a b : α
hf : Antitone f
⊢ f '' [[a, b]] ⊆ [[f a, f b]]

Tactic:
(hf.antitoneOn _).image_uIcc_subset

Premises used: Antitone.antitoneOn, AntitoneOn.image_uIcc_subset
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Icc (min a b) (max a b) = [[a, b]]

Tactic:
rfl

Premises used: Set.uIcc, rfl
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ [[a, b]] = Icc b a

Tactic:
uIcc_of_gt <| lt_of_not_ge h

Premises used: lt_of_not_ge, Set.uIcc_of_gt
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : ¬b ≤ a
⊢ [[a, b]] = Icc a b

Tactic:
uIcc_of_lt <| lt_of_not_ge h

Premises used: Set.uIcc_of_lt, lt_of_not_ge
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
rw : [[a, b]] = Icc (min a b) (max a b)
h₁ : b ≤ b
h₂ : a ≤ a
⊢ [[a, b]] = Icc a b ∪ Icc b a

Tactic:
rw [Icc_union_Icc', max_comm]

Premises used: Set.Icc_union_Icc', max_comm
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ [[a, b]] = Icc (min a b) (max a b)

Tactic:
rfl
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ b ≤ b

Tactic:
rfl
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ a ≤ a

Tactic:
rfl
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ a ∈ [[b, c]] ↔ b ≤ a ∧ a ≤ c ∨ c ≤ a ∧ a ≤ b

Tactic:
simp [uIcc_eq_union]

Premises used: Set.uIcc_eq_union
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
ha : c < a
hb : c < b
⊢ c ∉ [[a, b]]

Tactic:
notMem_Icc_of_lt <| lt_min_iff.mpr ⟨ha, hb⟩

Premises used: Iff.mpr, Set.Mem, And.intro, Set.uIcc, Set.notMem_Icc_of_lt, lt_min_iff
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
ha : a < c
hb : b < c
⊢ c ∉ [[a, b]]

Tactic:
notMem_Icc_of_gt <| max_lt_iff.mpr ⟨ha, hb⟩

Premises used: Iff.mpr, Set.Mem, max_lt_iff, Set.notMem_Icc_of_gt, And.intro, Set.uIcc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ [[a₁, b₁]] ⊆ [[a₂, b₂]] ↔ min a₂ b₂ ≤ min a₁ b₁ ∧ max a₁ b₁ ≤ max a₂ b₂

Tactic:
uIcc_subset_uIcc_iff_le'

Premises used: Set.uIcc_subset_uIcc_iff_le'
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c x : α
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
⊢ x ∈ [[a, c]] → x ∈ [[a, b]] ∪ [[b, c]]

Tactic:
simp only [mem_uIcc, mem_union]

Premises used: Set.mem_union, Set.mem_uIcc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
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
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
⊢ 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

Premises used: le_total
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
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
inl₂₁ : a ≤ x → x ≤ c → ¬x ≤ b → ¬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

Tactic:
tauto