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 β
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
a b : α
⊢ b ∈ h₀_finset_Ici a ↔ b ∈ h₁_finset_Ici a
have h : a ≤ b ↔ b ∈ h₁_finset_Ici a
Tactic: rw [h₀_finset_mem_Ici, h₁_finset_mem_Ici]
-- 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_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
a b : α
h : a ≤ b ↔ b ∈ h₁_finset_Ici a
⊢ b ∈ h₀_finset_Ici a ↔ b ∈ h₁_finset_Ici a
have h₁ : a ≤ b ↔ a ≤ b
Tactic: rw [h₀_finset_mem_Ici, h₁_finset_mem_Ici]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
⊢ { finsetIoi := h₀_finset_Ioi, finsetIci := h₀_finset_Ici, finset_mem_Ici := h₀_finset_mem_Ici,
      finset_mem_Ioi := h₀_finset_mem_Ioi : LocallyFiniteOrderTop α } =
    { finsetIoi := h₁_finset_Ioi, finsetIci := h₁_finset_Ici, finset_mem_Ici := h₁_finset_mem_Ici,
      finset_mem_Ioi := h₁_finset_mem_Ioi }
have hIci : h₀_finset_Ici = h₁_finset_Ici
Tactic: have hIci : h₀_finset_Ici = h₁_finset_Ici := by
      ext a b
      rw [h₀_finset_mem_Ici, h₁_finset_mem_Ici]
-- 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_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
hIci : h₀_finset_Ici = h₁_finset_Ici
⊢ h₀_finset_Ioi = h₁_finset_Ioi
have h : ∀ (a b : α), b ∈ h₀_finset_Ioi a ↔ b ∈ h₁_finset_Ioi a
Tactic: ext a b
-- 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_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
hIci : h₀_finset_Ici = h₁_finset_Ici
a b : α
⊢ b ∈ h₀_finset_Ioi a ↔ b ∈ h₁_finset_Ioi a
have h : a < b ↔ b ∈ h₁_finset_Ioi a
Tactic: rw [h₀_finset_mem_Ioi, h₁_finset_mem_Ioi]
-- 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_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
hIci : h₀_finset_Ici = h₁_finset_Ici
a b : α
h : a < b ↔ b ∈ h₁_finset_Ioi a
⊢ b ∈ h₀_finset_Ioi a ↔ b ∈ h₁_finset_Ioi a
have h₁ : a < b ↔ a < b
Tactic: rw [h₀_finset_mem_Ioi, h₁_finset_mem_Ioi]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Defs (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
hIci : h₀_finset_Ici = h₁_finset_Ici
⊢ { finsetIoi := h₀_finset_Ioi, finsetIci := h₀_finset_Ici, finset_mem_Ici := h₀_finset_mem_Ici,
      finset_mem_Ioi := h₀_finset_mem_Ioi : LocallyFiniteOrderTop α } =
    { finsetIoi := h₁_finset_Ioi, finsetIci := h₁_finset_Ici, finset_mem_Ici := h₁_finset_mem_Ici,
      finset_mem_Ioi := h₁_finset_mem_Ioi }
have hIoi : h₀_finset_Ioi = h₁_finset_Ioi
Tactic: have hIoi : h₀_finset_Ioi = h₁_finset_Ioi := by
      ext a b
      rw [h₀_finset_mem_Ioi, h₁_finset_mem_Ioi]
-- 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_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
hIci : h₀_finset_Ici = h₁_finset_Ici
hIoi : h₀_finset_Ioi = h₁_finset_Ioi
⊢ { finsetIoi := h₀_finset_Ioi, finsetIci := h₀_finset_Ici, finset_mem_Ici := h₀_finset_mem_Ici,
      finset_mem_Ioi := h₀_finset_mem_Ioi : LocallyFiniteOrderTop α } =
    { finsetIoi := h₁_finset_Ioi, finsetIci := h₁_finset_Ici, finset_mem_Ici := h₁_finset_mem_Ici,
      finset_mem_Ioi := h₁_finset_mem_Ioi }
have simp_rw : { finsetIoi := h₀_finset_Ioi, finsetIci := h₁_finset_Ici, finset_mem_Ici := sorry, finset_mem_Ioi := h₀_finset_mem_Ioi :
    LocallyFiniteOrderTop α } =
  { finsetIoi := h₁_finset_Ioi, finsetIci := h₁_finset_Ici, finset_mem_Ici := h₁_finset_mem_Ici,
    finset_mem_Ioi := h₁_finset_mem_Ioi }
Tactic: simp_rw [hIci, hIoi]
-- 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 : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ Membership.mem (γ := Finset α)
      (preimage.{u_1, u_2} (β := β) (Icc ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
        ((⇑f : (a : α) → β) : (a : α) → β) ⋯)
      x ↔
    a ≤ x ∧ x ≤ b
have rw : Membership.mem.{u_2, u_2} (α := β) (γ := Finset β) (Icc ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
    ((f : (a : α) → β) x : β) ↔
  a ≤ x ∧ x ≤ b
Tactic: rw [mem_preimage, mem_Icc, f.le_iff_le, f.le_iff_le]
-- 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 : LocallyFiniteOrder β
f : α ↪o β
a b x : α
rw :
  Membership.mem.{u_2, u_2} (α := β) (γ := Finset β) (Icc ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
      ((f : (a : α) → β) x : β) ↔
    a ≤ x ∧ x ≤ b
⊢ Membership.mem (γ := Finset α)
      (preimage.{u_1, u_2} (β := β) (Icc ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
        ((⇑f : (a : α) → β) : (a : α) → β) ⋯)
      x ↔
    a ≤ x ∧ x ≤ b
have rw₁ : LE.le.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) x : β) ∧
    LE.le.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) b : β) ↔
  a ≤ x ∧ x ≤ b
Tactic: rw [mem_preimage, mem_Icc, f.le_iff_le, f.le_iff_le]
-- 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 : LocallyFiniteOrder β
f : α ↪o β
a b x : α
rw :
  Membership.mem.{u_2, u_2} (α := β) (γ := Finset β) (Icc ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
      ((f : (a : α) → β) x : β) ↔
    a ≤ x ∧ x ≤ b
rw₁ :
  LE.le.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) x : β) ∧
      LE.le.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) b : β) ↔
    a ≤ x ∧ x ≤ b
