awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
rw : x ∈ finsetIcc a b ∧ ¬b ≤ x ↔ a ≤ x ∧ x < b
⊢ x ∈ {x ∈ finsetIcc a b | ¬b ≤ x} ↔ a ≤ x ∧ x < b
have rw₁ : (a ≤ x ∧ x ≤ b) ∧ ¬b ≤ x ↔ a ≤ x ∧ x < b
Tactic: rw [Finset.mem_filter, mem_Icc, and_assoc, lt_iff_le_not_ge]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
rw : x ∈ finsetIcc a b ∧ ¬b ≤ x ↔ a ≤ x ∧ x < b
rw₁ : (a ≤ x ∧ x ≤ b) ∧ ¬b ≤ x ↔ a ≤ x ∧ x < b
⊢ x ∈ {x ∈ finsetIcc a b | ¬b ≤ x} ↔ a ≤ x ∧ x < b
have rw₂ : a ≤ x ∧ x ≤ b ∧ ¬b ≤ x ↔ a ≤ x ∧ x < b
Tactic: rw [Finset.mem_filter, mem_Icc, and_assoc, lt_iff_le_not_ge]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
rw : x ∈ finsetIcc a b ∧ ¬b ≤ x ↔ a ≤ x ∧ x < b
rw₁ : (a ≤ x ∧ x ≤ b) ∧ ¬b ≤ x ↔ a ≤ x ∧ x < b
rw₂ : a ≤ x ∧ x ≤ b ∧ ¬b ≤ x ↔ a ≤ x ∧ x < b
⊢ x ∈ {x ∈ finsetIcc a b | ¬b ≤ x} ↔ a ≤ x ∧ x < b
have rw₃ : a ≤ x ∧ x ≤ b ∧ ¬b ≤ x ↔ a ≤ x ∧ x ≤ b ∧ ¬b ≤ x
Tactic: rw [Finset.mem_filter, mem_Icc, and_assoc, lt_iff_le_not_ge]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ {x ∈ finsetIcc a b | ¬x ≤ a} ↔ a < x ∧ x ≤ b
have rw : x ∈ finsetIcc a b ∧ ¬x ≤ a ↔ a < x ∧ x ≤ b
Tactic: rw [Finset.mem_filter, mem_Icc, and_right_comm, lt_iff_le_not_ge]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
rw : x ∈ finsetIcc a b ∧ ¬x ≤ a ↔ a < x ∧ x ≤ b
⊢ x ∈ {x ∈ finsetIcc a b | ¬x ≤ a} ↔ a < x ∧ x ≤ b
have rw₁ : (a ≤ x ∧ x ≤ b) ∧ ¬x ≤ a ↔ a < x ∧ x ≤ b
Tactic: rw [Finset.mem_filter, mem_Icc, and_right_comm, lt_iff_le_not_ge]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
rw : x ∈ finsetIcc a b ∧ ¬x ≤ a ↔ a < x ∧ x ≤ b
rw₁ : (a ≤ x ∧ x ≤ b) ∧ ¬x ≤ a ↔ a < x ∧ x ≤ b
⊢ x ∈ {x ∈ finsetIcc a b | ¬x ≤ a} ↔ a < x ∧ x ≤ b
have rw₂ : (a ≤ x ∧ ¬x ≤ a) ∧ x ≤ b ↔ a < x ∧ x ≤ b
Tactic: rw [Finset.mem_filter, mem_Icc, and_right_comm, lt_iff_le_not_ge]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
rw : x ∈ finsetIcc a b ∧ ¬x ≤ a ↔ a < x ∧ x ≤ b
rw₁ : (a ≤ x ∧ x ≤ b) ∧ ¬x ≤ a ↔ a < x ∧ x ≤ b
rw₂ : (a ≤ x ∧ ¬x ≤ a) ∧ x ≤ b ↔ a < x ∧ x ≤ b
⊢ x ∈ {x ∈ finsetIcc a b | ¬x ≤ a} ↔ a < x ∧ x ≤ b
have rw₃ : (a ≤ x ∧ ¬x ≤ a) ∧ x ≤ b ↔ (a ≤ x ∧ ¬x ≤ a) ∧ x ≤ b
Tactic: rw [Finset.mem_filter, mem_Icc, and_right_comm, lt_iff_le_not_ge]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ {x ∈ finsetIcc a b | ¬x ≤ a ∧ ¬b ≤ x} ↔ a < x ∧ x < b
have rw : x ∈ finsetIcc a b ∧ ¬x ≤ a ∧ ¬b ≤ x ↔ a < x ∧ x < b
Tactic: rw [Finset.mem_filter, mem_Icc, and_and_and_comm, lt_iff_le_not_ge, lt_iff_le_not_ge]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
rw : x ∈ finsetIcc a b ∧ ¬x ≤ a ∧ ¬b ≤ x ↔ a < x ∧ x < b
⊢ x ∈ {x ∈ finsetIcc a b | ¬x ≤ a ∧ ¬b ≤ x} ↔ a < x ∧ x < b
have rw₁ : (a ≤ x ∧ x ≤ b) ∧ ¬x ≤ a ∧ ¬b ≤ x ↔ a < x ∧ x < b
Tactic: rw [Finset.mem_filter, mem_Icc, and_and_and_comm, lt_iff_le_not_ge, lt_iff_le_not_ge]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
rw : x ∈ finsetIcc a b ∧ ¬x ≤ a ∧ ¬b ≤ x ↔ a < x ∧ x < b
rw₁ : (a ≤ x ∧ x ≤ b) ∧ ¬x ≤ a ∧ ¬b ≤ x ↔ a < x ∧ x < b
⊢ x ∈ {x ∈ finsetIcc a b | ¬x ≤ a ∧ ¬b ≤ x} ↔ a < x ∧ x < b
have rw₂ : (a ≤ x ∧ ¬x ≤ a) ∧ x ≤ b ∧ ¬b ≤ x ↔ a < x ∧ x < b
Tactic: rw [Finset.mem_filter, mem_Icc, and_and_and_comm, lt_iff_le_not_ge, lt_iff_le_not_ge]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
rw : x ∈ finsetIcc a b ∧ ¬x ≤ a ∧ ¬b ≤ x ↔ a < x ∧ x < b
rw₁ : (a ≤ x ∧ x ≤ b) ∧ ¬x ≤ a ∧ ¬b ≤ x ↔ a < x ∧ x < b
rw₂ : (a ≤ x ∧ ¬x ≤ a) ∧ x ≤ b ∧ ¬b ≤ x ↔ a < x ∧ x < b
⊢ x ∈ {x ∈ finsetIcc a b | ¬x ≤ a ∧ ¬b ≤ x} ↔ a < x ∧ x < b
have rw₃ : (a ≤ x ∧ ¬x ≤ a) ∧ x ≤ b ∧ ¬b ≤ x ↔ (a ≤ x ∧ ¬x ≤ a) ∧ x < b
Tactic: rw [Finset.mem_filter, mem_Icc, and_and_and_comm, lt_iff_le_not_ge, lt_iff_le_not_ge]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
rw : x ∈ finsetIcc a b ∧ ¬x ≤ a ∧ ¬b ≤ x ↔ a < x ∧ x < b
rw₁ : (a ≤ x ∧ x ≤ b) ∧ ¬x ≤ a ∧ ¬b ≤ x ↔ a < x ∧ x < b
rw₂ : (a ≤ x ∧ ¬x ≤ a) ∧ x ≤ b ∧ ¬b ≤ x ↔ a < x ∧ x < b
rw₃ : (a ≤ x ∧ ¬x ≤ a) ∧ x ≤ b ∧ ¬b ≤ x ↔ (a ≤ x ∧ ¬x ≤ a) ∧ x < b
⊢ x ∈ {x ∈ finsetIcc a b | ¬x ≤ a ∧ ¬b ≤ x} ↔ a < x ∧ x < b
have rw₄ : (a ≤ x ∧ ¬x ≤ a) ∧ x ≤ b ∧ ¬b ≤ x ↔ (a ≤ x ∧ ¬x ≤ a) ∧ x ≤ b ∧ ¬b ≤ x
Tactic: rw [Finset.mem_filter, mem_Icc, and_and_and_comm, lt_iff_le_not_ge, lt_iff_le_not_ge]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ {x ∈ finsetIcc a b | x ≠ b} ↔ a ≤ x ∧ x < b
have rw : x ∈ finsetIcc a b ∧ x ≠ b ↔ a ≤ x ∧ x < b
Tactic: rw [Finset.mem_filter, mem_Icc, and_assoc, lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
rw : x ∈ finsetIcc a b ∧ x ≠ b ↔ a ≤ x ∧ x < b
⊢ x ∈ {x ∈ finsetIcc a b | x ≠ b} ↔ a ≤ x ∧ x < b
have rw₁ : (a ≤ x ∧ x ≤ b) ∧ x ≠ b ↔ a ≤ x ∧ x < b
Tactic: rw [Finset.mem_filter, mem_Icc, and_assoc, lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
rw : x ∈ finsetIcc a b ∧ x ≠ b ↔ a ≤ x ∧ x < b
rw₁ : (a ≤ x ∧ x ≤ b) ∧ x ≠ b ↔ a ≤ x ∧ x < b
⊢ x ∈ {x ∈ finsetIcc a b | x ≠ b} ↔ a ≤ x ∧ x < b
have rw₂ : a ≤ x ∧ x ≤ b ∧ x ≠ b ↔ a ≤ x ∧ x < b
Tactic: rw [Finset.mem_filter, mem_Icc, and_assoc, lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
rw : x ∈ finsetIcc a b ∧ x ≠ b ↔ a ≤ x ∧ x < b
rw₁ : (a ≤ x ∧ x ≤ b) ∧ x ≠ b ↔ a ≤ x ∧ x < b
rw₂ : a ≤ x ∧ x ≤ b ∧ x ≠ b ↔ a ≤ x ∧ x < b
⊢ x ∈ {x ∈ finsetIcc a b | x ≠ b} ↔ a ≤ x ∧ x < b
have rw₃ : a ≤ x ∧ x ≤ b ∧ x ≠ b ↔ a ≤ x ∧ x ≤ b ∧ x ≠ b
Tactic: rw [Finset.mem_filter, mem_Icc, and_assoc, lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ {x ∈ finsetIcc a b | a ≠ x} ↔ a < x ∧ x ≤ b
have rw : x ∈ finsetIcc a b ∧ a ≠ x ↔ a < x ∧ x ≤ b
Tactic: rw [Finset.mem_filter, mem_Icc, and_right_comm, lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
rw : x ∈ finsetIcc a b ∧ a ≠ x ↔ a < x ∧ x ≤ b
⊢ x ∈ {x ∈ finsetIcc a b | a ≠ x} ↔ a < x ∧ x ≤ b
have rw₁ : (a ≤ x ∧ x ≤ b) ∧ a ≠ x ↔ a < x ∧ x ≤ b
Tactic: rw [Finset.mem_filter, mem_Icc, and_right_comm, lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
rw : x ∈ finsetIcc a b ∧ a ≠ x ↔ a < x ∧ x ≤ b
rw₁ : (a ≤ x ∧ x ≤ b) ∧ a ≠ x ↔ a < x ∧ x ≤ b
⊢ x ∈ {x ∈ finsetIcc a b | a ≠ x} ↔ a < x ∧ x ≤ b
have rw₂ : (a ≤ x ∧ a ≠ x) ∧ x ≤ b ↔ a < x ∧ x ≤ b
Tactic: rw [Finset.mem_filter, mem_Icc, and_right_comm, lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
rw : x ∈ finsetIcc a b ∧ a ≠ x ↔ a < x ∧ x ≤ b
rw₁ : (a ≤ x ∧ x ≤ b) ∧ a ≠ x ↔ a < x ∧ x ≤ b
rw₂ : (a ≤ x ∧ a ≠ x) ∧ x ≤ b ↔ a < x ∧ x ≤ b
⊢ x ∈ {x ∈ finsetIcc a b | a ≠ x} ↔ a < x ∧ x ≤ b
have rw₃ : (a ≤ x ∧ a ≠ x) ∧ x ≤ b ↔ (a ≤ x ∧ a ≠ x) ∧ x ≤ b
Tactic: rw [Finset.mem_filter, mem_Icc, and_right_comm, lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ {x ∈ finsetIcc a b | a ≠ x ∧ x ≠ b} ↔ a < x ∧ x < b
have rw : x ∈ finsetIcc a b ∧ a ≠ x ∧ x ≠ b ↔ a < x ∧ x < b
Tactic: rw [Finset.mem_filter, mem_Icc, and_and_and_comm, lt_iff_le_and_ne, lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
rw : x ∈ finsetIcc a b ∧ a ≠ x ∧ x ≠ b ↔ a < x ∧ x < b
⊢ x ∈ {x ∈ finsetIcc a b | a ≠ x ∧ x ≠ b} ↔ a < x ∧ x < b
have rw₁ : (a ≤ x ∧ x ≤ b) ∧ a ≠ x ∧ x ≠ b ↔ a < x ∧ x < b
Tactic: rw [Finset.mem_filter, mem_Icc, and_and_and_comm, lt_iff_le_and_ne, lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
rw : x ∈ finsetIcc a b ∧ a ≠ x ∧ x ≠ b ↔ a < x ∧ x < b
rw₁ : (a ≤ x ∧ x ≤ b) ∧ a ≠ x ∧ x ≠ b ↔ a < x ∧ x < b
⊢ x ∈ {x ∈ finsetIcc a b | a ≠ x ∧ x ≠ b} ↔ a < x ∧ x < b
have rw₂ : (a ≤ x ∧ a ≠ x) ∧ x ≤ b ∧ x ≠ b ↔ a < x ∧ x < b
Tactic: rw [Finset.mem_filter, mem_Icc, and_and_and_comm, lt_iff_le_and_ne, lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
rw : x ∈ finsetIcc a b ∧ a ≠ x ∧ x ≠ b ↔ a < x ∧ x < b
rw₁ : (a ≤ x ∧ x ≤ b) ∧ a ≠ x ∧ x ≠ b ↔ a < x ∧ x < b
rw₂ : (a ≤ x ∧ a ≠ x) ∧ x ≤ b ∧ x ≠ b ↔ a < x ∧ x < b
⊢ x ∈ {x ∈ finsetIcc a b | a ≠ x ∧ x ≠ b} ↔ a < x ∧ x < b
have rw₃ : (a ≤ x ∧ a ≠ x) ∧ x ≤ b ∧ x ≠ b ↔ (a ≤ x ∧ a ≠ x) ∧ x < b
Tactic: rw [Finset.mem_filter, mem_Icc, and_and_and_comm, lt_iff_le_and_ne, lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
rw : x ∈ finsetIcc a b ∧ a ≠ x ∧ x ≠ b ↔ a < x ∧ x < b
rw₁ : (a ≤ x ∧ x ≤ b) ∧ a ≠ x ∧ x ≠ b ↔ a < x ∧ x < b
rw₂ : (a ≤ x ∧ a ≠ x) ∧ x ≤ b ∧ x ≠ b ↔ a < x ∧ x < b
rw₃ : (a ≤ x ∧ a ≠ x) ∧ x ≤ b ∧ x ≠ b ↔ (a ≤ x ∧ a ≠ x) ∧ x < b
⊢ x ∈ {x ∈ finsetIcc a b | a ≠ x ∧ x ≠ b} ↔ a < x ∧ x < b
have rw₄ : (a ≤ x ∧ a ≠ x) ∧ x ≤ b ∧ x ≠ b ↔ (a ≤ x ∧ a ≠ x) ∧ x ≤ b ∧ x ≠ b
Tactic: rw [Finset.mem_filter, mem_Icc, and_and_and_comm, lt_iff_le_and_ne, lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
finsetIci : α → Finset α
mem_Ici : ∀ (a x : α), x ∈ finsetIci a ↔ a ≤ x
a x : α
⊢ x ∈ {x ∈ finsetIci a | ¬x ≤ a} ↔ a < x
have rw : x ∈ finsetIci a ∧ ¬x ≤ a ↔ a < x
Tactic: rw [mem_filter, mem_Ici, lt_iff_le_not_ge]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
finsetIci : α → Finset α
mem_Ici : ∀ (a x : α), x ∈ finsetIci a ↔ a ≤ x
a x : α
rw : x ∈ finsetIci a ∧ ¬x ≤ a ↔ a < x
⊢ x ∈ {x ∈ finsetIci a | ¬x ≤ a} ↔ a < x
have rw₁ : a ≤ x ∧ ¬x ≤ a ↔ a < x
Tactic: rw [mem_filter, mem_Ici, lt_iff_le_not_ge]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
finsetIci : α → Finset α
mem_Ici : ∀ (a x : α), x ∈ finsetIci a ↔ a ≤ x
a x : α
rw : x ∈ finsetIci a ∧ ¬x ≤ a ↔ a < x
rw₁ : a ≤ x ∧ ¬x ≤ a ↔ a < x
⊢ x ∈ {x ∈ finsetIci a | ¬x ≤ a} ↔ a < x
have rw₂ : a ≤ x ∧ ¬x ≤ a ↔ a ≤ x ∧ ¬x ≤ a
Tactic: rw [mem_filter, mem_Ici, lt_iff_le_not_ge]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : DecidableEq α
finsetIci : α → Finset α
mem_Ici : ∀ (a x : α), x ∈ finsetIci a ↔ a ≤ x
a x : α
⊢ x ∈ {x ∈ finsetIci a | a ≠ x} ↔ a < x
have rw : x ∈ finsetIci a ∧ a ≠ x ↔ a < x
Tactic: rw [mem_filter, mem_Ici, lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : DecidableEq α
finsetIci : α → Finset α
mem_Ici : ∀ (a x : α), x ∈ finsetIci a ↔ a ≤ x
a x : α
rw : x ∈ finsetIci a ∧ a ≠ x ↔ a < x
⊢ x ∈ {x ∈ finsetIci a | a ≠ x} ↔ a < x
have rw₁ : a ≤ x ∧ a ≠ x ↔ a < x
Tactic: rw [mem_filter, mem_Ici, lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : DecidableEq α
finsetIci : α → Finset α
mem_Ici : ∀ (a x : α), x ∈ finsetIci a ↔ a ≤ x
a x : α
rw : x ∈ finsetIci a ∧ a ≠ x ↔ a < x
rw₁ : a ≤ x ∧ a ≠ x ↔ a < x
⊢ x ∈ {x ∈ finsetIci a | a ≠ x} ↔ a < x
have rw₂ : a ≤ x ∧ a ≠ x ↔ a ≤ x ∧ a ≠ x
Tactic: rw [mem_filter, mem_Ici, lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : OrderTop α
a_1 x_1 a x : α
⊢ x ∈ Icc a ⊤ ↔ a ≤ x
have rw : a ≤ x ∧ x ≤ ⊤ ↔ a ≤ x
Tactic: rw [mem_Icc, and_iff_left le_top]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : OrderTop α
a_1 x_1 a x : α
rw : a ≤ x ∧ x ≤ ⊤ ↔ a ≤ x
⊢ x ∈ Icc a ⊤ ↔ a ≤ x
have rw₁ : a ≤ x ↔ a ≤ x
Tactic: rw [mem_Icc, and_iff_left le_top]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : OrderTop α
a_1 x_1 a x : α
⊢ x ∈ Ioc a ⊤ ↔ a < x
have rw : a < x ∧ x ≤ ⊤ ↔ a < x
Tactic: rw [mem_Ioc, and_iff_left le_top]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : OrderTop α
a_1 x_1 a x : α
rw : a < x ∧ x ≤ ⊤ ↔ a < x
⊢ x ∈ Ioc a ⊤ ↔ a < x
have rw₁ : a < x ↔ a < x
Tactic: rw [mem_Ioc, and_iff_left le_top]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
h : ∀ (a b : α), (Set.Icc a b).Finite
a b x : α
⊢ Membership.mem (γ := Finset α) ((fun (a b : α) ↦ ⋯.toFinset (s := Set.Icc a b)) a b) x ↔ a ≤ x ∧ x ≤ b
have rw : x ∈ Set.Icc a b ↔ a ≤ x ∧ x ≤ b
Tactic: rw [Set.Finite.mem_toFinset, Set.mem_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
h : ∀ (a b : α), (Set.Icc a b).Finite
a b x : α
rw : x ∈ Set.Icc a b ↔ a ≤ x ∧ x ≤ b
⊢ Membership.mem (γ := Finset α) ((fun (a b : α) ↦ ⋯.toFinset (s := Set.Icc a b)) a b) x ↔ a ≤ x ∧ x ≤ b
have rw₁ : a ≤ x ∧ x ≤ b ↔ a ≤ x ∧ x ≤ b
Tactic: rw [Set.Finite.mem_toFinset, Set.mem_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
h₀ h₁ : LocallyFiniteOrder α
⊢ h₀ = h₁
have obtain : ∀ (h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α)
  (h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b)
  (h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b)
  (h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b)
  (h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b),
  { finsetIcc := h₀_finset_Icc, finsetIco := h₀_finset_Ico, finsetIoc := h₀_finset_Ioc, finsetIoo := h₀_finset_Ioo,
      finset_mem_Icc := h₀_finset_mem_Icc, finset_mem_Ico := h₀_finset_mem_Ico, finset_mem_Ioc := h₀_finset_mem_Ioc,
      finset_mem_Ioo := h₀_finset_mem_Ioo : LocallyFiniteOrder α } =
    h₁
Tactic: obtain ⟨h₀_finset_Icc, h₀_finset_Ico, h₀_finset_Ioc, h₀_finset_Ioo,
      h₀_finset_mem_Icc, h₀_finset_mem_Ico, h₀_finset_mem_Ioc, h₀_finset_mem_Ioo⟩ := h₀
Cleared hypotheses: h₀
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
h₁ : LocallyFiniteOrder α
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
⊢ { finsetIcc := h₀_finset_Icc, finsetIco := h₀_finset_Ico, finsetIoc := h₀_finset_Ioc, finsetIoo := h₀_finset_Ioo,
      finset_mem_Icc := h₀_finset_mem_Icc, finset_mem_Ico := h₀_finset_mem_Ico, finset_mem_Ioc := h₀_finset_mem_Ioc,
      finset_mem_Ioo := h₀_finset_mem_Ioo : LocallyFiniteOrder α } =
    h₁
have obtain : ∀ (h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α)
  (h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b)
  (h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b)
  (h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b)
  (h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b),
  { finsetIcc := h₀_finset_Icc, finsetIco := h₀_finset_Ico, finsetIoc := h₀_finset_Ioc, finsetIoo := h₀_finset_Ioo,
      finset_mem_Icc := h₀_finset_mem_Icc, finset_mem_Ico := h₀_finset_mem_Ico, finset_mem_Ioc := h₀_finset_mem_Ioc,
      finset_mem_Ioo := h₀_finset_mem_Ioo : LocallyFiniteOrder α } =
    { finsetIcc := h₁_finset_Icc, finsetIco := h₁_finset_Ico, finsetIoc := h₁_finset_Ioc, finsetIoo := h₁_finset_Ioo,
      finset_mem_Icc := h₁_finset_mem_Icc, finset_mem_Ico := h₁_finset_mem_Ico, finset_mem_Ioc := h₁_finset_mem_Ioc,
      finset_mem_Ioo := h₁_finset_mem_Ioo }
Tactic: obtain ⟨h₁_finset_Icc, h₁_finset_Ico, h₁_finset_Ioc, h₁_finset_Ioo,
      h₁_finset_mem_Icc, h₁_finset_mem_Ico, h₁_finset_mem_Ioc, h₁_finset_mem_Ioo⟩ := h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
⊢ h₀_finset_Icc = h₁_finset_Icc
have h : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ x ∈ h₁_finset_Icc a b
Tactic: ext a b x
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
a b x : α
⊢ x ∈ h₀_finset_Icc a b ↔ x ∈ h₁_finset_Icc a b
have h : a ≤ x ∧ x ≤ b ↔ x ∈ h₁_finset_Icc a b
Tactic: rw [h₀_finset_mem_Icc, h₁_finset_mem_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
a b x : α
h : a ≤ x ∧ x ≤ b ↔ x ∈ h₁_finset_Icc a b
⊢ x ∈ h₀_finset_Icc a b ↔ x ∈ h₁_finset_Icc a b
have h₁ : a ≤ x ∧ x ≤ b ↔ a ≤ x ∧ x ≤ b
Tactic: rw [h₀_finset_mem_Icc, h₁_finset_mem_Icc]