awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
⊢ (if h : j.castSucc < i then
      Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove ((i.succAbove j).castPred ⋯) = x) ↦ α x)
        (p ((i.succAbove j).castPred ⋯)) ⋯
    else
      @Eq.rec _ (i.succAbove ((i.succAbove j).pred ⋯))
        (fun (x : Fin (n + 1)) (h : i.succAbove ((i.succAbove j).pred ⋯) = x) ↦ α x)
        (p ((i.succAbove j).pred ⋯) : α (i.succAbove ((i.succAbove j).pred ⋯))) _ ⋯) =
    p j
have pos : ∀ (hlt : j.castSucc < i),
  Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove ((i.succAbove j).castPred sorry) = x) ↦ α x)
      (p ((i.succAbove j).castPred sorry)) sorry =
    p j
Tactic: split_ifs with hlt
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
pos :
  ∀ (hlt : j.castSucc < i),
    Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove ((i.succAbove j).castPred ⋯) = x) ↦ α x)
        (p ((i.succAbove j).castPred ⋯)) ⋯ =
      p j
⊢ (if h : j.castSucc < i then
      Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove ((i.succAbove j).castPred ⋯) = x) ↦ α x)
        (p ((i.succAbove j).castPred ⋯)) ⋯
    else
      @Eq.rec _ (i.succAbove ((i.succAbove j).pred ⋯))
        (fun (x : Fin (n + 1)) (h : i.succAbove ((i.succAbove j).pred ⋯) = x) ↦ α x)
        (p ((i.succAbove j).pred ⋯) : α (i.succAbove ((i.succAbove j).pred ⋯))) _ ⋯) =
    p j
have neg : ∀ (hlt : ¬j.castSucc < i),
  @Eq.rec _ (i.succAbove ((i.succAbove j).pred sorry))
      (fun (x : Fin (n + 1)) (h : i.succAbove ((i.succAbove j).pred sorry) = x) ↦ α x)
      (p ((i.succAbove j).pred sorry) : α (i.succAbove ((i.succAbove j).pred sorry))) _ sorry =
    p j
Tactic: split_ifs with hlt
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : j.castSucc < i
⊢ Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove ((i.succAbove j).castPred ⋯) = x) ↦ α x)
      (p ((i.succAbove j).castPred ⋯)) ⋯ =
    p j
have pos : ∀ (H₁ : i.succAbove j ≠ last n) (H₂ : i.succAbove ((i.succAbove j).castPred H₁) = i.succAbove j),
  Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove ((i.succAbove j).castPred H₁) = x) ↦ α x)
      (p ((i.succAbove j).castPred H₁)) H₂ =
    p j
Tactic: generalize_proofs H₁ H₂
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : j.castSucc < i
H₁ : i.succAbove j ≠ last n
H₂ : i.succAbove ((i.succAbove j).castPred H₁) = i.succAbove j
⊢ Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove ((i.succAbove j).castPred H₁) = x) ↦ α x)
      (p ((i.succAbove j).castPred H₁)) H₂ =
    p j
have pos : ∀ (H₂ : i.succAbove ((i.succAbove j).castPred H₁) = i.succAbove j),
  Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove ((i.succAbove j).castPred H₁) = x) ↦ α x)
      (p ((i.succAbove j).castPred H₁)) H₂ =
    p j
Tactic: revert H₂
Cleared hypotheses: H₂
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : j.castSucc < i
H₁ : i.succAbove j ≠ last n
⊢ ∀ (H₂ : i.succAbove ((i.succAbove j).castPred H₁) = i.succAbove j),
    Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove ((i.succAbove j).castPred H₁) = x) ↦ α x)
        (p ((i.succAbove j).castPred H₁)) H₂ =
      p j
have pos : ∀ (k : Fin n) (hk : (i.succAbove j).castPred H₁ = k) (H₂ : i.succAbove k = i.succAbove j),
  Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove k = x) ↦ α x) (p k) H₂ = p j
