awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : Preorder β
f : α → β
refine : ∀ (h : ∀ (a b : α), a ⩿ b → f a ≤ f b) (a b : α) (hab : a ≤ b), f a ≤ f b
⊢ Monotone f ↔ ∀ (a b : α), a ⩿ b → f a ≤ f b

Tactic:
refine ⟨fun hf _ _ h ↦ hf h.le, fun h a b hab ↦ ?_⟩
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : Preorder β
f : α → β
h : ∀ (a b : α), a ⩿ b → f a ≤ f b
a b : α
hab : a ≤ b
⊢ f a ≤ f b

Tactic:
simpa [transGen_eq_self] using TransGen.lift f h <| le_iff_transGen_wcovBy.mp hab

Premises used: le_iff_transGen_wcovBy, Relation.transGen_eq_self, Iff.mp, Relation.TransGen.lift
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : Preorder β
f : α → β
⊢ Monotone f ↔ ∀ (a b : α), a ⋖ b → f a ≤ f b

Tactic:
⟨fun hf _ _ h ↦ hf h.le, fun h a b hab ↦ ?_⟩

Premises used: Iff.intro, CovBy.le
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : Preorder β
f : α → β
refine : ∀ (h : ∀ (a b : α), a ⋖ b → f a ≤ f b) (a b : α) (hab : a ≤ b), f a ≤ f b
⊢ Monotone f ↔ ∀ (a b : α), a ⋖ b → f a ≤ f b

Tactic:
refine ⟨fun hf _ _ h ↦ hf h.le, fun h a b hab ↦ ?_⟩
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : Preorder β
f : α → β
h : ∀ (a b : α), a ⋖ b → f a ≤ f b
a b : α
hab : a ≤ b
⊢ f a ≤ f b

Tactic:
simpa [reflTransGen_eq_self] using ReflTransGen.lift f h <| le_iff_reflTransGen_covBy.mp hab

Premises used: Relation.ReflTransGen.lift, Relation.reflTransGen_eq_self, le_iff_reflTransGen_covBy, Iff.mp
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : Preorder β
f : α → β
⊢ StrictMono f ↔ ∀ (a b : α), a ⋖ b → f a < f b

Tactic:
⟨fun hf _ _ h ↦ hf h.lt, fun h a b hab ↦ ?_⟩

Premises used: Iff.intro, CovBy.lt
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : Preorder β
f : α → β
refine : ∀ (h : ∀ (a b : α), a ⋖ b → f a < f b) (a b : α) (hab : a < b), f a < f b
⊢ StrictMono f ↔ ∀ (a b : α), a ⋖ b → f a < f b

Tactic:
refine ⟨fun hf _ _ h ↦ hf h.lt, fun h a b hab ↦ ?_⟩
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : Preorder β
f : α → β
h : ∀ (a b : α), a ⋖ b → f a < f b
a b : α
hab : a < b
⊢ ∀ (hab : TransGen CovBy a b), TransGen LT.lt (f a) (f b)

Tactic:
have := Relation.TransGen.lift f h (a := a) (b := b)
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : Preorder β
f : α → β
h : ∀ (a b : α), a ⋖ b → f a < f b
a b : α
hab : a < b
this : ∀ (hab : TransGen CovBy a b), TransGen LT.lt (f a) (f b)
⊢ ∀ (hab : a < b), f a < f b

Tactic:
rw [← lt_iff_transGen_covBy, transGen_eq_self] at this

Premises used: lt_iff_transGen_covBy, Relation.transGen_eq_self
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : Preorder β
f : α → β
h : ∀ (a b : α), a ⋖ b → f a < f b
a b : α
hab : a < b
this : ∀ (hab : a < b), f a < f b
⊢ f a < f b

Tactic:
this hab
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : Preorder β
f : α → β
h : ∀ (a b : α), a ⋖ b → f a < f b
a b : α
hab : a < b
this : ∀ (hab : a < b), f a < f b
⊢ f a < f b

Tactic:
exact this hab
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : Preorder β
f : α → β
⊢ Antitone f ↔ ∀ (a b : α), a ⩿ b → f b ≤ f a

