-- Mathlib/LinearAlgebra/LinearIndependent/Basic.lean
theorem LinearIndependent.restrict_scalars [Semiring K] [SMulWithZero R K] [Module K M]
    [IsScalarTower R K M] (hinj : Injective fun r : R ↦ r • (1 : K))
    (li : LinearIndependent K v) : LinearIndependent R v

Proof state:
ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r => r • 1
li : LinearIndependent K v
x y : ι →₀ R
hxy : (Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) y
f : R → K := fun r => r • 1
⊢ x = y

Tactic:
have := @li (x.mapRange f (by simp [f])) (y.mapRange f (by simp [f])) ?_

Result:
case refine_2
ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r => r • 1
li : LinearIndependent K v
x y : ι →₀ R
hxy : (Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) y
f : R → K := fun r => r • 1
this : Finsupp.mapRange f ⋯ x = Finsupp.mapRange f ⋯ y
⊢ x = y

case refine_1
ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r => r • 1
li : LinearIndependent K v
x y : ι →₀ R
hxy : (Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) y
f : R → K := fun r => r • 1
⊢ (Finsupp.linearCombination K v) (Finsupp.mapRange f ⋯ x) = (Finsupp.linearCombination K v) (Finsupp.mapRange f ⋯ y)

Proof state:
case refine_1
ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r => r • 1
li : LinearIndependent K v
x y : ι →₀ R
hxy : (Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) y
f : R → K := fun r => r • 1
⊢ (Finsupp.linearCombination K v) (Finsupp.mapRange f ⋯ x) = (Finsupp.linearCombination K v) (Finsupp.mapRange f ⋯ y)

Tactic:
simpa [Finsupp.linearCombination, f, Finsupp.sum_mapRange_index]

Result:
no goals

Proof state:
case refine_2
ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r => r • 1
li : LinearIndependent K v
x y : ι →₀ R
hxy : (Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) y
f : R → K := fun r => r • 1
this : Finsupp.mapRange f ⋯ x = Finsupp.mapRange f ⋯ y
⊢ x = y

Tactic:
ext i

Result:
case refine_2.h
ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r => r • 1
li : LinearIndependent K v
x y : ι →₀ R
hxy : (Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) y
f : R → K := fun r => r • 1
this : Finsupp.mapRange f ⋯ x = Finsupp.mapRange f ⋯ y
i : ι
⊢ x i = y i

Proof state:
case refine_2.h
ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r => r • 1
li : LinearIndependent K v
x y : ι →₀ R
hxy : (Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) y
f : R → K := fun r => r • 1
this : Finsupp.mapRange f ⋯ x = Finsupp.mapRange f ⋯ y
i : ι
⊢ x i = y i

Tactic:
exact hinj congr($this i)

Result:
no goals

Proof state:
ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r => r • 1
li : LinearIndependent K v
⊢ LinearIndependent R v

Tactic:
intro x y hxy

Result:
ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r => r • 1
li : LinearIndependent K v
x y : ι →₀ R
hxy : (Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) y
⊢ x = y

Proof state:
ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r => r • 1
li : LinearIndependent K v
x y : ι →₀ R
hxy : (Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) y
f : R → K := fun r => r • 1
⊢ f 0 = 0

Tactic:
simp [f]

Result:
no goals

Proof state:
ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r => r • 1
li : LinearIndependent K v
x y : ι →₀ R
hxy : (Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) y
⊢ x = y

Tactic:
let f := fun r : R => r • (1 : K)

Result:
ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r => r • 1
li : LinearIndependent K v
x y : ι →₀ R
hxy : (Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) y
f : R → K := fun r => r • 1
⊢ x = y