Tactic: generalize hk : castPred ((succAbove i) j) H₁ = k
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (hypothesis)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : j.castSucc < i
H₁ : i.succAbove j ≠ last n
k : Fin n
hk : (i.succAbove j).castPred H₁ = k
⊢ ∀ (H₂ : i.succAbove k = i.succAbove j),
    Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove k = x) ↦ α x) (p k) H₂ = p j
have hk₁ : j = k
Tactic: rw [castPred_succAbove _ _ hlt] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : j.castSucc < i
H₁ : i.succAbove j ≠ last n
k : Fin n
hk : j = k
⊢ ∀ (H₂ : i.succAbove k = i.succAbove j),
    Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove k = x) ↦ α x) (p k) H₂ = p j
have pos : ∀ (H₂ : i.succAbove j = i.succAbove j),
  Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove j = x) ↦ α x) (p j) H₂ = p j
Tactic: cases hk
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : ¬j.castSucc < i
⊢ @Eq.rec _ (i.succAbove ((i.succAbove j).pred ⋯))
      (fun (x : Fin (n + 1)) (h : i.succAbove ((i.succAbove j).pred ⋯) = x) ↦ α x)
      (p ((i.succAbove j).pred ⋯) : α (i.succAbove ((i.succAbove j).pred ⋯))) _ ⋯ =
    p j
have neg : ∀ (H₀ : NeZero (n + 1)) (H₁ : i.succAbove j ≠ 0) (H₂ : i.succAbove ((i.succAbove j).pred H₁) = i.succAbove j),
  Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove ((i.succAbove j).pred H₁) = x) ↦ α x)
      (p ((i.succAbove j).pred H₁)) H₂ =
    p j
Tactic: generalize_proofs H₀ H₁ H₂
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : ¬j.castSucc < i
H₀ : NeZero (n + 1)
H₁ : i.succAbove j ≠ 0
H₂ : i.succAbove ((i.succAbove j).pred H₁) = i.succAbove j
⊢ Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove ((i.succAbove j).pred H₁) = x) ↦ α x)
      (p ((i.succAbove j).pred H₁)) H₂ =
    p j
have neg : ∀ (H₂ : i.succAbove ((i.succAbove j).pred H₁) = i.succAbove j),
  Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove ((i.succAbove j).pred H₁) = x) ↦ α x)
      (p ((i.succAbove j).pred H₁)) H₂ =
    p j
Tactic: revert H₂
Cleared hypotheses: H₂
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : ¬j.castSucc < i
H₀ : NeZero (n + 1)
H₁ : i.succAbove j ≠ 0
⊢ ∀ (H₂ : i.succAbove ((i.succAbove j).pred H₁) = i.succAbove j),
    Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove ((i.succAbove j).pred H₁) = x) ↦ α x)
        (p ((i.succAbove j).pred H₁)) H₂ =
      p j
have neg : ∀ (k : Fin n) (hk : (i.succAbove j).pred H₁ = k) (H₂ : i.succAbove k = i.succAbove j),
  Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove k = x) ↦ α x) (p k) H₂ = p j
Tactic: generalize hk : pred (succAbove i j) H₁ = k
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (hypothesis)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : ¬j.castSucc < i
H₀ : NeZero (n + 1)
H₁ : i.succAbove j ≠ 0
k : Fin n
hk : (i.succAbove j).pred H₁ = k
⊢ ∀ (H₂ : i.succAbove k = i.succAbove j),
    Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove k = x) ↦ α x) (p k) H₂ = p j
have hk₁ : j = k
Tactic: rw [pred_succAbove _ _ (Fin.not_lt.1 hlt)] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : ¬j.castSucc < i
H₀ : NeZero (n + 1)
H₁ : i.succAbove j ≠ 0
k : Fin n
hk : j = k
⊢ ∀ (H₂ : i.succAbove k = i.succAbove j),
    Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove k = x) ↦ α x) (p k) H₂ = p j
have neg : ∀ (H₂ : i.succAbove j = i.succAbove j),
  Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove j = x) ↦ α x) (p j) H₂ = p j
