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
a b : α
j : ℕ
hj₁ : 0 < j
hj₂ : j - 1 < k
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 =
    ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (⟨j - 1, hj₂⟩ : Fin k)).2
have h₁ : j = (j - 1).succ
Tactic: convert! F.intervalGapsWithin_succ_fst_of_lt h a b (j - 1) hj₂
-- 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 : α
j : ℕ
hj : j < k
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 =
    ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (⟨j, hj⟩ : Fin k)).1
have this : (↑j : Fin (k + 1)) ≠ last k
Tactic: have : (j : Fin (k + 1)) ≠ last k := by grind [val_cast_of_lt]
-- 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 : α
j : ℕ
hj : j < k
this : (↑j : Fin (k + 1)) ≠ last k
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 =
    ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (⟨j, hj⟩ : Fin k)).1
have simp : Eq.{u_1 + 1} (α := α) ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (castPred (↑j : Fin (k + 1)) sorry)).1
  ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (⟨j, hj⟩ : Fin k)).1
Tactic: simp only [intervalGapsWithin, intervalGapsWithin.snd, this, ↓reduceDIte]
-- 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 : α
j : ℕ
hj : j < k
this : (↑j : Fin (k + 1)) ≠ last k
⊢ Eq.{u_1 + 1} (α := α) ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (castPred (↑j : Fin (k + 1)) ⋯)).1
    ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (⟨j, hj⟩ : Fin k)).1
