awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : (↑a : α) ≤ x ∧ x < (↑b : α)
⊢ p x

Tactic:
exact hp hx.1 hx.2.le a.prop b.prop

Premises used: LT.lt.le, And.right, And.left, Subtype.prop
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ioc (↑a : α) (↑b : α))) = Ioc (↑a : α) (↑b : α)

Tactic:
Finset.subtype_map_of_mem fun x hx => ?_

Premises used: Finset.subtype_map_of_mem
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
refine : ∀ (x : α) (hx : x ∈ Ioc (↑a : α) (↑b : α)), p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ioc (↑a : α) (↑b : α))) = Ioc (↑a : α) (↑b : α)

Tactic:
refine Finset.subtype_map_of_mem fun x hx => ?_

Premises used: Finset.subtype_map_of_mem
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : x ∈ Ioc (↑a : α) (↑b : α)
⊢ (↑a : α) < x ∧ x ≤ (↑b : α)

Tactic:
rw [mem_Ioc] at hx

Premises used: Finset.mem_Ioc
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : (↑a : α) < x ∧ x ≤ (↑b : α)
⊢ p x

Tactic:
hp hx.1.le hx.2 a.prop b.prop

Premises used: LT.lt.le, And.right, And.left, Subtype.prop
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : (↑a : α) < x ∧ x ≤ (↑b : α)
⊢ p x

Tactic:
exact hp hx.1.le hx.2 a.prop b.prop

Premises used: LT.lt.le, And.right, And.left, Subtype.prop
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ioo (↑a : α) (↑b : α))) = Ioo (↑a : α) (↑b : α)

Tactic:
Finset.subtype_map_of_mem fun x hx => ?_

Premises used: Finset.subtype_map_of_mem
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
refine : ∀ (x : α) (hx : x ∈ Ioo (↑a : α) (↑b : α)), p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ioo (↑a : α) (↑b : α))) = Ioo (↑a : α) (↑b : α)

Tactic:
refine Finset.subtype_map_of_mem fun x hx => ?_

Premises used: Finset.subtype_map_of_mem
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : x ∈ Ioo (↑a : α) (↑b : α)
⊢ (↑a : α) < x ∧ x < (↑b : α)

Tactic:
rw [mem_Ioo] at hx

Premises used: Finset.mem_Ioo
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : (↑a : α) < x ∧ x < (↑b : α)
⊢ p x

Tactic:
hp hx.1.le hx.2.le a.prop b.prop

Premises used: LT.lt.le, And.right, And.left, Subtype.prop
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : (↑a : α) < x ∧ x < (↑b : α)
⊢ p x

Tactic:
exact hp hx.1.le hx.2.le a.prop b.prop

Premises used: LT.lt.le, And.right, And.left, Subtype.prop
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrderTop α
a : Subtype p
⊢ Ici a = Finset.subtype p (Ici (↑a : α))

Tactic:
rfl

Premises used: Finset.map, Finset.Ici, Finset.subtype, rfl
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrderTop α
a : Subtype p
⊢ Ioi a = Finset.subtype p (Ioi (↑a : α))

Tactic:
rfl

Premises used: Finset.Ioi, Finset.map, Finset.subtype, rfl
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrderTop α
a : Subtype p
hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ici (↑a : α))) = Ici (↑a : α)

Tactic:
Finset.subtype_map_of_mem fun x hx => hp (mem_Ici.1 hx) a.prop

Premises used: Finset.subtype_map_of_mem, Finset.mem_Ici, Subtype.prop, Iff.mp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrderTop α
a : Subtype p
hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ici (↑a : α))) = Ici (↑a : α)

Tactic:
exact Finset.subtype_map_of_mem fun x hx => hp (mem_Ici.1 hx) a.prop

Premises used: Finset.subtype_map_of_mem, Finset.mem_Ici, Subtype.prop, Iff.mp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrderTop α
a : Subtype p
hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ioi (↑a : α))) = Ioi (↑a : α)

