awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
b x : WithTop α
a : α
coe :
  Membership.mem (γ := Finset (WithTop α))
      (match (motive := WithTop α → WithTop α → Finset (WithTop α)) (↑a : WithTop α), ⊤ with
        | none, x => ∅
        | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b) :
        Finset (WithTop α))
      x ↔
    (↑a : WithTop α) < x ∧ x < ⊤
coe₁ :
  ∀ (a_1 : α),
    Membership.mem (γ := Finset (WithTop α))
        (match (motive := WithTop α → WithTop α → Finset (WithTop α)) (↑a : WithTop α), (↑a_1 : WithTop α) with
          | none, x => ∅
          | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
          | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b) :
          Finset (WithTop α))
        x ↔
      (↑a : WithTop α) < x ∧ x < (↑a_1 : WithTop α)
⊢ Membership.mem (γ := Finset (WithTop α))
      (match (motive := WithTop α → WithTop α → Finset (WithTop α)) (↑a : WithTop α), b with
        | none, x => ∅
        | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b) :
        Finset (WithTop α))
      x ↔
    (↑a : WithTop α) < x ∧ x < b

Tactic:
cases b
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
x : WithTop α
top :
  Membership.mem (γ := Finset (WithTop α))
      (match (motive := WithTop α → WithTop α → Finset (WithTop α)) ⊤, ⊤ with
        | none, x => ∅
        | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b) :
        Finset (WithTop α))
      ⊤ ↔
    LT.lt.{u_1} (α := WithTop α) ⊤ ⊤ ∧ LT.lt.{u_1} (α := WithTop α) ⊤ ⊤
top₁ :
  ∀ (a : α),
    Membership.mem (γ := Finset (WithTop α))
        (match (motive := WithTop α → WithTop α → Finset (WithTop α)) ⊤, ⊤ with
          | none, x => ∅
          | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
          | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b) :
          Finset (WithTop α))
        (↑a : WithTop α) ↔
      ⊤ < (↑a : WithTop α) ∧ (↑a : WithTop α) < ⊤
⊢ Membership.mem (γ := Finset (WithTop α))
      (match (motive := WithTop α → WithTop α → Finset (WithTop α)) ⊤, ⊤ with
        | none, x => ∅
        | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b) :
        Finset (WithTop α))
      x ↔
    ⊤ < x ∧ x < ⊤

Tactic:
cases x
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
x : WithTop α
a : α
top :
  Membership.mem (γ := Finset (WithTop α))
      (match (motive := WithTop α → WithTop α → Finset (WithTop α)) ⊤, (↑a : WithTop α) with
        | none, x => ∅
        | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b) :
        Finset (WithTop α))
      ⊤ ↔
    LT.lt.{u_1} (α := WithTop α) ⊤ ⊤ ∧ ⊤ < (↑a : WithTop α)
top₁ :
  ∀ (a_1 : α),
    Membership.mem (γ := Finset (WithTop α))
        (match (motive := WithTop α → WithTop α → Finset (WithTop α)) ⊤, (↑a : WithTop α) with
          | none, x => ∅
          | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
          | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b) :
          Finset (WithTop α))
        (↑a_1 : WithTop α) ↔
      ⊤ < (↑a_1 : WithTop α) ∧ (↑a_1 : WithTop α) < (↑a : WithTop α)
⊢ Membership.mem (γ := Finset (WithTop α))
      (match (motive := WithTop α → WithTop α → Finset (WithTop α)) ⊤, (↑a : WithTop α) with
        | none, x => ∅
        | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b) :
        Finset (WithTop α))
      x ↔
    ⊤ < x ∧ x < (↑a : WithTop α)

Tactic:
cases x
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
x : WithTop α
a : α
coe :
  Membership.mem (γ := Finset (WithTop α))
      (match (motive := WithTop α → WithTop α → Finset (WithTop α)) (↑a : WithTop α), ⊤ with
        | none, x => ∅
        | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b) :
        Finset (WithTop α))
      ⊤ ↔
    (↑a : WithTop α) < ⊤ ∧ LT.lt.{u_1} (α := WithTop α) ⊤ ⊤
