[GOAL]
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
i : ι
m : M
k : κ
n : N
⊢ ↑(finsuppTensorFinsupp R M N ι κ) (Finsupp.single i m ⊗ₜ[R] Finsupp.single k n) = Finsupp.single (i, k) (m ⊗ₜ[R] n)
[PROOFSTEP]
classical simp [finsuppTensorFinsupp]
[GOAL]
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
i : ι
m : M
k : κ
n : N
⊢ ↑(finsuppTensorFinsupp R M N ι κ) (Finsupp.single i m ⊗ₜ[R] Finsupp.single k n) = Finsupp.single (i, k) (m ⊗ₜ[R] n)
[PROOFSTEP]
simp [finsuppTensorFinsupp]
[GOAL]
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
⊢ ↑(↑(finsuppTensorFinsupp R M N ι κ) (f ⊗ₜ[R] g)) (i, k) = ↑f i ⊗ₜ[R] ↑g k
[PROOFSTEP]
apply Finsupp.induction_linear f
[GOAL]
case h0
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
⊢ ↑(↑(finsuppTensorFinsupp R M N ι κ) (0 ⊗ₜ[R] g)) (i, k) = ↑0 i ⊗ₜ[R] ↑g k
[PROOFSTEP]
simp
[GOAL]
case hadd
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
⊢ ∀ (f g_1 : ι →₀ M),
    ↑(↑(finsuppTensorFinsupp R M N ι κ) (f ⊗ₜ[R] g)) (i, k) = ↑f i ⊗ₜ[R] ↑g k →
      ↑(↑(finsuppTensorFinsupp R M N ι κ) (g_1 ⊗ₜ[R] g)) (i, k) = ↑g_1 i ⊗ₜ[R] ↑g k →
        ↑(↑(finsuppTensorFinsupp R M N ι κ) ((f + g_1) ⊗ₜ[R] g)) (i, k) = ↑(f + g_1) i ⊗ₜ[R] ↑g k
[PROOFSTEP]
intro f₁ f₂ hf₁ hf₂
[GOAL]
case hadd
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
f₁ f₂ : ι →₀ M
hf₁ : ↑(↑(finsuppTensorFinsupp R M N ι κ) (f₁ ⊗ₜ[R] g)) (i, k) = ↑f₁ i ⊗ₜ[R] ↑g k
hf₂ : ↑(↑(finsuppTensorFinsupp R M N ι κ) (f₂ ⊗ₜ[R] g)) (i, k) = ↑f₂ i ⊗ₜ[R] ↑g k
⊢ ↑(↑(finsuppTensorFinsupp R M N ι κ) ((f₁ + f₂) ⊗ₜ[R] g)) (i, k) = ↑(f₁ + f₂) i ⊗ₜ[R] ↑g k
[PROOFSTEP]
simp [add_tmul, hf₁, hf₂]
[GOAL]
case hsingle
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
⊢ ∀ (a : ι) (b : M),
    ↑(↑(finsuppTensorFinsupp R M N ι κ) (Finsupp.single a b ⊗ₜ[R] g)) (i, k) = ↑(Finsupp.single a b) i ⊗ₜ[R] ↑g k
