awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Finset.Defs
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
hIcc : h₀_finset_Icc = h₁_finset_Icc
hIco : h₀_finset_Ico = h₁_finset_Ico
hIoc : h₀_finset_Ioc = h₁_finset_Ioc
⊢ h₀_finset_Ioo = h₁_finset_Ioo

Tactic:
have hIoo : h₀_finset_Ioo = h₁_finset_Ioo := by
      ext a b x
      rw [h₀_finset_mem_Ioo, h₁_finset_mem_Ioo]
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
h₀ h₁ : LocallyFiniteOrderTop α
obtain :
  ∀ (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 α } =
      h₁
⊢ h₀ = h₁

Tactic:
obtain ⟨h₀_finset_Ioi, h₀_finset_Ici, h₀_finset_mem_Ici, h₀_finset_mem_Ioi⟩ := h₀
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
h₁ : LocallyFiniteOrderTop α
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
obtain :
  ∀ (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 }
⊢ { finsetIoi := h₀_finset_Ioi, finsetIci := h₀_finset_Ici, finset_mem_Ici := h₀_finset_mem_Ici,
      finset_mem_Ioi := h₀_finset_mem_Ioi : LocallyFiniteOrderTop α } =
    h₁

Tactic:
obtain ⟨h₁_finset_Ioi, h₁_finset_Ici, h₁_finset_mem_Ici, h₁_finset_mem_Ioi⟩ := h₁
-- Module: Mathlib.Order.Interval.Finset.Defs
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
h : ∀ (a b : α), b ∈ h₀_finset_Ici a ↔ b ∈ h₁_finset_Ici a
⊢ h₀_finset_Ici = h₁_finset_Ici

Tactic:
ext a b
-- Module: Mathlib.Order.Interval.Finset.Defs
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
h₁ h₂ : a ≤ b ↔ a ≤ b
⊢ b ∈ h₀_finset_Ici a ↔ b ∈ h₁_finset_Ici a

Tactic:
rw [h₀_finset_mem_Ici, h₁_finset_mem_Ici]
-- Module: Mathlib.Order.Interval.Finset.Defs
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
⊢ 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]
-- Module: Mathlib.Order.Interval.Finset.Defs
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 : ∀ (a b : α), b ∈ h₀_finset_Ioi a ↔ b ∈ h₁_finset_Ioi a
⊢ h₀_finset_Ioi = h₁_finset_Ioi

Tactic:
ext a b
-- Module: Mathlib.Order.Interval.Finset.Defs
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
h₁ h₂ : a < b ↔ a < b
⊢ b ∈ h₀_finset_Ioi a ↔ b ∈ h₁_finset_Ioi a

Tactic:
rw [h₀_finset_mem_Ioi, h₁_finset_mem_Ioi]
-- Module: Mathlib.Order.Interval.Finset.Defs
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

Tactic:
have hIoi : h₀_finset_Ioi = h₁_finset_Ioi := by
      ext a b
      rw [h₀_finset_mem_Ioi, h₁_finset_mem_Ioi]
-- Module: Mathlib.Order.Interval.Finset.Defs
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
simp_rw :
  { finsetIoi := h₀_finset_Ioi, finsetIci := h₁_finset_Ici, 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 }
⊢ { 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 }

Tactic:
simp_rw [hIci, hIoi]
-- Module: Mathlib.Order.Interval.Finset.Defs
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
rw₃ rw₄ : a ≤ x ∧ x ≤ 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

Tactic:
rw [mem_preimage, mem_Icc, f.le_iff_le, f.le_iff_le]

Premises used: Finset.mem_Icc, Finset.mem_preimage, OrderEmbedding.le_iff_le
-- Module: Mathlib.Order.Interval.Finset.Defs
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
rw₃ rw₄ : a ≤ x ∧ x < 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

Tactic:
rw [mem_preimage, mem_Ico, f.le_iff_le, f.lt_iff_lt]

Premises used: Finset.mem_preimage, OrderEmbedding.lt_iff_lt, OrderEmbedding.le_iff_le, Finset.mem_Ico
-- Module: Mathlib.Order.Interval.Finset.Defs
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
rw₃ rw₄ : a < x ∧ x ≤ 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

Tactic:
rw [mem_preimage, mem_Ioc, f.lt_iff_lt, f.le_iff_le]

Premises used: Finset.mem_preimage, Finset.mem_Ioc, OrderEmbedding.lt_iff_lt, OrderEmbedding.le_iff_le
-- Module: Mathlib.Order.Interval.Finset.Defs
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
rw₃ rw₄ : a < x ∧ x < 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

Tactic:
rw [mem_preimage, mem_Ioo, f.lt_iff_lt, f.lt_iff_lt]

Premises used: Finset.mem_Ioo, Finset.mem_preimage, OrderEmbedding.lt_iff_lt
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : αᵒᵈ
⊢ Icc a b = map (Equiv.toEmbedding toDual) (Icc ((ofDual : (a : αᵒᵈ) → α) b) ((ofDual : (a : αᵒᵈ) → α) a))