coe₁ :
  ∀ (a_1 : α),
    Membership.mem (γ := Finset (WithTop α))
        (match (motive := WithTop α → WithTop α → Finset (WithTop α)) (↑a : WithTop α), ⊤ with
          | none, x => ∅
          | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
          | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b) :
          Finset (WithTop α))
        (↑a_1 : WithTop α) ↔
      (↑a : WithTop α) < (↑a_1 : WithTop α) ∧ (↑a_1 : WithTop α) < ⊤
⊢ Membership.mem (γ := Finset (WithTop α))
      (match (motive := WithTop α → WithTop α → Finset (WithTop α)) (↑a : WithTop α), ⊤ with
        | none, x => ∅
        | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b) :
        Finset (WithTop α))
      x ↔
    (↑a : WithTop α) < x ∧ x < ⊤

Tactic:
cases x
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
x : WithTop α
a a_1 : α
coe :
  Membership.mem (γ := Finset (WithTop α))
      (match (motive := WithTop α → WithTop α → Finset (WithTop α)) (↑a : WithTop α), (↑a_1 : WithTop α) with
        | none, x => ∅
        | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b) :
        Finset (WithTop α))
      ⊤ ↔
    (↑a : WithTop α) < ⊤ ∧ ⊤ < (↑a_1 : WithTop α)
coe₁ :
  ∀ (a_2 : α),
    Membership.mem (γ := Finset (WithTop α))
        (match (motive := WithTop α → WithTop α → Finset (WithTop α)) (↑a : WithTop α), (↑a_1 : WithTop α) with
          | none, x => ∅
          | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
          | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b) :
          Finset (WithTop α))
        (↑a_2 : WithTop α) ↔
      (↑a : WithTop α) < (↑a_2 : WithTop α) ∧ (↑a_2 : WithTop α) < (↑a_1 : WithTop α)
⊢ Membership.mem (γ := Finset (WithTop α))
      (match (motive := WithTop α → WithTop α → Finset (WithTop α)) (↑a : WithTop α), (↑a_1 : WithTop α) with
        | none, x => ∅
        | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b) :
        Finset (WithTop α))
      x ↔
    (↑a : WithTop α) < x ∧ x < (↑a_1 : WithTop α)

