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

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

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

State before:
case h
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
z : Fin (n + 1) → A
x : A
i : Fin 1
⊢ Function.update (fun x => z 0) 0 x i = x
Tactic:
have i0 : i = 0 := by simp only [eq_iff_true_of_subsingleton]
State after:
case h
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
z : Fin (n + 1) → A
x : A
i : Fin 1
i0 : i = 0
⊢ Function.update (fun x => z 0) 0 x i = x

State before:
case h
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
z : Fin (n + 1) → A
x : A
i : Fin 1
i0 : i = 0
⊢ Function.update (fun x => z 0) 0 x i = x
Tactic:
rw [i0]
State after:
case h
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
z : Fin (n + 1) → A
x : A
i : Fin 1
i0 : i = 0
⊢ Function.update (fun x => z 0) 0 x 0 = x

State before:
case h
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
z : Fin (n + 1) → A
x : A
i : Fin 1
i0 : i = 0
⊢ Function.update (fun x => z 0) 0 x 0 = x
Tactic:
simp only [Function.update_same]
State after:
no goals

State before:
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
z : Fin (n + 1) → A
x : A
i : Fin 1
⊢ i = 0
Tactic:
simp only [eq_iff_true_of_subsingleton]
State after:
no goals