Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a b x : WithTop α
⊢ (x ∈
      match a, b 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)) ↔
    a ≤ x ∧ x < b

Tactic:
cases a <;> cases b <;> cases x

Goal state after:
case top.top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
⊢ (⊤ ∈
      match ⊤, ⊤ 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)) ↔
    ⊤ ≤ ⊤ ∧ ⊤ < ⊤

case top.top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ : α
⊢ (↑a✝ ∈
      match ⊤, ⊤ 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)) ↔
    ⊤ ≤ ↑a✝ ∧ ↑a✝ < ⊤

case top.coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ : α
⊢ (⊤ ∈
      match ⊤, ↑a✝ 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)) ↔
    ⊤ ≤ ⊤ ∧ ⊤ < ↑a✝

case top.coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝¹ a✝ : α
⊢ (↑a✝ ∈
      match ⊤, ↑a✝¹ 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)) ↔
    ⊤ ≤ ↑a✝ ∧ ↑a✝ < ↑a✝¹

case coe.top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ : α
⊢ (⊤ ∈
      match ↑a✝, ⊤ 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)) ↔
    ↑a✝ ≤ ⊤ ∧ ⊤ < ⊤

case coe.top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝¹ a✝ : α
⊢ (↑a✝ ∈
      match ↑a✝¹, ⊤ 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)) ↔
    ↑a✝¹ ≤ ↑a✝ ∧ ↑a✝ < ⊤

case coe.coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝¹ a✝ : α
⊢ (⊤ ∈
      match ↑a✝¹, ↑a✝ 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)) ↔
    ↑a✝¹ ≤ ⊤ ∧ ⊤ < ↑a✝

case coe.coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝² a✝¹ a✝ : α
⊢ (↑a✝ ∈
      match ↑a✝², ↑a✝¹ 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)) ↔
    ↑a✝² ≤ ↑a✝ ∧ ↑a✝ < ↑a✝¹