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 α
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 (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico 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 (Ici a)
          | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico 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 (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico 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 (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b) :
        Finset (WithTop α))
      ⊤ ↔
    LE.le.{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 (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico 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 (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b) :
        Finset (WithTop α))
      ⊤ ↔
    LE.le.{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 (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico 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 (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico 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 (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico 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 (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico 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 (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico 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
β : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
a b x : WithTop α
top :
  Membership.mem (γ := Finset (WithTop α))
      (match (motive := WithTop α → WithTop α → Finset (WithTop α)) ⊤, b with
        | none, x => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ioi a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b) :
        Finset (WithTop α))
      x ↔
    ⊤ < x ∧ x ≤ b
coe :
  ∀ (a : α),
    Membership.mem (γ := Finset (WithTop α))
        (match (motive := WithTop α → WithTop α → Finset (WithTop α)) (↑a : WithTop α), b with
          | none, x => ∅
          | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ioi a)
          | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b) :
          Finset (WithTop α))
        x ↔
      (↑a : WithTop α) < x ∧ x ≤ b
⊢ Membership.mem (γ := Finset (WithTop α))
      (match (motive := WithTop α → WithTop α → Finset (WithTop α)) a, b with
        | none, x => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ioi a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b) :
        Finset (WithTop α))
      x ↔
    a < x ∧ x ≤ b

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

Tactic:
cases a
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
b 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 α))
      x ↔
    ⊤ < x ∧ x < ⊤
top₁ :
  ∀ (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 α))
        x ↔
      ⊤ < x ∧ x < (↑a : WithTop α)
⊢ Membership.mem (γ := Finset (WithTop α))
      (match (motive := WithTop α → WithTop α → Finset (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 ↔
    ⊤ < x ∧ x < b

Tactic:
cases b