awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : PartialOrder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : DecidableLE (α × β)
a b : α
c : β
⊢ map (Embedding.sectL α c) (Ico a b) = Ico (a, c) (b, c)

Tactic:
aesop (add safe forward [le_antisymm, le_of_lt])

Premises used: le_of_lt, le_antisymm
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : PartialOrder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : DecidableLE (α × β)
a b : α
c : β
⊢ map (Embedding.sectL α c) (Ioo a b) = Ioo (a, c) (b, c)

Tactic:
aesop (add safe forward [le_antisymm, le_of_lt])

Premises used: le_of_lt, le_antisymm
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : DecidableLE (α × β)
c : α
a b : β
⊢ map (Embedding.sectR c β) [[a, b]] = [[(c, a), (c, b)]]

Tactic:
aesop (add safe forward [le_antisymm])

Premises used: le_antisymm
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : DecidableLE (α × β)
c : α
a b : β
⊢ map (Embedding.sectR c β) (Icc a b) = Icc (c, a) (c, b)

Tactic:
aesop (add safe forward [le_antisymm])

Premises used: le_antisymm
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : DecidableLE (α × β)
c : α
a b : β
⊢ map (Embedding.sectR c β) (Ioc a b) = Ioc (c, a) (c, b)

Tactic:
aesop (add safe forward [le_antisymm, le_of_lt])

Premises used: le_of_lt, le_antisymm
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : DecidableLE (α × β)
c : α
a b : β
⊢ map (Embedding.sectR c β) (Ico a b) = Ico (c, a) (c, b)

Tactic:
aesop (add safe forward [le_antisymm, le_of_lt])

Premises used: le_of_lt, le_antisymm
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : DecidableLE (α × β)
c : α
a b : β
⊢ map (Embedding.sectR c β) (Ioo a b) = Ioo (c, a) (c, b)

Tactic:
aesop (add safe forward [le_antisymm, le_of_lt])

Premises used: le_of_lt, le_antisymm
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : DecidableEq α
a : α
h : ∀ (a_1 : α), a_1 ∈ (Ici a).erase a ↔ a_1 ∈ Ioi a
⊢ (Ici a).erase a = Ioi a

Tactic:
ext
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : DecidableEq α
a a_1 : α
h : a_1 ≠ a ∧ a_1 ∈ Ici a ↔ a_1 ∈ Ioi a
h₁ : a_1 ≠ a ∧ a ≤ a_1 ↔ a_1 ∈ Ioi a
h₂ : a_1 ≠ a ∧ a ≤ a_1 ↔ a < a_1
h₃ : a_1 ≠ a ∧ a ≤ a_1 ↔ a ≤ a_1 ∧ a ≠ a_1
h₄ : a_1 ≠ a ∧ a ≤ a_1 ↔ a ≠ a_1 ∧ a ≤ a_1
⊢ a_1 ∈ (Ici a).erase a ↔ a_1 ∈ Ioi a

Tactic:
simp_rw [Finset.mem_erase, mem_Ici, mem_Ioi, lt_iff_le_and_ne, and_comm, ne_comm]

Premises used: lt_iff_le_and_ne, Finset.mem_Ici, and_comm, Finset.mem_Ioi, Finset.mem_erase, ne_comm
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : DecidableEq α
a : α
h : ∀ (a_1 : α), a_1 ∈ insert a (Ioi a) ↔ a_1 ∈ Ici a
⊢ insert a (Ioi a) = Ici a

Tactic:
ext
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : DecidableEq α
a a_1 : α
h : a_1 = a ∨ a_1 ∈ Ioi a ↔ a_1 ∈ Ici a
h₁ : a_1 = a ∨ a_1 ∈ Ioi a ↔ a ≤ a_1
h₂ : a_1 = a ∨ a < a_1 ↔ a ≤ a_1
h₃ : a_1 = a ∨ a < a_1 ↔ a < a_1 ∨ a = a_1
h₄ : a_1 = a ∨ a < a_1 ↔ a = a_1 ∨ a < a_1
⊢ a_1 ∈ insert a (Ioi a) ↔ a_1 ∈ Ici a

Tactic:
simp_rw [Finset.mem_insert, mem_Ici, mem_Ioi, le_iff_lt_or_eq, or_comm, eq_comm]