Tactic:
monotone_iff_forall_wcovBy (β := βᵒᵈ) f

Premises used: Antitone, monotone_iff_forall_wcovBy
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : Preorder β
f : α → β
⊢ Antitone f ↔ ∀ (a b : α), a ⋖ b → f b ≤ f a

Tactic:
monotone_iff_forall_covBy (β := βᵒᵈ) f

Premises used: Antitone, monotone_iff_forall_covBy
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : Preorder β
f : α → β
⊢ StrictAnti f ↔ ∀ (a b : α), a ⋖ b → f b < f a

Tactic:
strictMono_iff_forall_covBy (β := βᵒᵈ) f

Premises used: strictMono_iff_forall_covBy, StrictAnti
-- Module: Mathlib.Order.Interval.Finset.Box
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : LocallyFiniteOrder α
m n : ℕ
hmn : m ≤ n
ha : LE.le.{u_1} (α := α) (-(↑n : α)) (-(↑m : α))
hb : LE.le.{u_1} (α := α) (↑m : α) (↑n : α)
⊢ LE.le.{u_1} (α := Finset α) ((fun (n : ℕ) ↦ (Icc (-(↑n : α)) (↑n : α) : Finset α)) m)
    ((fun (n : ℕ) ↦ (Icc (-(↑n : α)) (↑n : α) : Finset α)) n)

Tactic:
apply Icc_subset_Icc

Premises used: Finset.Icc_subset_Icc
-- Module: Mathlib.Order.Interval.Finset.Box
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : LocallyFiniteOrder α
m n : ℕ
hmn : m ≤ n
⊢ LE.le.{u_1} (α := α) (-(↑n : α)) (-(↑m : α))

Tactic:
simpa using Nat.mono_cast hmn

Premises used: Nat.mono_cast
-- Module: Mathlib.Order.Interval.Finset.Box
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : LocallyFiniteOrder α
m n : ℕ
hmn : m ≤ n
⊢ LE.le.{u_1} (α := α) (↑m : α) (↑n : α)

Tactic:
simpa using Nat.mono_cast hmn

Premises used: Nat.mono_cast
-- Module: Mathlib.Order.Interval.Finset.Box
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : LocallyFiniteOrder α
⊢ Monotone.{0, u_1} (β := Finset α) fun (n : ℕ) ↦ Icc (-(↑n : α)) (↑n : α)

Tactic:
refine fun m n hmn ↦ by apply Icc_subset_Icc <;> simpa using Nat.mono_cast hmn
-- Module: Mathlib.Order.Interval.Finset.Box
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
⊢ Eq (α := Finset α) (box 0) {0}

Tactic:
simp [box]

Premises used: Finset.box
-- Module: Mathlib.Order.Interval.Finset.Box
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
n : ℕ
rw :
  Eq.{u_1 + 1} (α := Finset α) (Icc (-(↑(n + 1) : α)) (↑(n + 1) : α) \ Icc (-(↑n : α)) (↑n : α))
    (Icc (-(↑n.succ : α)) (↑n.succ : α) \ Icc (-(↑n : α)) (↑n : α))
⊢ Eq.{u_1 + 1} (α := Finset α) (box (n + 1)) (Icc (-(↑n.succ : α)) (↑n.succ : α) \ Icc (-(↑n : α)) (↑n : α))

Tactic:
rw [box, Icc_neg_mono.disjointed_add_one]

Premises used: Monotone.disjointed_add_one, Finset.box
-- Module: Mathlib.Order.Interval.Finset.Box
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
n : ℕ
⊢ Eq.{u_1 + 1} (α := Finset α) (Icc (-(↑(n + 1) : α)) (↑(n + 1) : α) \ Icc (-(↑n : α)) (↑n : α))
    (Icc (-(↑n.succ : α)) (↑n.succ : α) \ Icc (-(↑n : α)) (↑n : α))

Tactic:
simp only [Nat.cast_add_one, Nat.succ_eq_add_one]

