-- 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 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 g_1 : ι →₀ M),
    ((finsuppTensorFinsupp R S M N ι κ) (f ⊗ₜ[R] g)) (i, k) = f i ⊗ₜ[R] g k →
      ((finsuppTensorFinsupp R S M N ι κ) (g_1 ⊗ₜ[R] g)) (i, k) = g_1 i ⊗ₜ[R] g k →
        ((finsuppTensorFinsupp R S M N ι κ) ((f + g_1) ⊗ₜ[R] g)) (i, k) = (f + g_1) i ⊗ₜ[R] g k

Tactic:
intro f₁ f₂ hf₁ hf₂

Result:
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

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
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

Tactic:
simp [tmul_add, hg₁, hg₂]

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
⊢ ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] Finsupp.single k' n)) (i, k) =
    (Finsupp.single i' m) i ⊗ₜ[R] (Finsupp.single k' n) k

Tactic:
simp_rw [finsuppTensorFinsupp_single, Finsupp.single_apply, Prod.mk.inj_iff, ite_and]

Result:
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

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
⊢ ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] Finsupp.single k' n)) (i, k) =
    (Finsupp.single i' m) i ⊗ₜ[R] (Finsupp.single k' n) k

Tactic:
classical
simp_rw [finsuppTensorFinsupp_single, Finsupp.single_apply, Prod.mk.inj_iff, ite_and]
split_ifs <;> simp

Result:
no goals

Proof state:
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 ι κ) (f ⊗ₜ[R] g)) (i, k) = f i ⊗ₜ[R] g k

Tactic:
apply Finsupp.induction_linear f

Result:
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

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 g_1 : ι →₀ M),
    ((finsuppTensorFinsupp R S M N ι κ) (f ⊗ₜ[R] g)) (i, k) = f i ⊗ₜ[R] g k →
      ((finsuppTensorFinsupp R S M N ι κ) (g_1 ⊗ₜ[R] g)) (i, k) = g_1 i ⊗ₜ[R] g k →
        ((finsuppTensorFinsupp R S M N ι κ) ((f + g_1) ⊗ₜ[R] g)) (i, k) = (f + g_1) i ⊗ₜ[R] g k

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

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
⊢ ∀ (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

Tactic:
intro k' n

Result:
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
⊢ ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] Finsupp.single k' n)) (i, k) =
    (Finsupp.single i' m) i ⊗ₜ[R] (Finsupp.single k' n) k