awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
neg₅ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      ¬(↑k : ℕ) + 1 < (↑j : ℕ) → ¬(↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 + 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 : ℕ) → (↑k : ℕ) < (↑j : ℕ) + 1 → (↑k : ℕ) < (↑j : ℕ) → (↑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 : ℕ)
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
neg₅ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      ¬(↑k : ℕ) + 1 < (↑j : ℕ) → ¬(↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 + 1 = (↑k : ℕ) + 1 + 1
pos₆ : ¬(↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑j : ℕ) + 1 → (↑k : ℕ) < (↑j : ℕ) → (↑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 pos₇ : ¬(↑j : ℕ) < (↑i : ℕ) →
  (↑k : ℕ) < (↑i : ℕ) →
    (↑k : ℕ) < (↑j : ℕ) + 1 → ¬(↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) + 1 < (↑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
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
neg₅ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      ¬(↑k : ℕ) + 1 < (↑j : ℕ) → ¬(↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 + 1 = (↑k : ℕ) + 1 + 1
pos₆ : ¬(↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑j : ℕ) + 1 → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) = (↑k : ℕ)
pos₇ :
  ¬(↑j : ℕ) < (↑i : ℕ) →
    (↑k : ℕ) < (↑i : ℕ) →
      (↑k : ℕ) < (↑j : ℕ) + 1 → ¬(↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) + 1 < (↑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 neg₆ : ¬(↑j : ℕ) < (↑i : ℕ) →
  (↑k : ℕ) < (↑i : ℕ) →
    (↑k : ℕ) < (↑j : ℕ) + 1 → ¬(↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ) + 1 + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPredOrder (goal)
Goal:
⊢ SuccOrder (Fin 0)
have le_succ : ∀ (a : Fin 0), a ≤ a.elim0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPredOrder (goal)
Goal:
le_succ : ∀ (a : Fin 0), a ≤ a.elim0
⊢ SuccOrder (Fin 0)
have max_of_succ_le : ∀ {a : Fin 0}, a.elim0 ≤ a → IsMax a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPredOrder (goal)
Goal:
le_succ : ∀ (a : Fin 0), a ≤ a.elim0
max_of_succ_le : ∀ {a : Fin 0}, a.elim0 ≤ a → IsMax a
⊢ SuccOrder (Fin 0)
have succ_le_of_lt : ∀ {a b : Fin 0}, a < b → a.elim0 ≤ b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPredOrder (goal)
Goal:
le_succ : ∀ (a : Fin 0), a ≤ a.elim0
max_of_succ_le : ∀ {a : Fin 0}, a.elim0 ≤ a → IsMax a
succ_le_of_lt : ∀ {a b : Fin 0}, a < b → a.elim0 ≤ b
⊢ SuccOrder (Fin 0)
have succ : Fin 0 → Fin 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPredOrder (goal)
Goal:
n : ℕ
i : Fin (n + 1)
hi : ¬IsMax i
j : Fin (n + 1)
⊢ i < j ↔
    (fun (i : Fin (n + 1)) ↦ (lastCases (motive := fun (x : Fin (n + 1)) ↦ Fin (n + 1)) (last n) succ i : Fin (n + 1)))
        i ≤
      j
have obtain : ∀ (i : Fin n) (hi : ¬IsMax i.castSucc),
  i.castSucc < j ↔
    (fun (i : Fin (n + 1)) ↦ (lastCases (motive := fun (x : Fin (n + 1)) ↦ Fin (n + 1)) (last n) succ i : Fin (n + 1)))
        i.castSucc ≤
      j
Tactic: obtain ⟨i, rfl⟩ := Fin.eq_castSucc_of_ne_last (by simpa using hi)
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPredOrder (goal)
Goal:
n : ℕ
i : Fin (n + 1)
hi : IsMax i
⊢ (fun (i : Fin (n + 1)) ↦ (lastCases (motive := fun (x : Fin (n + 1)) ↦ Fin (n + 1)) (last n) succ i : Fin (n + 1)))
      i =
    i
have obtain : ∀ (hi : IsMax (last n)),
  (fun (i : Fin (n + 1)) ↦ (lastCases (motive := fun (x : Fin (n + 1)) ↦ Fin (n + 1)) (last n) succ i : Fin (n + 1)))
      (last n) =
    last n
Tactic: obtain rfl : i = Fin.last n := by simpa using hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPredOrder (goal)
Goal:
⊢ PredOrder (Fin 0)
have pred_le : ∀ (a : Fin 0), a.elim0 ≤ a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPredOrder (goal)
Goal:
pred_le : ∀ (a : Fin 0), a.elim0 ≤ a
⊢ PredOrder (Fin 0)
have min_of_le_pred : ∀ {a : Fin 0}, a ≤ a.elim0 → IsMin a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPredOrder (goal)
Goal:
pred_le : ∀ (a : Fin 0), a.elim0 ≤ a
min_of_le_pred : ∀ {a : Fin 0}, a ≤ a.elim0 → IsMin a
⊢ PredOrder (Fin 0)
have le_pred_of_lt : ∀ {a b : Fin 0}, a < b → a ≤ b.elim0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPredOrder (goal)
Goal:
pred_le : ∀ (a : Fin 0), a.elim0 ≤ a
min_of_le_pred : ∀ {a : Fin 0}, a ≤ a.elim0 → IsMin a
le_pred_of_lt : ∀ {a b : Fin 0}, a < b → a ≤ b.elim0
⊢ PredOrder (Fin 0)
have pred : Fin 0 → Fin 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPredOrder (goal)
Goal:
n : ℕ
i : Fin (n + 1)
hi : ¬IsMin i
j : Fin (n + 1)
⊢ j < i ↔
    j ≤ (fun (i : Fin (n + 1)) ↦ (cases (motive := fun (x : Fin (n + 1)) ↦ Fin (n + 1)) 0 castSucc i : Fin (n + 1))) i
have obtain : ∀ (i : Fin n) (hi : ¬IsMin i.succ),
  j < i.succ ↔
    j ≤
      (fun (i : Fin (n + 1)) ↦ (cases (motive := fun (x : Fin (n + 1)) ↦ Fin (n + 1)) 0 castSucc i : Fin (n + 1)))
        i.succ
Tactic: obtain ⟨i, rfl⟩ := Fin.eq_succ_of_ne_zero (by simpa using hi)
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPredOrder (goal)
Goal:
n : ℕ
i : Fin (n + 1)
hi : IsMin i
⊢ (fun (i : Fin (n + 1)) ↦ (cases (motive := fun (x : Fin (n + 1)) ↦ Fin (n + 1)) 0 castSucc i : Fin (n + 1))) i = i
have obtain : ∀ (hi : IsMin (α := Fin (n + 1)) 0),
  Eq (α := Fin (n + 1))
    ((fun (i : Fin (n + 1)) ↦ (cases (motive := fun (x : Fin (n + 1)) ↦ Fin (n + 1)) 0 castSucc i : Fin (n + 1))) 0) 0
Tactic: obtain rfl : i = 0 := by simpa using hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 2) → Sort u_1
x : α 0
p : (i : Fin n.succ) → α i.succ
⊢ Eq (α := α 1) (cons (α := α) x p 1 : α 1) (p 0)
have rw : Eq (α := α 1) (cons (α := α) x p 1) (cons (α := α) x p (succ 0))
Tactic: rw [← cons_succ x p]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 2) → Sort u_1
x : α 0
p : (i : Fin n.succ) → α i.succ
⊢ Eq (α := α (last (n + 1))) (cons (α := α) x p (last (n + 1)) : α (last (n + 1))) (p (last n))
have rw : Eq (α := α (last (n + 1))) (cons (α := α) x p (last (n + 1))) (cons (α := α) x p (last n).succ)
Tactic: rw [← cons_succ x p]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
⊢ cons (α := α) x (update (β := fun (i : Fin n) ↦ α i.succ) p i y) = update (β := α) (cons (α := α) x p) i.succ y
have h : ∀ (j : Fin (n + 1)),
  cons (α := α) x (update (β := fun (i : Fin n) ↦ α i.succ) p i y) j = update (β := α) (cons (α := α) x p) i.succ y j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
⊢ cons (α := α) x (update (β := fun (i : Fin n) ↦ α i.succ) p i y) j = update (β := α) (cons (α := α) x p) i.succ y j
have h : Eq (α := α 0) (cons (α := α) x (update (β := fun (i : Fin n) ↦ α i.succ) p i y) 0)
  (update (β := α) (cons (α := α) x p) i.succ y 0)
Tactic: cases j using Fin.cases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
h :
  Eq (α := α 0) (cons (α := α) x (update (β := fun (i : Fin n) ↦ α i.succ) p i y) 0)
    (update (β := α) (cons (α := α) x p) i.succ y 0)
⊢ cons (α := α) x (update (β := fun (i : Fin n) ↦ α i.succ) p i y) j = update (β := α) (cons (α := α) x p) i.succ y j
have h₁ : ∀ (i_1 : Fin n),
  Eq (α := α i_1.succ) (cons (α := α) x (update (β := fun (i : Fin n) ↦ α i.succ) p i y) i_1.succ)
    (update (β := α) (cons (α := α) x p) i.succ y i_1.succ)
Tactic: cases j using Fin.cases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
⊢ update (β := α) (cons (α := α) x p) 0 z = cons (α := α) z p
have h : ∀ (j : Fin (n + 1)), update (β := α) (cons (α := α) x p) 0 z j = cons (α := α) z p j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
j : Fin (n + 1)
⊢ update (β := α) (cons (α := α) x p) 0 z j = cons (α := α) z p j
have h : Eq (α := α 0) (update (β := α) (cons (α := α) x p) 0 z 0) (cons (α := α) z p 0)
Tactic: cases j using Fin.cases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
j : Fin (n + 1)
h : Eq (α := α 0) (update (β := α) (cons (α := α) x p) 0 z 0) (cons (α := α) z p 0)
⊢ update (β := α) (cons (α := α) x p) 0 z j = cons (α := α) z p j
have h₁ : ∀ (i : Fin n), Eq (α := α i.succ) (update (β := α) (cons (α := α) x p) 0 z i.succ) (cons (α := α) z p i.succ)
Tactic: cases j using Fin.cases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
⊢ cons (α := α) (q 0) (tail (α := α) q) = q
have h : ∀ (j : Fin (n + 1)), cons (α := α) (q 0) (tail (α := α) q) j = q j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
⊢ cons (α := α) (q 0) (tail (α := α) q) j = q j
have h : Eq (α := α 0) (cons (α := α) (q 0) (tail (α := α) q) 0) (q 0)
Tactic: cases j using Fin.cases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
h : Eq (α := α 0) (cons (α := α) (q 0) (tail (α := α) q) 0) (q 0)
⊢ cons (α := α) (q 0) (tail (α := α) q) j = q j
have h₁ : ∀ (i : Fin n), Eq (α := α i.succ) (cons (α := α) (q 0) (tail (α := α) q) i.succ) (q i.succ)
Tactic: cases j using Fin.cases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Fin (n + 1) → Sort u
x_1 : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
z : α 0
motive : ((i : Fin n.succ) → α i) → Sort v
cons : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → motive (Fin.cons (α := α) x₀ x)
x : (i : Fin n.succ) → α i
⊢ motive (Fin.cons (α := α) (x 0) (tail (α := α) x)) = motive x
have rw : motive x = motive x
Tactic: rw [cons_self_tail]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
motive : ((i : Fin n.succ) → α i) → Sort v
cons : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → motive (Fin.cons (α := α) x₀ x)
x₀ : α 0
x : (i : Fin n) → α i.succ
⊢ consCases (α := α) (motive := fun (x : (i : Fin (n + 1)) → α i) ↦ motive x) cons (Fin.cons (α := α) x₀ x) = cons x₀ x
have rw : cons (Fin.cons (α := α) x₀ x 0) (tail (α := α) (Fin.cons (α := α) x₀ x)) = cons x₀ x
Tactic: rw [consCases, cast_eq]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i j : Fin (n + 1)
⊢ Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x i : α)
      (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x j) →
    i = j
have zero : Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x 0 : α)
    (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x j : α) →
  0 = j