⊢ Membership.mem (γ := Finset α)
      (preimage.{u_1, u_2} (β := β) (Icc ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
        ((⇑f : (a : α) → β) : (a : α) → β) ⋯)
      x ↔
    a ≤ x ∧ x ≤ b
have rw₂ : a ≤ x ∧ LE.le.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) b : β) ↔ a ≤ x ∧ x ≤ b
Tactic: rw [mem_preimage, mem_Icc, f.le_iff_le, f.le_iff_le]
-- 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 : LocallyFiniteOrder β
f : α ↪o β
a b x : α
rw :
  Membership.mem.{u_2, u_2} (α := β) (γ := Finset β) (Icc ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
      ((f : (a : α) → β) x : β) ↔
    a ≤ x ∧ x ≤ b
rw₁ :
  LE.le.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) x : β) ∧
      LE.le.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) b : β) ↔
    a ≤ x ∧ x ≤ b
rw₂ : a ≤ x ∧ LE.le.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) b : β) ↔ a ≤ x ∧ x ≤ b
⊢ Membership.mem (γ := Finset α)
      (preimage.{u_1, u_2} (β := β) (Icc ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
        ((⇑f : (a : α) → β) : (a : α) → β) ⋯)
      x ↔
    a ≤ x ∧ x ≤ b
have rw₃ : a ≤ x ∧ x ≤ b ↔ a ≤ x ∧ x ≤ b
Tactic: rw [mem_preimage, mem_Icc, f.le_iff_le, f.le_iff_le]
-- 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 : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ Membership.mem (γ := Finset α)
      (preimage.{u_1, u_2} (β := β) (Ico ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
        ((⇑f : (a : α) → β) : (a : α) → β) ⋯)
      x ↔
    a ≤ x ∧ x < b
have rw : Membership.mem.{u_2, u_2} (α := β) (γ := Finset β) (Ico ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
    ((f : (a : α) → β) x : β) ↔
  a ≤ x ∧ x < b
Tactic: rw [mem_preimage, mem_Ico, f.le_iff_le, f.lt_iff_lt]
-- 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 : LocallyFiniteOrder β
f : α ↪o β
a b x : α
rw :
  Membership.mem.{u_2, u_2} (α := β) (γ := Finset β) (Ico ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
      ((f : (a : α) → β) x : β) ↔
    a ≤ x ∧ x < b
⊢ Membership.mem (γ := Finset α)
      (preimage.{u_1, u_2} (β := β) (Ico ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
        ((⇑f : (a : α) → β) : (a : α) → β) ⋯)
      x ↔
    a ≤ x ∧ x < b
have rw₁ : LE.le.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) x : β) ∧
    LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) b : β) ↔
  a ≤ x ∧ x < b
Tactic: rw [mem_preimage, mem_Ico, f.le_iff_le, f.lt_iff_lt]
-- 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 : LocallyFiniteOrder β
f : α ↪o β
a b x : α
rw :
  Membership.mem.{u_2, u_2} (α := β) (γ := Finset β) (Ico ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
      ((f : (a : α) → β) x : β) ↔
    a ≤ x ∧ x < b
rw₁ :
  LE.le.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) x : β) ∧
      LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) b : β) ↔
    a ≤ x ∧ x < b
