Theorem: update_0_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
⊢ Function.update f 0 x i.succ = f i.succ
Tactic:
rw [Function.update_apply]
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
⊢ (if i.succ = 0 then x else f i.succ) = f i.succ

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
⊢ (if i.succ = 0 then x else f i.succ) = f i.succ
Tactic:
simp only [ite_eq_right_iff]
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
⊢ i.succ = 0 → x = f i.succ

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
⊢ i.succ = 0 → x = f i.succ
Tactic:
have i0 := Fin.succ_ne_zero i
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
i0 : i.succ ≠ 0
⊢ i.succ = 0 → x = f i.succ

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
i0 : i.succ ≠ 0
⊢ i.succ = 0 → x = f i.succ
Tactic:
intro 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
i0 : i.succ ≠ 0
h : i.succ = 0
⊢ x = f i.succ

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
i0 : i.succ ≠ 0
h : i.succ = 0
⊢ x = f i.succ
Tactic:
exfalso
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
i0 : i.succ ≠ 0
h : i.succ = 0
⊢ 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
i0 : i.succ ≠ 0
h : i.succ = 0
⊢ False
Tactic:
exact i0 h
State after:
no goals