awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (hypothesis)
Goal:
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt : i + 1 < n + 1 + m
h : i + 1 < n + 1
⊢ Eq.{u_2} (α := α) (cases (motive := fun (x : Fin (n + 1)) ↦ α) a as (⟨i + 1, ⋯⟩ : Fin (n + 1)) : α)
    (cases (motive := fun (x : Fin (n + m + 1)) ↦ α) a (addCases (motive := fun (x : Fin (n + m)) ↦ α) as bs)
        (Fin.cast ⋯ (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) :
      α)
have this : i < n
Tactic: have : i < n := Nat.lt_of_succ_lt_succ h
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (hypothesis)
Goal:
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt : i + 1 < n + 1 + m
h : ¬i + 1 < n + 1
⊢ Eq.{u_2} (α := α)
    (@Eq.rec _ (natAdd (n + 1) (subNat (n + 1) (Fin.cast ⋯ (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) ⋯))
        (fun (x : Fin (n + 1 + m))
            (h : natAdd (n + 1) (subNat (n + 1) (Fin.cast ⋯ (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) ⋯) = x) ↦
          α)
        (bs (subNat (n + 1) (Fin.cast ⋯ (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) ⋯)) _ ⋯ :
      α)
    (cases (motive := fun (x : Fin (n + m + 1)) ↦ α) a (addCases (motive := fun (x : Fin (n + m)) ↦ α) as bs)
        (Fin.cast ⋯ (⟨i + 1, isLt⟩ : Fin (n + 1 + m))) :
      α)
have this : ¬i < n
Tactic: have : ¬i < n := Nat.not_le_of_gt <| Nat.le_of_lt_succ <| Nat.gt_of_not_le h
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
⊢ append as (snoc (α := fun (a : Fin (m + 1)) ↦ α) bs b) = snoc (α := fun (i : Fin (n.add m + 1)) ↦ α) (append as bs) b
have h : ∀ (i : Fin (n + (m + 1))),
  append as (snoc (α := fun (a : Fin (m + 1)) ↦ α) bs b) i =
    snoc (α := fun (i : Fin (n.add m + 1)) ↦ α) (append as bs) b i
Tactic: funext i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : Fin (n + (m + 1))
⊢ append as (snoc (α := fun (a : Fin (m + 1)) ↦ α) bs b) i =
    snoc (α := fun (i : Fin (n.add m + 1)) ↦ α) (append as bs) b i
have h : ∀ (i : ℕ) (isLt : i < n + (m + 1)),
  append as (snoc (α := fun (a : Fin (m + 1)) ↦ α) bs b) (⟨i, isLt⟩ : Fin (n + (m + 1))) =
    snoc (α := fun (i : Fin (n.add m + 1)) ↦ α) (append as bs) b (⟨i, isLt⟩ : Fin (n + (m + 1)))
Tactic: rcases i with ⟨i, isLt⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
⊢ append as (snoc (α := fun (a : Fin (m + 1)) ↦ α) bs b) (⟨i, isLt⟩ : Fin (n + (m + 1))) =
    snoc (α := fun (i : Fin (n.add m + 1)) ↦ α) (append as bs) b (⟨i, isLt⟩ : Fin (n + (m + 1)))
have h : Eq.{u_2} (α := α) (if h : i < n then as ⟨i, sorry⟩ else if h_1 : i - n < m then bs ⟨i - n, sorry⟩ else b)
  (if h : i < n + m then if h_1 : i < n then as ⟨i, sorry⟩ else bs ⟨i - n, sorry⟩ else b)
Tactic: simp only [append, addCases, castLT, cast_mk, subNat_mk, natAdd_mk, cast, snoc.eq_1,
    eq_rec_constant, Nat.add_eq]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
⊢ Eq.{u_2} (α := α) (if h : i < n then as ⟨i, ⋯⟩ else if h_1 : i - n < m then bs ⟨i - n, ⋯⟩ else b)
    (if h : i < n + m then if h_1 : i < n then as ⟨i, ⋯⟩ else bs ⟨i - n, ⋯⟩ else b)
have pos : ∀ (lt_n : i < n) (lt_add : i < n + m), as (⟨i, sorry⟩ : Fin n) = as ⟨i, sorry⟩
Tactic: split_ifs with lt_n lt_add sub_lt nlt_add lt_add
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
pos : ∀ (lt_n : i < n) (lt_add : i < n + m), as (⟨i, ⋯⟩ : Fin n) = as ⟨i, ⋯⟩
⊢ Eq.{u_2} (α := α) (if h : i < n then as ⟨i, ⋯⟩ else if h_1 : i - n < m then bs ⟨i - n, ⋯⟩ else b)
    (if h : i < n + m then if h_1 : i < n then as ⟨i, ⋯⟩ else bs ⟨i - n, ⋯⟩ else b)
have neg : ∀ (lt_n : i < n) (lt_add : ¬i < n + m), as (⟨i, sorry⟩ : Fin n) = b
Tactic: split_ifs with lt_n lt_add sub_lt nlt_add lt_add
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
pos : ∀ (lt_n : i < n) (lt_add : i < n + m), as (⟨i, ⋯⟩ : Fin n) = as ⟨i, ⋯⟩
neg : ∀ (lt_n : i < n) (lt_add : ¬i < n + m), as (⟨i, ⋯⟩ : Fin n) = b
⊢ Eq.{u_2} (α := α) (if h : i < n then as ⟨i, ⋯⟩ else if h_1 : i - n < m then bs ⟨i - n, ⋯⟩ else b)
    (if h : i < n + m then if h_1 : i < n then as ⟨i, ⋯⟩ else bs ⟨i - n, ⋯⟩ else b)
have pos₁ : ∀ (lt_n : ¬i < n) (sub_lt : i - n < m) (nlt_add : i < n + m), bs (⟨i - n, sorry⟩ : Fin m) = bs ⟨i - n, sorry⟩
Tactic: split_ifs with lt_n lt_add sub_lt nlt_add lt_add
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
pos : ∀ (lt_n : i < n) (lt_add : i < n + m), as (⟨i, ⋯⟩ : Fin n) = as ⟨i, ⋯⟩
neg : ∀ (lt_n : i < n) (lt_add : ¬i < n + m), as (⟨i, ⋯⟩ : Fin n) = b
pos₁ : ∀ (lt_n : ¬i < n) (sub_lt : i - n < m) (nlt_add : i < n + m), bs (⟨i - n, ⋯⟩ : Fin m) = bs ⟨i - n, ⋯⟩
⊢ Eq.{u_2} (α := α) (if h : i < n then as ⟨i, ⋯⟩ else if h_1 : i - n < m then bs ⟨i - n, ⋯⟩ else b)
    (if h : i < n + m then if h_1 : i < n then as ⟨i, ⋯⟩ else bs ⟨i - n, ⋯⟩ else b)
have neg₁ : ∀ (lt_n : ¬i < n) (sub_lt : i - n < m) (nlt_add : ¬i < n + m), bs (⟨i - n, sorry⟩ : Fin m) = b
Tactic: split_ifs with lt_n lt_add sub_lt nlt_add lt_add
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
pos : ∀ (lt_n : i < n) (lt_add : i < n + m), as (⟨i, ⋯⟩ : Fin n) = as ⟨i, ⋯⟩
neg : ∀ (lt_n : i < n) (lt_add : ¬i < n + m), as (⟨i, ⋯⟩ : Fin n) = b
pos₁ : ∀ (lt_n : ¬i < n) (sub_lt : i - n < m) (nlt_add : i < n + m), bs (⟨i - n, ⋯⟩ : Fin m) = bs ⟨i - n, ⋯⟩
neg₁ : ∀ (lt_n : ¬i < n) (sub_lt : i - n < m) (nlt_add : ¬i < n + m), bs (⟨i - n, ⋯⟩ : Fin m) = b
⊢ Eq.{u_2} (α := α) (if h : i < n then as ⟨i, ⋯⟩ else if h_1 : i - n < m then bs ⟨i - n, ⋯⟩ else b)
    (if h : i < n + m then if h_1 : i < n then as ⟨i, ⋯⟩ else bs ⟨i - n, ⋯⟩ else b)
have pos₂ : ∀ (lt_n : ¬i < n) (sub_lt : ¬i - n < m) (lt_add : i < n + m), b = bs ⟨i - n, sorry⟩
Tactic: split_ifs with lt_n lt_add sub_lt nlt_add lt_add
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
pos : ∀ (lt_n : i < n) (lt_add : i < n + m), as (⟨i, ⋯⟩ : Fin n) = as ⟨i, ⋯⟩
neg : ∀ (lt_n : i < n) (lt_add : ¬i < n + m), as (⟨i, ⋯⟩ : Fin n) = b
pos₁ : ∀ (lt_n : ¬i < n) (sub_lt : i - n < m) (nlt_add : i < n + m), bs (⟨i - n, ⋯⟩ : Fin m) = bs ⟨i - n, ⋯⟩
neg₁ : ∀ (lt_n : ¬i < n) (sub_lt : i - n < m) (nlt_add : ¬i < n + m), bs (⟨i - n, ⋯⟩ : Fin m) = b
pos₂ : ∀ (lt_n : ¬i < n) (sub_lt : ¬i - n < m) (lt_add : i < n + m), b = bs ⟨i - n, ⋯⟩
⊢ Eq.{u_2} (α := α) (if h : i < n then as ⟨i, ⋯⟩ else if h_1 : i - n < m then bs ⟨i - n, ⋯⟩ else b)
    (if h : i < n + m then if h_1 : i < n then as ⟨i, ⋯⟩ else bs ⟨i - n, ⋯⟩ else b)
have neg₂ : ∀ (lt_n : ¬i < n) (sub_lt : ¬i - n < m) (lt_add : ¬i < n + m), b = b
Tactic: split_ifs with lt_n lt_add sub_lt nlt_add lt_add
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (hypothesis)
Goal:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : i < n
lt_add : ¬i < n + m
⊢ as (⟨i, ⋯⟩ : Fin n) = b
have this : i < n + m
Tactic: have := Nat.lt_add_right m lt_n
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : i - n < m
nlt_add : ¬i < n + m
⊢ bs (⟨i - n, ⋯⟩ : Fin m) = b
have neg : ∀ (isLt : n + m < n + (m + 1)) (lt_n : ¬n + m < n) (sub_lt : n + m - n < m) (nlt_add : ¬n + m < n + m),
  bs (⟨n + m - n, sorry⟩ : Fin m) = b
Tactic: obtain rfl := Nat.eq_of_le_of_lt_succ (Nat.not_lt.mp nlt_add) isLt
Cleared hypotheses: i, isLt, lt_n, sub_lt, nlt_add
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (hypothesis)
Goal:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : ¬i - n < m
lt_add : i < n + m
⊢ b = bs ⟨i - n, ⋯⟩
have this : i - n < m
Tactic: have := Nat.sub_lt_left_of_lt_add (Nat.not_lt.mp lt_n) lt_add
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n.succ → α
⊢ g ∘ init (α := fun (i : Fin (n + 1)) ↦ α) q = init (α := fun (a : Fin (n + 1)) ↦ β) (g ∘ q)
have h : ∀ (j : Fin n), (g ∘ init (α := fun (i : Fin (n + 1)) ↦ α) q) j = init (α := fun (a : Fin (n + 1)) ↦ β) (g ∘ q) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Fin (n + 1) → Sort u_1
x_1 : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
z : α (last n)
motive : ((i : Fin n.succ) → α i) → Sort u_2
snoc : (xs : (i : Fin n) → α i.castSucc) → (x : α (last n)) → motive (Fin.snoc (α := α) xs x)
x : (i : Fin n.succ) → α i
⊢ motive (Fin.snoc (α := α) (init (α := α) x) (x (last n))) = motive x
have rw : motive x = motive x
Tactic: rw [Fin.snoc_init_self]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
motive : ((i : Fin (n + 1)) → α i) → Sort u_2
snoc : (x : (i : Fin n) → α i.castSucc) → (x₀ : α (last n)) → motive (Fin.snoc (α := α) x x₀)
x : (i : Fin n) → init (α := fun (i : Fin (n + 1)) ↦ Sort u_1) α i
x₀ : α (last n)
⊢ snocCases (α := α) (motive := fun (x : (i : Fin (n + 1)) → α i) ↦ motive x) snoc (Fin.snoc (α := α) x x₀) = snoc x x₀
have rw : cast sorry (snoc (init (α := α) (Fin.snoc (α := α) x x₀)) (Fin.snoc (α := α) x x₀ (last n))) = snoc x x₀
Tactic: rw [snocCases, cast_eq_iff_heq, Fin.init_snoc, Fin.snoc_last]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
motive : ((i : Fin (n + 1)) → α i) → Sort u_2
snoc : (x : (i : Fin n) → α i.castSucc) → (x₀ : α (last n)) → motive (Fin.snoc (α := α) x x₀)
x : (i : Fin n) → init (α := fun (i : Fin (n + 1)) ↦ Sort u_1) α i
x₀ : α (last n)
rw : cast ⋯ (snoc (init (α := α) (Fin.snoc (α := α) x x₀)) (Fin.snoc (α := α) x x₀ (last n))) = snoc x x₀
⊢ snocCases (α := α) (motive := fun (x : (i : Fin (n + 1)) → α i) ↦ motive x) snoc (Fin.snoc (α := α) x x₀) = snoc x x₀
have rw₁ : HEq (α := motive (Fin.snoc (α := α) (init (α := α) (Fin.snoc (α := α) x x₀)) (Fin.snoc (α := α) x x₀ (last n))))
  (snoc (init (α := α) (Fin.snoc (α := α) x x₀)) (Fin.snoc (α := α) x x₀ (last n))) (snoc x x₀)
Tactic: rw [snocCases, cast_eq_iff_heq, Fin.init_snoc, Fin.snoc_last]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
motive : ((i : Fin (n + 1)) → α i) → Sort u_2
snoc : (x : (i : Fin n) → α i.castSucc) → (x₀ : α (last n)) → motive (Fin.snoc (α := α) x x₀)
x : (i : Fin n) → init (α := fun (i : Fin (n + 1)) ↦ Sort u_1) α i
x₀ : α (last n)
rw : cast ⋯ (snoc (init (α := α) (Fin.snoc (α := α) x x₀)) (Fin.snoc (α := α) x x₀ (last n))) = snoc x x₀
rw₁ :
  HEq (α := motive (Fin.snoc (α := α) (init (α := α) (Fin.snoc (α := α) x x₀)) (Fin.snoc (α := α) x x₀ (last n))))
    (snoc (init (α := α) (Fin.snoc (α := α) x x₀)) (Fin.snoc (α := α) x x₀ (last n))) (snoc x x₀)
⊢ snocCases (α := α) (motive := fun (x : (i : Fin (n + 1)) → α i) ↦ motive x) snoc (Fin.snoc (α := α) x x₀) = snoc x x₀
have rw₂ : HEq (α := motive (Fin.snoc (α := α) x (Fin.snoc (α := α) x x₀ (last n)))) (snoc x (Fin.snoc (α := α) x x₀ (last n)))
  (snoc x x₀)
Tactic: rw [snocCases, cast_eq_iff_heq, Fin.init_snoc, Fin.snoc_last]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_1
motive : ((i : Fin (n + 1)) → α i) → Sort u_2
snoc : (x : (i : Fin n) → α i.castSucc) → (x₀ : α (last n)) → motive (Fin.snoc (α := α) x x₀)
x : (i : Fin n) → init (α := fun (i : Fin (n + 1)) ↦ Sort u_1) α i
x₀ : α (last n)
rw : cast ⋯ (snoc (init (α := α) (Fin.snoc (α := α) x x₀)) (Fin.snoc (α := α) x x₀ (last n))) = snoc x x₀
rw₁ :
  HEq (α := motive (Fin.snoc (α := α) (init (α := α) (Fin.snoc (α := α) x x₀)) (Fin.snoc (α := α) x x₀ (last n))))
    (snoc (init (α := α) (Fin.snoc (α := α) x x₀)) (Fin.snoc (α := α) x x₀ (last n))) (snoc x x₀)
rw₂ :
  HEq (α := motive (Fin.snoc (α := α) x (Fin.snoc (α := α) x x₀ (last n)))) (snoc x (Fin.snoc (α := α) x x₀ (last n)))
    (snoc x x₀)
⊢ snocCases (α := α) (motive := fun (x : (i : Fin (n + 1)) → α i) ↦ motive x) snoc (Fin.snoc (α := α) x x₀) = snoc x x₀
have rw₃ : snoc x x₀ ≍ snoc x x₀
Tactic: rw [snocCases, cast_eq_iff_heq, Fin.init_snoc, Fin.snoc_last]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (hypothesis)
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
i : Fin n
h :
  Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ i.castSucc : α)
    (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ (last n) : α)
⊢ i.castSucc = last n
have h₁ : x i = x₀
Tactic: simp only [snoc_castSucc, snoc_last] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (hypothesis)
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
i : Fin n
h : x i = x₀
⊢ i.castSucc = last n
have hx₁ : ¬x i ∈ Set.range x
Tactic: rw [← h] at hx₀
Cleared hypotheses: hx₀, h
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
j : Fin (n + 1)
i : Fin n
h :
  Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ i.castSucc : α)
    (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ j : α)
⊢ i.castSucc = j
have cast : ∀ (j : Fin n)
  (h :
    Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ i.castSucc : α)
      (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ j.castSucc : α)),
  i.castSucc = j.castSucc
Tactic: induction j using lastCases with
    | cast j =>
      simpa only [castSucc_inj, ← Injective.eq_iff hx, snoc_castSucc] using h
    | last =>
      simp only [snoc_castSucc, snoc_last] at h
      rw [← h] at hx₀
      apply hx₀.elim (Set.mem_range_self i)
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
j : Fin (n + 1)
i : Fin n
h :
  Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ i.castSucc : α)
    (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ j : α)
