awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j_1 : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F : Set (α × α)).PairwiseDisjoint (α := Set α) fun (z : α × α) ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
hj₃ : Ne (α := Fin k) ⟨j - 1, ⋯⟩ ⟨j, ⋯⟩
G : Fin k ↪o Lex (α × α) := F.orderEmbOfFin h
this :
  Function.onFun (α := α × α) (β := Set α) Disjoint (fun (z : α × α) ↦ Icc z.1 z.2)
    ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩ : Lex (α × α)) ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩ : Lex (α × α))
neg :
  ∀
    (this :
      LT.lt.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).2),
    ¬Function.onFun (α := α × α) (β := Set α) Disjoint (fun (z : α × α) ↦ Icc z.1 z.2)
        ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩ : Lex (α × α))
        ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩ : Lex (α × α))
⊢ LE.le.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).2 ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1

Tactic:
contrapose! this
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j_1 : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F : Set (α × α)).PairwiseDisjoint (α := Set α) fun (z : α × α) ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
hj₃ : Ne (α := Fin k) ⟨j - 1, ⋯⟩ ⟨j, ⋯⟩
G : Fin k ↪o Lex (α × α) := F.orderEmbOfFin h
this : LT.lt.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).2
neg :
  ∃ (x : α),
    (((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).1 ≤ x ∧ x ≤ ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).2) ∧
      ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1 ≤ x ∧ x ≤ ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).2
⊢ ¬Function.onFun (α := α × α) (β := Set α) Disjoint (fun (z : α × α) ↦ Icc z.1 z.2)
      ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩ : Lex (α × α)) ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩ : Lex (α × α))

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

Premises used: Set.not_disjoint_iff, Set.mem_Icc
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j_1 : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F : Set (α × α)).PairwiseDisjoint (α := Set α) fun (z : α × α) ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
hj₃ : Ne (α := Fin k) ⟨j - 1, ⋯⟩ ⟨j, ⋯⟩
G : Fin k ↪o Lex (α × α) := F.orderEmbOfFin h
this : LT.lt.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).2
⊢ j < k

Tactic:
omega
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j_1 : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F : Set (α × α)).PairwiseDisjoint (α := Set α) fun (z : α × α) ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
hj₃ : Ne (α := Fin k) ⟨j - 1, ⋯⟩ ⟨j, ⋯⟩
G : Fin k ↪o Lex (α × α) := F.orderEmbOfFin h
this : LT.lt.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).2
h₁ :
  (LE.le.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1 ∧
      LE.le.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).2) ∧
    LE.le.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1 ∧
      LE.le.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).2
⊢ ∃ (x : α),
    (((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).1 ≤ x ∧ x ≤ ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).2) ∧
      ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1 ≤ x ∧ x ≤ ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).2

Tactic:
use (G ⟨j, by omega⟩).1

Premises used: Fin.mk, Prod.fst, DFunLike.coe
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j_1 : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F : Set (α × α)).PairwiseDisjoint (α := Set α) fun (z : α × α) ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
hj₃ : Ne (α := Fin k) ⟨j - 1, ⋯⟩ ⟨j, ⋯⟩
G : Fin k ↪o Lex (α × α) := F.orderEmbOfFin h
this : LT.lt.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).2
⊢ j - 1 < k

Tactic:
omega
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j_1 : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F : Set (α × α)).PairwiseDisjoint (α := Set α) fun (z : α × α) ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
hj₃ : Ne (α := Fin k) ⟨j - 1, ⋯⟩ ⟨j, ⋯⟩
G : Fin k ↪o Lex (α × α) := F.orderEmbOfFin h
this : LT.lt.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).2
⊢ LE.le (α := Fin k) ⟨j - 1, ⋯⟩ ⟨j, ⋯⟩

Tactic:
simp [le_iff_val_le_val]

Premises used: Fin.le_iff_val_le_val
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j_1 : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F : Set (α × α)).PairwiseDisjoint (α := Set α) fun (z : α × α) ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
hj₃ : Ne (α := Fin k) ⟨j - 1, ⋯⟩ ⟨j, ⋯⟩
G : Fin k ↪o Lex (α × α) := F.orderEmbOfFin h
this : LT.lt.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).2
⊢ LE.le.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1

