awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Icc a b ↔ x ≤ b ∧ a ≤ x

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ico a b ↔ x < b ∧ a ≤ x

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ioc a b ↔ x ≤ b ∧ a < x

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ioo a b ↔ x < b ∧ a < x

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ (↑(Icc a b) : Set α) = Set.Icc a b

Tactic:
Set.ext fun _ => mem_Icc

Premises used: Set.ext, Finset.mem_Icc
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ (↑(Ico a b) : Set α) = Set.Ico a b

Tactic:
Set.ext fun _ => mem_Ico

Premises used: Set.ext, Finset.mem_Ico
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ (↑(Ioo a b) : Set α) = Set.Ioo a b

Tactic:
Set.ext fun _ => mem_Ioo

Premises used: Set.ext, Finset.mem_Ioo
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : Fintype (↑(Set.Icc a b) : Type u_1)
x : α
⊢ x ∈ Icc a b ↔ x ∈ Set.Icc a b

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : Fintype (↑(Set.Ico a b) : Type u_1)
x : α
⊢ x ∈ Ico a b ↔ x ∈ Set.Ico a b

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : Fintype (↑(Set.Ioo a b) : Type u_1)
x : α
⊢ x ∈ Ioo a b ↔ x ∈ Set.Ioo a b

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a x : α
⊢ x ∈ Ici a ↔ a ≤ x

Tactic:
LocallyFiniteOrderTop.finset_mem_Ici _ _

Premises used: Set.Mem, setOf, LocallyFiniteOrderTop.finset_mem_Ici
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a x : α
⊢ x ∈ Ioi a ↔ a < x

Tactic:
LocallyFiniteOrderTop.finset_mem_Ioi _ _

Premises used: Set.Mem, setOf, LocallyFiniteOrderTop.finset_mem_Ioi
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a : α
⊢ (↑(Ici a) : Set α) = Set.Ici a

Tactic:
Set.ext fun _ => mem_Ici

Premises used: Set.ext, Finset.mem_Ici
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a : α
⊢ (↑(Ioi a) : Set α) = Set.Ioi a

Tactic:
Set.ext fun _ => mem_Ioi

Premises used: Set.ext, Finset.mem_Ioi
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a : α
inst_2 : Fintype (↑(Set.Ici a) : Type u_1)
x : α
⊢ x ∈ Ici a ↔ x ∈ Set.Ici a

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a : α
inst_2 : Fintype (↑(Set.Ioi a) : Type u_1)
x : α
⊢ x ∈ Ioi a ↔ x ∈ Set.Ioi a

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
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
rw₁ rw₂ : a ≤ x ↔ a ≤ x
⊢ x ∈ Icc a ⊤ ↔ a ≤ x

Tactic:
rw [mem_Icc, and_iff_left le_top]

Premises used: and_iff_left, Finset.mem_Icc, le_top
-- Module: Mathlib.Order.Interval.Finset.Defs
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
rw₁ rw₂ : a < x ↔ a < x
⊢ x ∈ Ioc a ⊤ ↔ a < x

Tactic:
rw [mem_Ioc, and_iff_left le_top]

Premises used: and_iff_left, le_top, Finset.mem_Ioc
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : OrderTop α
a : α
⊢ Ici a = Icc a ⊤

Tactic:
rfl

Premises used: Finset.Icc, rfl
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : OrderTop α
a : α
⊢ Ioi a = Ioc a ⊤

Tactic:
rfl

Premises used: rfl, Finset.Ioc
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a b x : α
⊢ x ∈ uIcc a b ↔ a ⊓ b ≤ x ∧ x ≤ a ⊔ b

Tactic:
mem_Icc

Premises used: Set.Mem, setOf, Finset.mem_Icc
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ (↑(uIcc a b) : Set α) = Set.uIcc a b

Tactic:
coe_Icc _ _

Premises used: setOf, Finset.coe_Icc, Set.uIcc
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : Fintype (↑(Set.uIcc a b) : Type u_1)
x : α
⊢ x ∈ uIcc a b ↔ x ∈ Set.uIcc a b

Tactic:
simp [Set.uIcc]

Premises used: Set.uIcc
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Finset.Icc a b ↔ x ∈ Icc a b

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Finset.Ico a b ↔ x ∈ Ico a b

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Finset.Ioo a b ↔ x ∈ Ioo a b

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ (Icc a b).Finite

Tactic:
(Icc a b).toFinite

Premises used: Set.toFinite, Set.Icc
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ (Ico a b).Finite

Tactic:
(Ico a b).toFinite

Premises used: Set.Ico, Set.toFinite
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ (Ioo a b).Finite

Tactic:
(Ioo a b).toFinite

Premises used: Set.toFinite, Set.Ioo
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a : α
⊢ (Ici a).Finite

Tactic:
(Ici a).toFinite

Premises used: Set.Ici, Set.toFinite
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a : α
⊢ (Ioi a).Finite

Tactic:
(Ioi a).toFinite

Premises used: Set.Ioi, Set.toFinite
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ (uIcc a b).Finite

Tactic:
(uIcc _ _).toFinite