⊢ Membership.mem (γ := Finset α)
      (preimage.{u_1, u_2} (β := β) (Ico ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
        ((⇑f : (a : α) → β) : (a : α) → β) ⋯)
      x ↔
    a ≤ x ∧ x < b
have rw₂ : a ≤ x ∧ LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) b : β) ↔ a ≤ x ∧ x < b
Tactic: rw [mem_preimage, mem_Ico, f.le_iff_le, f.lt_iff_lt]
-- 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 : LocallyFiniteOrder β
f : α ↪o β
a b x : α
rw :
  Membership.mem.{u_2, u_2} (α := β) (γ := Finset β) (Ico ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
      ((f : (a : α) → β) x : β) ↔
    a ≤ x ∧ x < b
rw₁ :
  LE.le.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) x : β) ∧
      LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) b : β) ↔
    a ≤ x ∧ x < b
rw₂ : a ≤ x ∧ LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) b : β) ↔ a ≤ x ∧ x < b
⊢ Membership.mem (γ := Finset α)
      (preimage.{u_1, u_2} (β := β) (Ico ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
        ((⇑f : (a : α) → β) : (a : α) → β) ⋯)
      x ↔
    a ≤ x ∧ x < b
have rw₃ : a ≤ x ∧ x < b ↔ a ≤ x ∧ x < b
Tactic: rw [mem_preimage, mem_Ico, f.le_iff_le, f.lt_iff_lt]
-- 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 : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ Membership.mem (γ := Finset α)
      (preimage.{u_1, u_2} (β := β) (Ioc ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
        ((⇑f : (a : α) → β) : (a : α) → β) ⋯)
      x ↔
    a < x ∧ x ≤ b
have rw : Membership.mem.{u_2, u_2} (α := β) (γ := Finset β) (Ioc ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
    ((f : (a : α) → β) x : β) ↔
  a < x ∧ x ≤ b
Tactic: rw [mem_preimage, mem_Ioc, f.lt_iff_lt, f.le_iff_le]
-- 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 : LocallyFiniteOrder β
f : α ↪o β
a b x : α
rw :
  Membership.mem.{u_2, u_2} (α := β) (γ := Finset β) (Ioc ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
      ((f : (a : α) → β) x : β) ↔
    a < x ∧ x ≤ b
⊢ Membership.mem (γ := Finset α)
      (preimage.{u_1, u_2} (β := β) (Ioc ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
        ((⇑f : (a : α) → β) : (a : α) → β) ⋯)
      x ↔
    a < x ∧ x ≤ b
have rw₁ : LT.lt.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) x : β) ∧
    LE.le.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) b : β) ↔
  a < x ∧ x ≤ b
Tactic: rw [mem_preimage, mem_Ioc, f.lt_iff_lt, f.le_iff_le]
-- 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 : LocallyFiniteOrder β
f : α ↪o β
a b x : α
rw :
  Membership.mem.{u_2, u_2} (α := β) (γ := Finset β) (Ioc ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
      ((f : (a : α) → β) x : β) ↔
    a < x ∧ x ≤ b
rw₁ :
  LT.lt.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) x : β) ∧
      LE.le.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) b : β) ↔
    a < x ∧ x ≤ b