[PROOFSTEP]
intro i' m
[GOAL]
case hsingle
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
⊢ ↑(↑(finsuppTensorFinsupp R M N ι κ) (Finsupp.single i' m ⊗ₜ[R] g)) (i, k) = ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑g k
[PROOFSTEP]
apply Finsupp.induction_linear g
[GOAL]
case hsingle.h0
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
⊢ ↑(↑(finsuppTensorFinsupp R M N ι κ) (Finsupp.single i' m ⊗ₜ[R] 0)) (i, k) = ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑0 k
[PROOFSTEP]
simp
[GOAL]
case hsingle.hadd
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
⊢ ∀ (f g : κ →₀ N),
    ↑(↑(finsuppTensorFinsupp R M N ι κ) (Finsupp.single i' m ⊗ₜ[R] f)) (i, k) = ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑f k →
      ↑(↑(finsuppTensorFinsupp R M N ι κ) (Finsupp.single i' m ⊗ₜ[R] g)) (i, k) = ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑g k →
        ↑(↑(finsuppTensorFinsupp R M N ι κ) (Finsupp.single i' m ⊗ₜ[R] (f + g))) (i, k) =
          ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑(f + g) k
[PROOFSTEP]
intro g₁ g₂ hg₁ hg₂
[GOAL]
case hsingle.hadd
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
g₁ g₂ : κ →₀ N
hg₁ : ↑(↑(finsuppTensorFinsupp R M N ι κ) (Finsupp.single i' m ⊗ₜ[R] g₁)) (i, k) = ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑g₁ k
hg₂ : ↑(↑(finsuppTensorFinsupp R M N ι κ) (Finsupp.single i' m ⊗ₜ[R] g₂)) (i, k) = ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑g₂ k
⊢ ↑(↑(finsuppTensorFinsupp R M N ι κ) (Finsupp.single i' m ⊗ₜ[R] (g₁ + g₂))) (i, k) =
    ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑(g₁ + g₂) k
[PROOFSTEP]
simp [tmul_add, hg₁, hg₂]
[GOAL]
case hsingle.hsingle
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
⊢ ∀ (a : κ) (b : N),
    ↑(↑(finsuppTensorFinsupp R M N ι κ) (Finsupp.single i' m ⊗ₜ[R] Finsupp.single a b)) (i, k) =
      ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑(Finsupp.single a b) k
[PROOFSTEP]
intro k' n
[GOAL]
case hsingle.hsingle
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
⊢ ↑(↑(finsuppTensorFinsupp R M N ι κ) (Finsupp.single i' m ⊗ₜ[R] Finsupp.single k' n)) (i, k) =
    ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑(Finsupp.single k' n) k
[PROOFSTEP]
simp only [finsuppTensorFinsupp_single]
  -- split_ifs; finish can close the goal from here
[GOAL]
case hsingle.hsingle
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
⊢ ↑(Finsupp.single (i', k') (m ⊗ₜ[R] n)) (i, k) = ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑(Finsupp.single k' n) k
[PROOFSTEP]
by_cases h1 : (i', k') = (i, k)
[GOAL]
case pos
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
h1 : (i', k') = (i, k)
⊢ ↑(Finsupp.single (i', k') (m ⊗ₜ[R] n)) (i, k) = ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑(Finsupp.single k' n) k
[PROOFSTEP]
simp only [Prod.mk.inj_iff] at h1 
[GOAL]
case pos
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
h1 : i' = i ∧ k' = k
⊢ ↑(Finsupp.single (i', k') (m ⊗ₜ[R] n)) (i, k) = ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑(Finsupp.single k' n) k
[PROOFSTEP]
simp [h1]
[GOAL]
case neg
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
h1 : ¬(i', k') = (i, k)
⊢ ↑(Finsupp.single (i', k') (m ⊗ₜ[R] n)) (i, k) = ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑(Finsupp.single k' n) k
[PROOFSTEP]
simp only [Prod.mk.inj_iff, not_and_or] at h1 
[GOAL]
case neg
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
h1 : ¬i' = i ∨ ¬k' = k
⊢ ↑(Finsupp.single (i', k') (m ⊗ₜ[R] n)) (i, k) = ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑(Finsupp.single k' n) k
[PROOFSTEP]
cases' h1 with h1 h1
[GOAL]
case neg.inl
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
h1 : ¬i' = i
⊢ ↑(Finsupp.single (i', k') (m ⊗ₜ[R] n)) (i, k) = ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑(Finsupp.single k' n) k
[PROOFSTEP]
simp [h1]
[GOAL]
case neg.inr
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
h1 : ¬k' = k
⊢ ↑(Finsupp.single (i', k') (m ⊗ₜ[R] n)) (i, k) = ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑(Finsupp.single k' n) k
[PROOFSTEP]
simp [h1]
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
S : Type u_1
inst✝ : CommRing S
α : Type u_2
β : Type u_3
f : α →₀ S
g : β →₀ S
a : α
b : β
⊢ ↑(↑(finsuppTensorFinsupp' S α β) (f ⊗ₜ[S] g)) (a, b) = ↑f a * ↑g b
[PROOFSTEP]
simp [finsuppTensorFinsupp']
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
S : Type u_1
inst✝ : CommRing S
α : Type u_2
β : Type u_3
a : α
b : β
r₁ r₂ : S
⊢ ↑(finsuppTensorFinsupp' S α β) (Finsupp.single a r₁ ⊗ₜ[S] Finsupp.single b r₂) = Finsupp.single (a, b) (r₁ * r₂)
[PROOFSTEP]
ext ⟨a', b'⟩
[GOAL]
case h.mk
R : Type u
M : Type v
N : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
S : Type u_1
inst✝ : CommRing S
α : Type u_2
β : Type u_3
a : α
b : β
r₁ r₂ : S
a' : α
b' : β
⊢ ↑(↑(finsuppTensorFinsupp' S α β) (Finsupp.single a r₁ ⊗ₜ[S] Finsupp.single b r₂)) (a', b') =
    ↑(Finsupp.single (a, b) (r₁ * r₂)) (a', b')
[PROOFSTEP]
classical aesop (add norm [Finsupp.single_apply])
[GOAL]
case h.mk
R : Type u
M : Type v
N : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
S : Type u_1
inst✝ : CommRing S
α : Type u_2
β : Type u_3
a : α
b : β
r₁ r₂ : S
a' : α
b' : β
⊢ ↑(↑(finsuppTensorFinsupp' S α β) (Finsupp.single a r₁ ⊗ₜ[S] Finsupp.single b r₂)) (a', b') =
    ↑(Finsupp.single (a, b) (r₁ * r₂)) (a', b')
[PROOFSTEP]
aesop (add norm [Finsupp.single_apply])