cast :
  ∀ (j : Fin n)
    (h :
      Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ i.castSucc : α)
        (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ j.castSucc : α)),
    i.castSucc = j.castSucc
⊢ i.castSucc = j
have cast₁ : ∀
  (h :
    Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ i.castSucc : α)
      (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ (last n) : α)),
  i.castSucc = last n
Tactic: induction j using lastCases with
    | cast j =>
      simpa only [castSucc_inj, ← Injective.eq_iff hx, snoc_castSucc] using h
    | last =>
      simp only [snoc_castSucc, snoc_last] at h
      rw [← h] at hx₀
      apply hx₀.elim (Set.mem_range_self i)
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (hypothesis)
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
j : Fin n
h :
  Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ (last n) : α)
    (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ j.castSucc : α)
⊢ last n = j.castSucc
have h₁ : x₀ = x j
Tactic: simp only [snoc_castSucc, snoc_last] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (hypothesis)
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
j : Fin n
h : x₀ = x j
⊢ last n = j.castSucc
have hx₁ : ¬x j ∈ Set.range x
Tactic: rw [h] at hx₀
Cleared hypotheses: hx₀, h
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
j : Fin (n + 1)
h :
  Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ (last n) : α)
    (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ j : α)
⊢ last n = j
have last : ∀ (j : Fin n)
  (h :
    Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ (last n) : α)
      (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ j.castSucc : α)),
  last n = j.castSucc