Tactic: cases i using Fin.cases
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i j : Fin (n + 1)
zero :
  Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x 0 : α)
      (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x j : α) →
    0 = j
⊢ Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x i : α)
      (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x j) →
    i = j
have succ : ∀ (i : Fin n),
  Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x i.succ : α)
      (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x j : α) →
    i.succ = j
Tactic: cases i using Fin.cases
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
j : Fin (n + 1)
⊢ Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x 0 : α)
      (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x j : α) →
    0 = j
have zero : Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x 0 : α)
    (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x 0 : α) →
  Eq (α := Fin (n + 1)) 0 0
Tactic: cases j using Fin.cases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
j : Fin (n + 1)
zero :
  Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x 0 : α)
      (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x 0 : α) →
    Eq (α := Fin (n + 1)) 0 0
⊢ Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x 0 : α)
      (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x j : α) →
    0 = j
have zero₁ : ∀ (i : Fin n),
  Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x 0 : α)
      (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x i.succ : α) →
    0 = i.succ
Tactic: cases j using Fin.cases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
j : Fin (n + 1)
i : Fin n
⊢ Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x i.succ : α)
      (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x j : α) →
    i.succ = j
have succ : Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x i.succ : α)
    (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x 0 : α) →
  i.succ = 0
Tactic: cases j using Fin.cases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
j : Fin (n + 1)
i : Fin n
succ :
  Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x i.succ : α)
      (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x 0 : α) →
    i.succ = 0
