-- Mathlib/RingTheory/TensorProduct/Free.lean
lemma _root_.Basis.baseChange_linearMap (b : Basis ι R M) (b' : Basis ι' R N) (ij : ι × ι') :
    baseChange A (b'.linearMap b ij) = (basis A b').linearMap (basis A b) ij

Proof state:
R : Type u_1
M : Type uM
ι : Type uι
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Fintype ι
ι' : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι'
inst✝³ : AddCommMonoid N
inst✝² : Module R N
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
⊢ baseChange A ((b'.linearMap b) ij) = ((basis A b').linearMap (basis A b)) ij

Tactic:
apply (basis A b').ext

Result:
R : Type u_1
M : Type uM
ι : Type uι
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Fintype ι
ι' : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι'
inst✝³ : AddCommMonoid N
inst✝² : Module R N
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
⊢ ∀ (i : ι'),
    (baseChange A ((b'.linearMap b) ij)) ((basis A b') i) = (((basis A b').linearMap (basis A b)) ij) ((basis A b') i)

Proof state:
R : Type u_1
M : Type uM
ι : Type uι
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Fintype ι
ι' : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι'
inst✝³ : AddCommMonoid N
inst✝² : Module R N
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
⊢ ∀ (i : ι'),
    (baseChange A ((b'.linearMap b) ij)) ((basis A b') i) = (((basis A b').linearMap (basis A b)) ij) ((basis A b') i)

Tactic:
intro k

Result:
R : Type u_1
M : Type uM
ι : Type uι
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Fintype ι
ι' : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι'
inst✝³ : AddCommMonoid N
inst✝² : Module R N
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
k : ι'
⊢ (baseChange A ((b'.linearMap b) ij)) ((basis A b') k) = (((basis A b').linearMap (basis A b)) ij) ((basis A b') k)

Proof state:
R : Type u_1
M : Type uM
ι : Type uι
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Fintype ι
ι' : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι'
inst✝³ : AddCommMonoid N
inst✝² : Module R N
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
k : ι'
⊢ (baseChange A ((b'.linearMap b) ij)) ((basis A b') k) = (((basis A b').linearMap (basis A b)) ij) ((basis A b') k)

Tactic:
conv_lhs => simp only [basis_apply, baseChange_tmul]

Result:
R : Type u_1
M : Type uM
ι : Type uι
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Fintype ι
ι' : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι'
inst✝³ : AddCommMonoid N
inst✝² : Module R N
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
k : ι'
⊢ 1 ⊗ₜ[R] ((b'.linearMap b) ij) (b' k) = (((basis A b').linearMap (basis A b)) ij) ((basis A b') k)

Proof state:
R : Type u_1
M : Type uM
ι : Type uι
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Fintype ι
ι' : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι'
inst✝³ : AddCommMonoid N
inst✝² : Module R N
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
k : ι'
⊢ 1 ⊗ₜ[R] ((b'.linearMap b) ij) (b' k) = (((basis A b').linearMap (basis A b)) ij) ((basis A b') k)

Tactic:
simp_rw [Basis.linearMap_apply_apply, basis_apply]

Result:
R : Type u_1
M : Type uM
ι : Type uι
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Fintype ι
ι' : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι'
inst✝³ : AddCommMonoid N
inst✝² : Module R N
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
k : ι'
⊢ (1 ⊗ₜ[R] if ij.2 = k then b ij.1 else 0) = if ij.2 = k then 1 ⊗ₜ[R] b ij.1 else 0

Proof state:
R : Type u_1
M : Type uM
ι : Type uι
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Fintype ι
ι' : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι'
inst✝³ : AddCommMonoid N
inst✝² : Module R N
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
k : ι'
⊢ (1 ⊗ₜ[R] if ij.2 = k then b ij.1 else 0) = if ij.2 = k then 1 ⊗ₜ[R] b ij.1 else 0

Tactic:
split <;> simp only [TensorProduct.tmul_zero]

Result:
no goals