-- Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
theorem finsuppTensorFinsupp_apply (f : ι →₀ M) (g : κ →₀ N) (i : ι) (k : κ) :
    finsuppTensorFinsupp R S M N ι κ (f ⊗ₜ g) (i, k) = f i ⊗ₜ g k

Proof state:
case hsingle.h0
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
⊢ ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] 0)) (i, k) = (Finsupp.single i' m) i ⊗ₜ[R] 0 k

Tactic:
simp

Result:
no goals

Proof state:
case hsingle
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
⊢ ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] g)) (i, k) = (Finsupp.single i' m) i ⊗ₜ[R] g k

Tactic:
apply Finsupp.induction_linear g

Result:
case hsingle.h0
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
⊢ ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] 0)) (i, k) = (Finsupp.single i' m) i ⊗ₜ[R] 0 k

case hsingle.hadd
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
⊢ ∀ (f g : κ →₀ N),
    ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] f)) (i, k) = (Finsupp.single i' m) i ⊗ₜ[R] f k →
      ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] g)) (i, k) = (Finsupp.single i' m) i ⊗ₜ[R] g k →
        ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] (f + g))) (i, k) =
          (Finsupp.single i' m) i ⊗ₜ[R] (f + g) k

case hsingle.hsingle
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
⊢ ∀ (a : κ) (b : N),
    ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] Finsupp.single a b)) (i, k) =
      (Finsupp.single i' m) i ⊗ₜ[R] (Finsupp.single a b) k

Proof state:
case hsingle
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
⊢ ∀ (a : ι) (b : M),
    ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single a b ⊗ₜ[R] g)) (i, k) = (Finsupp.single a b) i ⊗ₜ[R] g k

Tactic:
intro i' m

Result:
case hsingle
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
⊢ ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] g)) (i, k) = (Finsupp.single i' m) i ⊗ₜ[R] g k

Proof state:
case hsingle.hadd
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
⊢ ∀ (f g : κ →₀ N),
    ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] f)) (i, k) = (Finsupp.single i' m) i ⊗ₜ[R] f k →
      ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] g)) (i, k) = (Finsupp.single i' m) i ⊗ₜ[R] g k →
        ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] (f + g))) (i, k) =
          (Finsupp.single i' m) i ⊗ₜ[R] (f + g) k

Tactic:
intro g₁ g₂ hg₁ hg₂

Result:
case hsingle.hadd
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
g₁ g₂ : κ →₀ N
hg₁ : ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] g₁)) (i, k) = (Finsupp.single i' m) i ⊗ₜ[R] g₁ k
hg₂ : ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] g₂)) (i, k) = (Finsupp.single i' m) i ⊗ₜ[R] g₂ k
⊢ ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] (g₁ + g₂))) (i, k) =
    (Finsupp.single i' m) i ⊗ₜ[R] (g₁ + g₂) k

Proof state:
case hadd
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
f₁ f₂ : ι →₀ M
hf₁ : ((finsuppTensorFinsupp R S M N ι κ) (f₁ ⊗ₜ[R] g)) (i, k) = f₁ i ⊗ₜ[R] g k
hf₂ : ((finsuppTensorFinsupp R S M N ι κ) (f₂ ⊗ₜ[R] g)) (i, k) = f₂ i ⊗ₜ[R] g k
⊢ ((finsuppTensorFinsupp R S M N ι κ) ((f₁ + f₂) ⊗ₜ[R] g)) (i, k) = (f₁ + f₂) i ⊗ₜ[R] g k

Tactic:
simp [add_tmul, hf₁, hf₂]

Result:
no goals

Proof state:
case hsingle.hsingle
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
⊢ (if i' = i then if k' = k then m ⊗ₜ[R] n else 0 else 0) = (if i' = i then m else 0) ⊗ₜ[R] if k' = k then n else 0

Tactic:
split_ifs <;> simp

Result:
no goals

Proof state:
case h0
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
⊢ ((finsuppTensorFinsupp R S M N ι κ) (0 ⊗ₜ[R] g)) (i, k) = 0 i ⊗ₜ[R] g k

Tactic:
simp

Result:
no goals