Tactic:
map_refl.symm

Premises used: Finset.Icc, Finset.map_refl, OrderDual, Eq.symm, Function.Embedding.refl
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : αᵒᵈ
⊢ Ico a b = map (Equiv.toEmbedding toDual) (Ioc ((ofDual : (a : αᵒᵈ) → α) b) ((ofDual : (a : αᵒᵈ) → α) a))

Tactic:
map_refl.symm

Premises used: Finset.map_refl, OrderDual, Eq.symm, Function.Embedding.refl, Finset.Ioc
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : αᵒᵈ
⊢ Ioo a b = map (Equiv.toEmbedding toDual) (Ioo ((ofDual : (a : αᵒᵈ) → α) b) ((ofDual : (a : αᵒᵈ) → α) a))

Tactic:
map_refl.symm

Premises used: Finset.map_refl, OrderDual, Eq.symm, Function.Embedding.refl, Finset.Ioo
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ Icc ((toDual : (a : α) → αᵒᵈ) a) ((toDual : (a : α) → αᵒᵈ) b) = map (Equiv.toEmbedding toDual) (Icc b a)

Tactic:
map_refl.symm

Premises used: Finset.Icc, Finset.map_refl, OrderDual, Eq.symm, Function.Embedding.refl
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ Ico ((toDual : (a : α) → αᵒᵈ) a) ((toDual : (a : α) → αᵒᵈ) b) = map (Equiv.toEmbedding toDual) (Ioc b a)

Tactic:
map_refl.symm

Premises used: Finset.map_refl, OrderDual, Eq.symm, Function.Embedding.refl, Finset.Ioc
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ Ioo ((toDual : (a : α) → αᵒᵈ) a) ((toDual : (a : α) → αᵒᵈ) b) = map (Equiv.toEmbedding toDual) (Ioo b a)

Tactic:
map_refl.symm

Premises used: Finset.map_refl, OrderDual, Eq.symm, Function.Embedding.refl, Finset.Ioo
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : αᵒᵈ
⊢ Icc ((ofDual : (a : αᵒᵈ) → α) a) ((ofDual : (a : αᵒᵈ) → α) b) = map (Equiv.toEmbedding ofDual) (Icc b a)

Tactic:
map_refl.symm

Premises used: Finset.Icc, Finset.map_refl, OrderDual, Eq.symm, Function.Embedding.refl
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : αᵒᵈ
⊢ Ico ((ofDual : (a : αᵒᵈ) → α) a) ((ofDual : (a : αᵒᵈ) → α) b) = map (Equiv.toEmbedding ofDual) (Ioc b a)

Tactic:
map_refl.symm

Premises used: Finset.Ico, Finset.map_refl, OrderDual, Eq.symm, Function.Embedding.refl, Finset.Ioc
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : αᵒᵈ
⊢ Ioo ((ofDual : (a : αᵒᵈ) → α) a) ((ofDual : (a : αᵒᵈ) → α) b) = map (Equiv.toEmbedding ofDual) (Ioo b a)

Tactic:
map_refl.symm

Premises used: Finset.map_refl, OrderDual, Eq.symm, Function.Embedding.refl, Finset.Ioo
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a : αᵒᵈ
⊢ Iic a = map (Equiv.toEmbedding toDual) (Ici ((ofDual : (a : αᵒᵈ) → α) a))

Tactic:
map_refl.symm

Premises used: Finset.Ici, Finset.map_refl, OrderDual, Eq.symm, Function.Embedding.refl
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a : αᵒᵈ
⊢ Iio a = map (Equiv.toEmbedding toDual) (Ioi ((ofDual : (a : αᵒᵈ) → α) a))

Tactic:
map_refl.symm

Premises used: Finset.Ioi, Finset.map_refl, OrderDual, Eq.symm, Function.Embedding.refl
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a : α
⊢ Iic ((toDual : (a : α) → αᵒᵈ) a) = map (Equiv.toEmbedding toDual) (Ici a)

Tactic:
map_refl.symm

Premises used: Finset.Ici, Finset.map_refl, OrderDual, Eq.symm, Function.Embedding.refl
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a : α
⊢ Iio ((toDual : (a : α) → αᵒᵈ) a) = map (Equiv.toEmbedding toDual) (Ioi a)

Tactic:
map_refl.symm

Premises used: Finset.Ioi, Finset.map_refl, OrderDual, Eq.symm, Function.Embedding.refl
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a : αᵒᵈ
⊢ Ici ((ofDual : (a : αᵒᵈ) → α) a) = map (Equiv.toEmbedding ofDual) (Iic a)

Tactic:
map_refl.symm

Premises used: Finset.Ici, Finset.map_refl, Finset.Iic, OrderDual, Eq.symm, Function.Embedding.refl
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a : αᵒᵈ
⊢ Ioi ((ofDual : (a : αᵒᵈ) → α) a) = map (Equiv.toEmbedding ofDual) (Iio a)