Tactic:
have hG : (G ⟨j - 1, by omega⟩).1 ≤ (G ⟨j, by omega⟩).1 :=
    Prod.Lex.le_iff'.mp (G.monotone (by simp [le_iff_val_le_val])) |>.left
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j_1 : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F : Set (α × α)).PairwiseDisjoint (α := Set α) fun (z : α × α) ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
hj₃ : Ne (α := Fin k) ⟨j - 1, ⋯⟩ ⟨j, ⋯⟩
G : Fin k ↪o Lex (α × α) := F.orderEmbOfFin h
this : LT.lt.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).2
hG : LE.le.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1
⊢ j < k

Tactic:
omega
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j_1 : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F : Set (α × α)).PairwiseDisjoint (α := Set α) fun (z : α × α) ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
hj₃ : Ne (α := Fin k) ⟨j - 1, ⋯⟩ ⟨j, ⋯⟩
G : Fin k ↪o Lex (α × α) := F.orderEmbOfFin h
this : LT.lt.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).2
hG : LE.le.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1
⊢ Membership.mem (α := α × α) F ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩ : Lex (α × α))

Tactic:
simp [G, F.orderEmbOfFin_mem (α := α ×ₗ α)]

Premises used: Finset.orderEmbOfFin_mem
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j_1 : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F : Set (α × α)).PairwiseDisjoint (α := Set α) fun (z : α × α) ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
hj₃ : Ne (α := Fin k) ⟨j - 1, ⋯⟩ ⟨j, ⋯⟩
G : Fin k ↪o Lex (α × α) := F.orderEmbOfFin h
this : LT.lt.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).2
hG : LE.le.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1
⊢ a ≤ ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1 ∧
    LE.le.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).2 ∧
      ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).2 ≤ b

Tactic:
have hFabi := hFab (z := G ⟨j, by omega⟩) (by simp [G, F.orderEmbOfFin_mem (α := α ×ₗ α)])
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j_1 : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F : Set (α × α)).PairwiseDisjoint (α := Set α) fun (z : α × α) ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
hj₃ : Ne (α := Fin k) ⟨j - 1, ⋯⟩ ⟨j, ⋯⟩
G : Fin k ↪o Lex (α × α) := F.orderEmbOfFin h
this : LT.lt.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).2
hG : LE.le.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1
hFabi :
  a ≤ ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1 ∧
    LE.le.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).2 ∧
      ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).2 ≤ b
⊢ (LE.le.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1 ∧
      LE.le.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).2) ∧
    LE.le.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1 ∧
      LE.le.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).2

Tactic:
simp [hFabi, this.le, hG]

