awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ (i.succAbove j).succAbove (j.predAbove i) = i
have inr : j.succ.succAbove (j.predAbove i) = i
Tactic: rw [succAbove_of_le_castSucc _ _ h,
      succ_succAbove_predAbove (Fin.ne_of_lt <| le_castSucc_iff.mp h)]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
inr : j.succ.succAbove (j.predAbove i) = i
⊢ (i.succAbove j).succAbove (j.predAbove i) = i
have inr₁ : i = i
Tactic: rw [succAbove_of_le_castSucc _ _ h,
      succ_succAbove_predAbove (Fin.ne_of_lt <| le_castSucc_iff.mp h)]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (hypothesis)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ (i.succAbove j).succAbove (j.predAbove i) = i
have x : j.castSucc < i ∨ i ≤ j.castSucc
Tactic: cases Fin.lt_or_le j.castSucc i with
  | inl h => rw [succAbove_of_castSucc_lt _ _ h, succAbove_predAbove (Fin.ne_of_gt h)]
  | inr h =>
    rw [succAbove_of_le_castSucc _ _ h,
      succ_succAbove_predAbove (Fin.ne_of_lt <| le_castSucc_iff.mp h)]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
⊢ (i.succAbove j).succAbove ((j.predAbove i).succAbove k) = i.succAbove (j.succAbove k)
have h : (↑((i.succAbove j).succAbove ((j.predAbove i).succAbove k)) : ℕ) = (↑(i.succAbove (j.succAbove k)) : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
⊢ (↑((i.succAbove j).succAbove ((j.predAbove i).succAbove k)) : ℕ) = (↑(i.succAbove (j.succAbove k)) : ℕ)
have h : (if
      (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) <
        if (↑j : ℕ) < (↑i : ℕ) then (↑j : ℕ) else (↑j : ℕ) + 1 then
    if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
  else (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1) =
  if (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) < (↑i : ℕ) then
    if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
  else (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1
Tactic: simp only [succAbove, predAbove, lt_def, val_castSucc, apply_dite Fin.val, val_pred, coe_castPred,
    dite_eq_ite, apply_ite Fin.val, val_succ]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
⊢ (if
        (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) <
          if (↑j : ℕ) < (↑i : ℕ) then (↑j : ℕ) else (↑j : ℕ) + 1 then
      if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1) =
    if (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) < (↑i : ℕ) then
      if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1
have pos : (↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) - 1 → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
pos : (↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) - 1 → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ)
⊢ (if
        (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) <
          if (↑j : ℕ) < (↑i : ℕ) then (↑j : ℕ) else (↑j : ℕ) + 1 then
      if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1) =
    if (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) < (↑i : ℕ) then
      if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1
have neg : (↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) - 1 → (↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ) + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
pos : (↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) - 1 → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ)
neg :
  (↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) - 1 → (↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ) + 1
⊢ (if
        (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) <
          if (↑j : ℕ) < (↑i : ℕ) then (↑j : ℕ) else (↑j : ℕ) + 1 then
      if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1) =
    if (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) < (↑i : ℕ) then
      if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1
have pos₁ : (↑j : ℕ) < (↑i : ℕ) →
  (↑k : ℕ) < (↑i : ℕ) - 1 → ¬(↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
pos : (↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) - 1 → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ)
neg :
  (↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) - 1 → (↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ) + 1
pos₁ :
  (↑j : ℕ) < (↑i : ℕ) →
    (↑k : ℕ) < (↑i : ℕ) - 1 → ¬(↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1
⊢ (if
        (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) <
          if (↑j : ℕ) < (↑i : ℕ) then (↑j : ℕ) else (↑j : ℕ) + 1 then
      if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1) =
    if (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) < (↑i : ℕ) then
      if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1
have neg₁ : (↑j : ℕ) < (↑i : ℕ) →
  (↑k : ℕ) < (↑i : ℕ) - 1 → ¬(↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1 + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
pos : (↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) - 1 → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ)
neg :
  (↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) - 1 → (↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ) + 1
pos₁ :
  (↑j : ℕ) < (↑i : ℕ) →
    (↑k : ℕ) < (↑i : ℕ) - 1 → ¬(↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1
neg₁ :
  (↑j : ℕ) < (↑i : ℕ) →
    (↑k : ℕ) < (↑i : ℕ) - 1 → ¬(↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1 + 1
⊢ (if
        (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) <
          if (↑j : ℕ) < (↑i : ℕ) then (↑j : ℕ) else (↑j : ℕ) + 1 then
      if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1) =
    if (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) < (↑i : ℕ) then
      if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1
have pos₂ : (↑j : ℕ) < (↑i : ℕ) →
  ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
    (↑k : ℕ) + 1 < (↑j : ℕ) → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
pos : (↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) - 1 → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ)
neg :
  (↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) - 1 → (↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ) + 1
pos₁ :
  (↑j : ℕ) < (↑i : ℕ) →
    (↑k : ℕ) < (↑i : ℕ) - 1 → ¬(↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1
neg₁ :
  (↑j : ℕ) < (↑i : ℕ) →
    (↑k : ℕ) < (↑i : ℕ) - 1 → ¬(↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1 + 1
pos₂ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      (↑k : ℕ) + 1 < (↑j : ℕ) → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ)
⊢ (if
        (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) <
          if (↑j : ℕ) < (↑i : ℕ) then (↑j : ℕ) else (↑j : ℕ) + 1 then
      if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1) =
    if (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) < (↑i : ℕ) then
      if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1
have neg₂ : (↑j : ℕ) < (↑i : ℕ) →
  ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
    (↑k : ℕ) + 1 < (↑j : ℕ) → (↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
pos : (↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) - 1 → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ)
neg :
  (↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) - 1 → (↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ) + 1
pos₁ :
  (↑j : ℕ) < (↑i : ℕ) →
    (↑k : ℕ) < (↑i : ℕ) - 1 → ¬(↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1
neg₁ :
  (↑j : ℕ) < (↑i : ℕ) →
    (↑k : ℕ) < (↑i : ℕ) - 1 → ¬(↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1 + 1
pos₂ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      (↑k : ℕ) + 1 < (↑j : ℕ) → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ)
neg₂ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      (↑k : ℕ) + 1 < (↑j : ℕ) → (↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1
⊢ (if
        (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) <
          if (↑j : ℕ) < (↑i : ℕ) then (↑j : ℕ) else (↑j : ℕ) + 1 then
      if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1) =
    if (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) < (↑i : ℕ) then
      if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1
have pos₃ : (↑j : ℕ) < (↑i : ℕ) →
  ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
    (↑k : ℕ) + 1 < (↑j : ℕ) → ¬(↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
pos : (↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) - 1 → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ)
neg :
  (↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) - 1 → (↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ) + 1
pos₁ :
  (↑j : ℕ) < (↑i : ℕ) →
    (↑k : ℕ) < (↑i : ℕ) - 1 → ¬(↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1
neg₁ :
  (↑j : ℕ) < (↑i : ℕ) →
    (↑k : ℕ) < (↑i : ℕ) - 1 → ¬(↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1 + 1
pos₂ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      (↑k : ℕ) + 1 < (↑j : ℕ) → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ)
neg₂ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      (↑k : ℕ) + 1 < (↑j : ℕ) → (↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1
pos₃ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      (↑k : ℕ) + 1 < (↑j : ℕ) → ¬(↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1
⊢ (if
        (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) <
          if (↑j : ℕ) < (↑i : ℕ) then (↑j : ℕ) else (↑j : ℕ) + 1 then
      if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1) =
    if (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) < (↑i : ℕ) then
      if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1
have neg₃ : (↑j : ℕ) < (↑i : ℕ) →
  ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
    (↑k : ℕ) + 1 < (↑j : ℕ) → ¬(↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1 + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
pos : (↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) - 1 → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ)
neg :
  (↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) - 1 → (↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ) + 1
pos₁ :
  (↑j : ℕ) < (↑i : ℕ) →
    (↑k : ℕ) < (↑i : ℕ) - 1 → ¬(↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1
neg₁ :
  (↑j : ℕ) < (↑i : ℕ) →
    (↑k : ℕ) < (↑i : ℕ) - 1 → ¬(↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1 + 1
pos₂ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      (↑k : ℕ) + 1 < (↑j : ℕ) → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ)
neg₂ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      (↑k : ℕ) + 1 < (↑j : ℕ) → (↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1
pos₃ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      (↑k : ℕ) + 1 < (↑j : ℕ) → ¬(↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1
neg₃ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      (↑k : ℕ) + 1 < (↑j : ℕ) → ¬(↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1 + 1
⊢ (if
        (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) <
          if (↑j : ℕ) < (↑i : ℕ) then (↑j : ℕ) else (↑j : ℕ) + 1 then
      if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1) =
    if (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) < (↑i : ℕ) then
      if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1
have pos₄ : (↑j : ℕ) < (↑i : ℕ) →
  ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
    ¬(↑k : ℕ) + 1 < (↑j : ℕ) → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) + 1 + 1 = (↑k : ℕ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
pos : (↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) - 1 → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ)
neg :
  (↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) - 1 → (↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ) + 1
pos₁ :
  (↑j : ℕ) < (↑i : ℕ) →
    (↑k : ℕ) < (↑i : ℕ) - 1 → ¬(↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1
neg₁ :
  (↑j : ℕ) < (↑i : ℕ) →
    (↑k : ℕ) < (↑i : ℕ) - 1 → ¬(↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1 + 1
pos₂ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      (↑k : ℕ) + 1 < (↑j : ℕ) → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ)
neg₂ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      (↑k : ℕ) + 1 < (↑j : ℕ) → (↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1
pos₃ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      (↑k : ℕ) + 1 < (↑j : ℕ) → ¬(↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1
neg₃ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      (↑k : ℕ) + 1 < (↑j : ℕ) → ¬(↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1 + 1
pos₄ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      ¬(↑k : ℕ) + 1 < (↑j : ℕ) → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) + 1 + 1 = (↑k : ℕ)
⊢ (if
        (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) <
          if (↑j : ℕ) < (↑i : ℕ) then (↑j : ℕ) else (↑j : ℕ) + 1 then
      if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1) =
    if (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) < (↑i : ℕ) then
      if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1
have neg₄ : (↑j : ℕ) < (↑i : ℕ) →
  ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
    ¬(↑k : ℕ) + 1 < (↑j : ℕ) → (↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) + 1 + 1 = (↑k : ℕ) + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
pos : (↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) - 1 → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ)
neg :
  (↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) - 1 → (↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ) + 1
pos₁ :
  (↑j : ℕ) < (↑i : ℕ) →
    (↑k : ℕ) < (↑i : ℕ) - 1 → ¬(↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1
neg₁ :
  (↑j : ℕ) < (↑i : ℕ) →
    (↑k : ℕ) < (↑i : ℕ) - 1 → ¬(↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1 + 1
pos₂ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      (↑k : ℕ) + 1 < (↑j : ℕ) → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ)
neg₂ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      (↑k : ℕ) + 1 < (↑j : ℕ) → (↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1
pos₃ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      (↑k : ℕ) + 1 < (↑j : ℕ) → ¬(↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1
neg₃ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      (↑k : ℕ) + 1 < (↑j : ℕ) → ¬(↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1 + 1
pos₄ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      ¬(↑k : ℕ) + 1 < (↑j : ℕ) → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) + 1 + 1 = (↑k : ℕ)
neg₄ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      ¬(↑k : ℕ) + 1 < (↑j : ℕ) → (↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) + 1 + 1 = (↑k : ℕ) + 1
⊢ (if
        (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) <
          if (↑j : ℕ) < (↑i : ℕ) then (↑j : ℕ) else (↑j : ℕ) + 1 then
      if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1) =
    if (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) < (↑i : ℕ) then
      if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1
have pos₅ : (↑j : ℕ) < (↑i : ℕ) →
  ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
    ¬(↑k : ℕ) + 1 < (↑j : ℕ) → ¬(↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 + 1 = (↑k : ℕ) + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
pos : (↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) - 1 → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ)
neg :
  (↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) - 1 → (↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ) + 1
pos₁ :
  (↑j : ℕ) < (↑i : ℕ) →
    (↑k : ℕ) < (↑i : ℕ) - 1 → ¬(↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1
neg₁ :
  (↑j : ℕ) < (↑i : ℕ) →
    (↑k : ℕ) < (↑i : ℕ) - 1 → ¬(↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1 + 1
pos₂ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      (↑k : ℕ) + 1 < (↑j : ℕ) → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ)
neg₂ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      (↑k : ℕ) + 1 < (↑j : ℕ) → (↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1
pos₃ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      (↑k : ℕ) + 1 < (↑j : ℕ) → ¬(↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1
neg₃ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      (↑k : ℕ) + 1 < (↑j : ℕ) → ¬(↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1 + 1
pos₄ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      ¬(↑k : ℕ) + 1 < (↑j : ℕ) → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) + 1 + 1 = (↑k : ℕ)
neg₄ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      ¬(↑k : ℕ) + 1 < (↑j : ℕ) → (↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) + 1 + 1 = (↑k : ℕ) + 1
pos₅ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      ¬(↑k : ℕ) + 1 < (↑j : ℕ) → ¬(↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 + 1 = (↑k : ℕ) + 1
⊢ (if
        (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) <
          if (↑j : ℕ) < (↑i : ℕ) then (↑j : ℕ) else (↑j : ℕ) + 1 then
      if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1) =
    if (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) < (↑i : ℕ) then
      if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1
have neg₅ : (↑j : ℕ) < (↑i : ℕ) →
  ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
    ¬(↑k : ℕ) + 1 < (↑j : ℕ) → ¬(↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 + 1 = (↑k : ℕ) + 1 + 1
Tactic: split_ifs