Theorem: smul_cmmap_smul (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)) (s : 𝕜) (u : A),
    smulCmmapFn x xs (Function.update z i (s • u)) = s • smulCmmapFn x xs (Function.update z i u)
Tactic:
intro d z i s u
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)
s : 𝕜
u : A
⊢ smulCmmapFn x xs (Function.update z i (s • u)) = s • smulCmmapFn x xs (Function.update z i u)

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)
s : 𝕜
u : A
⊢ smulCmmapFn x xs (Function.update z i (s • u)) = s • smulCmmapFn x xs (Function.update z i u)
Tactic:
rw [smulCmmapFn]
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)
s : 𝕜
u : A
⊢ ((x.toFun fun x => Function.update z i (s • u) 0) • xs.toFun fun i_1 => Function.update z i (s • u) i_1.succ) =
    s • smulCmmapFn x xs (Function.update z i u)

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)
s : 𝕜
u : A
⊢ ((x.toFun fun x => Function.update z i (s • u) 0) • xs.toFun fun i_1 => Function.update z i (s • u) i_1.succ) =
    s • smulCmmapFn x xs (Function.update z i u)
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)
s : 𝕜
u : A
i0 : i = 0
⊢ ((x.toFun fun x => Function.update z i (s • u) 0) • xs.toFun fun i_1 => Function.update z i (s • u) i_1.succ) =
    s • smulCmmapFn x xs (Function.update z i u)

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)
s : 𝕜
u : A
i0 : ¬i = 0
⊢ ((x.toFun fun x => Function.update z i (s • u) 0) • xs.toFun fun i_1 => Function.update z i (s • u) i_1.succ) =
    s • smulCmmapFn x xs (Function.update z i u)

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)
s : 𝕜
u : A
i0 : i = 0
⊢ ((x.toFun fun x => Function.update z i (s • u) 0) • xs.toFun fun i_1 => Function.update z i (s • u) i_1.succ) =
    s • smulCmmapFn x xs (Function.update z i u)
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)
s : 𝕜
u : A
i0 : i = 0
⊢ ((x.toFun fun x => Function.update z 0 (s • u) 0) • xs.toFun fun i => Function.update z 0 (s • u) i.succ) =
    s • smulCmmapFn x xs (Function.update z 0 u)

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)
s : 𝕜
u : A
i0 : i = 0
⊢ ((x.toFun fun x => Function.update z 0 (s • u) 0) • xs.toFun fun i => Function.update z 0 (s • u) i.succ) =
    s • smulCmmapFn x xs (Function.update z 0 u)
Tactic:
have su := x.map_smul (fun _ ↦ z 0) 0 s u
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)
s : 𝕜
u : A
i0 : i = 0
su : x (Function.update (fun x => z 0) 0 (s • u)) = s • x (Function.update (fun x => z 0) 0 u)
⊢ ((x.toFun fun x => Function.update z 0 (s • u) 0) • xs.toFun fun i => Function.update z 0 (s • u) i.succ) =
    s • smulCmmapFn x xs (Function.update z 0 u)

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)
s : 𝕜
u : A
i0 : i = 0
su : x (Function.update (fun x => z 0) 0 (s • u)) = s • x (Function.update (fun x => z 0) 0 u)
⊢ ((x.toFun fun x => Function.update z 0 (s • u) 0) • xs.toFun fun i => Function.update z 0 (s • u) i.succ) =
    s • smulCmmapFn x xs (Function.update z 0 u)
Tactic:
rw [update_0_0 z _, update_0_0 z _] at su
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)
s : 𝕜
u : A
i0 : i = 0
su : (x fun x => s • u) = s • x fun x => u
⊢ ((x.toFun fun x => Function.update z 0 (s • u) 0) • xs.toFun fun i => Function.update z 0 (s • u) i.succ) =
    s • smulCmmapFn x xs (Function.update z 0 u)

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)
s : 𝕜
u : A
i0 : i = 0
su : (x fun x => s • u) = s • x fun x => u
⊢ ((x.toFun fun x => Function.update z 0 (s • u) 0) • xs.toFun fun i => Function.update z 0 (s • u) i.succ) =
    s • smulCmmapFn x xs (Function.update z 0 u)
Tactic:
simp only [Function.update_same, MultilinearMap.toFun_eq_coe, ContinuousMultilinearMap.coe_coe,
  su, smul_eq_mul, ne_eq, update_0_succ d z _ _, smulCmmapFn, ←smul_assoc]
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)
s : 𝕜
u : A
i0 : ¬i = 0
⊢ ((x.toFun fun x => Function.update z i (s • u) 0) • xs.toFun fun i_1 => Function.update z i (s • u) i_1.succ) =
    s • smulCmmapFn x xs (Function.update z i u)
Tactic:
have su := xs.map_smul (fun j ↦ z j.succ) (i.pred i0) s u
State after:
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)
s : 𝕜
u : A
i0 : ¬i = 0
su :
  xs (Function.update (fun j => z j.succ) (i.pred i0) (s • u)) =
    s • xs (Function.update (fun j => z j.succ) (i.pred i0) u)
⊢ ((x.toFun fun x => Function.update z i (s • u) 0) • xs.toFun fun i_1 => Function.update z i (s • u) i_1.succ) =
    s • smulCmmapFn x xs (Function.update z i u)

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)
s : 𝕜
u : A
i0 : ¬i = 0
su :
  xs (Function.update (fun j => z j.succ) (i.pred i0) (s • u)) =
    s • xs (Function.update (fun j => z j.succ) (i.pred i0) u)
⊢ ((x.toFun fun x => Function.update z i (s • u) 0) • xs.toFun fun i_1 => Function.update z i (s • u) i_1.succ) =
    s • smulCmmapFn x xs (Function.update z i u)
Tactic:
simp only [ne_eq, MultilinearMap.toFun_eq_coe, ContinuousMultilinearMap.coe_coe,
  update_nz_0 d z i0, update_nz_succ d z _ i0, su, smul_comm _ s, smulCmmapFn]
State after:
no goals