-- Mathlib/LinearAlgebra/Basis/Basic.lean
theorem Basis.restrictScalars_repr_apply (m : span R (Set.range b)) (i : ι) :
    algebraMap R S ((b.restrictScalars R).repr m i) = b.repr m i

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : NoZeroSMulDivisors R S
b : Basis ι S M
m : ↥(span R (range ⇑b))
i x✝ : ι
⊢ (mapRange.linearMap (Algebra.linearMap R S) ∘ₗ ↑(restrictScalars R b).repr) ((restrictScalars R b) x✝) =
    ((↑R ↑b.repr).domRestrict (span R (range ⇑b))) ((restrictScalars R b) x✝)

Tactic:
simp only [LinearMap.coe_comp, LinearEquiv.coe_toLinearMap, Function.comp_apply, map_one,
  Basis.repr_self, Finsupp.mapRange.linearMap_apply, Finsupp.mapRange_single,
  Algebra.linearMap_apply, LinearMap.domRestrict_apply, LinearEquiv.coe_coe,
  Basis.restrictScalars_apply, LinearMap.coe_restrictScalars]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : NoZeroSMulDivisors R S
b : Basis ι S M
m : ↥(span R (range ⇑b))
i : ι
this :
  mapRange.linearMap (Algebra.linearMap R S) ∘ₗ ↑(restrictScalars R b).repr =
    (↑R ↑b.repr).domRestrict (span R (range ⇑b))
⊢ (algebraMap R S) (((restrictScalars R b).repr m) i) = (b.repr ↑m) i

Tactic:
exact DFunLike.congr_fun (LinearMap.congr_fun this m) i

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : NoZeroSMulDivisors R S
b : Basis ι S M
m : ↥(span R (range ⇑b))
i : ι
⊢ (algebraMap R S) (((restrictScalars R b).repr m) i) = (b.repr ↑m) i

Tactic:
suffices
  Finsupp.mapRange.linearMap (Algebra.linearMap R S) ∘ₗ (b.restrictScalars R).repr.toLinearMap =
    ((b.repr : M →ₗ[S] ι →₀ S).restrictScalars R).domRestrict _
  by exact DFunLike.congr_fun (LinearMap.congr_fun this m) i

Result:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : NoZeroSMulDivisors R S
b : Basis ι S M
m : ↥(span R (range ⇑b))
i : ι
⊢ mapRange.linearMap (Algebra.linearMap R S) ∘ₗ ↑(restrictScalars R b).repr =
    (↑R ↑b.repr).domRestrict (span R (range ⇑b))

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : NoZeroSMulDivisors R S
b : Basis ι S M
m : ↥(span R (range ⇑b))
i : ι
⊢ mapRange.linearMap (Algebra.linearMap R S) ∘ₗ ↑(restrictScalars R b).repr =
    (↑R ↑b.repr).domRestrict (span R (range ⇑b))

Tactic:
refine Basis.ext (b.restrictScalars R) fun _ => ?_

Result:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : NoZeroSMulDivisors R S
b : Basis ι S M
m : ↥(span R (range ⇑b))
i x✝ : ι
⊢ (mapRange.linearMap (Algebra.linearMap R S) ∘ₗ ↑(restrictScalars R b).repr) ((restrictScalars R b) x✝) =
    ((↑R ↑b.repr).domRestrict (span R (range ⇑b))) ((restrictScalars R b) x✝)