⊢ Membership.mem (γ := Finset α)
      (preimage.{u_1, u_2} (β := β) (Ioc ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
        ((⇑f : (a : α) → β) : (a : α) → β) ⋯)
      x ↔
    a < x ∧ x ≤ b
have rw₂ : a < x ∧ LE.le.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) b : β) ↔ a < x ∧ x ≤ b
Tactic: rw [mem_preimage, mem_Ioc, f.lt_iff_lt, f.le_iff_le]
-- 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 : LocallyFiniteOrder β
f : α ↪o β
a b x : α
rw :
  Membership.mem.{u_2, u_2} (α := β) (γ := Finset β) (Ioc ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
      ((f : (a : α) → β) x : β) ↔
    a < x ∧ x ≤ b
rw₁ :
  LT.lt.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) x : β) ∧
      LE.le.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) b : β) ↔
    a < x ∧ x ≤ b
rw₂ : a < x ∧ LE.le.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) b : β) ↔ a < x ∧ x ≤ b
⊢ Membership.mem (γ := Finset α)
      (preimage.{u_1, u_2} (β := β) (Ioc ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
        ((⇑f : (a : α) → β) : (a : α) → β) ⋯)
      x ↔
    a < x ∧ x ≤ b
have rw₃ : a < x ∧ x ≤ b ↔ a < x ∧ x ≤ b
Tactic: rw [mem_preimage, mem_Ioc, f.lt_iff_lt, f.le_iff_le]
-- 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 : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ Membership.mem (γ := Finset α)
      (preimage.{u_1, u_2} (β := β) (Ioo ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
        ((⇑f : (a : α) → β) : (a : α) → β) ⋯)
      x ↔
    a < x ∧ x < b
have rw : Membership.mem.{u_2, u_2} (α := β) (γ := Finset β) (Ioo ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
    ((f : (a : α) → β) x : β) ↔
  a < x ∧ x < b
Tactic: rw [mem_preimage, mem_Ioo, f.lt_iff_lt, f.lt_iff_lt]
-- 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 : LocallyFiniteOrder β
f : α ↪o β
a b x : α
rw :
  Membership.mem.{u_2, u_2} (α := β) (γ := Finset β) (Ioo ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
      ((f : (a : α) → β) x : β) ↔
    a < x ∧ x < b
⊢ Membership.mem (γ := Finset α)
      (preimage.{u_1, u_2} (β := β) (Ioo ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
        ((⇑f : (a : α) → β) : (a : α) → β) ⋯)
      x ↔
    a < x ∧ x < b
have rw₁ : LT.lt.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) x : β) ∧
    LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) b : β) ↔
  a < x ∧ x < b
Tactic: rw [mem_preimage, mem_Ioo, f.lt_iff_lt, f.lt_iff_lt]
-- 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 : LocallyFiniteOrder β
f : α ↪o β
a b x : α
rw :
  Membership.mem.{u_2, u_2} (α := β) (γ := Finset β) (Ioo ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
      ((f : (a : α) → β) x : β) ↔
    a < x ∧ x < b
rw₁ :
  LT.lt.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) x : β) ∧
      LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) b : β) ↔
    a < x ∧ x < b
⊢ Membership.mem (γ := Finset α)
      (preimage.{u_1, u_2} (β := β) (Ioo ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
        ((⇑f : (a : α) → β) : (a : α) → β) ⋯)
      x ↔
    a < x ∧ x < b
have rw₂ : a < x ∧ LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) b : β) ↔ a < x ∧ x < b
Tactic: rw [mem_preimage, mem_Ioo, f.lt_iff_lt, f.lt_iff_lt]
-- 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 : LocallyFiniteOrder β
f : α ↪o β
a b x : α
rw :
  Membership.mem.{u_2, u_2} (α := β) (γ := Finset β) (Ioo ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
      ((f : (a : α) → β) x : β) ↔
    a < x ∧ x < b
rw₁ :
  LT.lt.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) x : β) ∧
      LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) b : β) ↔
    a < x ∧ x < b