Premises used: Set.toFinite, Set.uIcc
-- Module: Mathlib.Order.Interval.Finset.Defs
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
rw₁ rw₂ : a ≤ x ∧ x ≤ b ↔ a ≤ x ∧ x ≤ b
⊢ Membership.mem (γ := Finset α) ((fun (a b : α) ↦ ⋯.toFinset (s := Set.Icc a b)) a b) x ↔ a ≤ x ∧ x ≤ b

Tactic:
rw [Set.Finite.mem_toFinset, Set.mem_Icc]

Premises used: Set.Finite.mem_toFinset, Set.mem_Icc
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : Fintype α
inst_3 : DecidableLT α
inst_4 : DecidableLE α
a b x : α
⊢ x ∈ (Set.Icc a b).toFinset ↔ a ≤ x ∧ x ≤ b

Tactic:
simp only [Set.mem_toFinset, Set.mem_Icc]

Premises used: Set.mem_Icc, Set.mem_toFinset
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : Fintype α
inst_3 : DecidableLT α
inst_4 : DecidableLE α
a b x : α
⊢ x ∈ (Set.Ico a b).toFinset ↔ a ≤ x ∧ x < b

Tactic:
simp only [Set.mem_toFinset, Set.mem_Ico]

Premises used: Set.mem_Ico, Set.mem_toFinset
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : Fintype α
inst_3 : DecidableLT α
inst_4 : DecidableLE α
a b x : α
⊢ x ∈ (Set.Ioc a b).toFinset ↔ a < x ∧ x ≤ b

Tactic:
simp only [Set.mem_toFinset, Set.mem_Ioc]

Premises used: Set.mem_Ioc, Set.mem_toFinset
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : Fintype α
inst_3 : DecidableLT α
inst_4 : DecidableLE α
a b x : α
⊢ x ∈ (Set.Ioo a b).toFinset ↔ a < x ∧ x < b

Tactic:
simp only [Set.mem_toFinset, Set.mem_Ioo]

Premises used: Set.mem_Ioo, Set.mem_toFinset
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
h₀ h₁ : LocallyFiniteOrder α
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₁
⊢ h₀ = 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₀
-- Module: Mathlib.Order.Interval.Finset.Defs
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
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 }
⊢ { 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₁
-- 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
h : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ x ∈ h₁_finset_Icc a b
⊢ h₀_finset_Icc = h₁_finset_Icc

Tactic:
ext a b x
-- 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
a b x : α
h : a ≤ x ∧ x ≤ b ↔ x ∈ h₁_finset_Icc a b
h₁ h₂ : a ≤ x ∧ x ≤ b ↔ a ≤ x ∧ x ≤ b
⊢ x ∈ h₀_finset_Icc a b ↔ x ∈ h₁_finset_Icc a b

Tactic:
rw [h₀_finset_mem_Icc, h₁_finset_mem_Icc]
-- 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
⊢ h₀_finset_Icc = h₁_finset_Icc

Tactic:
have hIcc : h₀_finset_Icc = h₁_finset_Icc := by
      ext a b x
      rw [h₀_finset_mem_Icc, h₁_finset_mem_Icc]
-- 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
h : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ x ∈ h₁_finset_Ico a b
⊢ h₀_finset_Ico = h₁_finset_Ico

Tactic:
ext a b x
-- 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
a b x : α
h : a ≤ x ∧ x < b ↔ x ∈ h₁_finset_Ico a b
h₁ h₂ : a ≤ x ∧ x < b ↔ a ≤ x ∧ x < b
⊢ x ∈ h₀_finset_Ico a b ↔ x ∈ h₁_finset_Ico a b

Tactic:
rw [h₀_finset_mem_Ico, h₁_finset_mem_Ico]
-- 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
⊢ h₀_finset_Ico = h₁_finset_Ico

Tactic:
have hIco : h₀_finset_Ico = h₁_finset_Ico := by
      ext a b x
      rw [h₀_finset_mem_Ico, h₁_finset_mem_Ico]
-- 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
h : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ x ∈ h₁_finset_Ioc a b
⊢ h₀_finset_Ioc = h₁_finset_Ioc

Tactic:
ext a b x
-- 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
a b x : α
h : a < x ∧ x ≤ b ↔ x ∈ h₁_finset_Ioc a b
h₁ h₂ : a < x ∧ x ≤ b ↔ a < x ∧ x ≤ b
⊢ x ∈ h₀_finset_Ioc a b ↔ x ∈ h₁_finset_Ioc a b

Tactic:
rw [h₀_finset_mem_Ioc, h₁_finset_mem_Ioc]
-- 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
⊢ h₀_finset_Ioc = h₁_finset_Ioc

Tactic:
have hIoc : h₀_finset_Ioc = h₁_finset_Ioc := by
      ext a b x
      rw [h₀_finset_mem_Ioc, h₁_finset_mem_Ioc]
-- 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 : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ x ∈ h₁_finset_Ioo a b
⊢ h₀_finset_Ioo = h₁_finset_Ioo

Tactic:
ext a b x
-- 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
a b x : α
h : a < x ∧ x < b ↔ x ∈ h₁_finset_Ioo a b
h₁ h₂ : a < x ∧ x < b ↔ a < x ∧ x < b
⊢ x ∈ h₀_finset_Ioo a b ↔ x ∈ h₁_finset_Ioo a b

Tactic:
rw [h₀_finset_mem_Ioo, h₁_finset_mem_Ioo]