Premises used: Nat.succ_eq_add_one, Nat.cast_add_one
-- Module: Mathlib.Order.Interval.Finset.Box
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
n : ℕ
rw :
  Disjoint.{u_1} (α := Finset α) (Icc (-(↑n.succ : α)) (↑n.succ : α) \ Icc (-(↑n : α)) (↑n : α))
    (Icc (-(↑n : α)) (↑n : α))
⊢ Disjoint.{u_1} (α := Finset α) (box (n + 1)) (Icc (-(↑n : α)) (↑n : α))

Tactic:
rw [box_succ_eq_sdiff]

Premises used: Finset.box_succ_eq_sdiff
-- Module: Mathlib.Order.Interval.Finset.Box
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
n : ℕ
⊢ Disjoint.{u_1} (α := Finset α) (Icc (-(↑n.succ : α)) (↑n.succ : α) \ Icc (-(↑n : α)) (↑n : α))
    (Icc (-(↑n : α)) (↑n : α))

Tactic:
disjoint_sdiff_self_left

Premises used: disjoint_sdiff_self_left
-- Module: Mathlib.Order.Interval.Finset.Box
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
n : ℕ
⊢ Disjoint.{u_1} (α := Finset α) (Icc (-(↑n.succ : α)) (↑n.succ : α) \ Icc (-(↑n : α)) (↑n : α))
    (Icc (-(↑n : α)) (↑n : α))

Tactic:
exact disjoint_sdiff_self_left

Premises used: disjoint_sdiff_self_left
-- Module: Mathlib.Order.Interval.Finset.Box
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
n : ℕ
⊢ Eq.{u_1 + 1} (α := Finset α) (box (n + 1) ∪ Icc (-(↑n : α)) (↑n : α)) (Icc (-(↑n.succ : α)) (↑n.succ : α))

Tactic:
Icc_neg_mono.disjointed_add_one_sup _

Premises used: Monotone.disjointed_add_one_sup
-- Module: Mathlib.Order.Interval.Finset.Box
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
n : ℕ
rw : Eq.{u_1 + 1} (α := Finset α) (box (n + 1) ∪ Icc (-(↑n : α)) (↑n : α)) (Icc (-(↑n.succ : α)) (↑n.succ : α))
rw₁ rw₂ : Eq.{u_1 + 1} (α := Finset α) (Icc (-(↑n.succ : α)) (↑n.succ : α)) (Icc (-(↑n.succ : α)) (↑n.succ : α))
⊢ Eq.{u_1 + 1} (α := Finset α) (disjUnion (box (n + 1)) (Icc (-(↑n : α)) (↑n : α)) ⋯)
    (Icc (-(↑n.succ : α)) (↑n.succ : α))

Tactic:
rw [disjUnion_eq_union, box_succ_union_prod]

Premises used: Finset.disjUnion_eq_union, Finset.box_succ_union_prod
-- Module: Mathlib.Order.Interval.Finset.Box
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : LocallyFiniteOrder α
n : ℕ
inst_4 : DecidableEq α
zero : Membership.mem (γ := Finset α) (box 0) 0 ↔ Eq (α := ℕ) 0 0
succ : ∀ (n : ℕ), Membership.mem (γ := Finset α) (box (n + 1)) 0 ↔ n + 1 = 0
⊢ Membership.mem (γ := Finset α) (box n) 0 ↔ n = 0

Tactic:
cases n
-- Module: Mathlib.Order.Interval.Finset.Box
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
⊢ Membership.mem (γ := Finset α) (box 0) 0 ↔ Eq (α := ℕ) 0 0

Tactic:
simp [box_succ_eq_sdiff]

Premises used: Finset.box_succ_eq_sdiff
-- Module: Mathlib.Order.Interval.Finset.Box
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
n : ℕ
⊢ Membership.mem (γ := Finset α) (box (n + 1)) 0 ↔ n + 1 = 0

Tactic:
simp [box_succ_eq_sdiff]