Premises used: Finset.mem_Ici, Finset.mem_insert, eq_comm, Finset.mem_Ioi, le_iff_lt_or_eq, or_comm
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderTop α
b : α
⊢ b ∉ Ioi b

Tactic:
fun h => lt_irrefl _ (mem_Ioi.1 h)

Premises used: lt_irrefl, Finset.mem_Ioi, Iff.mp, Not
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderTop α
a : α
rw : Ici a = insert a (Ioi a)
rw₁ rw₂ : Ici a = Ici a
⊢ Ici a = cons a (Ioi a) ⋯

Tactic:
rw [cons_eq_insert, Ioi_insert]

Premises used: Finset.Ioi_insert, Finset.cons_eq_insert
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderTop α
a : α
classical : Ici a = insert a (Ioi a)
classical₁ classical₂ : Ici a = Ici a
⊢ Ici a = cons a (Ioi a) ⋯

Tactic:
classical rw [cons_eq_insert, Ioi_insert]

Premises used: Finset.Ioi_insert, Finset.cons_eq_insert
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderTop α
a : α
rw : #(Ioi a) = #(cons a (Ioi a) ⋯) - 1
rw₁ : #(Ioi a) = #(Ioi a) + 1 - 1
rw₂ rw₃ : #(Ioi a) = #(Ioi a)
⊢ #(Ioi a) = #(Ici a) - 1

Tactic:
rw [Ici_eq_cons_Ioi, card_cons, Nat.add_sub_cancel_right]

Premises used: Nat.add_sub_cancel_right, Finset.Ici_eq_cons_Ioi, Finset.card_cons
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : DecidableEq α
b : α
h : ∀ (a : α), a ∈ (Iic b).erase b ↔ a ∈ Iio b
⊢ (Iic b).erase b = Iio b

Tactic:
ext
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : DecidableEq α
b a : α
h : a ≠ b ∧ a ∈ Iic b ↔ a ∈ Iio b
h₁ : a ≠ b ∧ a ≤ b ↔ a ∈ Iio b
h₂ : a ≠ b ∧ a ≤ b ↔ a < b
h₃ : a ≠ b ∧ a ≤ b ↔ a ≤ b ∧ a ≠ b
⊢ a ∈ (Iic b).erase b ↔ a ∈ Iio b

Tactic:
simp_rw [Finset.mem_erase, mem_Iic, mem_Iio, lt_iff_le_and_ne, and_comm]

Premises used: lt_iff_le_and_ne, Finset.mem_Iic, and_comm, Finset.mem_erase, Finset.mem_Iio
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : DecidableEq α
b : α
h : ∀ (a : α), a ∈ insert b (Iio b) ↔ a ∈ Iic b
⊢ insert b (Iio b) = Iic b

Tactic:
ext
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : DecidableEq α
b a : α
h : a = b ∨ a ∈ Iio b ↔ a ∈ Iic b
h₁ : a = b ∨ a ∈ Iio b ↔ a ≤ b
h₂ : a = b ∨ a < b ↔ a ≤ b
h₃ : a = b ∨ a < b ↔ a < b ∨ a = b
⊢ a ∈ insert b (Iio b) ↔ a ∈ Iic b

Tactic:
simp_rw [Finset.mem_insert, mem_Iic, mem_Iio, le_iff_lt_or_eq, or_comm]

Premises used: Finset.mem_Iic, Finset.mem_insert, le_iff_lt_or_eq, Finset.mem_Iio, or_comm
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderBot α
b : α
⊢ b ∉ Iio b

Tactic:
fun h => lt_irrefl _ (mem_Iio.1 h)

Premises used: lt_irrefl, Iff.mp, Finset.mem_Iio, Not
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderBot α
b : α
rw : Iic b = insert b (Iio b)
rw₁ rw₂ : Iic b = Iic b
⊢ Iic b = cons b (Iio b) ⋯

Tactic:
rw [cons_eq_insert, Iio_insert]

Premises used: Finset.cons_eq_insert, Finset.Iio_insert
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderBot α
b : α
classical : Iic b = insert b (Iio b)
classical₁ classical₂ : Iic b = Iic b
⊢ Iic b = cons b (Iio b) ⋯

Tactic:
classical rw [cons_eq_insert, Iio_insert]

