Theorem: update_nz_succ (Ray/Misc/Multilinear.lean)

State before:
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
⊢ (fun j => Function.update f i x j.succ) = Function.update (fun j => f j.succ) (i.pred i0) x
Tactic:
apply funext
State after:
case h
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
⊢ ∀ (x_1 : Fin n), Function.update f i x x_1.succ = Function.update (fun j => f j.succ) (i.pred i0) x x_1

State before:
case h
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
⊢ ∀ (x_1 : Fin n), Function.update f i x x_1.succ = Function.update (fun j => f j.succ) (i.pred i0) x x_1
Tactic:
intro k
State after:
case h
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
k : Fin n
⊢ Function.update f i x k.succ = Function.update (fun j => f j.succ) (i.pred i0) x k

State before:
case h
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
k : Fin n
⊢ Function.update f i x k.succ = Function.update (fun j => f j.succ) (i.pred i0) x k
Tactic:
by_cases ki : k.succ = i
State after:
case pos
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
k : Fin n
ki : k.succ = i
⊢ Function.update f i x k.succ = Function.update (fun j => f j.succ) (i.pred i0) x k

case neg
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
k : Fin n
ki : ¬k.succ = i
⊢ Function.update f i x k.succ = Function.update (fun j => f j.succ) (i.pred i0) x k

State before:
case pos
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
k : Fin n
ki : k.succ = i
⊢ Function.update f i x k.succ = Function.update (fun j => f j.succ) (i.pred i0) x k
Tactic:
have ki' : k = i.pred i0 := by simp_rw [← ki, Fin.pred_succ]
State after:
case pos
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
k : Fin n
ki : k.succ = i
ki' : k = i.pred i0
⊢ Function.update f i x k.succ = Function.update (fun j => f j.succ) (i.pred i0) x k

State before:
case pos
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
k : Fin n
ki : k.succ = i
ki' : k = i.pred i0
⊢ Function.update f i x k.succ = Function.update (fun j => f j.succ) (i.pred i0) x k
Tactic:
rw [ki, ki']
State after:
case pos
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
k : Fin n
ki : k.succ = i
ki' : k = i.pred i0
⊢ Function.update f i x i = Function.update (fun j => f j.succ) (i.pred i0) x (i.pred i0)

State before:
case pos
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
k : Fin n
ki : k.succ = i
ki' : k = i.pred i0
⊢ Function.update f i x i = Function.update (fun j => f j.succ) (i.pred i0) x (i.pred i0)
Tactic:
rw [Function.update_same]
State after:
case pos
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
k : Fin n
ki : k.succ = i
ki' : k = i.pred i0
⊢ x = Function.update (fun j => f j.succ) (i.pred i0) x (i.pred i0)

State before:
case pos
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
k : Fin n
ki : k.succ = i
ki' : k = i.pred i0
⊢ x = Function.update (fun j => f j.succ) (i.pred i0) x (i.pred i0)
Tactic:
rw [Function.update_same]
State after:
no goals

State before:
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
k : Fin n
ki : k.succ = i
⊢ k = i.pred i0
Tactic:
simp_rw [← ki, Fin.pred_succ]
State after:
no goals

State before:
case neg
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
k : Fin n
ki : ¬k.succ = i
⊢ Function.update f i x k.succ = Function.update (fun j => f j.succ) (i.pred i0) x k
Tactic:
rw [Function.update_noteq ki]
State after:
case neg
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
k : Fin n
ki : ¬k.succ = i
⊢ f k.succ = Function.update (fun j => f j.succ) (i.pred i0) x k

State before:
case neg
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
k : Fin n
ki : ¬k.succ = i
⊢ f k.succ = Function.update (fun j => f j.succ) (i.pred i0) x k
Tactic:
rw [Function.update_noteq _]
State after:
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
k : Fin n
ki : ¬k.succ = i
⊢ k ≠ i.pred i0

State before:
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
k : Fin n
ki : ¬k.succ = i
⊢ k ≠ i.pred i0
Tactic:
by_contra h
State after:
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
k : Fin n
ki : ¬k.succ = i
h : k = i.pred i0
⊢ False

State before:
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
k : Fin n
ki : ¬k.succ = i
h : k = i.pred i0
⊢ False
Tactic:
simp only [h, Fin.succ_pred, not_true_eq_false] at ki
State after:
no goals