⊢ Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x i.succ : α)
      (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x j : α) →
    i.succ = j
have succ₁ : ∀ (i_1 : Fin n),
  Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x i.succ : α)
      (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x i_1.succ : α) →
    i.succ = i_1.succ
Tactic: cases j using Fin.cases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
⊢ Injective.{1, u_1 + 1} (α := Fin (n + 1)) (β := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x) ↔
    ¬x₀ ∈ Set.range x ∧ Injective x
have refine_1 : ∀ (h : Injective.{1, u_1 + 1} (α := Fin (n + 1)) (β := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x)),
  ¬x₀ ∈ Set.range x
Tactic: refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ cons_injective_of_injective h.1 h.2⟩
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
refine_1 :
  ∀ (h : Injective.{1, u_1 + 1} (α := Fin (n + 1)) (β := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x)),
    ¬x₀ ∈ Set.range x
⊢ Injective.{1, u_1 + 1} (α := Fin (n + 1)) (β := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x) ↔
    ¬x₀ ∈ Set.range x ∧ Injective x
have refine_2 : ∀ (h : Injective.{1, u_1 + 1} (α := Fin (n + 1)) (β := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x)), Injective x
Tactic: refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ cons_injective_of_injective h.1 h.2⟩
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (hypothesis)
Goal:
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
h : Injective.{1, u_1 + 1} (α := Fin (n + 1)) (β := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x)
i : Fin n
hi : x i = x₀
⊢ False
have h₁ : Eq.{u_1 + 1} (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x i.succ : α)
    (cons (α := fun (a : Fin n.succ) ↦ α) x₀ x 0 : α) →
  i.succ = 0
Tactic: replace h := @h i.succ 0
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
z : α 0
⊢ tail (α := α) (update (β := α) q 0 z) = tail (α := α) q
have h : ∀ (j : Fin n), tail (α := α) (update (β := α) q 0 z) j = tail (α := α) q j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
⊢ tail (α := α) (update (β := α) q i.succ y) = update (β := fun (a : Fin n) ↦ α a.succ) (tail (α := α) q) i y
have h : ∀ (j : Fin n),
  tail (α := α) (update (β := α) q i.succ y) j = update (β := fun (a : Fin n) ↦ α a.succ) (tail (α := α) q) i y j
Tactic: ext j