internlm/Lean-Github huggingface dataset:
Theorem: update_nz_succ
Proof 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]
Proof 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
Theorem: update_nz_succ
Proof 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']
Proof 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)
Theorem: update_nz_succ
Proof 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]
Proof 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)
Theorem: update_nz_succ
Proof 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]
Proof state after:
no goals
Theorem: update_nz_succ
Proof 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]
Proof state after:
no goals
Theorem: update_nz_succ
Proof 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]
Proof 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
Theorem: update_nz_succ
Proof 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 _]
Proof 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
Theorem: update_nz_succ
Proof 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
Proof 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
Theorem: update_nz_succ
Proof 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
Proof state after:
no goals
Theorem: smul_cmmap_add
Proof 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
Proof 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)
Theorem: smul_cmmap_add
Proof 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
Proof 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)
Theorem: smul_cmmap_add
Proof 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]
Proof 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)
Theorem: smul_cmmap_add
Proof 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
Proof 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)
Theorem: smul_cmmap_add
Proof 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
Proof 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)
Theorem: smul_cmmap_add
Proof 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]
Proof state after:
no goals
Theorem: smul_cmmap_add
Proof 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]
Proof state after:
no goals
Theorem: smul_cmmap_smul
Proof 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
Proof 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)
Theorem: smul_cmmap_smul
Proof 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]
Proof 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)
Theorem: smul_cmmap_smul
Proof 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
Proof 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)
Theorem: smul_cmmap_smul
Proof 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]
Proof 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)
Theorem: smul_cmmap_smul
Proof 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
Proof 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)
Theorem: smul_cmmap_smul
Proof 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
Proof 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)
Theorem: smul_cmmap_smul
Proof 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]
Proof state after:
no goals
Theorem: smul_cmmap_smul
Proof 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
Proof 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)
Theorem: smul_cmmap_smul
Proof 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]
Proof state after:
no goals