Premises used: Finset.cons_eq_insert, Finset.Iio_insert
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderBot α
a : α
rw : #(Iio a) = #(cons a (Iio a) ⋯) - 1
rw₁ : #(Iio a) = #(Iio a) + 1 - 1
rw₂ rw₃ : #(Iio a) = #(Iio a)
⊢ #(Iio a) = #(Iic a) - 1

Tactic:
rw [Iic_eq_cons_Iio, card_cons, Nat.add_sub_cancel_right]

Premises used: Nat.add_sub_cancel_right, Finset.Iic_eq_cons_Iio, Finset.card_cons
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : LocallyFiniteOrderBot α
a : α
⊢ (Iic a).sup' ⋯ id = a

Tactic:
le_antisymm (sup'_le _ _ fun _ ↦ mem_Iic.1) <| le_sup' (f := id) <| mem_Iic.2 <| le_refl a

Premises used: Iff.mpr, le_refl, Finset.mem_Iic, id, le_antisymm, Finset.sup'_le, Iff.mp, Finset.le_sup'
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : LocallyFiniteOrderBot α
inst_2 : OrderBot α
a : α
⊢ (Iic a).sup id = a

Tactic:
le_antisymm (Finset.sup_le fun _ ↦ mem_Iic.1) <| le_sup (f := id) <| mem_Iic.2 <| le_refl a

Premises used: Iff.mpr, le_refl, Finset.mem_Iic, Finset.sup_le, le_antisymm, Iff.mp, Finset.le_sup
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : SemilatticeSup α
inst_1 : LocallyFiniteOrderBot α
inst_2 : OrderBot α
inst_3 : DecidableEq α
f : ι → α
s : Finset ι
⊢ image f s ⊆ Iic (s.sup f)

Tactic:
fun i hi ↦ mem_Iic.2 ?_

Premises used: Iff.mpr, Finset.mem_Iic
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : SemilatticeSup α
inst_1 : LocallyFiniteOrderBot α
inst_2 : OrderBot α
inst_3 : DecidableEq α
f : ι → α
s : Finset ι
refine : ∀ (i : α) (hi : i ∈ image f s), i ≤ s.sup f
⊢ image f s ⊆ Iic (s.sup f)

Tactic:
refine fun i hi ↦ mem_Iic.2 ?_

Premises used: Iff.mpr, Finset.mem_Iic
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : SemilatticeSup α
inst_1 : LocallyFiniteOrderBot α
inst_2 : OrderBot α
inst_3 : DecidableEq α
f : ι → α
s : Finset ι
i : α
hi : i ∈ image f s
obtain : ∀ (j : ι) (hj : j ∈ s) (hi : f j ∈ image f s), f j ≤ s.sup f
⊢ i ≤ s.sup f

Tactic:
obtain ⟨j, hj, rfl⟩ := mem_image.1 hi

Premises used: Finset.mem_image, Iff.mp, rfl
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : SemilatticeSup α
inst_1 : LocallyFiniteOrderBot α
inst_2 : OrderBot α
inst_3 : DecidableEq α
f : ι → α
s : Finset ι
j : ι
hj : j ∈ s
hi : f j ∈ image f s
⊢ f j ≤ s.sup f

Tactic:
le_sup hj

Premises used: Finset.le_sup
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : SemilatticeSup α
inst_1 : LocallyFiniteOrderBot α
inst_2 : OrderBot α
inst_3 : DecidableEq α
f : ι → α
s : Finset ι
j : ι
hj : j ∈ s
hi : f j ∈ image f s
⊢ f j ≤ s.sup f

Tactic:
exact le_sup hj

Premises used: Finset.le_sup
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : LocallyFiniteOrderBot α
inst_2 : OrderBot α
s : Finset α
⊢ s ⊆ Iic (s.sup id)

Tactic:
fun _ h ↦ mem_Iic.2 <| le_sup (f := id) h

Premises used: Iff.mpr, Finset.mem_Iic, Finset.le_sup
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : SemilatticeInf α
inst_1 : LocallyFiniteOrderTop α
a : α
⊢ (Ici a).inf' ⋯ id = a

Tactic:
ge_antisymm (le_inf' _ _ fun _ ↦ mem_Ici.1) <| inf'_le (f := id) <| mem_Ici.2 <| le_refl a

Premises used: Iff.mpr, le_refl, Finset.mem_Ici, id, ge_antisymm, Finset.le_inf', Iff.mp, Finset.inf'_le
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : SemilatticeInf α
inst_1 : LocallyFiniteOrderTop α
inst_2 : OrderTop α
a : α
⊢ (Ici a).inf id = a

Tactic:
le_antisymm (inf_le (f := id) <| mem_Ici.2 <| le_refl a) <| Finset.le_inf fun _ ↦ mem_Ici.1

Premises used: Iff.mpr, le_refl, Finset.mem_Ici, le_antisymm, Iff.mp, Finset.le_inf, Finset.inf_le
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a₁ b₁ a₂ b₂ : α
h : a₁ < b₁
rw : (↑(Ico a₁ b₁) : Set α) ⊆ (↑(Ico a₂ b₂) : Set α) ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
rw₁ : Set.Ico a₁ b₁ ⊆ (↑(Ico a₂ b₂) : Set α) ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
rw₂ : Set.Ico a₁ b₁ ⊆ Set.Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
rw₃ rw₄ : a₂ ≤ a₁ ∧ b₁ ≤ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
⊢ Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Tactic:
rw [← coe_subset, coe_Ico, coe_Ico, Set.Ico_subset_Ico_iff h]

Premises used: Finset.coe_Ico, Set.Ico_subset_Ico_iff, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
rw : (↑(Ico a b ∪ Ico b c) : Set α) = (↑(Ico a c) : Set α)
rw₁ : (↑(Ico a b) : Set α) ∪ (↑(Ico b c) : Set α) = (↑(Ico a c) : Set α)
rw₂ : Set.Ico a b ∪ (↑(Ico b c) : Set α) = (↑(Ico a c) : Set α)
rw₃ : Set.Ico a b ∪ Set.Ico b c = (↑(Ico a c) : Set α)
rw₄ : Set.Ico a b ∪ Set.Ico b c = Set.Ico a c
rw₅ rw₆ : Set.Ico a c = Set.Ico a c
⊢ Ico a b ∪ Ico b c = Ico a c

Tactic:
rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico_eq_Ico hab hbc]

Premises used: Finset.coe_Ico, Finset.coe_inj, Set.Ico_union_Ico_eq_Ico, Finset.coe_union
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
rw : (↑(Ioc a b ∪ Ioc b c) : Set α) = (↑(Ioc a c) : Set α)
rw₁ : (↑(Ioc a b) : Set α) ∪ (↑(Ioc b c) : Set α) = (↑(Ioc a c) : Set α)
rw₂ : Set.Ioc a b ∪ (↑(Ioc b c) : Set α) = (↑(Ioc a c) : Set α)
rw₃ : Set.Ioc a b ∪ Set.Ioc b c = (↑(Ioc a c) : Set α)
rw₄ : Set.Ioc a b ∪ Set.Ioc b c = Set.Ioc a c
rw₅ rw₆ : Set.Ioc a c = Set.Ioc a c
⊢ Ioc a b ∪ Ioc b c = Ioc a c

Tactic:
rw [← coe_inj, coe_union, coe_Ioc, coe_Ioc, coe_Ioc, Set.Ioc_union_Ioc_eq_Ioc h₁ h₂]

Premises used: Set.Ioc_union_Ioc_eq_Ioc, Finset.coe_inj, Finset.coe_Ioc, Finset.coe_union
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
rw : Set.Ico a c ⊆ Set.Ico a b ∪ Set.Ico b c
⊢ Ico a c ⊆ Ico a b ∪ Ico b c

Tactic:
rw [← coe_subset, coe_union, coe_Ico, coe_Ico, coe_Ico]

Premises used: Finset.coe_Ico, Finset.coe_union, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ Set.Ico a c ⊆ Set.Ico a b ∪ Set.Ico b c

Tactic:
Set.Ico_subset_Ico_union_Ico

Premises used: Set.Ico_subset_Ico_union_Ico
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ Set.Ico a c ⊆ Set.Ico a b ∪ Set.Ico b c

Tactic:
exact Set.Ico_subset_Ico_union_Ico

Premises used: Set.Ico_subset_Ico_union_Ico
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
rw : (↑(Ico a b ∪ Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
rw₁ : (↑(Ico a b) : Set α) ∪ (↑(Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
rw₂ : Set.Ico a b ∪ (↑(Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
rw₃ : Set.Ico a b ∪ Set.Ico c d = (↑(Ico (min a c) (max b d)) : Set α)
rw₄ : Set.Ico a b ∪ Set.Ico c d = Set.Ico (min a c) (max b d)
rw₅ rw₆ : Set.Ico (min a c) (max b d) = Set.Ico (min a c) (max b d)
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)

Tactic:
rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico h₁ h₂]

Premises used: Finset.coe_Ico, Finset.coe_inj, Set.Ico_union_Ico, Finset.coe_union
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
hcb : c ≤ b
had : a ≤ d
rw : (↑(Ico a b ∪ Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
rw₁ : (↑(Ico a b) : Set α) ∪ (↑(Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
rw₂ : Set.Ico a b ∪ (↑(Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
rw₃ : Set.Ico a b ∪ Set.Ico c d = (↑(Ico (min a c) (max b d)) : Set α)
rw₄ : Set.Ico a b ∪ Set.Ico c d = Set.Ico (min a c) (max b d)
rw₅ rw₆ : Set.Ico (min a c) (max b d) = Set.Ico (min a c) (max b d)
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)

Tactic:
rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico' hcb had]

Premises used: Finset.coe_Ico, Finset.coe_inj, Set.Ico_union_Ico', Finset.coe_union
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
rw : (↑(Ico a b ∩ Ico c d) : Set α) = (↑(Ico (max a c) (min b d)) : Set α)
rw₁ : (↑(Ico a b) : Set α) ∩ (↑(Ico c d) : Set α) = (↑(Ico (max a c) (min b d)) : Set α)
rw₂ : Set.Ico a b ∩ (↑(Ico c d) : Set α) = (↑(Ico (max a c) (min b d)) : Set α)
rw₃ : Set.Ico a b ∩ Set.Ico c d = (↑(Ico (max a c) (min b d)) : Set α)
rw₄ : Set.Ico a b ∩ Set.Ico c d = Set.Ico (max a c) (min b d)
rw₅ rw₆ : Set.Ico (max a c) (min b d) = Set.Ico (max a c) (min b d)
⊢ Ico a b ∩ Ico c d = Ico (max a c) (min b d)

Tactic:
rw [← coe_inj, coe_inter, coe_Ico, coe_Ico, coe_Ico, Set.Ico_inter_Ico]

Premises used: Finset.coe_Ico, Set.Ico_inter_Ico, Finset.coe_inj, Finset.coe_inter
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
⊢ Ioc a b ∩ Ioc c d = Ioc (max a c) (min b d)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ {x ∈ Ico a b | x < c} = Ico a (min b c)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ {x ∈ Ico a b | c ≤ x} = Ico (max a c) b

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ {x ∈ Ioo a b | x < c} = Ioo a (min b c)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_3
inst : LinearOrder α
inst_1 : LocallyFiniteOrderBot α
a b : α
⊢ {x ∈ Iio a | x < b} = Iio (min a b)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ Ico a b \ Ico a c = Ico (max a c) b

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ Ico a b \ Ico c b = Ico a (min b c)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
simp_rw : Ioc a₁ a₂ ∩ Ioc b₁ b₂ = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁
simp_rw₁ : Ioc (max a₁ b₁) (min a₂ b₂) = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁
simp_rw₂ : ¬max a₁ b₁ < min a₂ b₂ ↔ min a₂ b₂ ≤ max a₁ b₁
⊢ Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁

Tactic:
simp_rw [disjoint_iff_inter_eq_empty, Ioc_inter_Ioc, Ioc_eq_empty_iff, not_lt]

Premises used: Finset.Ioc_inter_Ioc, Finset.Ioc_eq_empty_iff, Finset.disjoint_iff_inter_eq_empty, not_lt
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : LocallyFiniteOrderBot α
⊢ Iic b \ Ioc a b = Iic (min a b)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : LocallyFiniteOrderBot α
hab : a ≤ b
rw : Iic (min a b) = Iic a
rw₁ rw₂ : Iic a = Iic a
⊢ Iic b \ Ioc a b = Iic a

Tactic:
rw [Iic_diff_Ioc, min_eq_left hab]

Premises used: min_eq_left, Finset.Iic_diff_Ioc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : LocallyFiniteOrderBot α
h : a ≤ b
⊢ Iic a ∪ Ioc a b = Iic b

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrderBot α
s : Set α
hs : s.Infinite
⊢ ∀ (a : α), ∃ b ∈ s, a < b

Tactic:
not_bddAbove_iff.1 hs.not_bddAbove

Premises used: Set.Infinite.not_bddAbove, Iff.mp, not_bddAbove_iff
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrderBot α
s : Set α
inst_2 : Nonempty α
⊢ s.Infinite ↔ ∀ (a : α), ∃ b ∈ s, a < b

Tactic:
⟨Set.Infinite.exists_gt, Set.infinite_of_forall_exists_gt⟩

Premises used: Set.Infinite.exists_gt, Set.infinite_of_forall_exists_gt, Iff.intro
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrderTop α
s : Set α
hs : s.Infinite
⊢ ∀ (a : α), ∃ b ∈ s, b < a

Tactic:
not_bddBelow_iff.1 hs.not_bddBelow

Premises used: not_bddBelow_iff, Iff.mp, Set.Infinite.not_bddBelow
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrderTop α
s : Set α
inst_2 : Nonempty α
⊢ s.Infinite ↔ ∀ (a : α), ∃ b ∈ s, b < a

Tactic:
⟨Set.Infinite.exists_lt, Set.infinite_of_forall_exists_lt⟩

Premises used: Set.Infinite.exists_lt, Set.infinite_of_forall_exists_lt, Iff.intro
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : Fintype α
inst_2 : LocallyFiniteOrderTop α
inst_3 : LocallyFiniteOrderBot α
a : α
h : ∀ (a_1 : α), a_1 ∈ (Ioi a).disjUnion (Iio a) ⋯ ↔ Membership.mem (γ := Finset α) {a}ᶜ a_1
⊢ (Ioi a).disjUnion (Iio a) ⋯ = {a}ᶜ

Tactic:
ext
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : Fintype α
inst_2 : LocallyFiniteOrderTop α
inst_3 : LocallyFiniteOrderBot α
a a_1 : α
⊢ a_1 ∈ (Ioi a).disjUnion (Iio a) ⋯ ↔ Membership.mem (γ := Finset α) {a}ᶜ a_1

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ [[(toDual : (a : α) → αᵒᵈ) a, (toDual : (a : α) → αᵒᵈ) b]] = map (Equiv.toEmbedding toDual) [[a, b]]

Tactic:
Icc_toDual (a ⊔ b) (a ⊓ b)

Premises used: Finset.Icc_toDual, Max.max, Min.min, Finset.uIcc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
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, Finset.uIcc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
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, Finset.uIcc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a b : α
rw : Icc (a ⊓ b) (a ⊔ b) = [[b, a]]
rw₁ : Icc (a ⊓ b) (a ⊔ b) = Icc (b ⊓ a) (b ⊔ a)
rw₂ : Icc (b ⊓ a) (a ⊔ b) = Icc (b ⊓ a) (b ⊔ a)
rw₃ rw₄ : Icc (b ⊓ a) (b ⊔ a) = Icc (b ⊓ a) (b ⊔ a)
⊢ [[a, b]] = [[b, a]]

Tactic:
rw [uIcc, uIcc, inf_comm, sup_comm]

Premises used: inf_comm, sup_comm, Finset.uIcc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a : α
⊢ [[a, a]] = {a}

Tactic:
simp [uIcc]

Premises used: Finset.uIcc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ [[a, b]].Nonempty

Tactic:
nonempty_Icc.2 inf_le_sup

Premises used: Iff.mpr, Finset.nonempty_Icc, inf_le_sup, Finset.uIcc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ Icc a b ⊆ [[a, b]]

Tactic:
Icc_subset_Icc inf_le_left le_sup_right

Premises used: Set.Mem, setOf, le_sup_right, Finset.Icc_subset_Icc, inf_le_left
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ Icc b a ⊆ [[a, b]]

Tactic:
Icc_subset_Icc inf_le_right le_sup_left

Premises used: le_sup_left, Set.Mem, setOf, inf_le_right, Finset.Icc_subset_Icc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ a ∈ [[a, b]]

Tactic:
mem_Icc.2 ⟨inf_le_left, le_sup_left⟩

Premises used: Iff.mpr, le_sup_left, Set.Mem, setOf, Finset.mem_Icc, And.intro, inf_le_left
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ b ∈ [[a, b]]

Tactic:
mem_Icc.2 ⟨inf_le_right, le_sup_right⟩

Premises used: Iff.mpr, Set.Mem, setOf, inf_le_right, Finset.mem_Icc, le_sup_right, And.intro