awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
h : Injective.{1, u_2 + 1} (α := Fin (n + 1)) (β := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀)
⊢ Injective x

Tactic:
simpa [Function.comp] using h.comp (Fin.castSucc_injective _)

Premises used: Function.comp, Fin.castSucc_injective, Function.Injective.comp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
h : Injective.{1, u_2 + 1} (α := Fin (n + 1)) (β := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀)
i : Fin n
hi : x i = x₀
⊢ i.castSucc = last n

Tactic:
rw [← @snoc_last n (fun i ↦ α) x₀ x, ← @snoc_castSucc n (fun i ↦ α) x₀ x i,
      h.eq_iff] at hi

Premises used: Fin.snoc_castSucc, Function.Injective.eq_iff, Fin.snoc_last
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
h : Injective.{1, u_2 + 1} (α := Fin (n + 1)) (β := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀)
i : Fin n
hi : i.castSucc = last n
⊢ False

Tactic:
ne_last_of_lt i.castSucc_lt_last hi

Premises used: Fin.castSucc_lt_last, Fin.ne_last_of_lt
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
h : Injective.{1, u_2 + 1} (α := Fin (n + 1)) (β := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀)
i : Fin n
hi : i.castSucc = last n
⊢ False

Tactic:
exact ne_last_of_lt i.castSucc_lt_last hi

Premises used: Fin.castSucc_lt_last, Fin.ne_last_of_lt
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
P : Fin (n + 1) → Prop
⊢ (∀ (i : Fin (n + 1)), P i) ↔ P (last n) ∧ ∀ (i : Fin n), P i.castSucc

Tactic:
⟨fun h ↦ ⟨h _, fun _ ↦ h _⟩, fun h ↦ lastCases h.1 h.2⟩

Premises used: Fin.lastCases, Fin.last, And.intro, Iff.intro, Fin.castSucc
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
P : Fin (m + n) → Prop
⊢ (∀ (i : Fin (m + n)), P i) ↔ (∀ (i : Fin m), P (castAdd n i)) ∧ ∀ (j : Fin n), P (natAdd m j)

Tactic:
⟨fun h => ⟨fun _ => h _, fun _ => h _⟩, fun ⟨hm, hn⟩ => Fin.addCases hm hn⟩

Premises used: Fin.natAdd, Fin.castAdd, _private.0.Fin.forall_fin_add.match_1, Fin.addCases, And.intro, Iff.intro
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
γ : Fin (m + n) → Sort u_3
P : ((i : Fin (m + n)) → γ i) → Prop
h :
  ∀ (vₘ : (i : Fin m) → γ (castAdd n i)) (vₙ : (j : Fin n) → γ (natAdd m j)),
    P fun (i : Fin (m + n)) ↦ addCases (motive := fun (x : Fin (m + n)) ↦ γ x) vₘ vₙ i
v : (i : Fin (m + n)) → γ i
⊢ P fun (i : Fin (m + n)) ↦
    addCases (motive := fun (x : Fin (m + n)) ↦ γ x) (fun (i : Fin m) ↦ v (castAdd n i))
      (fun (j : Fin n) ↦ v (natAdd m j)) i

Tactic:
h (fun i => v (castAdd n i)) (fun j => v (natAdd m j))

Premises used: Fin.natAdd, Fin.castAdd
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
γ : Fin (m + n) → Sort u_3
P : ((i : Fin (m + n)) → γ i) → Prop
h :
  ∀ (vₘ : (i : Fin m) → γ (castAdd n i)) (vₙ : (j : Fin n) → γ (natAdd m j)),
    P fun (i : Fin (m + n)) ↦ addCases (motive := fun (x : Fin (m + n)) ↦ γ x) vₘ vₙ i
v : (i : Fin (m + n)) → γ i
h₁ :
  ∀ (x : Fin (m + n)),
    v =
      addCases (motive := fun (x : Fin (m + n)) ↦ γ x) (fun (i : Fin m) ↦ v (castAdd n i)) fun (j : Fin n) ↦
        v (natAdd m j)