Tactic:
cases x
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
⊢ Membership.mem (γ := Finset (WithTop α))
      (match (motive := WithTop α → WithTop α → Finset (WithTop α)) ⊤, ⊤ with
        | none, x => ∅
        | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b) :
        Finset (WithTop α))
      ⊤ ↔
    LT.lt.{u_1} (α := WithTop α) ⊤ ⊤ ∧ LT.lt.{u_1} (α := WithTop α) ⊤ ⊤

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
a : α
⊢ Membership.mem (γ := Finset (WithTop α))
      (match (motive := WithTop α → WithTop α → Finset (WithTop α)) ⊤, ⊤ with
        | none, x => ∅
        | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b) :
        Finset (WithTop α))
      (↑a : WithTop α) ↔
    ⊤ < (↑a : WithTop α) ∧ (↑a : WithTop α) < ⊤

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
a : α
⊢ Membership.mem (γ := Finset (WithTop α))
      (match (motive := WithTop α → WithTop α → Finset (WithTop α)) ⊤, (↑a : WithTop α) with
        | none, x => ∅
        | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b) :
        Finset (WithTop α))
      ⊤ ↔
    LT.lt.{u_1} (α := WithTop α) ⊤ ⊤ ∧ ⊤ < (↑a : WithTop α)

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
a a_1 : α
⊢ Membership.mem (γ := Finset (WithTop α))
      (match (motive := WithTop α → WithTop α → Finset (WithTop α)) ⊤, (↑a : WithTop α) with
        | none, x => ∅
        | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b) :
        Finset (WithTop α))
      (↑a_1 : WithTop α) ↔
    ⊤ < (↑a_1 : WithTop α) ∧ (↑a_1 : WithTop α) < (↑a : WithTop α)

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
a : α
⊢ Membership.mem (γ := Finset (WithTop α))
      (match (motive := WithTop α → WithTop α → Finset (WithTop α)) (↑a : WithTop α), ⊤ with
        | none, x => ∅
        | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b) :
        Finset (WithTop α))
      ⊤ ↔
    (↑a : WithTop α) < ⊤ ∧ LT.lt.{u_1} (α := WithTop α) ⊤ ⊤

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
a a_1 : α
⊢ Membership.mem (γ := Finset (WithTop α))
      (match (motive := WithTop α → WithTop α → Finset (WithTop α)) (↑a : WithTop α), ⊤ with
        | none, x => ∅
        | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b) :
        Finset (WithTop α))
      (↑a_1 : WithTop α) ↔
    (↑a : WithTop α) < (↑a_1 : WithTop α) ∧ (↑a_1 : WithTop α) < ⊤

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
a a_1 : α
⊢ Membership.mem (γ := Finset (WithTop α))
      (match (motive := WithTop α → WithTop α → Finset (WithTop α)) (↑a : WithTop α), (↑a_1 : WithTop α) with
        | none, x => ∅
        | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b) :
        Finset (WithTop α))
      ⊤ ↔
    (↑a : WithTop α) < ⊤ ∧ ⊤ < (↑a_1 : WithTop α)

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
a a_1 a_2 : α
⊢ Membership.mem (γ := Finset (WithTop α))
      (match (motive := WithTop α → WithTop α → Finset (WithTop α)) (↑a : WithTop α), (↑a_1 : WithTop α) with
        | none, x => ∅
        | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b) :
        Finset (WithTop α))
      (↑a_2 : WithTop α) ↔
    (↑a : WithTop α) < (↑a_2 : WithTop α) ∧ (↑a_2 : WithTop α) < (↑a_1 : WithTop α)

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
a : α
⊢ Icc (↑a : WithTop α) ⊤ = (insertNone : (a : Finset α) → Finset (Option α)) (Ici a)

Tactic:
rfl

Premises used: Function.Embedding.some, Finset.Icc, WithTop.some, rfl, Function.Embedding.coeWithTop, WithTop
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
a b : α
⊢ Icc (↑a : WithTop α) (↑b : WithTop α) = Finset.map Embedding.some (Icc a b)

Tactic:
rfl

Premises used: Finset.map, Finset.Icc, WithTop.some, rfl, WithTop
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
a : α
⊢ Ico (↑a : WithTop α) ⊤ = Finset.map Embedding.some (Ici a)

Tactic:
rfl

Premises used: Finset.map, Finset.Ico, WithTop.some, rfl, WithTop
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
a b : α
⊢ Ico (↑a : WithTop α) (↑b : WithTop α) = Finset.map Embedding.some (Ico a b)

Tactic:
rfl

Premises used: Finset.map, Finset.Ico, WithTop.some, rfl, WithTop
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
a : α
⊢ Ioc (↑a : WithTop α) ⊤ = (insertNone : (a : Finset α) → Finset (Option α)) (Ioi a)

Tactic:
rfl

Premises used: Function.Embedding.some, WithTop.some, rfl, Function.Embedding.coeWithTop, Finset.Ioc, WithTop
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
a b : α
⊢ Ioc (↑a : WithTop α) (↑b : WithTop α) = Finset.map Embedding.some (Ioc a b)

Tactic:
rfl

Premises used: Finset.map, WithTop.some, rfl, Finset.Ioc, WithTop
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
a : α
⊢ Ioo (↑a : WithTop α) ⊤ = Finset.map Embedding.some (Ioi a)

Tactic:
rfl

Premises used: Finset.map, WithTop.some, Finset.Ioo, rfl, WithTop
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
a b : α
⊢ Ioo (↑a : WithTop α) (↑b : WithTop α) = Finset.map Embedding.some (Ioo a b)

Tactic:
rfl