Premises used: LT.lt.le
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j ∈ Iio (k + 1)
j' : ℕ
hj' : j' ∈ Iio (k + 1)
hjj' : j ≠ j'
rw :
  ∀ (hj : j < k + 1) ⦃j' : ℕ⦄ (hj' : j' < k + 1) (hjj' : j ≠ j'),
    Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint
      (fun (j : ℕ) ↦
        Ioc (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2)
      j j'
⊢ Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint
    (fun (j : ℕ) ↦
      Ioc (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2)
    j j'

Tactic:
rw [mem_Iio] at hj hj'

Premises used: Set.mem_Iio
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
inr :
  ∀
    (this :
      ∀ ⦃j : ℕ⦄ (hj : j < k + 1) ⦃j' : ℕ⦄ (hj' : j' < k + 1) (hjj' : j ≠ j') (hij' : j < j'),
        Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint
          (fun (j : ℕ) ↦
            Ioc (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2)
          j j')
    (hij' : ¬j < j'),
    Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint
      (fun (j : ℕ) ↦
        Ioc (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2)
      j j'
wlog :
  ∀ ⦃j : ℕ⦄ (hj : j < k + 1) ⦃j' : ℕ⦄ (hj' : j' < k + 1) (hjj' : j ≠ j') (hij' : j < j'),
    Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint
      (fun (j : ℕ) ↦
        Ioc (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2)
      j j'
⊢ Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint
    (fun (j : ℕ) ↦
      Ioc (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2)
    j j'

Tactic:
wlog hij' : j < j' generalizing j j'
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
this :
  ∀ ⦃j : ℕ⦄ (hj : j < k + 1) ⦃j' : ℕ⦄ (hj' : j' < k + 1) (hjj' : j ≠ j') (hij' : j < j'),
    Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint
      (fun (j : ℕ) ↦
        Ioc (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2)
      j j'
hij' : ¬j < j'
⊢ j' < j

Tactic:
omega
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
this :
  ∀ ⦃j : ℕ⦄ (hj : j < k + 1) ⦃j' : ℕ⦄ (hj' : j' < k + 1) (hjj' : j ≠ j') (hij' : j < j'),
    Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint
      (fun (j : ℕ) ↦
        Ioc (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2)
      j j'
hij' : ¬j < j'
⊢ Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint
    (fun (j : ℕ) ↦
      Ioc (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2)
    j j'

Tactic:
exact (this hj' hj hjj'.symm (by omega)).symm

Premises used: Ne.symm, Disjoint.symm
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
rw :
  Ioc (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 ∩
      Ioc (F.intervalGapsWithin h a b (↑j' : Fin (k + 1))).1 (F.intervalGapsWithin h a b (↑j' : Fin (k + 1))).2 =
    ∅
⊢ Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint
    (fun (j : ℕ) ↦
      Ioc (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2)
    j j'

Tactic:
rw [Function.onFun, Set.disjoint_iff_inter_eq_empty]

Premises used: Function.onFun, Set.disjoint_iff_inter_eq_empty
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
this : (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 ≤ (F.intervalGapsWithin h a b (↑j' : Fin (k + 1))).1
⊢ Ioc (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 ∩
      Ioc (F.intervalGapsWithin h a b (↑j' : Fin (k + 1))).1 (F.intervalGapsWithin h a b (↑j' : Fin (k + 1))).2 =
    ∅

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
suffices : (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 ≤ (F.intervalGapsWithin h a b (↑j' : Fin (k + 1))).1
⊢ Ioc (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 ∩
      Ioc (F.intervalGapsWithin h a b (↑j' : Fin (k + 1))).1 (F.intervalGapsWithin h a b (↑j' : Fin (k + 1))).2 =
    ∅

Tactic:
suffices (F.intervalGapsWithin h a b j).2 ≤ (F.intervalGapsWithin h a b j').1 by grind
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
⊢ j' - 1 + 1 = j'

Tactic:
omega
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
⊢ j' - 1 + 1 = j'

Tactic:
have hj'₀ : j' - 1 + 1 = j' := by omega
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
hj'₀ : j' - 1 + 1 = j'
⊢ j' - 1 ∈ Iio k

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
hj'₀ : j' - 1 + 1 = j'
⊢ LE.le.{u_1} (α := α)
    ((fun (j : ℕ) ↦
          ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
        (j' - 1)).1
    ((fun (j : ℕ) ↦
          ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
        (j' - 1)).2

Tactic:
have := hFab (F.intervalGapsWithin_mapsTo h a b (x := j' - 1) (by grind)) |>.right.left
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
hj'₀ : j' - 1 + 1 = j'
this :
  LE.le.{u_1} (α := α)
    ((fun (j : ℕ) ↦
          ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
        (j' - 1)).1
    ((fun (j : ℕ) ↦
          ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
        (j' - 1)).2
⊢ (F.intervalGapsWithin h a b (↑(j' - 1) : Fin (k + 1))).2 ≤ (F.intervalGapsWithin h a b (↑j' : Fin (k + 1))).1

Tactic:
simp only [Nat.succ_eq_add_one, hj'₀] at this

Premises used: Nat.succ_eq_add_one
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
hj'₀ : j' - 1 + 1 = j'
this : (F.intervalGapsWithin h a b (↑(j' - 1) : Fin (k + 1))).2 ≤ (F.intervalGapsWithin h a b (↑j' : Fin (k + 1))).1
grw : (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 ≤ (F.intervalGapsWithin h a b (↑(j' - 1) : Fin (k + 1))).2
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 ≤ (F.intervalGapsWithin h a b (↑j' : Fin (k + 1))).1

Tactic:
grw [← this]
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
hj'₀ : j' - 1 + 1 = j'
this : (F.intervalGapsWithin h a b (↑(j' - 1) : Fin (k + 1))).2 ≤ (F.intervalGapsWithin h a b (↑j' : Fin (k + 1))).1
F_1 : Finset (α × α)
h_1 : #F_1 = k
a_1 b_1 : α
⊢ j < k

Tactic:
omega
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
hj'₀ : j' - 1 + 1 = j'
this : (F.intervalGapsWithin h a b (↑(j' - 1) : Fin (k + 1))).2 ≤ (F.intervalGapsWithin h a b (↑j' : Fin (k + 1))).1
F_1 : Finset (α × α)
h_1 : #F_1 = k
a_1 b_1 : α
⊢ j' - 1 < k

Tactic:
omega
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
hj'₀ : j' - 1 + 1 = j'
this : (F.intervalGapsWithin h a b (↑(j' - 1) : Fin (k + 1))).2 ≤ (F.intervalGapsWithin h a b (↑j' : Fin (k + 1))).1
rw :
  LE.le.{u_1} (α := α) ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1
    ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) ⟨j' - 1, ⋯⟩).1
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 ≤ (F.intervalGapsWithin h a b (↑(j' - 1) : Fin (k + 1))).2

Tactic:
rw [intervalGapsWithin_snd_of_lt (hj := by omega),
      intervalGapsWithin_snd_of_lt (hj := by omega)]

Premises used: Finset.intervalGapsWithin_snd_of_lt
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
hj'₀ : j' - 1 + 1 = j'
this : (F.intervalGapsWithin h a b (↑(j' - 1) : Fin (k + 1))).2 ≤ (F.intervalGapsWithin h a b (↑j' : Fin (k + 1))).1
⊢ LE.le (α := Fin k) ⟨j, ⋯⟩ ⟨j' - 1, ⋯⟩

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
hj'₀ : j' - 1 + 1 = j'
this : (F.intervalGapsWithin h a b (↑(j' - 1) : Fin (k + 1))).2 ≤ (F.intervalGapsWithin h a b (↑j' : Fin (k + 1))).1
⊢ LE.le.{u_1} (α := α) ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1
    ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) ⟨j' - 1, ⋯⟩).1

Tactic:
exact Prod.Lex.le_iff'.mp (F.orderEmbOfFin (α := α ×ₗ α) h |>.monotone (by grind)) |>.left

Premises used: OrderEmbedding.monotone, Finset.orderEmbOfFin, And.left, Iff.mp, Prod.Lex.le_iff'
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a_1 b_1 c a b x : ℕ
rw : a ≤ x ∧ x < a + (b + 1 - a) ↔ a ≤ x ∧ x ≤ b
⊢ x ∈ { val := (↑(List.range' a (b + 1 - a)) : Multiset ℕ), nodup := ⋯ : Finset ℕ } ↔ a ≤ x ∧ x ≤ b

Tactic:
rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]

Premises used: Multiset.mem_coe, Finset.mem_mk, List.mem_range'_1
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a_1 b_1 c a b x : ℕ
⊢ a ≤ x ∧ x < a + (b + 1 - a) ↔ a ≤ x ∧ x ≤ b

Tactic:
lia
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a_1 b_1 c a b x : ℕ
rw : a ≤ x ∧ x < a + (b - a) ↔ a ≤ x ∧ x < b
⊢ x ∈ { val := (↑(List.range' a (b - a)) : Multiset ℕ), nodup := ⋯ : Finset ℕ } ↔ a ≤ x ∧ x < b

Tactic:
rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]

Premises used: Multiset.mem_coe, Finset.mem_mk, List.mem_range'_1
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a_1 b_1 c a b x : ℕ
⊢ a ≤ x ∧ x < a + (b - a) ↔ a ≤ x ∧ x < b

Tactic:
lia
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a_1 b_1 c a b x : ℕ
rw : a + 1 ≤ x ∧ x < a + 1 + (b - a) ↔ a < x ∧ x ≤ b
⊢ x ∈ { val := (↑(List.range' (a + 1) (b - a)) : Multiset ℕ), nodup := ⋯ : Finset ℕ } ↔ a < x ∧ x ≤ b

Tactic:
rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]

Premises used: Multiset.mem_coe, Finset.mem_mk, List.mem_range'_1
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a_1 b_1 c a b x : ℕ
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - a) ↔ a < x ∧ x ≤ b

Tactic:
lia
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a_1 b_1 c a b x : ℕ
rw : a + 1 ≤ x ∧ x < a + 1 + (b - a - 1) ↔ a < x ∧ x < b
⊢ x ∈ { val := (↑(List.range' (a + 1) (b - a - 1)) : Multiset ℕ), nodup := ⋯ : Finset ℕ } ↔ a < x ∧ x < b

Tactic:
rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]

Premises used: Multiset.mem_coe, Finset.mem_mk, List.mem_range'_1
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a_1 b_1 c a b x : ℕ
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - a - 1) ↔ a < x ∧ x < b

Tactic:
lia
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b c : ℕ
⊢ Unique ↥(Iic ⊥)

Tactic:
infer_instance
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b : ℕ
⊢ Icc a b = { val := (↑(List.range' a (b + 1 - a)) : Multiset ℕ), nodup := ⋯ }

Tactic:
rfl

Premises used: Finset.Icc, rfl