-- Mathlib/LinearAlgebra/TensorProduct/Pi.lean
@[simp]
private lemma piRightInv_single (x : N) (i : ι) (m : M i) :
    piRightInv R S N M (Pi.single i (x ⊗ₜ m)) = x ⊗ₜ Pi.single i m

Proof state:
case h
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
i : ι
m : M i
j : ι
⊢ Pi.single i (x ⊗ₜ[R] m) j = x ⊗ₜ[R] Pi.single i m j

Tactic:
rw [← tmul_single]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
i : ι
m : M i
⊢ (TensorProduct.piRightInv R S N M) (Pi.single i (x ⊗ₜ[R] m)) = x ⊗ₜ[R] Pi.single i m

Tactic:
have : Pi.single i (x ⊗ₜ m) = fun j ↦ x ⊗ₜ[R] (Pi.single i m j) := by
  ext j
  rw [← tmul_single]

Result:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
i : ι
m : M i
this : Pi.single i (x ⊗ₜ[R] m) = fun j => x ⊗ₜ[R] Pi.single i m j
⊢ (TensorProduct.piRightInv R S N M) (Pi.single i (x ⊗ₜ[R] m)) = x ⊗ₜ[R] Pi.single i m

Proof state:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
i : ι
m : M i
⊢ Pi.single i (x ⊗ₜ[R] m) = fun j => x ⊗ₜ[R] Pi.single i m j

Tactic:
ext j

Result:
case h
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
i : ι
m : M i
j : ι
⊢ Pi.single i (x ⊗ₜ[R] m) j = x ⊗ₜ[R] Pi.single i m j

Proof state:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
i : ι
m : M i
this : Pi.single i (x ⊗ₜ[R] m) = fun j => x ⊗ₜ[R] Pi.single i m j
⊢ (TensorProduct.piRightInv R S N M) (Pi.single i (x ⊗ₜ[R] m)) = x ⊗ₜ[R] Pi.single i m

Tactic:
rw [this]

Result:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
i : ι
m : M i
this : Pi.single i (x ⊗ₜ[R] m) = fun j => x ⊗ₜ[R] Pi.single i m j
⊢ ((TensorProduct.piRightInv R S N M) fun j => x ⊗ₜ[R] Pi.single i m j) = x ⊗ₜ[R] Pi.single i m

Proof state:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
i : ι
m : M i
this : Pi.single i (x ⊗ₜ[R] m) = fun j => x ⊗ₜ[R] Pi.single i m j
⊢ ((TensorProduct.piRightInv R S N M) fun j => x ⊗ₜ[R] Pi.single i m j) = x ⊗ₜ[R] Pi.single i m

Tactic:
simp

Result:
no goals