Premises used: Finset.map, WithTop.some, Finset.Ioo, rfl, WithTop
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder β
f : α ≃o β
⊢ ∀ (a b x : α),
    x ∈
        map f.symm.toEquiv (r := fun (x1 x2 : β) ↦ x1 ≤ x2) (s := fun (x1 x2 : α) ↦ x1 ≤ x2).toEmbedding
          (Icc ((f : (a : α) → β) a) ((f : (a : α) → β) b)) ↔
      a ≤ x ∧ x ≤ b

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder β
f : α ≃o β
⊢ ∀ (a b x : α),
    x ∈
        map f.symm.toEquiv (r := fun (x1 x2 : β) ↦ x1 ≤ x2) (s := fun (x1 x2 : α) ↦ x1 ≤ x2).toEmbedding
          (Ico ((f : (a : α) → β) a) ((f : (a : α) → β) b)) ↔
      a ≤ x ∧ x < b

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder β
f : α ≃o β
⊢ ∀ (a b x : α),
    x ∈
        map f.symm.toEquiv (r := fun (x1 x2 : β) ↦ x1 ≤ x2) (s := fun (x1 x2 : α) ↦ x1 ≤ x2).toEmbedding
          (Ioc ((f : (a : α) → β) a) ((f : (a : α) → β) b)) ↔
      a < x ∧ x ≤ b

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder β
f : α ≃o β
⊢ ∀ (a b x : α),
    x ∈
        map f.symm.toEquiv (r := fun (x1 x2 : β) ↦ x1 ≤ x2) (s := fun (x1 x2 : α) ↦ x1 ≤ x2).toEmbedding
          (Ioo ((f : (a : α) → β) a) ((f : (a : α) → β) b)) ↔
      a < x ∧ x < b

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrderTop β
f : α ≃o β
⊢ ∀ (a x : α),
    x ∈
        map f.symm.toEquiv (r := fun (x1 x2 : β) ↦ x1 ≤ x2) (s := fun (x1 x2 : α) ↦ x1 ≤ x2).toEmbedding
          (Ici ((f : (a : α) → β) a)) ↔
      a ≤ x

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrderTop β
f : α ≃o β
⊢ ∀ (a x : α),
    x ∈
        map f.symm.toEquiv (r := fun (x1 x2 : β) ↦ x1 ≤ x2) (s := fun (x1 x2 : α) ↦ x1 ≤ x2).toEmbedding
          (Ioi ((f : (a : α) → β) a)) ↔
      a < x

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrder α
a b x : Subtype p
simp_rw : (↑x : α) ∈ Icc (↑a : α) (↑b : α) ↔ a ≤ x ∧ x ≤ b
simp_rw₁ : (↑a : α) ≤ (↑x : α) ∧ (↑x : α) ≤ (↑b : α) ↔ a ≤ x ∧ x ≤ b
⊢ x ∈ Finset.subtype p (Icc (↑a : α) (↑b : α)) ↔ a ≤ x ∧ x ≤ b

Tactic:
simp_rw [Finset.mem_subtype, mem_Icc, Subtype.coe_le_coe]

Premises used: Subtype.coe_le_coe, Finset.mem_Icc, Finset.mem_subtype
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrder α
a b x : Subtype p
simp_rw : (↑x : α) ∈ Ico (↑a : α) (↑b : α) ↔ a ≤ x ∧ x < b
simp_rw₁ : (↑a : α) ≤ (↑x : α) ∧ (↑x : α) < (↑b : α) ↔ a ≤ x ∧ x < b
simp_rw₂ : a ≤ x ∧ (↑x : α) < (↑b : α) ↔ a ≤ x ∧ x < b
⊢ x ∈ Finset.subtype p (Ico (↑a : α) (↑b : α)) ↔ a ≤ x ∧ x < b

Tactic:
simp_rw [Finset.mem_subtype, mem_Ico, Subtype.coe_le_coe, Subtype.coe_lt_coe]

Premises used: Subtype.coe_lt_coe, Subtype.coe_le_coe, Finset.mem_subtype, Finset.mem_Ico
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrder α
a b x : Subtype p
simp_rw : (↑x : α) ∈ Ioc (↑a : α) (↑b : α) ↔ a < x ∧ x ≤ b
simp_rw₁ : (↑a : α) < (↑x : α) ∧ (↑x : α) ≤ (↑b : α) ↔ a < x ∧ x ≤ b
simp_rw₂ : (↑a : α) < (↑x : α) ∧ x ≤ b ↔ a < x ∧ x ≤ b
⊢ x ∈ Finset.subtype p (Ioc (↑a : α) (↑b : α)) ↔ a < x ∧ x ≤ b

