awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
x : 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 ≤ ⊤
have 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 α) ⊤ ⊤
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
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 α) ⊤ ⊤
⊢ 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 ≤ ⊤
have 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 α) ≤ ⊤
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
x : WithTop α
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 α)
have 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 α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
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 α)
⊢ 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 α)
have 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 α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
x : WithTop α
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 ↔
    (↑a : WithTop α) < x ∧ x ≤ ⊤
have 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 α) ⊤ ⊤
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
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 α) ⊤ ⊤
⊢ 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 ≤ ⊤
have 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 α) ≤ ⊤
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
x : WithTop α
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 α))
      x ↔
    (↑a : WithTop α) < x ∧ x ≤ (↑a_1 : WithTop α)
have 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 α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
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 α)
⊢ 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 α)
have 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 α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
a b x : WithTop α
⊢ 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
have 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
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
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
⊢ 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
have 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
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
b x : 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
have 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 < ⊤
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
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 < ⊤
⊢ 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
have 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 α)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
b x : WithTop α
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
have 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 < ⊤
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
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 < ⊤
⊢ 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
have 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 α)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
x : 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 < ⊤
have 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 α) ⊤ ⊤
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
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 α) ⊤ ⊤
⊢ 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 < ⊤
have 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 α) < ⊤
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
x : WithTop α
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 α)
have 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 α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
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 α)
⊢ 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 α)
have 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 α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : LocallyFiniteOrder α
x : WithTop α
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 ↔
    (↑a : WithTop α) < x ∧ x < ⊤
have 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 α) ⊤ ⊤
Tactic: cases x
Cleared hypotheses: x