Tactic: cases hk
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
a : α p
f : (i : Fin n) → α (p.succAbove i)
⊢ p.removeNth (α := α) (p.insertNth (α := α) a f) = f
have h : ∀ (x : Fin n), p.removeNth (α := α) (p.insertNth (α := α) a f) x = f x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
a : α p
f : (i : Fin n) → α (p.succAbove i)
x : Fin n
⊢ p.removeNth (α := α) (p.insertNth (α := α) a f) x = f x
have h : p.insertNth (α := α) a f (p.succAbove x) = f x
Tactic: unfold removeNth
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
f : (i : Fin (n + 1)) → α i
⊢ removeNth (α := α) 0 f = tail (α := α) f
have h : ∀ (x : Fin n), removeNth (α := α) 0 f x = tail (α := α) f x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Type u_3
f : Fin (n + 1) → α
⊢ (last n).removeNth (α := fun (i : Fin (n + 1)) ↦ α) f = init (α := fun (i : Fin (n + 1)) ↦ α) f
have h : ∀ (x : Fin n), (last n).removeNth (α := fun (i : Fin (n + 1)) ↦ α) f x = init (α := fun (i : Fin (n + 1)) ↦ α) f x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
i j : Fin (n + 1)
h : j < i
x : α i
p : (k : Fin n) → α (i.succAbove k)
⊢ i.insertNth (α := α) x p j =
    Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred ⋯) = x) ↦ α x) (p (j.castPred ⋯)) ⋯
have rw : i.succAboveCases (α := fun (x : Fin (n + 1)) ↦ α x) x p j =
  Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred sorry) = x) ↦ α x) (p (j.castPred sorry)) sorry
Tactic: rw [insertNth, succAboveCases, dif_neg (Fin.ne_of_lt h), dif_pos h]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
i j : Fin (n + 1)
h : j < i
x : α i
p : (k : Fin n) → α (i.succAbove k)
rw :
  i.succAboveCases (α := fun (x : Fin (n + 1)) ↦ α x) x p j =
    Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred ⋯) = x) ↦ α x) (p (j.castPred ⋯)) ⋯
⊢ i.insertNth (α := α) x p j =
    Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred ⋯) = x) ↦ α x) (p (j.castPred ⋯)) ⋯
have rw₁ : Eq.{u_1} (α := α j)
  (if hj : j = i then Eq.rec (motive := fun (x : Fin (n + 1)) (x_1 : i = x) ↦ α x) x sorry
    else
      if hlt : j < i then
        Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred sorry) = x) ↦ α x) (p (j.castPred sorry)) sorry
      else Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.pred sorry) = x) ↦ α x) (p (j.pred sorry)) sorry :
    α j)
  (Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred sorry) = x) ↦ α x) (p (j.castPred sorry)) sorry : α j)
Tactic: rw [insertNth, succAboveCases, dif_neg (Fin.ne_of_lt h), dif_pos h]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
i j : Fin (n + 1)
h : j < i
x : α i
p : (k : Fin n) → α (i.succAbove k)
rw :
  i.succAboveCases (α := fun (x : Fin (n + 1)) ↦ α x) x p j =
    Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred ⋯) = x) ↦ α x) (p (j.castPred ⋯)) ⋯
rw₁ :
  Eq.{u_1} (α := α j)
    (if hj : j = i then Eq.rec (motive := fun (x : Fin (n + 1)) (x_1 : i = x) ↦ α x) x ⋯
      else
        if hlt : j < i then
          Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred ⋯) = x) ↦ α x) (p (j.castPred ⋯)) ⋯
        else Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.pred ⋯) = x) ↦ α x) (p (j.pred ⋯)) ⋯ :
      α j)
    (Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred ⋯) = x) ↦ α x) (p (j.castPred ⋯)) ⋯ : α j)
⊢ i.insertNth (α := α) x p j =
    Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred ⋯) = x) ↦ α x) (p (j.castPred ⋯)) ⋯
have rw₂ : Eq.{u_1} (α := α j)
  (if hlt : j < i then
      Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred sorry) = x) ↦ α x) (p (j.castPred sorry)) sorry
    else
      @Eq.rec _ (i.succAbove (j.pred sorry)) (fun (x : Fin (n + 1)) (h : i.succAbove (j.pred sorry) = x) ↦ α x)
        (p (j.pred sorry) : α (i.succAbove (j.pred sorry))) _ sorry :
    α j)
  (Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred sorry) = x) ↦ α x) (p (j.castPred sorry)) sorry : α j)