Tactic:
Finset.subtype_map_of_mem fun x hx => hp (mem_Ioi.1 hx).le a.prop

Premises used: Finset.subtype_map_of_mem, LT.lt.le, Finset.mem_Ioi, Subtype.prop, Iff.mp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrderTop α
a : Subtype p
hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ioi (↑a : α))) = Ioi (↑a : α)

Tactic:
exact Finset.subtype_map_of_mem fun x hx => hp (mem_Ioi.1 hx).le a.prop

Premises used: Finset.subtype_map_of_mem, LT.lt.le, Finset.mem_Ioi, Subtype.prop, Iff.mp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrder α
s : Set α
h₀ : BddBelow s
h₁ : BddAbove s
⊢ s.Finite

Tactic:
let ⟨a, ha⟩ := h₀
  let ⟨b, hb⟩ := h₁
  (Set.finite_Icc a b).subset fun _x hx ↦ ⟨ha hx, hb hx⟩

Premises used: Set.Finite, _private.0.BddBelow.finite_of_bddAbove.match_1, Set.Finite.subset, Set.finite_Icc, And.intro, _private.0.BddBelow.finite_of_bddAbove.match_2
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_3
s : Set α
inst : SemilatticeSup α
inst_1 : LocallyFiniteOrder α
inst_2 : OrderBot α
⊢ s.Finite ↔ BddAbove s

Tactic:
⟨fun h ↦ ⟨h.toFinset.sup id, fun _ hx ↦ Finset.le_sup (f := id) ((Finite.mem_toFinset h).mpr hx)⟩,
    fun ⟨m, hm⟩ ↦ (Set.finite_Icc ⊥ m).subset (fun _ hx ↦ ⟨bot_le, hm hx⟩)⟩

Premises used: Iff.mpr, Set.Finite.mem_toFinset, Set.Finite, _private.0.Set.finite_iff_bddAbove.match_1, id, Set.Finite.subset, Bot.bot, Set.finite_Icc, Set.Finite.toFinset, And.intro, Iff.intro, Exists.intro, Finset.sup, bot_le, Finset.le_sup
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_3
s : Set α
inst : Nonempty α
inst_1 : Lattice α
inst_2 : LocallyFiniteOrder α
inl : Set.Finite.{u_3} (α := α) ∅ ↔ BddBelow.{u_3} (α := α) ∅ ∧ BddAbove.{u_3} (α := α) ∅
inr : ∀ (hs : s.Nonempty), s.Finite ↔ BddBelow s ∧ BddAbove s
⊢ s.Finite ↔ BddBelow s ∧ BddAbove s

Tactic:
obtain (rfl | hs) := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_3
inst : Nonempty α
inst_1 : Lattice α
inst_2 : LocallyFiniteOrder α
⊢ Set.Finite.{u_3} (α := α) ∅ ↔ BddBelow.{u_3} (α := α) ∅ ∧ BddAbove.{u_3} (α := α) ∅

Tactic:
simp only [Set.finite_empty, bddBelow_empty, bddAbove_empty, and_self]

Premises used: Set.finite_empty, and_self, bddBelow_empty, bddAbove_empty
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_3
s : Set α
inst : Nonempty α
inst_1 : Lattice α
inst_2 : LocallyFiniteOrder α
hs : s.Nonempty
⊢ s.Finite ↔ BddBelow s ∧ BddAbove s

Tactic:
⟨fun h ↦ ⟨⟨h.toFinset.inf' ((Finite.toFinset_nonempty h).mpr hs) id,
    fun x hx ↦ Finset.inf'_le id ((Finite.mem_toFinset h).mpr hx)⟩,
    ⟨h.toFinset.sup' ((Finite.toFinset_nonempty h).mpr hs) id, fun x hx ↦ Finset.le_sup' id
    ((Finite.mem_toFinset h).mpr hx)⟩⟩,
    fun ⟨h₀, h₁⟩ ↦ BddBelow.finite_of_bddAbove h₀ h₁⟩

