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 : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrderTop α
inst_3 : LocallyFiniteOrderTop β
inst_4 : DecidableLE (α × β)
a x : α × β
rw : x.1 ∈ Ici a.1 ∧ x.2 ∈ Ici a.2 ↔ a ≤ x
rw₁ : a.1 ≤ x.1 ∧ x.2 ∈ Ici a.2 ↔ a ≤ x
⊢ Membership.mem (γ := Finset (α × β)) ((fun (x : α × β) ↦ Ici x.1 ×ˢ Ici x.2) a) x ↔ a ≤ x
have rw₂ : a.1 ≤ x.1 ∧ a.2 ≤ x.2 ↔ a ≤ x
Tactic: rw [mem_product, mem_Ici, mem_Ici, le_def]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrderTop α
inst_3 : LocallyFiniteOrderTop β
inst_4 : DecidableLE (α × β)
a x : α × β
rw : x.1 ∈ Ici a.1 ∧ x.2 ∈ Ici a.2 ↔ a ≤ x
rw₁ : a.1 ≤ x.1 ∧ x.2 ∈ Ici a.2 ↔ a ≤ x
rw₂ : a.1 ≤ x.1 ∧ a.2 ≤ x.2 ↔ a ≤ x
⊢ Membership.mem (γ := Finset (α × β)) ((fun (x : α × β) ↦ Ici x.1 ×ˢ Ici x.2) a) x ↔ a ≤ x
have rw₃ : a.1 ≤ x.1 ∧ a.2 ≤ x.2 ↔ a.1 ≤ x.1 ∧ a.2 ≤ x.2
Tactic: rw [mem_product, mem_Ici, mem_Ici, le_def]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Finset α
⊢ LE.le.{u_1} (α := Finset (WithTop α)) ((fun (s : Finset α) ↦ cons ⊤ (Finset.map Embedding.coeWithTop s) ⋯) s)
      ((fun (s : Finset α) ↦ cons ⊤ (Finset.map Embedding.coeWithTop s) ⋯) t) ↔
    s ≤ t
have rw : Subset.{u_1} (α := Finset (WithTop α)) ((fun (s : Finset α) ↦ cons ⊤ (Finset.map Embedding.coeWithTop s) sorry) s)
    ((fun (s : Finset α) ↦ cons ⊤ (Finset.map Embedding.coeWithTop s) sorry) t) ↔
  s ≤ t
Tactic: rw [le_iff_subset, cons_subset_cons, map_subset_map, le_iff_subset]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Finset α
rw :
  Subset.{u_1} (α := Finset (WithTop α)) ((fun (s : Finset α) ↦ cons ⊤ (Finset.map Embedding.coeWithTop s) ⋯) s)
      ((fun (s : Finset α) ↦ cons ⊤ (Finset.map Embedding.coeWithTop s) ⋯) t) ↔
    s ≤ t
⊢ LE.le.{u_1} (α := Finset (WithTop α)) ((fun (s : Finset α) ↦ cons ⊤ (Finset.map Embedding.coeWithTop s) ⋯) s)
      ((fun (s : Finset α) ↦ cons ⊤ (Finset.map Embedding.coeWithTop s) ⋯) t) ↔
    s ≤ t
have rw₁ : Finset.map Embedding.coeWithTop s ⊆ Finset.map Embedding.coeWithTop t ↔ s ≤ t
Tactic: rw [le_iff_subset, cons_subset_cons, map_subset_map, le_iff_subset]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Finset α
rw :
  Subset.{u_1} (α := Finset (WithTop α)) ((fun (s : Finset α) ↦ cons ⊤ (Finset.map Embedding.coeWithTop s) ⋯) s)
      ((fun (s : Finset α) ↦ cons ⊤ (Finset.map Embedding.coeWithTop s) ⋯) t) ↔
    s ≤ t
rw₁ : Finset.map Embedding.coeWithTop s ⊆ Finset.map Embedding.coeWithTop t ↔ s ≤ t
⊢ LE.le.{u_1} (α := Finset (WithTop α)) ((fun (s : Finset α) ↦ cons ⊤ (Finset.map Embedding.coeWithTop s) ⋯) s)
      ((fun (s : Finset α) ↦ cons ⊤ (Finset.map Embedding.coeWithTop s) ⋯) t) ↔
    s ≤ t
have rw₂ : s ⊆ t ↔ s ≤ t
Tactic: rw [le_iff_subset, cons_subset_cons, map_subset_map, le_iff_subset]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Finset α
rw :
  Subset.{u_1} (α := Finset (WithTop α)) ((fun (s : Finset α) ↦ cons ⊤ (Finset.map Embedding.coeWithTop s) ⋯) s)
      ((fun (s : Finset α) ↦ cons ⊤ (Finset.map Embedding.coeWithTop s) ⋯) t) ↔
    s ≤ t