Tactic: rw [insertNth, succAboveCases, dif_neg (Fin.ne_of_lt h), dif_pos h]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
i j : Fin (n + 1)
h : j < i
x : α i
p : (k : Fin n) → α (i.succAbove k)
rw :
  i.succAboveCases (α := fun (x : Fin (n + 1)) ↦ α x) x p j =
    Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred ⋯) = x) ↦ α x) (p (j.castPred ⋯)) ⋯
rw₁ :
  Eq.{u_1} (α := α j)
    (if hj : j = i then Eq.rec (motive := fun (x : Fin (n + 1)) (x_1 : i = x) ↦ α x) x ⋯
      else
        if hlt : j < i then
          Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred ⋯) = x) ↦ α x) (p (j.castPred ⋯)) ⋯
        else Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.pred ⋯) = x) ↦ α x) (p (j.pred ⋯)) ⋯ :
      α j)
    (Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred ⋯) = x) ↦ α x) (p (j.castPred ⋯)) ⋯ : α j)
rw₂ :
  Eq.{u_1} (α := α j)
    (if hlt : j < i then
        Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred ⋯) = x) ↦ α x) (p (j.castPred ⋯)) ⋯
      else
        @Eq.rec _ (i.succAbove (j.pred ⋯)) (fun (x : Fin (n + 1)) (h : i.succAbove (j.pred ⋯) = x) ↦ α x)
          (p (j.pred ⋯) : α (i.succAbove (j.pred ⋯))) _ ⋯ :
      α j)
    (Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred ⋯) = x) ↦ α x) (p (j.castPred ⋯)) ⋯ : α j)
⊢ i.insertNth (α := α) x p j =
    Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred ⋯) = x) ↦ α x) (p (j.castPred ⋯)) ⋯
have rw₃ : Eq.{u_1} (α := α j)
  (Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred sorry) = x) ↦ α x) (p (j.castPred sorry)) sorry : α j)
  (Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred sorry) = x) ↦ α x) (p (j.castPred sorry)) sorry : α j)
Tactic: rw [insertNth, succAboveCases, dif_neg (Fin.ne_of_lt h), dif_pos h]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
i j : Fin (n + 1)
h : i < j
x : α i
p : (k : Fin n) → α (i.succAbove k)
⊢ i.insertNth (α := α) x p j =
    Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.pred ⋯) = x) ↦ α x) (p (j.pred ⋯)) ⋯
have rw : i.succAboveCases (α := fun (x : Fin (n + 1)) ↦ α x) x p j =
  Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.pred sorry) = x) ↦ α x) (p (j.pred sorry)) sorry
Tactic: rw [insertNth, succAboveCases, dif_neg (Fin.ne_of_gt h), dif_neg (Fin.lt_asymm h)]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
i j : Fin (n + 1)
h : i < j
x : α i
p : (k : Fin n) → α (i.succAbove k)
rw :
  i.succAboveCases (α := fun (x : Fin (n + 1)) ↦ α x) x p j =
    Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.pred ⋯) = x) ↦ α x) (p (j.pred ⋯)) ⋯
⊢ i.insertNth (α := α) x p j =
    Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.pred ⋯) = x) ↦ α x) (p (j.pred ⋯)) ⋯
have rw₁ : Eq.{u_1} (α := α j)
  (if hj : j = i then Eq.rec (motive := fun (x : Fin (n + 1)) (x_1 : i = x) ↦ α x) x sorry
    else
      if hlt : j < i then
        Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred sorry) = x) ↦ α x) (p (j.castPred sorry)) sorry
      else Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.pred sorry) = x) ↦ α x) (p (j.pred sorry)) sorry :
    α j)
  (Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.pred sorry) = x) ↦ α x) (p (j.pred sorry)) sorry : α j)
Tactic: rw [insertNth, succAboveCases, dif_neg (Fin.ne_of_gt h), dif_neg (Fin.lt_asymm h)]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
i j : Fin (n + 1)
h : i < j
x : α i
p : (k : Fin n) → α (i.succAbove k)
rw :
  i.succAboveCases (α := fun (x : Fin (n + 1)) ↦ α x) x p j =
    Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.pred ⋯) = x) ↦ α x) (p (j.pred ⋯)) ⋯