rw₂ : a < x ∧ LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) b : β) ↔ a < x ∧ x < b
⊢ Membership.mem (γ := Finset α)
      (preimage.{u_1, u_2} (β := β) (Ioo ((f : (a : α) → β) a) ((f : (a : α) → β) b) : Finset β)
        ((⇑f : (a : α) → β) : (a : α) → β) ⋯)
      x ↔
    a < x ∧ x < b
have rw₃ : a < x ∧ x < b ↔ a < x ∧ x < b
Tactic: rw [mem_preimage, mem_Ioo, f.lt_iff_lt, f.lt_iff_lt]
-- 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 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : DecidableLE (α × β)
a b x : α × β
⊢ Membership.mem (γ := Finset (α × β)) ((fun (x y : α × β) ↦ Icc x.1 y.1 ×ˢ Icc x.2 y.2) a b) x ↔ a ≤ x ∧ x ≤ b
have rw : x.1 ∈ Icc a.1 b.1 ∧ x.2 ∈ Icc a.2 b.2 ↔ a ≤ x ∧ x ≤ b
Tactic: rw [mem_product, mem_Icc, mem_Icc, and_and_and_comm, le_def, 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 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : DecidableLE (α × β)
a b x : α × β
rw : x.1 ∈ Icc a.1 b.1 ∧ x.2 ∈ Icc a.2 b.2 ↔ a ≤ x ∧ x ≤ b
⊢ Membership.mem (γ := Finset (α × β)) ((fun (x y : α × β) ↦ Icc x.1 y.1 ×ˢ Icc x.2 y.2) a b) x ↔ a ≤ x ∧ x ≤ b
have rw₁ : (a.1 ≤ x.1 ∧ x.1 ≤ b.1) ∧ x.2 ∈ Icc a.2 b.2 ↔ a ≤ x ∧ x ≤ b
Tactic: rw [mem_product, mem_Icc, mem_Icc, and_and_and_comm, le_def, 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 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : DecidableLE (α × β)
a b x : α × β
rw : x.1 ∈ Icc a.1 b.1 ∧ x.2 ∈ Icc a.2 b.2 ↔ a ≤ x ∧ x ≤ b
rw₁ : (a.1 ≤ x.1 ∧ x.1 ≤ b.1) ∧ x.2 ∈ Icc a.2 b.2 ↔ a ≤ x ∧ x ≤ b
⊢ Membership.mem (γ := Finset (α × β)) ((fun (x y : α × β) ↦ Icc x.1 y.1 ×ˢ Icc x.2 y.2) a b) x ↔ a ≤ x ∧ x ≤ b
have rw₂ : (a.1 ≤ x.1 ∧ x.1 ≤ b.1) ∧ a.2 ≤ x.2 ∧ x.2 ≤ b.2 ↔ a ≤ x ∧ x ≤ b
Tactic: rw [mem_product, mem_Icc, mem_Icc, and_and_and_comm, le_def, 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 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : DecidableLE (α × β)
a b x : α × β
rw : x.1 ∈ Icc a.1 b.1 ∧ x.2 ∈ Icc a.2 b.2 ↔ a ≤ x ∧ x ≤ b
rw₁ : (a.1 ≤ x.1 ∧ x.1 ≤ b.1) ∧ x.2 ∈ Icc a.2 b.2 ↔ a ≤ x ∧ x ≤ b
rw₂ : (a.1 ≤ x.1 ∧ x.1 ≤ b.1) ∧ a.2 ≤ x.2 ∧ x.2 ≤ b.2 ↔ a ≤ x ∧ x ≤ b
⊢ Membership.mem (γ := Finset (α × β)) ((fun (x y : α × β) ↦ Icc x.1 y.1 ×ˢ Icc x.2 y.2) a b) x ↔ a ≤ x ∧ x ≤ b
have rw₃ : (a.1 ≤ x.1 ∧ a.2 ≤ x.2) ∧ x.1 ≤ b.1 ∧ x.2 ≤ b.2 ↔ a ≤ x ∧ x ≤ b
Tactic: rw [mem_product, mem_Icc, mem_Icc, and_and_and_comm, le_def, 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 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : DecidableLE (α × β)
a b x : α × β
rw : x.1 ∈ Icc a.1 b.1 ∧ x.2 ∈ Icc a.2 b.2 ↔ a ≤ x ∧ x ≤ b
rw₁ : (a.1 ≤ x.1 ∧ x.1 ≤ b.1) ∧ x.2 ∈ Icc a.2 b.2 ↔ a ≤ x ∧ x ≤ b
rw₂ : (a.1 ≤ x.1 ∧ x.1 ≤ b.1) ∧ a.2 ≤ x.2 ∧ x.2 ≤ b.2 ↔ a ≤ x ∧ x ≤ b
rw₃ : (a.1 ≤ x.1 ∧ a.2 ≤ x.2) ∧ x.1 ≤ b.1 ∧ x.2 ≤ b.2 ↔ a ≤ x ∧ x ≤ b
⊢ Membership.mem (γ := Finset (α × β)) ((fun (x y : α × β) ↦ Icc x.1 y.1 ×ˢ Icc x.2 y.2) a b) x ↔ a ≤ x ∧ x ≤ b
have rw₄ : (a.1 ≤ x.1 ∧ a.2 ≤ x.2) ∧ x.1 ≤ b.1 ∧ x.2 ≤ b.2 ↔ (a.1 ≤ x.1 ∧ a.2 ≤ x.2) ∧ x ≤ b
Tactic: rw [mem_product, mem_Icc, mem_Icc, and_and_and_comm, le_def, 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 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : DecidableLE (α × β)
a b x : α × β
rw : x.1 ∈ Icc a.1 b.1 ∧ x.2 ∈ Icc a.2 b.2 ↔ a ≤ x ∧ x ≤ b
rw₁ : (a.1 ≤ x.1 ∧ x.1 ≤ b.1) ∧ x.2 ∈ Icc a.2 b.2 ↔ a ≤ x ∧ x ≤ b
rw₂ : (a.1 ≤ x.1 ∧ x.1 ≤ b.1) ∧ a.2 ≤ x.2 ∧ x.2 ≤ b.2 ↔ a ≤ x ∧ x ≤ b
rw₃ : (a.1 ≤ x.1 ∧ a.2 ≤ x.2) ∧ x.1 ≤ b.1 ∧ x.2 ≤ b.2 ↔ a ≤ x ∧ x ≤ b
rw₄ : (a.1 ≤ x.1 ∧ a.2 ≤ x.2) ∧ x.1 ≤ b.1 ∧ x.2 ≤ b.2 ↔ (a.1 ≤ x.1 ∧ a.2 ≤ x.2) ∧ x ≤ b
⊢ Membership.mem (γ := Finset (α × β)) ((fun (x y : α × β) ↦ Icc x.1 y.1 ×ˢ Icc x.2 y.2) a b) x ↔ a ≤ x ∧ x ≤ b
have rw₅ : (a.1 ≤ x.1 ∧ a.2 ≤ x.2) ∧ x.1 ≤ b.1 ∧ x.2 ≤ b.2 ↔ (a.1 ≤ x.1 ∧ a.2 ≤ x.2) ∧ x.1 ≤ b.1 ∧ x.2 ≤ b.2
Tactic: rw [mem_product, mem_Icc, mem_Icc, and_and_and_comm, le_def, 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 : α × β
⊢ Membership.mem (γ := Finset (α × β)) ((fun (x : α × β) ↦ Ici x.1 ×ˢ Ici x.2) a) x ↔ a ≤ x
have rw : x.1 ∈ Ici a.1 ∧ x.2 ∈ Ici a.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
⊢ Membership.mem (γ := Finset (α × β)) ((fun (x : α × β) ↦ Ici x.1 ×ˢ Ici x.2) a) x ↔ a ≤ x
have rw₁ : a.1 ≤ x.1 ∧ x.2 ∈ Ici a.2 ↔ a ≤ x
Tactic: rw [mem_product, mem_Ici, mem_Ici, le_def]