Tactic:
map_refl.symm

Premises used: Finset.Ioi, Finset.Iio, Finset.map_refl, OrderDual, Eq.symm, Function.Embedding.refl
-- Module: Mathlib.Order.Interval.Finset.Defs
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
rw₅ 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
⊢ Membership.mem (γ := Finset (α × β)) ((fun (x y : α × β) ↦ Icc x.1 y.1 ×ˢ Icc x.2 y.2) a b) x ↔ a ≤ x ∧ x ≤ b

Tactic:
rw [mem_product, mem_Icc, mem_Icc, and_and_and_comm, le_def, le_def]

Premises used: Finset.mem_Icc, and_and_and_comm, Finset.mem_product, Prod.le_def
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : DecidableLE (α × β)
x y : α × β
⊢ Icc x y = Icc x.1 y.1 ×ˢ Icc x.2 y.2

Tactic:
rfl

Premises used: Finset.Icc, rfl
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : DecidableLE (α × β)
a₁ a₂ : α
b₁ b₂ : β
⊢ Icc a₁ a₂ ×ˢ Icc b₁ b₂ = Icc (a₁, b₁) (a₂, b₂)

Tactic:
rfl

Premises used: Finset.Icc, rfl
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : DecidableLE (α × β)
x y : α × β
⊢ #(Icc x y) = #(Icc x.1 y.1) * #(Icc x.2 y.2)

Tactic:
card_product ..

Premises used: Finset.card_product, Finset.Icc
-- Module: Mathlib.Order.Interval.Finset.Defs
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
rw₃ rw₄ : a.1 ≤ x.1 ∧ a.2 ≤ x.2 ↔ a.1 ≤ x.1 ∧ a.2 ≤ x.2
⊢ Membership.mem (γ := Finset (α × β)) ((fun (x : α × β) ↦ Ici x.1 ×ˢ Ici x.2) a) x ↔ a ≤ x

Tactic:
rw [mem_product, mem_Ici, mem_Ici, le_def]

Premises used: Finset.mem_Ici, Finset.mem_product, Prod.le_def
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrderTop α
inst_3 : LocallyFiniteOrderTop β
inst_4 : DecidableLE (α × β)
x : α × β
⊢ Ici x = Ici x.1 ×ˢ Ici x.2

Tactic:
rfl

Premises used: Finset.Ici, rfl
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrderTop α
inst_3 : LocallyFiniteOrderTop β
inst_4 : DecidableLE (α × β)
a : α
b : β
⊢ Ici a ×ˢ Ici b = Ici (a, b)

Tactic:
rfl

Premises used: Finset.Ici, rfl
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrderTop α
inst_3 : LocallyFiniteOrderTop β
inst_4 : DecidableLE (α × β)
x : α × β
⊢ #(Ici x) = #(Ici x.1) * #(Ici x.2)

Tactic:
card_product _ _

Premises used: Finset.card_product, Finset.Ici
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Lattice α
inst_1 : Lattice β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : DecidableLE (α × β)
x y : α × β
⊢ uIcc x y = uIcc x.1 y.1 ×ˢ uIcc x.2 y.2

Tactic:
rfl

Premises used: Finset.Icc, rfl, Finset.uIcc
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Lattice α
inst_1 : Lattice β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : DecidableLE (α × β)
a₁ a₂ : α
b₁ b₂ : β
⊢ uIcc a₁ a₂ ×ˢ uIcc b₁ b₂ = uIcc (a₁, b₁) (a₂, b₂)

Tactic:
rfl

Premises used: Finset.Icc, rfl, Finset.uIcc
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Lattice α
inst_1 : Lattice β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : DecidableLE (α × β)
x y : α × β
⊢ #(uIcc x y) = #(uIcc x.1 y.1) * #(uIcc x.2 y.2)

Tactic:
card_product ..

Premises used: Finset.card_product, Finset.Icc, Finset.uIcc
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
s : Finset α
⊢ ⊤ ∉ Finset.map Embedding.coeWithTop s

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
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
rw₃ 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

Tactic:
rw [le_iff_subset, cons_subset_cons, map_subset_map, le_iff_subset]

Premises used: Finset.cons_subset_cons, Finset.le_iff_subset, Finset.map_subset_map
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
s : Finset α
a : α
⊢ Membership.mem (γ := Finset (WithTop α)) ((insertTop : (a : Finset α) → Finset (WithTop α)) s : Finset (WithTop α))
      (↑a : WithTop α) ↔
    a ∈ s

Tactic:
simp [insertTop]

Premises used: WithTop.insertTop
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
s : Finset α
⊢ Membership.mem (γ := Finset (WithTop α)) ((insertTop : (a : Finset α) → Finset (WithTop α)) s : Finset (WithTop α)) ⊤

Tactic:
simp [insertTop]

Premises used: WithTop.insertTop
-- Module: Mathlib.Order.Interval.Finset.Defs
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
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
⊢ 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

Tactic:
cases a