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 α
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 α) ⊤ ⊤
⊢ 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₁ : ∀ (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: 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 => 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 α)
have 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 α)
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 => 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 α)
⊢ 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 α)
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 => 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: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrder α
a b x : Subtype p
⊢ x ∈ Finset.subtype p (Icc (↑a : α) (↑b : α)) ↔ a ≤ x ∧ x ≤ b
have simp_rw : (↑x : α) ∈ Icc (↑a : α) (↑b : α) ↔ a ≤ x ∧ x ≤ b
Tactic: simp_rw [Finset.mem_subtype, mem_Icc, Subtype.coe_le_coe]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
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
⊢ x ∈ Finset.subtype p (Icc (↑a : α) (↑b : α)) ↔ a ≤ x ∧ x ≤ b
have simp_rw₁ : (↑a : α) ≤ (↑x : α) ∧ (↑x : α) ≤ (↑b : α) ↔ a ≤ x ∧ x ≤ b
Tactic: simp_rw [Finset.mem_subtype, mem_Icc, Subtype.coe_le_coe]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrder α
a b x : Subtype p
⊢ x ∈ Finset.subtype p (Ico (↑a : α) (↑b : α)) ↔ a ≤ x ∧ x < b
have simp_rw : (↑x : α) ∈ Ico (↑a : α) (↑b : α) ↔ a ≤ x ∧ x < b
Tactic: simp_rw [Finset.mem_subtype, mem_Ico, Subtype.coe_le_coe, Subtype.coe_lt_coe]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
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
⊢ x ∈ Finset.subtype p (Ico (↑a : α) (↑b : α)) ↔ a ≤ x ∧ x < b
have simp_rw₁ : (↑a : α) ≤ (↑x : α) ∧ (↑x : α) < (↑b : α) ↔ a ≤ x ∧ x < b
Tactic: simp_rw [Finset.mem_subtype, mem_Ico, Subtype.coe_le_coe, Subtype.coe_lt_coe]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
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
⊢ x ∈ Finset.subtype p (Ico (↑a : α) (↑b : α)) ↔ a ≤ x ∧ x < b
have simp_rw₂ : a ≤ x ∧ (↑x : α) < (↑b : α) ↔ a ≤ x ∧ x < b
Tactic: simp_rw [Finset.mem_subtype, mem_Ico, Subtype.coe_le_coe, Subtype.coe_lt_coe]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrder α
a b x : Subtype p
⊢ x ∈ Finset.subtype p (Ioc (↑a : α) (↑b : α)) ↔ a < x ∧ x ≤ b
have simp_rw : (↑x : α) ∈ Ioc (↑a : α) (↑b : α) ↔ a < x ∧ x ≤ b
Tactic: simp_rw [Finset.mem_subtype, mem_Ioc, Subtype.coe_le_coe, Subtype.coe_lt_coe]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
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
⊢ x ∈ Finset.subtype p (Ioc (↑a : α) (↑b : α)) ↔ a < x ∧ x ≤ b
have simp_rw₁ : (↑a : α) < (↑x : α) ∧ (↑x : α) ≤ (↑b : α) ↔ a < x ∧ x ≤ b
Tactic: simp_rw [Finset.mem_subtype, mem_Ioc, Subtype.coe_le_coe, Subtype.coe_lt_coe]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
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
⊢ x ∈ Finset.subtype p (Ioc (↑a : α) (↑b : α)) ↔ a < x ∧ x ≤ b
have simp_rw₂ : (↑a : α) < (↑x : α) ∧ x ≤ b ↔ a < x ∧ x ≤ b
Tactic: simp_rw [Finset.mem_subtype, mem_Ioc, Subtype.coe_le_coe, Subtype.coe_lt_coe]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrder α
a b x : Subtype p
⊢ x ∈ Finset.subtype p (Ioo (↑a : α) (↑b : α)) ↔ a < x ∧ x < b
have simp_rw : (↑x : α) ∈ Ioo (↑a : α) (↑b : α) ↔ a < x ∧ x < b
Tactic: simp_rw [Finset.mem_subtype, mem_Ioo, Subtype.coe_lt_coe]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
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
⊢ x ∈ Finset.subtype p (Ioo (↑a : α) (↑b : α)) ↔ a < x ∧ x < b
have simp_rw₁ : (↑a : α) < (↑x : α) ∧ (↑x : α) < (↑b : α) ↔ a < x ∧ x < b
Tactic: simp_rw [Finset.mem_subtype, mem_Ioo, Subtype.coe_lt_coe]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrderTop α
a x : Subtype p
⊢ x ∈ Finset.subtype p (Ici (↑a : α)) ↔ a ≤ x
have simp_rw : (↑x : α) ∈ Ici (↑a : α) ↔ a ≤ x
Tactic: simp_rw [Finset.mem_subtype, mem_Ici, Subtype.coe_le_coe]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
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
⊢ x ∈ Finset.subtype p (Ici (↑a : α)) ↔ a ≤ x
have simp_rw₁ : (↑a : α) ≤ (↑x : α) ↔ a ≤ x
Tactic: simp_rw [Finset.mem_subtype, mem_Ici, Subtype.coe_le_coe]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : LocallyFiniteOrderTop α
a x : Subtype p
⊢ x ∈ Finset.subtype p (Ioi (↑a : α)) ↔ a < x
have simp_rw : (↑x : α) ∈ Ioi (↑a : α) ↔ a < x
Tactic: simp_rw [Finset.mem_subtype, mem_Ioi, Subtype.coe_lt_coe]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
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
⊢ x ∈ Finset.subtype p (Ioi (↑a : α)) ↔ a < x
have simp_rw₁ : (↑a : α) < (↑x : α) ↔ a < x
Tactic: simp_rw [Finset.mem_subtype, mem_Ioi, Subtype.coe_lt_coe]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
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 : α)
have refine : ∀ (x : α) (hx : x ∈ Icc (↑a : α) (↑b : α)), p x
Tactic: refine Finset.subtype_map_of_mem fun x hx => ?_
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (hypothesis)
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 : α)
⊢ p x
have hx₁ : (↑a : α) ≤ x ∧ x ≤ (↑b : α)
Tactic: rw [mem_Icc] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
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 : α)
have refine : ∀ (x : α) (hx : x ∈ Ico (↑a : α) (↑b : α)), p x
Tactic: refine Finset.subtype_map_of_mem fun x hx => ?_
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (hypothesis)
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 : α)
⊢ p x
have hx₁ : (↑a : α) ≤ x ∧ x < (↑b : α)
Tactic: rw [mem_Ico] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
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 (Ioc (↑a : α) (↑b : α))) = Ioc (↑a : α) (↑b : α)
have refine : ∀ (x : α) (hx : x ∈ Ioc (↑a : α) (↑b : α)), p x
Tactic: refine Finset.subtype_map_of_mem fun x hx => ?_
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (hypothesis)
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 ∈ Ioc (↑a : α) (↑b : α)
⊢ p x
have hx₁ : (↑a : α) < x ∧ x ≤ (↑b : α)
Tactic: rw [mem_Ioc] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
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 (Ioo (↑a : α) (↑b : α))) = Ioo (↑a : α) (↑b : α)
have refine : ∀ (x : α) (hx : x ∈ Ioo (↑a : α) (↑b : α)), p x
Tactic: refine Finset.subtype_map_of_mem fun x hx => ?_
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (hypothesis)
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 ∈ Ioo (↑a : α) (↑b : α)
⊢ p x
have hx₁ : (↑a : α) < x ∧ x < (↑b : α)
Tactic: rw [mem_Ioo] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_3
s : Set α
inst : Nonempty α
inst_1 : Lattice α
inst_2 : LocallyFiniteOrder α
⊢ s.Finite ↔ BddBelow s ∧ BddAbove s
have inl : Set.Finite.{u_3} (α := α) ∅ ↔ BddBelow.{u_3} (α := α) ∅ ∧ BddAbove.{u_3} (α := α) ∅
Tactic: obtain (rfl | hs) := s.eq_empty_or_nonempty
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_3
s : Set α
inst : Nonempty α
inst_1 : Lattice α
inst_2 : LocallyFiniteOrder α
inl : Set.Finite.{u_3} (α := α) ∅ ↔ BddBelow.{u_3} (α := α) ∅ ∧ BddAbove.{u_3} (α := α) ∅
⊢ s.Finite ↔ BddBelow s ∧ BddAbove s
have inr : ∀ (hs : s.Nonempty), s.Finite ↔ BddBelow s ∧ BddAbove s
Tactic: obtain (rfl | hs) := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
y : α
inst_2 : DecidableLE α
inst_3 : LocallyFiniteOrder α
a b : { x : α // x ≤ y }
⊢ b ∈ Icc a (Subtype.mk (p := fun (x : α) ↦ x ≤ y) y ⋯) ↔ a ≤ b
have simp : a ≤ b → b ≤ Subtype.mk (p := fun (x : α) ↦ x ≤ y) y sorry
Tactic: simp only [Finset.mem_Icc, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
y : α
inst_2 : DecidableLE α
inst_3 : LocallyFiniteOrder α
a b : { x : α // x ≤ y }
⊢ b ∈ Ioc a (Subtype.mk (p := fun (x : α) ↦ x ≤ y) y ⋯) ↔ a < b
have simp : a < b → b ≤ Subtype.mk (p := fun (x : α) ↦ x ≤ y) y sorry
Tactic: simp only [Finset.mem_Ioc, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
y : α
inst_2 : DecidableLT α
inst_3 : LocallyFiniteOrder α
a b : { x : α // x < y }
⊢ Membership.mem (γ := Finset { x : α // x < y }) (Finset.subtype (fun (x : α) ↦ x < y) (Ico (↑a : α) y)) b ↔ a ≤ b
have simp : a ≤ b → (↑b : α) < y
Tactic: simp only [Finset.mem_subtype, Finset.mem_Ico, Subtype.coe_le_coe, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → Prop
inst_1 : DecidablePred p
y : α
inst_2 : DecidableLT α
inst_3 : LocallyFiniteOrder α
a b : { x : α // x < y }
⊢ Membership.mem (γ := Finset { x : α // x < y }) (Finset.subtype (fun (x : α) ↦ x < y) (Ioo (↑a : α) y)) b ↔ a < b
have simp : a < b → (↑b : α) < y
Tactic: simp only [Finset.mem_subtype, Finset.mem_Ioo, Subtype.coe_lt_coe, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : Fintype (↑(Icc a b) : Type u_3)
⊢ (Icc a b).toFinset = Finset.Icc a b
have h : ∀ (a_1 : α), a_1 ∈ (Icc a b).toFinset ↔ a_1 ∈ Finset.Icc a b
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : Fintype (↑(Ico a b) : Type u_3)
⊢ (Ico a b).toFinset = Finset.Ico a b
have h : ∀ (a_1 : α), a_1 ∈ (Ico a b).toFinset ↔ a_1 ∈ Finset.Ico a b
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : Fintype (↑(Ioo a b) : Type u_3)
⊢ (Ioo a b).toFinset = Finset.Ioo a b
have h : ∀ (a_1 : α), a_1 ∈ (Ioo a b).toFinset ↔ a_1 ∈ Finset.Ioo a b
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a : α
inst_2 : Fintype (↑(Ici a) : Type u_3)
⊢ (Ici a).toFinset = Finset.Ici a
have h : ∀ (a_1 : α), a_1 ∈ (Ici a).toFinset ↔ a_1 ∈ Finset.Ici a
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a : α
inst_2 : Fintype (↑(Ioi a) : Type u_3)
⊢ (Ioi a).toFinset = Finset.Ioi a
have h : ∀ (a_1 : α), a_1 ∈ (Ioi a).toFinset ↔ a_1 ∈ Finset.Ioi a
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
⊢ DenselyOrdered X ↔ Subsingleton X
have refine : ∀ (H : DenselyOrdered X), Subsingleton X
Tactic: refine ⟨fun H ↦ ?_, fun h ↦ h.instDenselyOrdered⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
H : DenselyOrdered X
⊢ Subsingleton X
have rw : ¬∃ (x : X) (y : X), x < y
Tactic: rw [← not_nontrivial_iff_subsingleton, nontrivial_iff_lt]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
⊢ DenselyOrdered.{u_1} (↑s : Type u_1) ↔ s.Subsingleton
have refine : ∀ (H : DenselyOrdered.{u_1} (↑s : Type u_1)), s.Subsingleton
Tactic: refine ⟨fun H ↦ ?_, fun h ↦ h.denselyOrdered⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered.{u_1} (↑s : Type u_1)
⊢ s.Subsingleton
have rw : ¬∃ (x : (↑s : Type u_1)) (y : (↑s : Type u_1)), x < y
Tactic: rw [← Set.subsingleton_coe, ← not_nontrivial_iff_subsingleton, nontrivial_iff_lt]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H_1 : DenselyOrdered.{u_1} (↑s : Type u_1)
this : DenselyOrdered.{u_1} (↑(some ⁻¹' s) : Type u_1)
x y : (↑s : Type u_1)
H : x < y
⊢ False
have rw : ∀ (this : (some ⁻¹' s).Subsingleton) (x y : (↑s : Type u_1)) (H : x < y), False
Tactic: rw [_root_.denselyOrdered_set_iff_subsingleton] at this
Cleared hypotheses: this, x, y, H
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H_1 : DenselyOrdered.{u_1} (↑s : Type u_1)
this : (some ⁻¹' s).Subsingleton
x y : (↑s : Type u_1)
H : x < y
⊢ False
have obtain : ∀ (z : (↑s : Type u_1)) (hz : x < z) (hz' : z < y), False
Tactic: obtain ⟨z, hz, hz'⟩ := exists_between H
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (hypothesis)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H_1 : DenselyOrdered.{u_1} (↑s : Type u_1)
this : (some ⁻¹' s).Subsingleton
x y : (↑s : Type u_1)
H : x < y
z : (↑s : Type u_1)
hz : x < z
hz' : z < y
⊢ False
have hz0 : ⊥ < (↑z : WithBot X)
Tactic: have hz0 : (⊥ : WithBot X) < z := by simp [(Subtype.coe_lt_coe.mpr hz).trans_le']
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H_1 : DenselyOrdered.{u_1} (↑s : Type u_1)
this : (some ⁻¹' s).Subsingleton
x y : (↑s : Type u_1)
H : x < y
z : (↑s : Type u_1)
hz : x < z
hz' : z < y
hz0 : ⊥ < (↑z : WithBot X)
⊢ (↑z : WithBot X).unbot ⋯ < (↑y : WithBot X).unbot ⋯
have rwa : (↑((↑z : WithBot X).unbot sorry) : WithBot X) < (↑((↑y : WithBot X).unbot sorry) : WithBot X)
Tactic: rwa [← WithBot.coe_lt_coe, WithBot.coe_unbot, WithBot.coe_unbot]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H_1 : DenselyOrdered.{u_1} (↑s : Type u_1)
this : (some ⁻¹' s).Subsingleton
x y : (↑s : Type u_1)
H : x < y
z : (↑s : Type u_1)
hz : x < z
hz' : z < y
hz0 : ⊥ < (↑z : WithBot X)
rwa : (↑((↑z : WithBot X).unbot ⋯) : WithBot X) < (↑((↑y : WithBot X).unbot ⋯) : WithBot X)
⊢ (↑z : WithBot X).unbot ⋯ < (↑y : WithBot X).unbot ⋯
have rwa₁ : (↑z : WithBot X) < (↑((↑y : WithBot X).unbot sorry) : WithBot X)
Tactic: rwa [← WithBot.coe_lt_coe, WithBot.coe_unbot, WithBot.coe_unbot]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H_1 : DenselyOrdered.{u_1} (↑s : Type u_1)
this : (some ⁻¹' s).Subsingleton
x y : (↑s : Type u_1)
H : x < y
z : (↑s : Type u_1)
hz : x < z
hz' : z < y
hz0 : ⊥ < (↑z : WithBot X)
rwa : (↑((↑z : WithBot X).unbot ⋯) : WithBot X) < (↑((↑y : WithBot X).unbot ⋯) : WithBot X)
rwa₁ : (↑z : WithBot X) < (↑((↑y : WithBot X).unbot ⋯) : WithBot X)
⊢ (↑z : WithBot X).unbot ⋯ < (↑y : WithBot X).unbot ⋯
have rwa₂ : (↑z : WithBot X) < (↑y : WithBot X)
Tactic: rwa [← WithBot.coe_lt_coe, WithBot.coe_unbot, WithBot.coe_unbot]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (hypothesis)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H_1 : DenselyOrdered.{u_1} (↑s : Type u_1)
this : (some ⁻¹' s).Subsingleton
x y : (↑s : Type u_1)
H : x < y
z : (↑s : Type u_1)
hz : x < z
hz' : z < y
hz0 : ⊥ < (↑z : WithBot X)
⊢ False
have hz'₁ : (↑z : WithBot X).unbot sorry < (↑y : WithBot X).unbot sorry
Tactic: replace hz' : WithBot.unbot z.val hz0.ne' < WithBot.unbot y (hz0.trans hz').ne' := by
      rwa [← WithBot.coe_lt_coe, WithBot.coe_unbot, WithBot.coe_unbot]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H_1 : DenselyOrdered.{u_1} (↑s : Type u_1)
this : (some ⁻¹' s).Subsingleton
x y : (↑s : Type u_1)
H : x < y
z : (↑s : Type u_1)
hz : x < z
hz'_1 : z < y
hz0 : ⊥ < (↑z : WithBot X)
hz' : (↑z : WithBot X).unbot ⋯ < (↑y : WithBot X).unbot ⋯
⊢ False
have refine_1 : (↑z : WithBot X).unbot sorry ∈ some ⁻¹' s
Tactic: refine absurd (this ?_ ?_) hz'.ne
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H_1 : DenselyOrdered.{u_1} (↑s : Type u_1)
this : (some ⁻¹' s).Subsingleton
x y : (↑s : Type u_1)
H : x < y
z : (↑s : Type u_1)
hz : x < z
hz'_1 : z < y
hz0 : ⊥ < (↑z : WithBot X)
hz' : (↑z : WithBot X).unbot ⋯ < (↑y : WithBot X).unbot ⋯
refine_1 : (↑z : WithBot X).unbot ⋯ ∈ some ⁻¹' s
⊢ False
have refine_2 : (↑y : WithBot X).unbot sorry ∈ some ⁻¹' s
Tactic: refine absurd (this ?_ ?_) hz'.ne