-- Mathlib/Data/Fin/Tuple/Take.lean
theorem take_succ_eq_snoc (m : ℕ) (h : m < n) (v : (i : Fin n) → α i) :
    take m.succ h v = snoc (take m h.le v) (v ⟨m, h⟩)

Proof state:
case h
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m < n
v : (i : Fin n) → α i
i : Fin m.succ
⊢ take m.succ h v i = snoc (take m ⋯ v) (v ⟨m, h⟩) i

Tactic:
induction m with
| zero =>
  have h' : i = 0 := by ext; simp
  subst h'
  simp [take, snoc, castLE]
| succ m _ =>
  induction i using reverseInduction with
  | last => simp [take, snoc, castLT]; congr
  | cast i _ => simp [snoc_cast_add]

Result:
no goals

Proof state:
case h.zero
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
h : 0 < n
i : Fin (Nat.succ 0)
h' : i = 0
⊢ take (Nat.succ 0) h v i = snoc (take 0 ⋯ v) (v ⟨0, h⟩) i

Tactic:
subst h'

Result:
case h.zero
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
h : 0 < n
⊢ take (Nat.succ 0) h v 0 = snoc (take 0 ⋯ v) (v ⟨0, h⟩) 0

Proof state:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m < n
v : (i : Fin n) → α i
⊢ take m.succ h v = snoc (take m ⋯ v) (v ⟨m, h⟩)

Tactic:
ext i

Result:
case h
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m < n
v : (i : Fin n) → α i
i : Fin m.succ
⊢ take m.succ h v i = snoc (take m ⋯ v) (v ⟨m, h⟩) i

Proof state:
case h.succ.cast
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
m : ℕ
a✝¹ : ∀ (h : m < n) (i : Fin m.succ), take m.succ h v i = snoc (take m ⋯ v) (v ⟨m, h⟩) i
h : m + 1 < n
i : Fin (m + 1)
a✝ : take (m + 1).succ h v i.succ = snoc (take (m + 1) ⋯ v) (v ⟨m + 1, h⟩) i.succ
⊢ take (m + 1).succ h v i.castSucc = snoc (take (m + 1) ⋯ v) (v ⟨m + 1, h⟩) i.castSucc

Tactic:
simp [snoc_cast_add]

Result:
no goals

Proof state:
case h.succ.last
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
m : ℕ
a✝ : ∀ (h : m < n) (i : Fin m.succ), take m.succ h v i = snoc (take m ⋯ v) (v ⟨m, h⟩) i
h : m + 1 < n
⊢ take (m + 1).succ h v (last (m + 1)) = snoc (take (m + 1) ⋯ v) (v ⟨m + 1, h⟩) (last (m + 1))

Tactic:
simp [take, snoc, castLT]

Result:
case h.succ.last
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
m : ℕ
a✝ : ∀ (h : m < n) (i : Fin m.succ), take m.succ h v i = snoc (take m ⋯ v) (v ⟨m, h⟩) i
h : m + 1 < n
⊢ v (castLE h (last (m + 1))) = v ⟨m + 1, h⟩

Proof state:
case h
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
h : 0 < n
i : Fin (Nat.succ 0)
⊢ ↑i = ↑0

Tactic:
simp

Result:
no goals

Proof state:
case h.zero
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
h : 0 < n
⊢ take (Nat.succ 0) h v 0 = snoc (take 0 ⋯ v) (v ⟨0, h⟩) 0

Tactic:
simp [take, snoc, castLE]

Result:
no goals

Proof state:
case h.zero
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
h : 0 < n
i : Fin (Nat.succ 0)
⊢ take (Nat.succ 0) h v i = snoc (take 0 ⋯ v) (v ⟨0, h⟩) i

Tactic:
have h' : i = 0 := by ext; simp

Result:
case h.zero
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
h : 0 < n
i : Fin (Nat.succ 0)
h' : i = 0
⊢ take (Nat.succ 0) h v i = snoc (take 0 ⋯ v) (v ⟨0, h⟩) i

Proof state:
case h.succ.last
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
m : ℕ
a✝ : ∀ (h : m < n) (i : Fin m.succ), take m.succ h v i = snoc (take m ⋯ v) (v ⟨m, h⟩) i
h : m + 1 < n
⊢ v (castLE h (last (m + 1))) = v ⟨m + 1, h⟩

Tactic:
congr

Result:
no goals

Proof state:
case h.succ
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
m : ℕ
a✝ : ∀ (h : m < n) (i : Fin m.succ), take m.succ h v i = snoc (take m ⋯ v) (v ⟨m, h⟩) i
h : m + 1 < n
i : Fin (m + 1).succ
⊢ take (m + 1).succ h v i = snoc (take (m + 1) ⋯ v) (v ⟨m + 1, h⟩) i

Tactic:
induction i using reverseInduction with
| last => simp [take, snoc, castLT]; congr
| cast i _ => simp [snoc_cast_add]

Result:
no goals

Proof state:
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
h : 0 < n
i : Fin (Nat.succ 0)
⊢ i = 0

Tactic:
ext

Result:
case h
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
h : 0 < n
i : Fin (Nat.succ 0)
⊢ ↑i = ↑0