⊢ P v

Tactic:
convert! h (fun i => v (castAdd n i)) (fun j => v (natAdd m j))

Premises used: Fin.natAdd, Fin.castAdd
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
γ : Fin (m + n) → Sort u_3
P : ((i : Fin (m + n)) → γ i) → Prop
h :
  ∀ (vₘ : (i : Fin m) → γ (castAdd n i)) (vₙ : (j : Fin n) → γ (natAdd m j)),
    P fun (i : Fin (m + n)) ↦ addCases (motive := fun (x : Fin (m + n)) ↦ γ x) vₘ vₙ i
v : (i : Fin (m + n)) → γ i
x : Fin (m + n)
⊢ v =
    addCases (motive := fun (x : Fin (m + n)) ↦ γ x) (fun (i : Fin m) ↦ v (castAdd n i)) fun (j : Fin n) ↦
      v (natAdd m j)

Tactic:
(addCases_castAdd_natAdd v).symm

Premises used: Fin.addCases_castAdd_natAdd, Eq.symm
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
γ : Fin (m + n) → Sort u_3
P : ((i : Fin (m + n)) → γ i) → Prop
h :
  ∀ (vₘ : (i : Fin m) → γ (castAdd n i)) (vₙ : (j : Fin n) → γ (natAdd m j)),
    P fun (i : Fin (m + n)) ↦ addCases (motive := fun (x : Fin (m + n)) ↦ γ x) vₘ vₙ i
v : (i : Fin (m + n)) → γ i
x : Fin (m + n)
⊢ v =
    addCases (motive := fun (x : Fin (m + n)) ↦ γ x) (fun (i : Fin m) ↦ v (castAdd n i)) fun (j : Fin n) ↦
      v (natAdd m j)

Tactic:
exact (addCases_castAdd_natAdd v).symm

Premises used: Fin.addCases_castAdd_natAdd, Eq.symm
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
P : Fin (n + 1) → Prop
hi : P (last n)
⊢ P (last n) ∨ ∃ (i : Fin n), P i.castSucc

Tactic:
.inl hi

Premises used: Or.inl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
P : Fin (n + 1) → Prop
hi : P (last n)
⊢ P (last n) ∨ ∃ (i : Fin n), P i.castSucc

Tactic:
exact .inl hi
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
P : Fin (n + 1) → Prop
i : Fin n
hi : P i.castSucc
⊢ P (last n) ∨ ∃ (i : Fin n), P i.castSucc

Tactic:
.inr ⟨_, hi⟩

Premises used: Exists.intro, Or.inr
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
P : Fin (n + 1) → Prop
i : Fin n
hi : P i.castSucc
⊢ P (last n) ∨ ∃ (i : Fin n), P i.castSucc

Tactic:
exact .inr ⟨_, hi⟩
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
P : Fin (n + 1) → Prop
i : Fin (n + 1)
hi : P i
last : ∀ (hi : P (Fin.last n)), P (Fin.last n) ∨ ∃ (i : Fin n), P i.castSucc
cast : ∀ (i : Fin n) (hi : P i.castSucc), P (Fin.last n) ∨ ∃ (i : Fin n), P i.castSucc
⊢ P (Fin.last n) ∨ ∃ (i : Fin n), P i.castSucc

Tactic:
cases i using lastCases with
    | last => exact .inl hi
    | cast _ => exact .inr ⟨_, hi⟩

Premises used: cast, Fin.last
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
P : Fin (n + 1) → Prop
h : P (last n)
⊢ ∃ (i : Fin (n + 1)), P i

Tactic:
⟨_, ‹_›⟩

Premises used: Exists.intro
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
P : Fin (n + 1) → Prop
h : P (last n)
⊢ ∃ (i : Fin (n + 1)), P i

Tactic:
exact ⟨_, ‹_›⟩
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
P : Fin (n + 1) → Prop
i : Fin n
hi : P i.castSucc
⊢ ∃ (i : Fin (n + 1)), P i