Premises used: Iff.mpr, Finset.inf', Set.Finite.mem_toFinset, Set.Finite, id, _private.0.Set.finite_iff_bddBelow_bddAbove.match_3, Set.Finite.toFinset, And.intro, Iff.intro, Exists.intro, Finset.sup', Finset.le_sup', Set.Finite.toFinset_nonempty, Finset.inf'_le, BddBelow.finite_of_bddAbove
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_3
s : Set α
inst : Nonempty α
inst_1 : Lattice α
inst_2 : LocallyFiniteOrder α
hs : s.Nonempty
⊢ s.Finite ↔ BddBelow s ∧ BddAbove s

Tactic:
exact ⟨fun h ↦ ⟨⟨h.toFinset.inf' ((Finite.toFinset_nonempty h).mpr hs) id,
    fun x hx ↦ Finset.inf'_le id ((Finite.mem_toFinset h).mpr hx)⟩,
    ⟨h.toFinset.sup' ((Finite.toFinset_nonempty h).mpr hs) id, fun x hx ↦ Finset.le_sup' id
    ((Finite.mem_toFinset h).mpr hx)⟩⟩,
    fun ⟨h₀, h₁⟩ ↦ BddBelow.finite_of_bddAbove h₀ h₁⟩
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
y : α
inst_2 : DecidableLE α
inst_3 : LocallyFiniteOrder α
a : { x : α // x ≤ y }
⊢ y ≤ y

Tactic:
rfl
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
y : α
inst_2 : DecidableLE α
inst_3 : LocallyFiniteOrder α
a b : { x : α // x ≤ y }
simp : a ≤ b → b ≤ Subtype.mk (p := fun (x : α) ↦ x ≤ y) y ⋯
⊢ b ∈ Icc a (Subtype.mk (p := fun (x : α) ↦ x ≤ y) y ⋯) ↔ a ≤ b

Tactic:
simp only [Finset.mem_Icc, and_iff_left_iff_imp]

Premises used: Finset.mem_Icc, and_iff_left_iff_imp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
y : α
inst_2 : DecidableLE α
inst_3 : LocallyFiniteOrder α
a b : { x : α // x ≤ y }
⊢ a ≤ b → b ≤ Subtype.mk (p := fun (x : α) ↦ x ≤ y) y ⋯

Tactic:
fun _ => b.property

Premises used: Subtype.property
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
y : α
inst_2 : DecidableLE α
inst_3 : LocallyFiniteOrder α
a b : { x : α // x ≤ y }
⊢ a ≤ b → b ≤ Subtype.mk (p := fun (x : α) ↦ x ≤ y) y ⋯

Tactic:
exact fun _ => b.property

Premises used: Subtype.property
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
y : α
inst_2 : DecidableLE α
inst_3 : LocallyFiniteOrder α
a b : { x : α // x ≤ y }
simp : a < b → b ≤ Subtype.mk (p := fun (x : α) ↦ x ≤ y) y ⋯
⊢ b ∈ Ioc a (Subtype.mk (p := fun (x : α) ↦ x ≤ y) y ⋯) ↔ a < b

Tactic:
simp only [Finset.mem_Ioc, and_iff_left_iff_imp]

Premises used: Finset.mem_Ioc, and_iff_left_iff_imp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
y : α
inst_2 : DecidableLE α
inst_3 : LocallyFiniteOrder α
a b : { x : α // x ≤ y }
⊢ a < b → b ≤ Subtype.mk (p := fun (x : α) ↦ x ≤ y) y ⋯

Tactic:
fun _ => b.property

Premises used: Subtype.property
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
y : α
inst_2 : DecidableLE α
inst_3 : LocallyFiniteOrder α
a b : { x : α // x ≤ y }
⊢ a < b → b ≤ Subtype.mk (p := fun (x : α) ↦ x ≤ y) y ⋯

Tactic:
exact fun _ => b.property

Premises used: Subtype.property
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
y : α
inst_2 : DecidableLT α
inst_3 : LocallyFiniteOrder α
a b : { x : α // x < y }
simp : a ≤ b → (↑b : α) < y
⊢ Membership.mem (γ := Finset { x : α // x < y }) (Finset.subtype (fun (x : α) ↦ x < y) (Ico (↑a : α) y)) b ↔ a ≤ b

Tactic:
simp only [Finset.mem_subtype, Finset.mem_Ico, Subtype.coe_le_coe, and_iff_left_iff_imp]

Premises used: Subtype.coe_le_coe, Finset.mem_subtype, and_iff_left_iff_imp, Finset.mem_Ico
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
y : α
inst_2 : DecidableLT α
inst_3 : LocallyFiniteOrder α
a b : { x : α // x < y }
⊢ a ≤ b → (↑b : α) < y

Tactic:
fun _ => b.property

Premises used: Subtype.property
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
y : α
inst_2 : DecidableLT α
inst_3 : LocallyFiniteOrder α
a b : { x : α // x < y }
⊢ a ≤ b → (↑b : α) < y

Tactic:
exact fun _ => b.property

Premises used: Subtype.property
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
y : α
inst_2 : DecidableLT α
inst_3 : LocallyFiniteOrder α
a b : { x : α // x < y }
simp : a < b → (↑b : α) < y
⊢ Membership.mem (γ := Finset { x : α // x < y }) (Finset.subtype (fun (x : α) ↦ x < y) (Ioo (↑a : α) y)) b ↔ a < b

Tactic:
simp only [Finset.mem_subtype, Finset.mem_Ioo, Subtype.coe_lt_coe, and_iff_left_iff_imp]

Premises used: Subtype.coe_lt_coe, Finset.mem_Ioo, Finset.mem_subtype, and_iff_left_iff_imp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
y : α
inst_2 : DecidableLT α
inst_3 : LocallyFiniteOrder α
a b : { x : α // x < y }
⊢ a < b → (↑b : α) < y

Tactic:
fun _ => b.property

Premises used: Subtype.property
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
y : α
inst_2 : DecidableLT α
inst_3 : LocallyFiniteOrder α
a b : { x : α // x < y }
⊢ a < b → (↑b : α) < y

Tactic:
exact fun _ => b.property

Premises used: Subtype.property
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
y : α
inst_2 : LocallyFiniteOrderBot α
⊢ Finite.{max 1 (u_1 + 1)} { x : α // x ≤ y }

Tactic:
simpa only [coe_Iic] using (Finset.Iic y).finite_toSet

Premises used: Finset.coe_Iic, Finset.Iic, Finset.finite_toSet
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
y : α
inst_2 : LocallyFiniteOrderBot α
⊢ Finite.{max 1 (u_1 + 1)} { x : α // x < y }

Tactic:
simpa only [coe_Iio] using (Finset.Iio y).finite_toSet

Premises used: Finset.Iio, Finset.coe_Iio, Finset.finite_toSet
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : Fintype (↑(Icc a b) : Type u_3)
h : ∀ (a_1 : α), a_1 ∈ (Icc a b).toFinset ↔ a_1 ∈ Finset.Icc a b
⊢ (Icc a b).toFinset = Finset.Icc a b

Tactic:
ext
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : Fintype (↑(Icc a b) : Type u_3)
a_1 : α
⊢ a_1 ∈ (Icc a b).toFinset ↔ a_1 ∈ Finset.Icc a b

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : Fintype (↑(Ico a b) : Type u_3)
h : ∀ (a_1 : α), a_1 ∈ (Ico a b).toFinset ↔ a_1 ∈ Finset.Ico a b
⊢ (Ico a b).toFinset = Finset.Ico a b

Tactic:
ext
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : Fintype (↑(Ico a b) : Type u_3)
a_1 : α
⊢ a_1 ∈ (Ico a b).toFinset ↔ a_1 ∈ Finset.Ico a b

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : Fintype (↑(Ioo a b) : Type u_3)
h : ∀ (a_1 : α), a_1 ∈ (Ioo a b).toFinset ↔ a_1 ∈ Finset.Ioo a b
⊢ (Ioo a b).toFinset = Finset.Ioo a b

Tactic:
ext
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : Fintype (↑(Ioo a b) : Type u_3)
a_1 : α
⊢ a_1 ∈ (Ioo a b).toFinset ↔ a_1 ∈ Finset.Ioo a b

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a : α
inst_2 : Fintype (↑(Ici a) : Type u_3)
h : ∀ (a_1 : α), a_1 ∈ (Ici a).toFinset ↔ a_1 ∈ Finset.Ici a
⊢ (Ici a).toFinset = Finset.Ici a

Tactic:
ext
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a : α
inst_2 : Fintype (↑(Ici a) : Type u_3)
a_1 : α
⊢ a_1 ∈ (Ici a).toFinset ↔ a_1 ∈ Finset.Ici a

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a : α
inst_2 : Fintype (↑(Ioi a) : Type u_3)
h : ∀ (a_1 : α), a_1 ∈ (Ioi a).toFinset ↔ a_1 ∈ Finset.Ioi a
⊢ (Ioi a).toFinset = Finset.Ioi a

Tactic:
ext
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a : α
inst_2 : Fintype (↑(Ioi a) : Type u_3)
a_1 : α
⊢ a_1 ∈ (Ioi a).toFinset ↔ a_1 ∈ Finset.Ioi a

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
y : α
F : Type u_3
M : Type u_4
N : Type u_5
inst_2 : Preorder M
inst_3 : Preorder N
inst_4 : EquivLike F M N
inst_5 : OrderIsoClass F M N
f : F
inst_6 : LocallyFiniteOrder N
⊢ ∀ (a b x : M),
    x ∈
        map { toFun := EquivLike.inv f, inj' := ⋯ : N ↪ M }
          (@finsetIcc _ inst_3 _ ((f : (a : M) → N) a) ((f : (a : M) → N) b)) ↔
      a ≤ x ∧ x ≤ b

Tactic:
simp [finset_mem_Icc, EquivLike.inv_apply_eq]

Premises used: LocallyFiniteOrder.finset_mem_Icc, EquivLike.inv_apply_eq
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
y : α
F : Type u_3
M : Type u_4
N : Type u_5
inst_2 : Preorder M
inst_3 : Preorder N
inst_4 : EquivLike F M N
inst_5 : OrderIsoClass F M N
f : F
inst_6 : LocallyFiniteOrder N
⊢ ∀ (a b x : M),
    x ∈
        map { toFun := EquivLike.inv f, inj' := ⋯ : N ↪ M }
          (@finsetIco _ inst_3 _ ((f : (a : M) → N) a) ((f : (a : M) → N) b)) ↔
      a ≤ x ∧ x < b

Tactic:
simp [finset_mem_Ico, EquivLike.inv_apply_eq, map_lt_map_iff]

Premises used: EquivLike.inv_apply_eq, map_lt_map_iff, LocallyFiniteOrder.finset_mem_Ico
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
y : α
F : Type u_3
M : Type u_4
N : Type u_5
inst_2 : Preorder M
inst_3 : Preorder N
inst_4 : EquivLike F M N
inst_5 : OrderIsoClass F M N
f : F
inst_6 : LocallyFiniteOrder N
⊢ ∀ (a b x : M),
    x ∈
        map { toFun := EquivLike.inv f, inj' := ⋯ : N ↪ M }
          (@finsetIoc _ inst_3 _ ((f : (a : M) → N) a) ((f : (a : M) → N) b)) ↔
      a < x ∧ x ≤ b

Tactic:
simp [finset_mem_Ioc, EquivLike.inv_apply_eq, map_lt_map_iff]

Premises used: EquivLike.inv_apply_eq, map_lt_map_iff, LocallyFiniteOrder.finset_mem_Ioc
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
y : α
F : Type u_3
M : Type u_4
N : Type u_5
inst_2 : Preorder M
inst_3 : Preorder N
inst_4 : EquivLike F M N
inst_5 : OrderIsoClass F M N
f : F
inst_6 : LocallyFiniteOrder N
⊢ ∀ (a b x : M),
    x ∈
        map { toFun := EquivLike.inv f, inj' := ⋯ : N ↪ M }
          (@finsetIoo _ inst_3 _ ((f : (a : M) → N) a) ((f : (a : M) → N) b)) ↔
      a < x ∧ x < b

Tactic:
simp [finset_mem_Ioo, EquivLike.inv_apply_eq, map_lt_map_iff]

Premises used: LocallyFiniteOrder.finset_mem_Ioo, EquivLike.inv_apply_eq, map_lt_map_iff
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
⊢ DenselyOrdered X ↔ Subsingleton X

Tactic:
⟨fun H ↦ ?_, fun h ↦ h.instDenselyOrdered⟩

Premises used: Iff.intro, Subsingleton.instDenselyOrdered
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
refine : ∀ (H : DenselyOrdered X), Subsingleton X
⊢ DenselyOrdered X ↔ Subsingleton X

Tactic:
refine ⟨fun H ↦ ?_, fun h ↦ h.instDenselyOrdered⟩
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
H : DenselyOrdered X
rw : ¬∃ (x : X) (y : X), x < y
⊢ Subsingleton X

Tactic:
rw [← not_nontrivial_iff_subsingleton, nontrivial_iff_lt]

Premises used: not_nontrivial_iff_subsingleton, nontrivial_iff_lt
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
H : DenselyOrdered X
a b : X
hab : a < b
⊢ False

Tactic:
not_lt_of_denselyOrdered_of_locallyFinite a b hab

Premises used: not_lt_of_denselyOrdered_of_locallyFinite
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
H : DenselyOrdered X
a b : X
hab : a < b
⊢ False

Tactic:
exact not_lt_of_denselyOrdered_of_locallyFinite a b hab

Premises used: not_lt_of_denselyOrdered_of_locallyFinite
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set X
⊢ DenselyOrdered.{u_1} (↑s : Type u_1) ↔ s.Subsingleton

Tactic:
simp [LocallyFiniteOrder.denselyOrdered_iff_subsingleton]

Premises used: LocallyFiniteOrder.denselyOrdered_iff_subsingleton
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set X
⊢ DenselyOrdered.{u_1} (↑s : Type u_1) ↔ s.Subsingleton

Tactic:
classical
  simp [LocallyFiniteOrder.denselyOrdered_iff_subsingleton]

Premises used: LocallyFiniteOrder.denselyOrdered_iff_subsingleton
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
⊢ DenselyOrdered.{u_1} (↑s : Type u_1) ↔ s.Subsingleton

Tactic:
⟨fun H ↦ ?_, fun h ↦ h.denselyOrdered⟩

Premises used: Iff.intro, Set.Subsingleton.denselyOrdered
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
refine : ∀ (H : DenselyOrdered.{u_1} (↑s : Type u_1)), s.Subsingleton
⊢ DenselyOrdered.{u_1} (↑s : Type u_1) ↔ s.Subsingleton

Tactic:
refine ⟨fun H ↦ ?_, fun h ↦ h.denselyOrdered⟩
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered.{u_1} (↑s : Type u_1)
rw : ¬∃ (x : (↑s : Type u_1)) (y : (↑s : Type u_1)), x < y
⊢ s.Subsingleton

Tactic:
rw [← Set.subsingleton_coe, ← not_nontrivial_iff_subsingleton, nontrivial_iff_lt]

Premises used: not_nontrivial_iff_subsingleton, Set.subsingleton_coe, nontrivial_iff_lt
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H_1 : DenselyOrdered.{u_1} (↑s : Type u_1)
this : DenselyOrdered.{u_1} (↑(some ⁻¹' s) : Type u_1)
x y : (↑s : Type u_1)
H : x < y
rw : ∀ (this : (some ⁻¹' s).Subsingleton) (x y : (↑s : Type u_1)) (H : x < y), False
⊢ False

Tactic:
rw [_root_.denselyOrdered_set_iff_subsingleton] at this

Premises used: denselyOrdered_set_iff_subsingleton