Tactic: induction j using lastCases with
    | cast j =>
      simp only [snoc_castSucc, snoc_last] at h
      rw [h] at hx₀
      apply hx₀.elim (Set.mem_range_self j)
    | last => simp
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
j : Fin (n + 1)
h :
  Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ (Fin.last n) : α)
    (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ j : α)
last :
  ∀ (j : Fin n)
    (h :
      Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ (Fin.last n) : α)
        (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ j.castSucc : α)),
    Fin.last n = j.castSucc
⊢ Fin.last n = j
have last₁ : ∀
  (h :
    Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ (Fin.last n) : α)
      (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ (Fin.last n) : α)),
  Fin.last n = Fin.last n
Tactic: induction j using lastCases with
    | cast j =>
      simp only [snoc_castSucc, snoc_last] at h
      rw [h] at hx₀
      apply hx₀.elim (Set.mem_range_self j)
    | last => simp
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
i j : Fin (n + 1)
h :
  Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ i : α)
    (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ j : α)
⊢ i = j
have cast : ∀ (i : Fin n)
  (h :
    Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ i.castSucc : α)
      (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ j : α)),
  i.castSucc = j
Tactic: induction i using lastCases with
  | cast i =>
    induction j using lastCases with
    | cast j =>
      simpa only [castSucc_inj, ← Injective.eq_iff hx, snoc_castSucc] using h
    | last =>
      simp only [snoc_castSucc, snoc_last] at h
      rw [← h] at hx₀
      apply hx₀.elim (Set.mem_range_self i)
  | last =>
    induction j using lastCases with
    | cast j =>
      simp only [snoc_castSucc, snoc_last] at h
      rw [h] at hx₀
      apply hx₀.elim (Set.mem_range_self j)
    | last => simp
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
i j : Fin (n + 1)
h :
  Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ i : α)
    (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ j : α)
