awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (goal)
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
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2
have neg : ∀ (hj₂ : ¬j = k), (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
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (goal)
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 (↑j : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2
have pos : (F.intervalGapsWithin h a b (last k)).1 ≤ b
Tactic: simp only [hj₂, natCast_eq_last, intervalGapsWithin_last_snd, ge_iff_le]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (goal)
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 ≤ b
have 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
Tactic: convert! hFab (F.intervalGapsWithin_mapsTo h a b (x := j - 1) (by grind)) |>.right.right using 1
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (goal)
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 (↑j : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2
have neg : LE.le.{u_1} (α := α) ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) ⟨j - 1, sorry⟩).2
  ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) ⟨j, sorry⟩).1
Tactic: rw [intervalGapsWithin_fst_of_lt_lt (hj₁ := by omega) (hj₂ := by omega),
      intervalGapsWithin_snd_of_lt (hj := by omega)]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (hypothesis)
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
⊢ LE.le.{u_1} (α := α) ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).2
    ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1
have hj₃ : Ne (α := Fin k) ⟨j - 1, sorry⟩ ⟨j, sorry⟩
Tactic: have hj₃ : (⟨j - 1, by omega⟩ : Fin k) ≠ ⟨j, by omega⟩ := by grind
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (hypothesis)
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
⊢ LE.le.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).2 ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1
have this : Function.onFun (α := α × α) (β := Set α) Disjoint (fun (z : α × α) ↦ Icc z.1 z.2)
  ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, sorry⟩ : Lex (α × α)) ((G : (a : Fin k) → Lex (α × α)) ⟨j, sorry⟩ : Lex (α × α))
Tactic: have := hF (by simp [G, F.orderEmbOfFin_mem (α := α ×ₗ α)])
    (by simp [G, F.orderEmbOfFin_mem (α := α ×ₗ α)]) (G.injective.ne (hj₃))
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (goal)
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 (α × α))
⊢ LE.le.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, ⋯⟩).2 ((G : (a : Fin k) → Lex (α × α)) ⟨j, ⋯⟩).1
have neg : ∀
  (this :
    LT.lt.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j, sorry⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, sorry⟩).2),
  ¬Function.onFun (α := α × α) (β := Set α) Disjoint (fun (z : α × α) ↦ Icc z.1 z.2)
      ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, sorry⟩ : Lex (α × α)) ((G : (a : Fin k) → Lex (α × α)) ⟨j, sorry⟩ : Lex (α × α))
Tactic: contrapose! this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (goal)
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
⊢ ¬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 (α × α))
have neg : ∃ (x : α),
  (((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, sorry⟩).1 ≤ x ∧ x ≤ ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, sorry⟩).2) ∧
    ((G : (a : Fin k) → Lex (α × α)) ⟨j, sorry⟩).1 ≤ x ∧ x ≤ ((G : (a : Fin k) → Lex (α × α)) ⟨j, sorry⟩).2
Tactic: simp only [Set.not_disjoint_iff, Set.mem_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (goal)
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
⊢ ∃ (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
have h₁ : (LE.le.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, sorry⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j, sorry⟩).1 ∧
    LE.le.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j, sorry⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, sorry⟩).2) ∧
  LE.le.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j, sorry⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j, sorry⟩).1 ∧
    LE.le.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j, sorry⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j, sorry⟩).2
Tactic: use (G ⟨j, by omega⟩).1
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (hypothesis)
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 ∧
      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