Tactic:
simp_rw [Finset.mem_subtype, mem_Ioc, Subtype.coe_le_coe, Subtype.coe_lt_coe]

Premises used: Subtype.coe_lt_coe, Subtype.coe_le_coe, Finset.mem_subtype, Finset.mem_Ioc
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrder α
a b x : Subtype p
simp_rw : (↑x : α) ∈ Ioo (↑a : α) (↑b : α) ↔ a < x ∧ x < b
simp_rw₁ : (↑a : α) < (↑x : α) ∧ (↑x : α) < (↑b : α) ↔ a < x ∧ x < b
⊢ x ∈ Finset.subtype p (Ioo (↑a : α) (↑b : α)) ↔ a < x ∧ x < b

Tactic:
simp_rw [Finset.mem_subtype, mem_Ioo, Subtype.coe_lt_coe]

Premises used: Subtype.coe_lt_coe, Finset.mem_Ioo, Finset.mem_subtype
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrderTop α
a x : Subtype p
simp_rw : (↑x : α) ∈ Ici (↑a : α) ↔ a ≤ x
simp_rw₁ : (↑a : α) ≤ (↑x : α) ↔ a ≤ x
⊢ x ∈ Finset.subtype p (Ici (↑a : α)) ↔ a ≤ x

Tactic:
simp_rw [Finset.mem_subtype, mem_Ici, Subtype.coe_le_coe]

Premises used: Finset.mem_Ici, Subtype.coe_le_coe, Finset.mem_subtype
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrderTop α
a x : Subtype p
simp_rw : (↑x : α) ∈ Ioi (↑a : α) ↔ a < x
simp_rw₁ : (↑a : α) < (↑x : α) ↔ a < x
⊢ x ∈ Finset.subtype p (Ioi (↑a : α)) ↔ a < x

Tactic:
simp_rw [Finset.mem_subtype, mem_Ioi, Subtype.coe_lt_coe]

Premises used: Subtype.coe_lt_coe, Finset.mem_Ioi, Finset.mem_subtype
-- 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
⊢ Icc a b = Finset.subtype p (Icc (↑a : α) (↑b : α))

Tactic:
rfl

Premises used: Finset.map, Finset.Icc, Finset.subtype, rfl
-- 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
⊢ Ico a b = Finset.subtype p (Ico (↑a : α) (↑b : α))

Tactic:
rfl

Premises used: Finset.map, Finset.Ico, Finset.subtype, rfl
-- 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
⊢ Ioo a b = Finset.subtype p (Ioo (↑a : α) (↑b : α))

Tactic:
rfl

Premises used: Finset.map, Finset.subtype, Finset.Ioo, rfl
-- 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 (Icc (↑a : α) (↑b : α))) = Icc (↑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 ∈ Icc (↑a : α) (↑b : α)), p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Icc (↑a : α) (↑b : α))) = Icc (↑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 ∈ Icc (↑a : α) (↑b : α)
⊢ (↑a : α) ≤ x ∧ x ≤ (↑b : α)

Tactic:
rw [mem_Icc] at hx

Premises used: Finset.mem_Icc
-- 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 hx.2 a.prop b.prop

Premises used: 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 hx.2 a.prop b.prop

Premises used: 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 (Ico (↑a : α) (↑b : α))) = Ico (↑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 ∈ Ico (↑a : α) (↑b : α)), p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ico (↑a : α) (↑b : α))) = Ico (↑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 ∈ Ico (↑a : α) (↑b : α)
⊢ (↑a : α) ≤ x ∧ x < (↑b : α)

Tactic:
rw [mem_Ico] at hx

Premises used: Finset.mem_Ico
-- 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 hx.2.le a.prop b.prop

Premises used: LT.lt.le, And.right, And.left, Subtype.prop