rw₁ :
  Eq.{u_1} (α := α j)
    (if hj : j = i then Eq.rec (motive := fun (x : Fin (n + 1)) (x_1 : i = x) ↦ α x) x ⋯
      else
        if hlt : j < i then
          Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred ⋯) = x) ↦ α x) (p (j.castPred ⋯)) ⋯
        else Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.pred ⋯) = x) ↦ α x) (p (j.pred ⋯)) ⋯ :
      α j)
    (Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.pred ⋯) = x) ↦ α x) (p (j.pred ⋯)) ⋯ : α j)
⊢ i.insertNth (α := α) x p j =
    Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.pred ⋯) = x) ↦ α x) (p (j.pred ⋯)) ⋯
have rw₂ : Eq.{u_1} (α := α j)
  (if hlt : j < i then
      Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred sorry) = x) ↦ α x) (p (j.castPred sorry)) sorry
    else
      @Eq.rec _ (i.succAbove (j.pred sorry)) (fun (x : Fin (n + 1)) (h : i.succAbove (j.pred sorry) = x) ↦ α x)
        (p (j.pred sorry) : α (i.succAbove (j.pred sorry))) _ sorry :
    α j)
  (Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.pred sorry) = x) ↦ α x) (p (j.pred sorry)) sorry : α j)
Tactic: rw [insertNth, succAboveCases, dif_neg (Fin.ne_of_gt h), dif_neg (Fin.lt_asymm h)]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
i j : Fin (n + 1)
h : i < j
x : α i
p : (k : Fin n) → α (i.succAbove k)
rw :
  i.succAboveCases (α := fun (x : Fin (n + 1)) ↦ α x) x p j =
    Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.pred ⋯) = x) ↦ α x) (p (j.pred ⋯)) ⋯
rw₁ :
  Eq.{u_1} (α := α j)
    (if hj : j = i then Eq.rec (motive := fun (x : Fin (n + 1)) (x_1 : i = x) ↦ α x) x ⋯
      else
        if hlt : j < i then
          Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred ⋯) = x) ↦ α x) (p (j.castPred ⋯)) ⋯
        else Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.pred ⋯) = x) ↦ α x) (p (j.pred ⋯)) ⋯ :
      α j)
    (Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.pred ⋯) = x) ↦ α x) (p (j.pred ⋯)) ⋯ : α j)
rw₂ :
  Eq.{u_1} (α := α j)
    (if hlt : j < i then
        Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred ⋯) = x) ↦ α x) (p (j.castPred ⋯)) ⋯
      else
        @Eq.rec _ (i.succAbove (j.pred ⋯)) (fun (x : Fin (n + 1)) (h : i.succAbove (j.pred ⋯) = x) ↦ α x)
          (p (j.pred ⋯) : α (i.succAbove (j.pred ⋯))) _ ⋯ :
      α j)
    (Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.pred ⋯) = x) ↦ α x) (p (j.pred ⋯)) ⋯ : α j)
⊢ i.insertNth (α := α) x p j =
    Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.pred ⋯) = x) ↦ α x) (p (j.pred ⋯)) ⋯
have rw₃ : Eq.{u_1} (α := α j)
  (@Eq.rec _ (i.succAbove (j.pred sorry)) (fun (x : Fin (n + 1)) (h : i.succAbove (j.pred sorry) = x) ↦ α x)
      (p (j.pred sorry) : α (i.succAbove (j.pred sorry))) _ sorry :
    α j)
  (Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.pred sorry) = x) ↦ α x) (p (j.pred sorry)) sorry : α j)
