-- Mathlib/Data/Fin/Tuple/Take.lean
theorem take_addCases_right {n' : ℕ} {motive : Fin (n + n') → Sort*} (m : ℕ) (h : m ≤ n')
    (u : (i : Fin n) → motive (castAdd n' i)) (v : (i : Fin n') → motive (natAdd n i)) :
      take (n + m) (Nat.add_le_add_left h n) (addCases u v) = addCases u (take m h v)

Proof state:
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
⊢ (take (n + m) ⋯ fun i => addCases u v i) = fun i => addCases u (take m h v) i

Tactic:
ext i

Result:
case h
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin (n + m)
⊢ take (n + m) ⋯ (fun i => addCases u v i) i = addCases u (take m h v) i

Proof state:
case h
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin (n + m)
⊢ take (n + m) ⋯ (fun i => addCases u v i) i = addCases u (take m h v) i

Tactic:
simp only [take, addCases, coe_castLE]

Result:
case h
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin (n + m)
⊢ (if h_1 : ↑i < n then u ((castLE ⋯ i).castLT ⋯) else ⋯ ▸ v (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯)) =
    if h : ↑i < n then u (i.castLT ⋯) else ⋯ ▸ v (castLE h (subNat n (Fin.cast ⋯ i) ⋯))

Proof state:
case pos
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin (n + m)
h' : ↑i < n
⊢ u ((castLE ⋯ i).castLT ⋯) = u (i.castLT ⋯)

Tactic:
congr

Result:
no goals

Proof state:
case h
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin (n + m)
⊢ (if h_1 : ↑i < n then u ((castLE ⋯ i).castLT ⋯) else ⋯ ▸ v (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯)) =
    if h : ↑i < n then u (i.castLT ⋯) else ⋯ ▸ v (castLE h (subNat n (Fin.cast ⋯ i) ⋯))

Tactic:
by_cases h' : i < n

Result:
case pos
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin (n + m)
h' : ↑i < n
⊢ (if h_1 : ↑i < n then u ((castLE ⋯ i).castLT ⋯) else ⋯ ▸ v (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯)) =
    if h : ↑i < n then u (i.castLT ⋯) else ⋯ ▸ v (castLE h (subNat n (Fin.cast ⋯ i) ⋯))

case neg
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin (n + m)
h' : ¬↑i < n
⊢ (if h_1 : ↑i < n then u ((castLE ⋯ i).castLT ⋯) else ⋯ ▸ v (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯)) =
    if h : ↑i < n then u (i.castLT ⋯) else ⋯ ▸ v (castLE h (subNat n (Fin.cast ⋯ i) ⋯))

Proof state:
case neg
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin (n + m)
h' : ¬↑i < n
⊢ (if h_1 : ↑i < n then u ((castLE ⋯ i).castLT ⋯) else ⋯ ▸ v (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯)) =
    if h : ↑i < n then u (i.castLT ⋯) else ⋯ ▸ v (castLE h (subNat n (Fin.cast ⋯ i) ⋯))

Tactic:
simp only [h', ↓reduceDIte, subNat, castLE, Fin.cast, eqRec_eq_cast]

Result:
no goals

Proof state:
case pos
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin (n + m)
h' : ↑i < n
⊢ (if h_1 : ↑i < n then u ((castLE ⋯ i).castLT ⋯) else ⋯ ▸ v (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯)) =
    if h : ↑i < n then u (i.castLT ⋯) else ⋯ ▸ v (castLE h (subNat n (Fin.cast ⋯ i) ⋯))

Tactic:
simp only [h', ↓reduceDIte]

Result:
case pos
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin (n + m)
h' : ↑i < n
⊢ u ((castLE ⋯ i).castLT ⋯) = u (i.castLT ⋯)