-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem mapCoeffs_apply (i : ι) : b.mapCoeffs f h i = b i :=
  apply_eq_iff.mpr <| by
    -- Porting note: in Lean 3, these were automatically inferred from the definition of
    -- `mapCoeffs`.
    letI : Module R' R := Module.compHom R (↑f.symm : R' →+* R)
    haveI : IsScalarTower R' R M :=
    { smul_assoc := fun x y z => by
        change (f.symm x * y) • z = x • (y • z)
        rw [mul_smul, ← h, f.apply_symm_apply] }
    simp

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
R' : Type u_10
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), f c • x = c • x
i : ι
⊢ (b.mapCoeffs f h).repr (b i) = single i 1

Tactic:
letI : Module R' R := Module.compHom R (↑f.symm : R' →+* R)

Result:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
R' : Type u_10
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), f c • x = c • x
i : ι
this : Module R' R := Module.compHom R ↑f.symm
⊢ (b.mapCoeffs f h).repr (b i) = single i 1

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
R' : Type u_10
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), f c • x = c • x
i : ι
this : Module R' R := Module.compHom R ↑f.symm
x : R'
y : R
z : M
⊢ (x • y) • z = x • y • z

Tactic:
change (f.symm x * y) • z = x • (y • z)

Result:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
R' : Type u_10
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), f c • x = c • x
i : ι
this : Module R' R := Module.compHom R ↑f.symm
x : R'
y : R
z : M
⊢ (f.symm x * y) • z = x • y • z

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
R' : Type u_10
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), f c • x = c • x
i : ι
this : Module R' R := Module.compHom R ↑f.symm
⊢ (b.mapCoeffs f h).repr (b i) = single i 1

Tactic:
haveI : IsScalarTower R' R M :=
{ smul_assoc := fun x y z => by
    change (f.symm x * y) • z = x • (y • z)
    rw [mul_smul, ← h, f.apply_symm_apply] }

Result:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
R' : Type u_10
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), f c • x = c • x
i : ι
this✝ : Module R' R := Module.compHom R ↑f.symm
this : IsScalarTower R' R M
⊢ (b.mapCoeffs f h).repr (b i) = single i 1

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
R' : Type u_10
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), f c • x = c • x
i : ι
this✝ : Module R' R := Module.compHom R ↑f.symm
this : IsScalarTower R' R M
⊢ (b.mapCoeffs f h).repr (b i) = single i 1

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
R' : Type u_10
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), f c • x = c • x
i : ι
this : Module R' R := Module.compHom R ↑f.symm
x : R'
y : R
z : M
⊢ (f.symm x * y) • z = x • y • z

Tactic:
rw [mul_smul, ← h, f.apply_symm_apply]

Result:
no goals