have hG : LE.le.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j - 1, sorry⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j, sorry⟩).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
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (hypothesis)
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
⊢ (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
have hFabi : a ≤ ((G : (a : Fin k) → Lex (α × α)) ⟨j, sorry⟩).1 ∧
  LE.le.{u_1} (α := α) ((G : (a : Fin k) → Lex (α × α)) ⟨j, sorry⟩).1 ((G : (a : Fin k) → Lex (α × α)) ⟨j, sorry⟩).2 ∧
    ((G : (a : Fin k) → Lex (α × α)) ⟨j, sorry⟩).2 ≤ b
Tactic: have hFabi := hFab (z := G ⟨j, by omega⟩) (by simp [G, F.orderEmbOfFin_mem (α := α ×ₗ α)])
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (goal)
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'
⊢ 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'
have 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'
Tactic: rw [mem_Iio] at hj hj'
Cleared hypotheses: hj, j', hj', hjj'
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (goal)
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'
⊢ 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'
have 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'
Tactic: wlog hij' : j < j' generalizing j j'
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (goal)
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'
⊢ 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'
have 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'
Tactic: wlog hij' : j < j' generalizing j j'
Cleared hypotheses: j, hj, j', hj', hjj'
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (goal)
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'
⊢ 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'
have 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 =
  ∅
Tactic: rw [Function.onFun, Set.disjoint_iff_inter_eq_empty]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (goal)
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'
⊢ 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 =
    ∅
have suffices : (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 ≤ (F.intervalGapsWithin h a b (↑j' : Fin (k + 1))).1
Tactic: suffices (F.intervalGapsWithin h a b j).2 ≤ (F.intervalGapsWithin h a b j').1 by grind
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (hypothesis)
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'
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 ≤ (F.intervalGapsWithin h a b (↑j' : Fin (k + 1))).1
have hj'₀ : j' - 1 + 1 = j'
Tactic: have hj'₀ : j' - 1 + 1 = j' := by omega
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (hypothesis)
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'
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 ≤ (F.intervalGapsWithin h a b (↑j' : Fin (k + 1))).1
have 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
Tactic: have := hFab (F.intervalGapsWithin_mapsTo h a b (x := j' - 1) (by grind)) |>.right.left
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (hypothesis)
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 : Fin (k + 1))).2 ≤ (F.intervalGapsWithin h a b (↑j' : Fin (k + 1))).1
have this₁ : (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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (goal)
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.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 ≤ (F.intervalGapsWithin h a b (↑j' : Fin (k + 1))).1
have grw : (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 ≤ (F.intervalGapsWithin h a b (↑(j' - 1) : Fin (k + 1))).2
Tactic: grw [← this]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (goal)
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.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 ≤ (F.intervalGapsWithin h a b (↑(j' - 1) : Fin (k + 1))).2
have rw : LE.le.{u_1} (α := α) ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) ⟨j, sorry⟩).1
  ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) ⟨j' - 1, sorry⟩).1
Tactic: rw [intervalGapsWithin_snd_of_lt (hj := by omega),
      intervalGapsWithin_snd_of_lt (hj := by omega)]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a_1 b_1 c a b x : ℕ
⊢ x ∈ { val := (↑(List.range' a (b + 1 - a)) : Multiset ℕ), nodup := ⋯ : Finset ℕ } ↔ a ≤ x ∧ x ≤ b
have rw : a ≤ x ∧ x < a + (b + 1 - a) ↔ a ≤ x ∧ x ≤ b
Tactic: rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a_1 b_1 c a b x : ℕ
⊢ x ∈ { val := (↑(List.range' a (b - a)) : Multiset ℕ), nodup := ⋯ : Finset ℕ } ↔ a ≤ x ∧ x < b
have rw : a ≤ x ∧ x < a + (b - a) ↔ a ≤ x ∧ x < b
Tactic: rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a_1 b_1 c a b x : ℕ
⊢ x ∈ { val := (↑(List.range' (a + 1) (b - a)) : Multiset ℕ), nodup := ⋯ : Finset ℕ } ↔ a < x ∧ x ≤ b
have rw : a + 1 ≤ x ∧ x < a + 1 + (b - a) ↔ a < x ∧ x ≤ b
Tactic: rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a_1 b_1 c a b x : ℕ
⊢ x ∈ { val := (↑(List.range' (a + 1) (b - a - 1)) : Multiset ℕ), nodup := ⋯ : Finset ℕ } ↔ a < x ∧ x < b
have rw : a + 1 ≤ x ∧ x < a + 1 + (b - a - 1) ↔ a < x ∧ x < b
Tactic: rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a : ℕ
⊢ Ico 0 a = range a
have rw : Ico ⊥ a = range a
Tactic: rw [← Nat.bot_eq_zero, ← Iio_eq_Ico, Iio_eq_range]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a : ℕ
rw : Ico ⊥ a = range a
⊢ Ico 0 a = range a
have rw₁ : Iio a = range a
Tactic: rw [← Nat.bot_eq_zero, ← Iio_eq_Ico, Iio_eq_range]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a : ℕ
rw : Ico ⊥ a = range a
rw₁ : Iio a = range a
⊢ Ico 0 a = range a
have rw₂ : range a = range a
Tactic: rw [← Nat.bot_eq_zero, ← Iio_eq_Ico, Iio_eq_range]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n : ℕ
⊢ range (n + 1) = Icc 0 n
have rw : Icc 0 (n + 1 - 1) = Icc 0 n
Tactic: rw [range_eq_Icc_zero_sub_one _ (Nat.add_one_ne_zero _), Nat.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n : ℕ
rw : Icc 0 (n + 1 - 1) = Icc 0 n
⊢ range (n + 1) = Icc 0 n
have rw₁ : Icc 0 n = Icc 0 n
Tactic: rw [range_eq_Icc_zero_sub_one _ (Nat.add_one_ne_zero _), Nat.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n : ℕ
⊢ range (n + 1) = Iic n
have rw : Icc 0 n = Iic n
Tactic: rw [range_succ_eq_Icc_zero]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a b : ℕ
⊢ max a b + 1 - min a b = (HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)).natAbs + 1
have rw : HSub.hSub (α := ℤ) (↑(max a b + 1) : ℤ) (↑(min a b) : ℤ) = (↑((HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)).natAbs + 1) : ℤ)
Tactic: rw [← Int.natCast_inj, Int.ofNat_sub]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a b : ℕ
rw :
  HSub.hSub (α := ℤ) (↑(max a b + 1) : ℤ) (↑(min a b) : ℤ) = (↑((HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)).natAbs + 1) : ℤ)
⊢ max a b + 1 - min a b = (HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)).natAbs + 1
have rw₁ : min a b ≤ max a b + 1
Tactic: rw [← Int.natCast_inj, Int.ofNat_sub]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
b : ℕ
⊢ #(Iic b) = b + 1
have rw : #(Icc ⊥ b) = b + 1
Tactic: rw [Iic_eq_Icc, card_Icc, Nat.bot_eq_zero, Nat.sub_zero]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
b : ℕ
rw : #(Icc ⊥ b) = b + 1
⊢ #(Iic b) = b + 1
have rw₁ : b + 1 - ⊥ = b + 1
Tactic: rw [Iic_eq_Icc, card_Icc, Nat.bot_eq_zero, Nat.sub_zero]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
b : ℕ
rw : #(Icc ⊥ b) = b + 1
rw₁ : b + 1 - ⊥ = b + 1
⊢ #(Iic b) = b + 1
have rw₂ : b + 1 - 0 = b + 1
Tactic: rw [Iic_eq_Icc, card_Icc, Nat.bot_eq_zero, Nat.sub_zero]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
b : ℕ
rw : #(Icc ⊥ b) = b + 1
rw₁ : b + 1 - ⊥ = b + 1
rw₂ : b + 1 - 0 = b + 1
⊢ #(Iic b) = b + 1
have rw₃ : b + 1 = b + 1
Tactic: rw [Iic_eq_Icc, card_Icc, Nat.bot_eq_zero, Nat.sub_zero]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
b : ℕ
⊢ #(Iio b) = b
have rw : #(Ico ⊥ b) = b
Tactic: rw [Iio_eq_Ico, card_Ico, Nat.bot_eq_zero, Nat.sub_zero]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
b : ℕ
rw : #(Ico ⊥ b) = b
⊢ #(Iio b) = b
have rw₁ : b - ⊥ = b
Tactic: rw [Iio_eq_Ico, card_Ico, Nat.bot_eq_zero, Nat.sub_zero]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
b : ℕ
rw : #(Ico ⊥ b) = b
rw₁ : b - ⊥ = b
⊢ #(Iio b) = b
have rw₂ : b - 0 = b
Tactic: rw [Iio_eq_Ico, card_Ico, Nat.bot_eq_zero, Nat.sub_zero]