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

State before:
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
n k : ℕ
a b : 𝕜
x : E
⊢ ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
Tactic:
induction' n with n h
State after:
case zero
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
⊢ ((termCmmap 𝕜 0 k x) fun x => (a, b)) = a ^ min k 0 • b ^ (0 - k) • x

case succ
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
⊢ ((termCmmap 𝕜 (n + 1) k x) fun x => (a, b)) = a ^ min k (n + 1) • b ^ (n + 1 - k) • x

State before:
case zero
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
⊢ ((termCmmap 𝕜 0 k x) fun x => (a, b)) = a ^ min k 0 • b ^ (0 - k) • x
Tactic:
simp only [termCmmap, ContinuousMultilinearMap.constOfIsEmpty_apply, min_zero, pow_zero,
  zero_tsub, one_smul, Nat.zero_eq]
State after:
no goals

State before:
case succ
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
⊢ ((termCmmap 𝕜 (n + 1) k x) fun x => (a, b)) = a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Tactic:
rw [termCmmap, smulCmmap_apply, h]
State after:
case succ
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
⊢ ((if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) fun x => (a, b)) • a ^ min k n • b ^ (n - k) • x =
    a ^ min k (n + 1) • b ^ (n + 1 - k) • x

State before:
case succ
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
⊢ ((if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) fun x => (a, b)) • a ^ min k n • b ^ (n - k) • x =
    a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Tactic:
by_cases nk : n < k
State after:
case pos
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : n < k
⊢ ((if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) fun x => (a, b)) • a ^ min k n • b ^ (n - k) • x =
    a ^ min k (n + 1) • b ^ (n + 1 - k) • x

case neg
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : ¬n < k
⊢ ((if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) fun x => (a, b)) • a ^ min k n • b ^ (n - k) • x =
    a ^ min k (n + 1) • b ^ (n + 1 - k) • x

State before:
case pos
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : n < k
⊢ ((if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) fun x => (a, b)) • a ^ min k n • b ^ (n - k) • x =
    a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Tactic:
simp [nk]
State after:
case pos
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : n < k
⊢ ((fstCmmap 𝕜 𝕜 𝕜) fun x => (a, b)) • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x

State before:
case pos
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : n < k
⊢ ((fstCmmap 𝕜 𝕜 𝕜) fun x => (a, b)) • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Tactic:
rw [fstCmmap_apply]
State after:
case pos
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : n < k
⊢ a • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x

State before:
case pos
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : n < k
⊢ a • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Tactic:
have nsk : n.succ ≤ k := Nat.succ_le_iff.mpr nk
State after:
case pos
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : n < k
nsk : n.succ ≤ k
⊢ a • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x

State before:
case pos
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : n < k
nsk : n.succ ≤ k
⊢ a • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Tactic:
rw [min_eq_right nk.le, min_eq_right nsk, Nat.sub_eq_zero_of_le nk.le,
  Nat.sub_eq_zero_of_le nsk]
State after:
case pos
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : n < k
nsk : n.succ ≤ k
⊢ a • a ^ n • b ^ 0 • x = a ^ n.succ • b ^ 0 • x

State before:
case pos
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : n < k
nsk : n.succ ≤ k
⊢ a • a ^ n • b ^ 0 • x = a ^ n.succ • b ^ 0 • x
Tactic:
simp only [pow_zero, one_smul, ← smul_assoc, smul_eq_mul, Nat.succ_eq_add_one, pow_succ']
State after:
no goals

State before:
case neg
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : ¬n < k
⊢ ((if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) fun x => (a, b)) • a ^ min k n • b ^ (n - k) • x =
    a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Tactic:
simp [nk]
State after:
case neg
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : ¬n < k
⊢ ((sndCmmap 𝕜 𝕜 𝕜) fun x => (a, b)) • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x

State before:
case neg
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : ¬n < k
⊢ ((sndCmmap 𝕜 𝕜 𝕜) fun x => (a, b)) • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Tactic:
simp at nk
State after:
case neg
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : k ≤ n
⊢ ((sndCmmap 𝕜 𝕜 𝕜) fun x => (a, b)) • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x

State before:
case neg
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : k ≤ n
⊢ ((sndCmmap 𝕜 𝕜 𝕜) fun x => (a, b)) • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Tactic:
rw [sndCmmap_apply]
State after:
case neg
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : k ≤ n
⊢ b • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x

State before:
case neg
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : k ≤ n
⊢ b • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Tactic:
have nsk : k ≤ n.succ := Nat.le_succ_of_le nk
State after:
case neg
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : k ≤ n
nsk : k ≤ n.succ
⊢ b • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x

State before:
case neg
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : k ≤ n
nsk : k ≤ n.succ
⊢ b • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Tactic:
rw [min_eq_left nk, min_eq_left nsk]
State after:
case neg
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : k ≤ n
nsk : k ≤ n.succ
⊢ b • a ^ k • b ^ (n - k) • x = a ^ k • b ^ (n + 1 - k) • x

State before:
case neg
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : k ≤ n
nsk : k ≤ n.succ
⊢ b • a ^ k • b ^ (n - k) • x = a ^ k • b ^ (n + 1 - k) • x
Tactic:
rw [smul_comm b _, ← smul_assoc b _ _, smul_eq_mul, ← pow_succ', ← Nat.sub_add_comm nk]
State after:
no goals