Premises used: Finset.box_succ_eq_sdiff
-- Module: Mathlib.Order.Interval.Finset.Box
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : LocallyFiniteOrder α
n : ℕ
inst_4 : DecidableEq α
x : α
hx : Membership.mem (γ := Finset α) (box n) x
hn : n = 0
rwa : ∀ (hx : Membership.mem (γ := Finset α) (box 0) x) (hn : n = 0), x = 0
rwa₁ : ∀ (hx : Membership.mem (γ := Finset α) {0} x) (hn : n = 0), x = 0
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (hx : x = 0) (hn : n = 0), x = 0
⊢ x = 0

Tactic:
rwa [hn, box_zero, mem_singleton] at hx

Premises used: Finset.mem_singleton, Finset.box_zero
-- Module: Mathlib.Order.Interval.Finset.Box
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : Ring β
inst_4 : PartialOrder β
inst_5 : IsOrderedRing β
inst_6 : LocallyFiniteOrder α
inst_7 : LocallyFiniteOrder β
inst_8 : DecidableEq α
inst_9 : DecidableEq β
inst_10 : DecidableLE (α × β)
n : ℕ
rw :
  card.{u_1} (α := α) (Icc (-(↑n.succ : α × β)).1 (↑n.succ : α × β).1) *
        card.{u_2} (α := β) (Icc (-(↑n.succ : α × β)).2 (↑n.succ : α × β).2) -
      card.{u_1} (α := α) (Icc (-(↑n : α × β)).1 (↑n : α × β).1) *
        card.{u_2} (α := β) (Icc (-(↑n : α × β)).2 (↑n : α × β).2) =
    card.{u_1} (α := α) (Icc (-(↑n.succ : α)) (↑n.succ : α)) *
        card.{u_2} (α := β) (Icc (-(↑n.succ : β)) (↑n.succ : β)) -
      card.{u_1} (α := α) (Icc (-(↑n : α)) (↑n : α)) * card.{u_2} (α := β) (Icc (-(↑n : β)) (↑n : β))
⊢ card (α := α × β) (box (n + 1)) =
    card.{u_1} (α := α) (Icc (-(↑n.succ : α)) (↑n.succ : α)) *
        card.{u_2} (α := β) (Icc (-(↑n.succ : β)) (↑n.succ : β)) -
      card.{u_1} (α := α) (Icc (-(↑n : α)) (↑n : α)) * card.{u_2} (α := β) (Icc (-(↑n : β)) (↑n : β))

Tactic:
rw [box_succ_eq_sdiff, card_sdiff_of_subset (Icc_neg_mono n.le_succ), Finset.card_Icc_prod,
    Finset.card_Icc_prod]

Premises used: Finset.card_sdiff_of_subset, Nat.le_succ, _private.0.Finset.Icc_neg_mono, Finset.box_succ_eq_sdiff, Finset.card_Icc_prod
-- Module: Mathlib.Order.Interval.Finset.Box
Goal:
n : ℕ
h : n + 1 ≠ 0
simp_rw :
  (HAdd.hAdd (α := ℤ) (↑n.succ : ℤ) 1 + (↑n.succ : ℤ)).toNat *
        (HAdd.hAdd (α := ℤ) (↑n.succ : ℤ) 1 + (↑n.succ : ℤ)).toNat -
      (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + (↑n : ℤ)).toNat * (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + (↑n : ℤ)).toNat =
    8 * (n + 1)
⊢ card (α := ℤ × ℤ) (box (n + 1)) = 8 * (n + 1)

Tactic:
simp_rw [Prod.card_box_succ, card_Icc, sub_neg_eq_add]

Premises used: Int.card_Icc, Prod.card_box_succ, sub_neg_eq_add
-- Module: Mathlib.Order.Interval.Finset.Box
Goal:
n : ℕ
h : n + 1 ≠ 0
⊢ (n.succ + 1 + n.succ) * (n.succ + 1 + n.succ) - (n + 1 + n) * (n + 1 + n) = 8 * (n + 1)

Tactic:
tsub_eq_of_eq_add ?_