cast :
  ∀ (i : Fin n)
    (h :
      Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ i.castSucc : α)
        (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ j : α)),
    i.castSucc = j
⊢ i = j
have last : ∀
  (h :
    Eq.{u_2 + 1} (α := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ (last n) : α)
      (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀ j : α)),
  last n = j
Tactic: induction i using lastCases with
  | cast i =>
    induction j using lastCases with
    | cast j =>
      simpa only [castSucc_inj, ← Injective.eq_iff hx, snoc_castSucc] using h
    | last =>
      simp only [snoc_castSucc, snoc_last] at h
      rw [← h] at hx₀
      apply hx₀.elim (Set.mem_range_self i)
  | last =>
    induction j using lastCases with
    | cast j =>
      simp only [snoc_castSucc, snoc_last] at h
      rw [h] at hx₀
      apply hx₀.elim (Set.mem_range_self j)
    | last => simp
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
⊢ Injective.{1, u_2 + 1} (α := Fin (n + 1)) (β := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀) ↔
    Injective x ∧ ¬x₀ ∈ Set.range x
have refine_1 : ∀ (h : Injective.{1, u_2 + 1} (α := Fin (n + 1)) (β := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀)), Injective x
Tactic: refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ snoc_injective_of_injective h.1 h.2⟩
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
refine_1 :
  ∀ (h : Injective.{1, u_2 + 1} (α := Fin (n + 1)) (β := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀)), Injective x
