Theorem: Fin.cons.map_sub (ForML/ContinuousMultilinearMap.lean)

State before:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : ℕ
E : Fin n → Type u_2
inst✝⁶ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝⁵ : (i : Fin n) → NormedSpace 𝕜 (E i)
E₁ : Fin n → Type u_3
inst✝⁴ : (i : Fin n) → NormedAddCommGroup (E₁ i)
inst✝³ : (i : Fin n) → NormedSpace 𝕜 (E₁ i)
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
α : Fin (Nat.succ n) → Type u_5
inst✝ : (i : Fin (Nat.succ n)) → AddGroup (α i)
a c : α 0
b d : (i : Fin n) → α (succ i)
⊢ cons a b - cons c d = cons (a - c) (b - d)
Tactic:
ext i
State after:
case h
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : ℕ
E : Fin n → Type u_2
inst✝⁶ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝⁵ : (i : Fin n) → NormedSpace 𝕜 (E i)
E₁ : Fin n → Type u_3
inst✝⁴ : (i : Fin n) → NormedAddCommGroup (E₁ i)
inst✝³ : (i : Fin n) → NormedSpace 𝕜 (E₁ i)
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
α : Fin (Nat.succ n) → Type u_5
inst✝ : (i : Fin (Nat.succ n)) → AddGroup (α i)
a c : α 0
b d : (i : Fin n) → α (succ i)
i : Fin (n + 1)
⊢ (cons a b - cons c d) i = cons (a - c) (b - d) i

State before:
case h
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : ℕ
E : Fin n → Type u_2
inst✝⁶ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝⁵ : (i : Fin n) → NormedSpace 𝕜 (E i)
E₁ : Fin n → Type u_3
inst✝⁴ : (i : Fin n) → NormedAddCommGroup (E₁ i)
inst✝³ : (i : Fin n) → NormedSpace 𝕜 (E₁ i)
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
α : Fin (Nat.succ n) → Type u_5
inst✝ : (i : Fin (Nat.succ n)) → AddGroup (α i)
a c : α 0
b d : (i : Fin n) → α (succ i)
i : Fin (n + 1)
⊢ (cons a b - cons c d) i = cons (a - c) (b - d) i
Tactic:
cases i using Fin.cases <;> simp
State after:
no goals