Tactic:
⟨_, ‹_›⟩

Premises used: Exists.intro
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
P : Fin (n + 1) → Prop
i : Fin n
hi : P i.castSucc
⊢ ∃ (i : Fin (n + 1)), P i

Tactic:
exact ⟨_, ‹_›⟩
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
⊢ (∀ (i : Fin (n + 1)), P i) ↔ P p ∧ ∀ (i : Fin n), P (p.succAbove i)

Tactic:
⟨fun h ↦ ⟨h _, fun _ ↦ h _⟩, fun h ↦ succAboveCases p h.1 h.2⟩

Premises used: Fin.succAbove, Fin.succAboveCases, And.intro, Iff.intro
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
P : Fin (n + 1) → Prop
p i : Fin (n + 1)
hi : P i
x : ∀ (hi : P p), P p ∨ ∃ (i : Fin n), P (p.succAbove i)
p₁ : ∀ (j : Fin n) (hi : P (p.succAbove j)), P p ∨ ∃ (i : Fin n), P (p.succAbove i)
⊢ P p ∨ ∃ (i : Fin n), P (p.succAbove i)

Tactic:
induction i using p.succAboveCases
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
hi : P p
⊢ P p ∨ ∃ (i : Fin n), P (p.succAbove i)

Tactic:
.inl hi

Premises used: Or.inl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
hi : P p
⊢ P p ∨ ∃ (i : Fin n), P (p.succAbove i)

Tactic:
exact .inl hi
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
j : Fin n
hi : P (p.succAbove j)
⊢ P p ∨ ∃ (i : Fin n), P (p.succAbove i)

Tactic:
.inr ⟨_, hi⟩

Premises used: Exists.intro, Or.inr
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
j : Fin n
hi : P (p.succAbove j)
⊢ P p ∨ ∃ (i : Fin n), P (p.succAbove i)

Tactic:
exact .inr ⟨_, hi⟩
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
h : P p
⊢ ∃ (i : Fin (n + 1)), P i

Tactic:
⟨_, ‹_›⟩

Premises used: Exists.intro
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
h : P p
⊢ ∃ (i : Fin (n + 1)), P i

Tactic:
exact ⟨_, ‹_›⟩
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
i : Fin n
hi : P (p.succAbove i)
⊢ ∃ (i : Fin (n + 1)), P i

Tactic:
⟨_, ‹_›⟩

Premises used: Exists.intro
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
i : Fin n
hi : P (p.succAbove i)
⊢ ∃ (i : Fin (n + 1)), P i

Tactic:
exact ⟨_, ‹_›⟩
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p i : Fin (n + 1)
⊢ i = p ∨ ∃ (j : Fin n), i = p.succAbove j

Tactic:
succAboveCases p (.inl rfl) (fun j => .inr ⟨j, rfl⟩) i

Premises used: Fin.succAboveCases
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
⊢ i.insertNth (α := α) x p i = x

Tactic:
simp [insertNth, succAboveCases]