rw₁ : Finset.map Embedding.coeWithTop s ⊆ Finset.map Embedding.coeWithTop t ↔ s ≤ t
rw₂ : s ⊆ t ↔ s ≤ t
⊢ LE.le.{u_1} (α := Finset (WithTop α)) ((fun (s : Finset α) ↦ cons ⊤ (Finset.map Embedding.coeWithTop s) ⋯) s)
      ((fun (s : Finset α) ↦ cons ⊤ (Finset.map Embedding.coeWithTop s) ⋯) t) ↔
    s ≤ t
have rw₃ : s ⊆ t ↔ s ⊆ t
Tactic: rw [le_iff_subset, cons_subset_cons, map_subset_map, le_iff_subset]
-- 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, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b) :
        Finset (WithTop α))
      x ↔
    a ≤ x ∧ x ≤ b
have top : Membership.mem (γ := Finset (WithTop α))
    (match (motive := WithTop α → WithTop α → Finset (WithTop α)) ⊤, b with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc 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, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b) :
        Finset (WithTop α))
      x ↔
    ⊤ ≤ x ∧ x ≤ b
⊢ Membership.mem (γ := Finset (WithTop α))
      (match (motive := WithTop α → WithTop α → Finset (WithTop α)) a, b with
        | none, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc 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, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc 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, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b) :
        Finset (WithTop α))
      x ↔
    ⊤ ≤ x ∧ x ≤ b
have top : Membership.mem (γ := Finset (WithTop α))
    (match (motive := WithTop α → WithTop α → Finset (WithTop α)) ⊤, ⊤ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc 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, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b) :
        Finset (WithTop α))
      x ↔
    ⊤ ≤ x ∧ x ≤ ⊤
⊢ Membership.mem (γ := Finset (WithTop α))
      (match (motive := WithTop α → WithTop α → Finset (WithTop α)) ⊤, b with
        | none, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc 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, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc 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, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc 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, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc 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, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b) :
        Finset (WithTop α))
      x ↔
    (↑a : WithTop α) ≤ x ∧ x ≤ ⊤
⊢ Membership.mem (γ := Finset (WithTop α))
      (match (motive := WithTop α → WithTop α → Finset (WithTop α)) (↑a : WithTop α), b with
        | none, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc 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, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc 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, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b) :
        Finset (WithTop α))
      x ↔
    ⊤ ≤ x ∧ x ≤ ⊤
have top : Membership.mem (γ := Finset (WithTop α))
    (match (motive := WithTop α → WithTop α → Finset (WithTop α)) ⊤, ⊤ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b) :
      Finset (WithTop α))
    ⊤ ↔
  LE.le.{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, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b) :
        Finset (WithTop α))
      ⊤ ↔
    LE.le.{u_1} (α := WithTop α) ⊤ ⊤ ∧ LE.le.{u_1} (α := WithTop α) ⊤ ⊤
⊢ Membership.mem (γ := Finset (WithTop α))
      (match (motive := WithTop α → WithTop α → Finset (WithTop α)) ⊤, ⊤ with
        | none, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b) :
        Finset (WithTop α))
      x ↔
    ⊤ ≤ x ∧ x ≤ ⊤
have top₁ : ∀ (a : α),
  Membership.mem (γ := Finset (WithTop α))
      (match (motive := WithTop α → WithTop α → Finset (WithTop α)) ⊤, ⊤ with
        | none, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc 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, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc 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, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b) :
      Finset (WithTop α))
    ⊤ ↔
  LE.le.{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, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b) :
        Finset (WithTop α))
      ⊤ ↔
    LE.le.{u_1} (α := WithTop α) ⊤ ⊤ ∧ ⊤ ≤ (↑a : WithTop α)
⊢ Membership.mem (γ := Finset (WithTop α))
      (match (motive := WithTop α → WithTop α → Finset (WithTop α)) ⊤, (↑a : WithTop α) with
        | none, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc 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, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc 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, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc 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, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc 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, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc 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, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc 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, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc 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, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc 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, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc 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, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc 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, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc 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, none => {⊤}
        | none, Option.some b => ∅
        | Option.some a, none => (insertTop : (a : Finset α) → Finset (WithTop α)) (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc 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 (Ici a)
        | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico 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 (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b) :
      Finset (WithTop α))
    x ↔
  ⊤ ≤ x ∧ x < b
Tactic: cases a
Cleared hypotheses: a