have e_self : castPred (↑j : Fin (k + 1)) sorry = ⟨j, hj⟩
Tactic: congr
-- 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 : α
j : ℕ
hj : j < k
this : (↑j : Fin (k + 1)) ≠ last k
⊢ castPred (↑j : Fin (k + 1)) ⋯ = ⟨j, hj⟩
have e_self : (↑(castPred (↑j : Fin (k + 1)) sorry) : ℕ) = (↑(⟨j, hj⟩ : Fin k) : ℕ)
Tactic: ext
-- 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 : α
j : ℕ
hj : j < k
this : (↑j : Fin (k + 1)) ≠ last k
⊢ (↑(castPred (↑j : Fin (k + 1)) ⋯) : ℕ) = (↑(⟨j, hj⟩ : Fin k) : ℕ)
have e_self : j < k.succ
Tactic: simp only [coe_castPred, val_natCast, Nat.mod_succ_eq_iff_lt]
-- 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 : α
j : ℕ
hj : j ∈ Iio k
⊢ (fun (j : ℕ) ↦
        ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
      j ∈
    (↑F : Set (α × α))
have hj₁ : j < k
Tactic: rw [mem_Iio] at hj
Cleared hypotheses: hj
-- 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 : α
j : ℕ
hj : j < k
⊢ (fun (j : ℕ) ↦
        ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
      j ∈
    (↑F : Set (α × α))
have simp : Membership.mem (α := α × α) F ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (⟨j, hj⟩ : Fin k) : Lex (α × α))
Tactic: simp only [intervalGapsWithin_snd_of_lt, intervalGapsWithin_succ_fst_of_lt,
    Prod.mk.eta, SetLike.mem_coe, hj]
-- 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 : α
j : ℕ
hj : j ∈ Iio k
j' : ℕ
hj' : j' ∈ Iio k
hjj' :
  Eq.{u_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)
    ((fun (j : ℕ) ↦
        ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
      j')
⊢ j = j'
have rw : ∀ (hj : j < k) ⦃j' : ℕ⦄ (hj' : j' < k)
  (hjj' :
    Eq.{u_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)
      ((fun (j : ℕ) ↦
          ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
        j')),
  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 (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
j' : ℕ
hj' : j' < k
hjj' :
  Eq.{u_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)
    ((fun (j : ℕ) ↦
        ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
      j')
⊢ j = j'
have hjj'₁ : Eq.{u_1 + 1} (α := α × α)
  (((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (⟨j, hj⟩ : Fin k)).1,
    ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (⟨j, hj⟩ : Fin k)).2)
  (((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (⟨j', hj'⟩ : Fin k)).1,
    ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (⟨j', hj'⟩ : Fin k)).2)
Tactic: simp only [hj, hj', intervalGapsWithin_snd_of_lt, intervalGapsWithin_succ_fst_of_lt] at hjj'
Cleared hypotheses: hjj'
-- 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 : α
z : α × α
hz : z ∈ (↑F : Set (α × α))
⊢ Membership.mem (γ := Set (α × α))
    ((fun (j : ℕ) ↦
        ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1)) ''
      Iio k)
    z
have hz₁ : Membership.mem (γ := Set (α × α)) (Set.range (ι := Fin k) (⇑(F.orderEmbOfFin h) : (a : Fin k) → Lex (α × α))) z
Tactic: rw [← F.range_orderEmbOfFin h (α := α ×ₗ α)] at hz
Cleared hypotheses: hz
-- 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 : α
z : α × α
hz : Membership.mem (γ := Set (α × α)) (Set.range (ι := Fin k) (⇑(F.orderEmbOfFin h) : (a : Fin k) → Lex (α × α))) z
⊢ Membership.mem (γ := Set (α × α))
    ((fun (j : ℕ) ↦
        ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1)) ''
      Iio k)
    z
have obtain : ∀ (j : Fin k) (hj : (F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) j = z),
  Membership.mem (γ := Set (α × α))
    ((fun (j : ℕ) ↦
        ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1)) ''
      Iio k)
    z
Tactic: obtain ⟨j, hj⟩ := hz
Cleared hypotheses: hz
-- 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 : α
z : α × α
j : Fin k
hj : (F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) j = z
⊢ Membership.mem (γ := Set (α × α))
    ((fun (j : ℕ) ↦
        ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1)) ''
      Iio k)
    z
have right : (fun (j : ℕ) ↦
      ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
    (↑j : ℕ) =
  z
Tactic: use j.val, j.prop
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (goal)
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
⊢ a ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1
have inr : ∀ (this : ∀ (j : ℕ) (hj : j < k + 1), a ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1) (hj : ¬j < k + 1),
  a ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1
Tactic: wlog hj : j < k + 1 generalizing j
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (goal)
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), a ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1) (hj : ¬j < k + 1),
    a ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1
⊢ a ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1
have wlog : ∀ (j : ℕ) (hj : j < k + 1), a ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1
Tactic: wlog hj : j < k + 1 generalizing j
-- 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 : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
⊢ a ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1
have pos : ∀ (hj : j = 0), a ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1
Tactic: by_cases hj : j = 0
-- 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 : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
pos : ∀ (hj : j = 0), a ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1
⊢ a ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1
have neg : ∀ (hj : ¬j = 0), a ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1
Tactic: by_cases hj : j = 0
-- 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 : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj_1 : j < k + 1
hj : ¬j = 0
⊢ a ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1
have 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
Tactic: have := hFab (F.intervalGapsWithin_mapsTo h a b (x := 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
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
⊢ a ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1
have hj₀ : j - 1 + 1 = j
Tactic: have hj₀ : j - 1 + 1 = j := by lia
-- 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 : α
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 : Fin (k + 1))).1
have 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
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
j : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 ≤ b
have 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
Tactic: wlog hj : j < k + 1 generalizing j
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (goal)
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
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 ≤ b
have wlog : ∀ (j : ℕ) (hj : j < k + 1), (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 ≤ b
Tactic: wlog hj : j < k + 1 generalizing j
-- 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 : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 ≤ b
have pos : ∀ (hj : j = k), (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 ≤ b
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 : α
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
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 ≤ b
have neg : ∀ (hj : ¬j = k), (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 ≤ b
Tactic: by_cases hj : j = k
-- 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 : α
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
have 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
Tactic: have := hFab (F.intervalGapsWithin_mapsTo h a b (x := j) (by grind))
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (goal)
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
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2
have 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
Tactic: wlog hj : j < k + 1 generalizing j
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (goal)
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
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2
have 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
Tactic: wlog hj : j < k + 1 generalizing j
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (goal)
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
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2
have h₁ : Eq (α := Fin (k + 1)) (↑j : Fin (k + 1)) (↑(↑(↑j : Fin (k + 1)) : ℕ) : Fin (k + 1))
Tactic: convert! this (j : Fin (k + 1)) (by grind) using 3
-- 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
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2
have pos : ∀ (hj₁ : j = 0), (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
-- 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
pos :
  ∀ (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
have neg : ∀ (hj₁ : ¬j = 0), (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
-- 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
⊢ (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 (↑0 : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑0 : Fin (k + 1))).2
Tactic: simp only [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
⊢ (F.intervalGapsWithin h a b (↑0 : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑0 : Fin (k + 1))).2
have pos : ∀ (hk : 0 = k), (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
-- 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
pos :
  ∀ (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
have neg : ∀ (hk : ¬0 = k), (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
-- 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 : 0 = k
⊢ (F.intervalGapsWithin h a b (↑0 : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑0 : Fin (k + 1))).2
have pos : a ≤ (F.intervalGapsWithin h a b 0).2
Tactic: simp only [natCast_zero, intervalGapsWithin_zero_fst]
-- 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
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2
have hk : k - 1 + 1 = k
Tactic: have hk : k - 1 + 1 = k := by omega
-- 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
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2
have pos : ∀ (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