Premises used: Fin.insertNth
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
simp :
  (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
⊢ i.insertNth (α := α) x p (i.succAbove j) = p j

Tactic:
simp only [insertNth, succAboveCases, dif_neg (succAbove_ne _ _), succAbove_lt_iff_castSucc_lt]

Premises used: Fin.succAbove_ne, Fin.insertNth, dif_neg, Fin.succAbove_lt_iff_castSucc_lt
-- Module: Mathlib.Data.Fin.Tuple.Basic
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
neg :
  ∀ (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
⊢ (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

Tactic:
split_ifs with hlt
-- Module: Mathlib.Data.Fin.Tuple.Basic
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
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
⊢ Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove ((i.succAbove j).castPred ⋯) = x) ↦ α x)
      (p ((i.succAbove j).castPred ⋯)) ⋯ =
    p j

Tactic:
generalize_proofs H₁ H₂
-- Module: Mathlib.Data.Fin.Tuple.Basic
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
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
⊢ 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₂
-- Module: Mathlib.Data.Fin.Tuple.Basic
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
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
⊢ ∀ (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 hk : castPred ((succAbove i) j) H₁ = k

Premises used: Fin.succAbove, Fin.castPred
-- Module: Mathlib.Data.Fin.Tuple.Basic
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
⊢ j = k

Tactic:
rw [castPred_succAbove _ _ hlt] at hk

Premises used: Iff.mpr, Fin.castPred_succAbove, Fin.succAbove_lt_iff_castSucc_lt, Fin.ne_last_of_lt
-- Module: Mathlib.Data.Fin.Tuple.Basic
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
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
⊢ ∀ (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:
cases hk
-- Module: Mathlib.Data.Fin.Tuple.Basic
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 j = i.succAbove j
⊢ Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove j = x) ↦ α x) (p j) H₂ = p j

Tactic:
rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
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
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
⊢ @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

Tactic:
generalize_proofs H₀ H₁ H₂
-- Module: Mathlib.Data.Fin.Tuple.Basic
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
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
⊢ 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₂
-- Module: Mathlib.Data.Fin.Tuple.Basic
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
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
⊢ ∀ (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 hk : pred (succAbove i j) H₁ = k

Premises used: Fin.succAbove, Fin.pred
-- Module: Mathlib.Data.Fin.Tuple.Basic
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
⊢ j = k

Tactic:
rw [pred_succAbove _ _ (Fin.not_lt.1 hlt)] at hk

Premises used: Iff.mpr, Fin.ne_zero_of_lt, Fin.lt_succAbove_iff_le_castSucc, Iff.mp, Fin.not_lt, Fin.pred_succAbove
-- Module: Mathlib.Data.Fin.Tuple.Basic
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
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
⊢ ∀ (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:
cases hk
-- Module: Mathlib.Data.Fin.Tuple.Basic
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 j = i.succAbove j
⊢ Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove j = x) ↦ α x) (p j) H₂ = p j

Tactic:
rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
⊢ @succAboveCases = @insertNth

Tactic:
rfl

Premises used: Fin.insertNth, rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
f : (i : Fin (n + 1)) → α i
i : Fin n
⊢ p.removeNth (α := α) f i = f (p.succAbove i)

Tactic:
rfl

Premises used: Fin.removeNth, rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Type u_3
n : ℕ
i : Fin (n + 1)
a : α
⊢ Eq.{u_3 + 1} (α := (i : Fin n) → α)
    (i.removeNth (α := fun (x : Fin (n + 1)) ↦ α) fun (x : Fin (n + 1)) ↦ a : (i : Fin n) → α) fun (x : Fin n) ↦ a

Tactic:
rfl

Premises used: Fin.removeNth, rfl
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
a : α p
f : (i : Fin n) → α (p.succAbove i)
h : ∀ (x : Fin n), p.removeNth (α := α) (p.insertNth (α := α) a f) x = f x
⊢ p.removeNth (α := α) (p.insertNth (α := α) a f) = f

Tactic:
ext
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
a : α p
f : (i : Fin n) → α (p.succAbove i)
x : Fin n
h : p.insertNth (α := α) a f (p.succAbove x) = f x
⊢ p.removeNth (α := α) (p.insertNth (α := α) a f) x = f x

Tactic:
unfold removeNth

Premises used: Fin.removeNth
-- Module: Mathlib.Data.Fin.Tuple.Basic
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.insertNth (α := α) a f (p.succAbove x) = f x

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
f : (i : Fin (n + 1)) → α i
h : ∀ (x : Fin n), removeNth (α := α) 0 f x = tail (α := α) f x
⊢ removeNth (α := α) 0 f = tail (α := α) f

Tactic:
ext
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
f : (i : Fin (n + 1)) → α i
x : Fin n
⊢ removeNth (α := α) 0 f x = tail (α := α) f x

Tactic:
simp [tail, removeNth]

Premises used: Fin.removeNth, Fin.tail
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_3
f : Fin (n + 1) → α
h : ∀ (x : Fin n), (last n).removeNth (α := fun (i : Fin (n + 1)) ↦ α) f x = init (α := fun (i : Fin (n + 1)) ↦ α) f x
⊢ (last n).removeNth (α := fun (i : Fin (n + 1)) ↦ α) f = init (α := fun (i : Fin (n + 1)) ↦ α) f

Tactic:
ext
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Type u_3
f : Fin (n + 1) → α
x : Fin n
⊢ (last n).removeNth (α := fun (i : Fin (n + 1)) ↦ α) f x = init (α := fun (i : Fin (n + 1)) ↦ α) f x

Tactic:
simp [init, removeNth]

Premises used: Fin.removeNth, Fin.init
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
β : Sort u_2
i : Fin (n + 1)
x : β
p : Fin n → β
⊢ i.insertNth (α := fun (a : Fin (n + 1)) ↦ β) x p ∘ i.succAbove = p

Tactic:
funext (insertNth_apply_succAbove i _ _)

Premises used: Fin.insertNth_apply_succAbove, funext
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
a : α p
f : (i : Fin n) → α (p.succAbove i)
g : (j : Fin (n + 1)) → α j
⊢ p.insertNth (α := α) a f = g ↔ a = g p ∧ f = p.removeNth (α := α) g

Tactic:
simp [funext_iff, forall_iff_succAbove p, removeNth]

Premises used: funext_iff, Fin.removeNth, Fin.forall_iff_succAbove
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
a : α p
f : (i : Fin n) → α (p.succAbove i)
g : (j : Fin (n + 1)) → α j
⊢ g = p.insertNth (α := α) a f ↔ g p = a ∧ p.removeNth (α := α) g = f

Tactic:
simpa [eq_comm] using insertNth_eq_iff

Premises used: eq_comm, Fin.insertNth_eq_iff
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
xₚ yₚ : α p
x y : (j : Fin n) → α (p.succAbove j)
h : p.insertNth (α := α) xₚ x = p.insertNth (α := α) yₚ y
⊢ xₚ = yₚ

Tactic:
simpa using congr_fun h p

Premises used: congr_fun
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
xₚ yₚ : α p
x y : (j : Fin n) → α (p.succAbove j)
h : p.insertNth (α := α) xₚ x = p.insertNth (α := α) yₚ y
i : Fin n
⊢ x i = y i

Tactic:
simpa using congr_fun h (succAbove p i)

Premises used: Fin.succAbove, congr_fun
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
x y : (i : Fin n) → α (p.succAbove i)
xₚ yₚ : α p
⊢ p.insertNth (α := α) xₚ x = p.insertNth (α := α) yₚ y ↔ xₚ = yₚ ∧ x = y

Tactic:
insertNth_injective2.eq_iff

Premises used: Fin.insertNth_injective2, Function.Injective2.eq_iff
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
x : (i : Fin n) → α (p.succAbove i)
⊢ Injective (β := (j : Fin (n + 1)) → α j) fun (x_1 : α p) ↦ p.insertNth (α := α) x_1 x

Tactic:
insertNth_injective2.left _

Premises used: Fin.insertNth_injective2, Function.Injective2.left
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
x : α p
⊢ Injective (p.insertNth (α := α) x)

Tactic:
insertNth_injective2.right _

Premises used: Fin.insertNth_injective2, Function.Injective2.right
-- Module: Mathlib.Data.Fin.Tuple.Basic
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)
rw₃ rw₄ :
  Eq.{u_1} (α := α j)
    (Eq.rec (motive := fun (x : Fin (n + 1)) (h : i.succAbove (j.castPred ⋯) = x) ↦ α x) (p (j.castPred ⋯)) ⋯ : α 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 ⋯)) ⋯

Tactic:
rw [insertNth, succAboveCases, dif_neg (Fin.ne_of_lt h), dif_pos h]

Premises used: Fin.ne_of_lt, Fin.insertNth, dif_pos, dif_neg