⊢ Injective.{1, u_2 + 1} (α := Fin (n + 1)) (β := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀) ↔
    Injective x ∧ ¬x₀ ∈ Set.range x
have refine_2 : ∀ (h : Injective.{1, u_2 + 1} (α := Fin (n + 1)) (β := α) (snoc (α := fun (a : Fin n.succ) ↦ α) x x₀)),
  ¬x₀ ∈ Set.range x
Tactic: refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ snoc_injective_of_injective h.1 h.2⟩
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (hypothesis)
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₀
⊢ False
have hi₁ : 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
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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 v
have 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)
Tactic: convert! h (fun i => v (castAdd n i)) (fun j => v (natAdd m j))
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
P : Fin (n + 1) → Prop
i : Fin (n + 1)
hi : P i
⊢ P (last n) ∨ ∃ (i : Fin n), P i.castSucc
have last : ∀ (hi : P (last n)), P (last n) ∨ ∃ (i : Fin n), P i.castSucc
Tactic: cases i using lastCases with
    | last => exact .inl hi
    | cast _ => exact .inr ⟨_, hi⟩
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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
⊢ P (Fin.last n) ∨ ∃ (i : Fin n), P i.castSucc
have cast : ∀ (i : Fin n) (hi : 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⟩
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
P : Fin (n + 1) → Prop
p i : Fin (n + 1)
hi : P i
⊢ P p ∨ ∃ (i : Fin n), P (p.succAbove i)
have x : ∀ (hi : P p), P p ∨ ∃ (i : Fin n), P (p.succAbove i)
Tactic: induction i using p.succAboveCases
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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 p ∨ ∃ (i : Fin n), P (p.succAbove i)
have p₁ : ∀ (j : Fin n) (hi : P (p.succAbove j)), P p ∨ ∃ (i : Fin n), P (p.succAbove i)
Tactic: induction i using p.succAboveCases
Cleared hypotheses: i, hi
-- 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
⊢ i.insertNth (α := α) x p (i.succAbove j) = p j
have simp : (if h : j.castSucc < i then
    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
  else
    @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: simp only [insertNth, succAboveCases, dif_neg (succAbove_ne _ _), succAbove_lt_iff_castSucc_lt]