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 : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj_1 : j < k + 1
hj : ¬j = 0
this :
  a ≤
      ((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 ∧
    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 ∧
      ((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 ≤
        b
hj₀ : j - 1 + 1 = j
⊢ a ≤ (F.intervalGapsWithin h a b (↑(j - 1) : Fin (k + 1))).2 ∧
    (F.intervalGapsWithin h a b (↑(j - 1) : Fin (k + 1))).2 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ∧
      (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ≤ b

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
j_1 : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj_1 : j < k + 1
hj : ¬j = 0
hj₀ : j - 1 + 1 = j
this :
  a ≤ (F.intervalGapsWithin h a b (↑(j - 1) : Fin (k + 1))).2 ∧
    (F.intervalGapsWithin h a b (↑(j - 1) : Fin (k + 1))).2 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ∧
      (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ≤ b
⊢ a ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1

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

Tactic:
wlog hj : j < k + 1 generalizing j
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
this : ∀ (j : ℕ) (hj : j < k + 1), (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 ≤ b
hj : ¬j < k + 1
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 ≤ b

Tactic:
grind [cast_val_eq_self]

Premises used: Fin.cast_val_eq_self
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j_1 : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
pos : ∀ (hj : j = k), (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 ≤ b
neg : ∀ (hj : ¬j = k), (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 ≤ b
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 ≤ b

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

Tactic:
simp [hj]
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j_1 : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj_1 : j < k + 1
hj : ¬j = k
⊢ j ∈ Iio k

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j_1 : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj_1 : j < k + 1
hj : ¬j = k
⊢ a ≤
      ((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 ∧
    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
        ((fun (j : ℕ) ↦
              ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2,
                (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
            j).2 ∧
      ((fun (j : ℕ) ↦
              ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2,
                (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
            j).2 ≤
        b

Tactic:
have := hFab (F.intervalGapsWithin_mapsTo h a b (x := j) (by grind))
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j_1 : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj_1 : j < k + 1
hj : ¬j = k
this :
  a ≤
      ((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 ∧
    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
        ((fun (j : ℕ) ↦
              ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2,
                (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
            j).2 ∧
      ((fun (j : ℕ) ↦
              ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2,
                (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
            j).2 ≤
        b
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 ≤ b

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
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
inr :
  ∀
    (this :
      ∀ (j : ℕ) (hj : j < k + 1),
        (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2)
    (hj : ¬j < k + 1),
    (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2
wlog :
  ∀ (j : ℕ) (hj : j < k + 1),
    (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2

Tactic:
wlog hj : j < k + 1 generalizing j
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
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
this :
  ∀ (j : ℕ) (hj : j < k + 1),
    (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2
hj : ¬j < k + 1
⊢ (↑(↑j : Fin (k + 1)) : ℕ) < k + 1

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
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
this :
  ∀ (j : ℕ) (hj : j < k + 1),
    (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2
hj : ¬j < k + 1
h₁ h₂ : Eq (α := Fin (k + 1)) (↑j : Fin (k + 1)) (↑(↑(↑j : Fin (k + 1)) : ℕ) : Fin (k + 1))
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2

Tactic:
convert! this (j : Fin (k + 1)) (by grind) using 3

Premises used: Fin.val, Nat.cast
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
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
this :
  ∀ (j : ℕ) (hj : j < k + 1),
    (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2
hj : ¬j < k + 1
⊢ Eq (α := Fin (k + 1)) (↑j : Fin (k + 1)) (↑(↑(↑j : Fin (k + 1)) : ℕ) : Fin (k + 1))

Tactic:
grind [cast_val_eq_self]

Premises used: Fin.cast_val_eq_self
-- 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
pos :
  ∀ (hj₁ : j = 0), (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2
neg :
  ∀ (hj₁ : ¬j = 0),
    (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2

Tactic:
by_cases hj₁ : j = 0
-- 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
pos : (F.intervalGapsWithin h a b (↑0 : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑0 : Fin (k + 1))).2
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2

Tactic:
simp only [hj₁]
-- 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
pos :
  ∀ (hk : 0 = k), (F.intervalGapsWithin h a b (↑0 : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑0 : Fin (k + 1))).2
neg :
  ∀ (hk : ¬0 = k), (F.intervalGapsWithin h a b (↑0 : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑0 : Fin (k + 1))).2
⊢ (F.intervalGapsWithin h a b (↑0 : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑0 : Fin (k + 1))).2

Tactic:
by_cases hk : 0 = k
-- 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 : 0 = k
pos : a ≤ (F.intervalGapsWithin h a b 0).2
⊢ (F.intervalGapsWithin h a b (↑0 : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑0 : Fin (k + 1))).2

Tactic:
simp only [natCast_zero, intervalGapsWithin_zero_fst]

Premises used: Fin.natCast_zero, Finset.intervalGapsWithin_zero_fst
-- 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 : 0 = k
⊢ 0 = last k

Tactic:
grind
-- 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 : 0 = k
⊢ a ≤ (F.intervalGapsWithin h a b 0).2

Tactic:
simp [show 0 = last k by grind, hab]
-- 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 : ¬0 = k
⊢ 0 ∈ Iio k

Tactic:
grind
-- 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 : ¬0 = k
⊢ (F.intervalGapsWithin h a b (↑0 : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑0 : Fin (k + 1))).2

Tactic:
exact hFab (F.intervalGapsWithin_mapsTo h a b (x := 0) (by grind)) |>.left

Premises used: And.left, Finset.intervalGapsWithin_mapsTo
-- 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
⊢ k - 1 + 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
⊢ k - 1 + 1 = k

Tactic:
have hk : k - 1 + 1 = k := by 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
pos :
  ∀ (hj₂ : j = k), (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2
neg :
  ∀ (hj₂ : ¬j = k),
    (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2

Tactic:
by_cases hj₂ : j = k
-- 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
pos : (F.intervalGapsWithin h a b (last k)).1 ≤ b
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2

Tactic:
simp only [hj₂, natCast_eq_last, intervalGapsWithin_last_snd, ge_iff_le]

Premises used: ge_iff_le, Finset.intervalGapsWithin_last_snd, Fin.natCast_eq_last
-- 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
⊢ j - 1 ∈ Iio k

Tactic:
grind
-- 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
h₁ :
  (F.intervalGapsWithin h a b (last k)).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 (last k)).1 ≤ b

Tactic:
convert! hFab (F.intervalGapsWithin_mapsTo h a b (x := j - 1) (by grind)) |>.right.right using 1

Premises used: And.right, Finset.intervalGapsWithin_mapsTo
-- 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
⊢ (F.intervalGapsWithin h a b (last k)).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:
simp [hj₂, hk]
-- 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
F_1 : Finset (α × α)
h_1 : #F_1 = k
a_1 b_1 : α
⊢ 0 < j

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
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
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
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
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
neg :
  LE.le.{u_1} (α := α) ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).2
    ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2

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

Premises used: Finset.intervalGapsWithin_snd_of_lt, Finset.intervalGapsWithin_fst_of_lt_lt
-- 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
⊢ 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
⊢ 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
⊢ Ne (α := Fin k) ⟨j - 1, ⋯⟩ ⟨j, ⋯⟩

Tactic:
grind
-- 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
⊢ Ne (α := Fin k) ⟨j - 1, ⋯⟩ ⟨j, ⋯⟩

Tactic:
have hj₃ : (⟨j - 1, by omega⟩ : Fin k) ≠ ⟨j, by omega⟩ := by grind
-- 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, ⋯⟩
neg :
  let G : Fin k ↪o Lex (α × α) := F.orderEmbOfFin h;
  LE.le.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).2 ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1
⊢ LE.le.{u_1} (α := α) ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).2
    ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1

Tactic:
set G := F.orderEmbOfFin (α := α ×ₗ α) h

Premises used: Finset.orderEmbOfFin
-- 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
⊢ Membership.mem (α := α × α) (↑F : Set (α × α)) ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩ : 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
⊢ Membership.mem (α := α × α) (↑F : Set (α × α)) ((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
⊢ 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:
have := hF (by simp [G, F.orderEmbOfFin_mem (α := α ×ₗ α)])
    (by simp [G, F.orderEmbOfFin_mem (α := α ×ₗ α)]) (G.injective.ne (hj₃))