Premises used: tsub_eq_of_eq_add
-- Module: Mathlib.Order.Interval.Finset.Box
Goal:
n : ℕ
h : n + 1 ≠ 0
refine : (n.succ + 1 + n.succ) * (n.succ + 1 + n.succ) = 8 * (n + 1) + (n + 1 + n) * (n + 1 + n)
⊢ (n.succ + 1 + n.succ) * (n.succ + 1 + n.succ) - (n + 1 + n) * (n + 1 + n) = 8 * (n + 1)

Tactic:
refine tsub_eq_of_eq_add ?_

Premises used: tsub_eq_of_eq_add
-- Module: Mathlib.Order.Interval.Finset.Box
Goal:
n : ℕ
h : n + 1 ≠ 0
zify :
  (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 + HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) *
      (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 + HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    8 * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 +
      (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + (↑n : ℤ)) * (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + (↑n : ℤ))
⊢ (n.succ + 1 + n.succ) * (n.succ + 1 + n.succ) = 8 * (n + 1) + (n + 1 + n) * (n + 1 + n)

Tactic:
zify
-- Module: Mathlib.Order.Interval.Finset.Box
Goal:
n : ℕ
h : n + 1 ≠ 0
⊢ (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 + HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) *
      (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 + HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    8 * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 +
      (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + (↑n : ℤ)) * (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + (↑n : ℤ))

Tactic:
ring
-- Module: Mathlib.Order.Interval.Finset.Box
Goal:
x : ℤ × ℤ
⊢ Membership.mem (γ := Finset (ℤ × ℤ)) (box 0) x ↔ max x.1.natAbs x.2.natAbs = 0

Tactic:
simp [Prod.ext_iff]

Premises used: Prod.ext_iff
-- Module: Mathlib.Order.Interval.Finset.Box
Goal:
x : ℤ × ℤ
n : ℕ
simp :
  ((-1 ≤ x.1 + (↑n : ℤ) ∧ -1 ≤ x.2 + (↑n : ℤ)) ∧
        x.1 ≤ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ∧ x.2 ≤ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) ∧
      (-(↑n : ℤ) ≤ x.1 → -(↑n : ℤ) ≤ x.2 → x.1 ≤ (↑n : ℤ) → (↑n : ℤ) < x.2) ↔
    max x.1.natAbs x.2.natAbs = n + 1
⊢ Membership.mem (γ := Finset (ℤ × ℤ)) (box (n + 1)) x ↔ max x.1.natAbs x.2.natAbs = n + 1

Tactic:
simp [box_succ_eq_sdiff, Prod.le_def]

Premises used: Finset.box_succ_eq_sdiff, Prod.le_def
-- Module: Mathlib.Order.Interval.Finset.Box
Goal:
x : ℤ × ℤ
n : ℕ
⊢ ((-1 ≤ x.1 + (↑n : ℤ) ∧ -1 ≤ x.2 + (↑n : ℤ)) ∧
        x.1 ≤ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ∧ x.2 ≤ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) ∧
      (-(↑n : ℤ) ≤ x.1 → -(↑n : ℤ) ≤ x.2 → x.1 ≤ (↑n : ℤ) → (↑n : ℤ) < x.2) ↔
    max x.1.natAbs x.2.natAbs = n + 1

Tactic:
omega
-- Module: Mathlib.Order.Interval.Finset.Box
Goal:
x : ℤ × ℤ
h :
  (fun (n : ℕ) ↦ Membership.mem (γ := Finset (ℤ × ℤ)) (box n) x) (max x.1.natAbs x.2.natAbs) ∧
    ∀ (y : ℕ), (fun (n : ℕ) ↦ Membership.mem (γ := Finset (ℤ × ℤ)) (box n) x) y → y = max x.1.natAbs x.2.natAbs
⊢ ∃! n : ℕ, Membership.mem (γ := Finset (ℤ × ℤ)) (box n) x

Tactic:
use max x.1.natAbs x.2.natAbs

Premises used: Prod.fst, Max.max, Int.natAbs, Prod.snd
-- Module: Mathlib.Order.Interval.Finset.Box
Goal:
x : ℤ × ℤ
⊢ (fun (n : ℕ) ↦ Membership.mem (γ := Finset (ℤ × ℤ)) (box n) x) (max x.1.natAbs x.2.natAbs) ∧
    ∀ (y : ℕ), (fun (n : ℕ) ↦ Membership.mem (γ := Finset (ℤ × ℤ)) (box n) x) y → y = max x.1.natAbs x.2.natAbs

Tactic:
simp only [mem_box, and_self_iff, forall_eq']

Premises used: forall_eq', Int.mem_box, and_self_iff
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
finsetIcc finsetIco finsetIoc finsetIoo : α → α → Finset α
finset_mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ x ≤ a ∧ b ≤ x
finset_mem_Ico : ∀ (a b x : α), x ∈ finsetIco a b ↔ x ≤ a ∧ b < x
finset_mem_Ioc : ∀ (a b x : α), x ∈ finsetIoc a b ↔ x < a ∧ b ≤ x
finset_mem_Ioo : ∀ (a b x : α), x ∈ finsetIoo a b ↔ x < a ∧ b < x
⊢ ∀ (a b x : α), x ∈ swap (φ := fun (a a_1 : α) ↦ Finset α) finsetIcc a b ↔ a ≤ x ∧ x ≤ b

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
finsetIcc finsetIco finsetIoc finsetIoo : α → α → Finset α
finset_mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ x ≤ a ∧ b ≤ x
finset_mem_Ico : ∀ (a b x : α), x ∈ finsetIco a b ↔ x ≤ a ∧ b < x
finset_mem_Ioc : ∀ (a b x : α), x ∈ finsetIoc a b ↔ x < a ∧ b ≤ x
finset_mem_Ioo : ∀ (a b x : α), x ∈ finsetIoo a b ↔ x < a ∧ b < x
⊢ ∀ (a b x : α), x ∈ swap (φ := fun (a a_1 : α) ↦ Finset α) finsetIoc a b ↔ a ≤ x ∧ x < b

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
finsetIcc finsetIco finsetIoc finsetIoo : α → α → Finset α
finset_mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ x ≤ a ∧ b ≤ x
finset_mem_Ico : ∀ (a b x : α), x ∈ finsetIco a b ↔ x ≤ a ∧ b < x
finset_mem_Ioc : ∀ (a b x : α), x ∈ finsetIoc a b ↔ x < a ∧ b ≤ x
finset_mem_Ioo : ∀ (a b x : α), x ∈ finsetIoo a b ↔ x < a ∧ b < x
⊢ ∀ (a b x : α), x ∈ swap (φ := fun (a a_1 : α) ↦ Finset α) finsetIco a b ↔ a < x ∧ x ≤ b

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
finsetIcc finsetIco finsetIoc finsetIoo : α → α → Finset α
finset_mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ x ≤ a ∧ b ≤ x
finset_mem_Ico : ∀ (a b x : α), x ∈ finsetIco a b ↔ x ≤ a ∧ b < x
finset_mem_Ioc : ∀ (a b x : α), x ∈ finsetIoc a b ↔ x < a ∧ b ≤ x
finset_mem_Ioo : ∀ (a b x : α), x ∈ finsetIoo a b ↔ x < a ∧ b < x
⊢ ∀ (a b x : α), x ∈ swap (φ := fun (a a_1 : α) ↦ Finset α) finsetIoo a b ↔ a < x ∧ x < b

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Defs
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
rw₃ rw₄ : a ≤ x ∧ x ≤ b ∧ ¬b ≤ x ↔ a ≤ x ∧ x ≤ b ∧ ¬b ≤ x
⊢ x ∈ {x ∈ finsetIcc a b | ¬b ≤ x} ↔ a ≤ x ∧ x < b

Tactic:
rw [Finset.mem_filter, mem_Icc, and_assoc, lt_iff_le_not_ge]

Premises used: lt_iff_le_not_ge, and_assoc, Finset.mem_filter
-- Module: Mathlib.Order.Interval.Finset.Defs
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
rw₃ rw₄ : (a ≤ x ∧ ¬x ≤ a) ∧ x ≤ b ↔ (a ≤ x ∧ ¬x ≤ a) ∧ x ≤ b
⊢ x ∈ {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]

Premises used: lt_iff_le_not_ge, and_right_comm, Finset.mem_filter
-- Module: Mathlib.Order.Interval.Finset.Defs
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
rw₄ rw₅ : (a ≤ x ∧ ¬x ≤ a) ∧ x ≤ b ∧ ¬b ≤ x ↔ (a ≤ x ∧ ¬x ≤ a) ∧ x ≤ b ∧ ¬b ≤ x
⊢ x ∈ {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]

Premises used: lt_iff_le_not_ge, and_and_and_comm, Finset.mem_filter
-- Module: Mathlib.Order.Interval.Finset.Defs
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
rw₃ rw₄ : a ≤ x ∧ x ≤ b ∧ x ≠ b ↔ a ≤ x ∧ x ≤ b ∧ x ≠ b
⊢ x ∈ {x ∈ finsetIcc a b | x ≠ b} ↔ a ≤ x ∧ x < b

Tactic:
rw [Finset.mem_filter, mem_Icc, and_assoc, lt_iff_le_and_ne]

Premises used: lt_iff_le_and_ne, and_assoc, Finset.mem_filter
-- Module: Mathlib.Order.Interval.Finset.Defs
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
rw₃ rw₄ : (a ≤ x ∧ a ≠ x) ∧ x ≤ b ↔ (a ≤ x ∧ a ≠ x) ∧ x ≤ b
⊢ x ∈ {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]

Premises used: lt_iff_le_and_ne, and_right_comm, Finset.mem_filter
-- Module: Mathlib.Order.Interval.Finset.Defs
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
rw₄ rw₅ : (a ≤ x ∧ a ≠ x) ∧ x ≤ b ∧ x ≠ b ↔ (a ≤ x ∧ a ≠ x) ∧ x ≤ b ∧ x ≠ b
⊢ x ∈ {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]

Premises used: lt_iff_le_and_ne, and_and_and_comm, Finset.mem_filter
-- Module: Mathlib.Order.Interval.Finset.Defs
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
rw₂ rw₃ : a ≤ x ∧ ¬x ≤ a ↔ a ≤ x ∧ ¬x ≤ a
⊢ x ∈ {x ∈ finsetIci a | ¬x ≤ a} ↔ a < x

Tactic:
rw [mem_filter, mem_Ici, lt_iff_le_not_ge]

Premises used: lt_iff_le_not_ge, Finset.mem_filter
-- Module: Mathlib.Order.Interval.Finset.Defs
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
rw₂ rw₃ : a ≤ x ∧ a ≠ x ↔ a ≤ x ∧ a ≠ x
⊢ x ∈ {x ∈ finsetIci a | a ≠ x} ↔ a < x

Tactic:
rw [mem_filter, mem_Ici, lt_iff_le_and_ne]

Premises used: lt_iff_le_and_ne, Finset.mem_filter
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Icc a b ↔ a ≤ x ∧ x ≤ b

Tactic:
LocallyFiniteOrder.finset_mem_Icc a b x

Premises used: LocallyFiniteOrder.finset_mem_Icc, Set.Mem, setOf
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ico a b ↔ a ≤ x ∧ x < b

Tactic:
LocallyFiniteOrder.finset_mem_Ico a b x

Premises used: Set.Mem, setOf, LocallyFiniteOrder.finset_mem_Ico
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ioc a b ↔ a < x ∧ x ≤ b

Tactic:
LocallyFiniteOrder.finset_mem_Ioc a b x

Premises used: Set.Mem, setOf, LocallyFiniteOrder.finset_mem_Ioc
-- Module: Mathlib.Order.Interval.Finset.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ioo a b ↔ a < x ∧ x < b

Tactic:
LocallyFiniteOrder.finset_mem_Ioo a b x

Premises used: Set.Mem, setOf, LocallyFiniteOrder.finset_mem_Ioo