Tactic: rw [insertNth, succAboveCases, dif_neg (Fin.ne_of_gt h), dif_neg (Fin.lt_asymm h)]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α 0
p : (j : Fin n) → α (succAbove 0 j)
⊢ insertNth (α := α) 0 x p = cons (α := α) x fun (j : Fin n) ↦ cast ⋯ (p j)
have refine : p = removeNth (α := α) 0 (cons (α := α) x fun (j : Fin n) ↦ cast sorry (p j))
Tactic: refine insertNth_eq_iff.2 ⟨by simp, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α 0
p : (j : Fin n) → α (succAbove 0 j)
⊢ p = removeNth (α := α) 0 (cons (α := α) x fun (j : Fin n) ↦ cast ⋯ (p j))
have h : ∀ (j : Fin n), p j = removeNth (α := α) 0 (cons (α := α) x fun (j : Fin n) ↦ cast sorry (p j)) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
⊢ (last n).insertNth (α := α) x p = snoc (α := α) (fun (j : Fin n) ↦ cast ⋯ (p j)) x
have refine : p = (last n).removeNth (α := α) (snoc (α := α) (fun (j : Fin n) ↦ cast sorry (p j)) x)
Tactic: refine insertNth_eq_iff.2 ⟨by simp, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
⊢ p = (last n).removeNth (α := α) (snoc (α := α) (fun (j : Fin n) ↦ cast ⋯ (p j)) x)
have h : ∀ (j : Fin n), p j = (last n).removeNth (α := α) (snoc (α := α) (fun (j : Fin n) ↦ cast sorry (p j)) x) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ p j = (last n).removeNth (α := α) (snoc (α := α) (fun (j : Fin n) ↦ cast ⋯ (p j)) x) j
have h : p j ≍ (last n).removeNth (α := α) (snoc (α := α) (fun (j : Fin n) ↦ cast sorry (p j)) x) j
Tactic: apply eq_of_heq
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ p j ≍ (last n).removeNth (α := α) (snoc (α := α) (fun (j : Fin n) ↦ cast ⋯ (p j)) x) j
have trans : HEq (p j) (β := α j.castSucc) (snoc (α := α) (fun (j : Fin n) ↦ cast sorry (p j)) x j.castSucc)
Tactic: trans snoc (fun j ↦ _root_.cast (congr_arg α (succAbove_last_apply j)) (p j)) x j.castSucc
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
trans : HEq (p j) (β := α j.castSucc) (snoc (α := α) (fun (j : Fin n) ↦ cast ⋯ (p j)) x j.castSucc)
⊢ p j ≍ (last n).removeNth (α := α) (snoc (α := α) (fun (j : Fin n) ↦ cast ⋯ (p j)) x) j
have trans₁ : HEq (α := α j.castSucc) (snoc (α := α) (fun (j : Fin n) ↦ cast sorry (p j)) x j.castSucc)
  ((last n).removeNth (α := α) (snoc (α := α) (fun (j : Fin n) ↦ cast sorry (p j)) x) j)
Tactic: trans snoc (fun j ↦ _root_.cast (congr_arg α (succAbove_last_apply j)) (p j)) x j.castSucc
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ HEq (p j) (β := α j.castSucc) (snoc (α := α) (fun (j : Fin n) ↦ cast ⋯ (p j)) x j.castSucc)
have rw : p j ≍ cast sorry (p j)
Tactic: rw [snoc_castSucc]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ HEq (α := α j.castSucc) (snoc (α := α) (fun (j : Fin n) ↦ cast ⋯ (p j)) x j.castSucc)
    ((last n).removeNth (α := α) (snoc (α := α) (fun (j : Fin n) ↦ cast ⋯ (p j)) x) j)
have a : j.castSucc = (last n).succAbove j
Tactic: apply congr_arg_heq
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ j.castSucc = (last n).succAbove j
have a : j.castSucc = j.castSucc
Tactic: rw [succAbove_last]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
j i₁ : Fin (n + 1)
⊢ Eq.{u_3} (α := α) (i.insertNth (α := fun (x : Fin (n + 1)) ↦ α) a f j.rev : α)
    (i.rev.insertNth (α := fun (x : Fin (n + 1)) ↦ α) a (f ∘ rev) j : α)
have x : Eq.{u_3} (α := α) (i.insertNth (α := fun (x : Fin (n + 1)) ↦ α) a f i.rev.rev : α)
  (i.rev.insertNth (α := fun (x : Fin (n + 1)) ↦ α) a (f ∘ rev) i.rev)
Tactic: induction j using Fin.succAboveCases
Cleared hypotheses: j