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

State before:
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
⊢ ∀ (d : DecidableEq (Fin (n + 1))) (z : Fin (n + 1) → A) (i : Fin (n + 1)) (u v : A),
    smulCmmapFn x xs (Function.update z i (u + v)) =
      smulCmmapFn x xs (Function.update z i u) + smulCmmapFn x xs (Function.update z i v)
Tactic:
intro d z i u v
State after:
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
d : DecidableEq (Fin (n + 1))
z : Fin (n + 1) → A
i : Fin (n + 1)
u v : A
⊢ smulCmmapFn x xs (Function.update z i (u + v)) =
    smulCmmapFn x xs (Function.update z i u) + smulCmmapFn x xs (Function.update z i v)

State before:
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
d : DecidableEq (Fin (n + 1))
z : Fin (n + 1) → A
i : Fin (n + 1)
u v : A
⊢ smulCmmapFn x xs (Function.update z i (u + v)) =
    smulCmmapFn x xs (Function.update z i u) + smulCmmapFn x xs (Function.update z i v)
Tactic:
by_cases i0 : i = 0
State after:
case pos
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
d : DecidableEq (Fin (n + 1))
z : Fin (n + 1) → A
i : Fin (n + 1)
u v : A
i0 : i = 0
⊢ smulCmmapFn x xs (Function.update z i (u + v)) =
    smulCmmapFn x xs (Function.update z i u) + smulCmmapFn x xs (Function.update z i v)

case neg
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
d : DecidableEq (Fin (n + 1))
z : Fin (n + 1) → A
i : Fin (n + 1)
u v : A
i0 : ¬i = 0
⊢ smulCmmapFn x xs (Function.update z i (u + v)) =
    smulCmmapFn x xs (Function.update z i u) + smulCmmapFn x xs (Function.update z i v)

State before:
case pos
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
d : DecidableEq (Fin (n + 1))
z : Fin (n + 1) → A
i : Fin (n + 1)
u v : A
i0 : i = 0
⊢ smulCmmapFn x xs (Function.update z i (u + v)) =
    smulCmmapFn x xs (Function.update z i u) + smulCmmapFn x xs (Function.update z i v)
Tactic:
rw [i0]
State after:
case pos
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
d : DecidableEq (Fin (n + 1))
z : Fin (n + 1) → A
i : Fin (n + 1)
u v : A
i0 : i = 0
⊢ smulCmmapFn x xs (Function.update z 0 (u + v)) =
    smulCmmapFn x xs (Function.update z 0 u) + smulCmmapFn x xs (Function.update z 0 v)

State before:
case pos
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
d : DecidableEq (Fin (n + 1))
z : Fin (n + 1) → A
i : Fin (n + 1)
u v : A
i0 : i = 0
⊢ smulCmmapFn x xs (Function.update z 0 (u + v)) =
    smulCmmapFn x xs (Function.update z 0 u) + smulCmmapFn x xs (Function.update z 0 v)
Tactic:
have uv := x.map_add (fun _ ↦ z 0) 0 u v
State after:
case pos
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
d : DecidableEq (Fin (n + 1))
z : Fin (n + 1) → A
i : Fin (n + 1)
u v : A
i0 : i = 0
uv :
  x (Function.update (fun x => z 0) 0 (u + v)) =
    x (Function.update (fun x => z 0) 0 u) + x (Function.update (fun x => z 0) 0 v)
⊢ smulCmmapFn x xs (Function.update z 0 (u + v)) =
    smulCmmapFn x xs (Function.update z 0 u) + smulCmmapFn x xs (Function.update z 0 v)

State before:
case pos
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
d : DecidableEq (Fin (n + 1))
z : Fin (n + 1) → A
i : Fin (n + 1)
u v : A
i0 : i = 0
uv :
  x (Function.update (fun x => z 0) 0 (u + v)) =
    x (Function.update (fun x => z 0) 0 u) + x (Function.update (fun x => z 0) 0 v)
⊢ smulCmmapFn x xs (Function.update z 0 (u + v)) =
    smulCmmapFn x xs (Function.update z 0 u) + smulCmmapFn x xs (Function.update z 0 v)
Tactic:
simp only [update_0_0 z _] at uv
State after:
case pos
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
d : DecidableEq (Fin (n + 1))
z : Fin (n + 1) → A
i : Fin (n + 1)
u v : A
i0 : i = 0
uv : (x fun x => u + v) = (x fun x => u) + x fun x => v
⊢ smulCmmapFn x xs (Function.update z 0 (u + v)) =
    smulCmmapFn x xs (Function.update z 0 u) + smulCmmapFn x xs (Function.update z 0 v)

State before:
case pos
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
d : DecidableEq (Fin (n + 1))
z : Fin (n + 1) → A
i : Fin (n + 1)
u v : A
i0 : i = 0
uv : (x fun x => u + v) = (x fun x => u) + x fun x => v
⊢ smulCmmapFn x xs (Function.update z 0 (u + v)) =
    smulCmmapFn x xs (Function.update z 0 u) + smulCmmapFn x xs (Function.update z 0 v)
Tactic:
simp only [Function.update_same, MultilinearMap.toFun_eq_coe, ContinuousMultilinearMap.coe_coe,
  ne_eq, uv, add_smul, smulCmmapFn, update_0_succ]
State after:
no goals

State before:
case neg
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
d : DecidableEq (Fin (n + 1))
z : Fin (n + 1) → A
i : Fin (n + 1)
u v : A
i0 : ¬i = 0
⊢ smulCmmapFn x xs (Function.update z i (u + v)) =
    smulCmmapFn x xs (Function.update z i u) + smulCmmapFn x xs (Function.update z i v)
Tactic:
simp only [smul_add, ne_eq, update_nz_0 d z i0, MultilinearMap.toFun_eq_coe,
  ContinuousMultilinearMap.coe_coe, update_nz_succ d z _ i0, MultilinearMap.map_add, smul_add,
  smulCmmapFn]
State after:
no goals