-- Mathlib/LinearAlgebra/PerfectPairing/Restrict.lean
private lemma restrictScalarsAux_injective
    (hi : Injective i)
    (hN : span R (LinearMap.range j : Set N) = ⊤)
    (hp : ∀ m n, p (i m) (j n) ∈ (algebraMap S R).range) :
    Injective (p.restrictScalarsAux i j hp)

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Module R M
inst✝¹³ : AddCommGroup N
inst✝¹² : Module R N
p : PerfectPairing R M N
S : Type u_4
M' : Type u_5
N' : Type u_6
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra S R
inst✝⁹ : Module S M
inst✝⁸ : Module S N
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S R N
inst✝⁵ : NoZeroSMulDivisors S R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M'
inst✝² : Module S M'
inst✝¹ : AddCommGroup N'
inst✝ : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective ⇑i
hN : span R ↑(LinearMap.range j) = ⊤
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange j (Algebra.linearMap S R) ⋯ p.toLin hp
x : M'
hx : ∀ (n : N), (p (i x)) n = 0
⊢ x = 0

Tactic:
rw [← i.map_eq_zero_iff hi, ← p.toLin.map_eq_zero_iff p.bijectiveLeft.injective]

Result:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Module R M
inst✝¹³ : AddCommGroup N
inst✝¹² : Module R N
p : PerfectPairing R M N
S : Type u_4
M' : Type u_5
N' : Type u_6
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra S R
inst✝⁹ : Module S M
inst✝⁸ : Module S N
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S R N
inst✝⁵ : NoZeroSMulDivisors S R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M'
inst✝² : Module S M'
inst✝¹ : AddCommGroup N'
inst✝ : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective ⇑i
hN : span R ↑(LinearMap.range j) = ⊤
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange j (Algebra.linearMap S R) ⋯ p.toLin hp
x : M'
hx : ∀ (n : N), (p (i x)) n = 0
⊢ p.toLin (i x) = 0

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Module R M
inst✝¹³ : AddCommGroup N
inst✝¹² : Module R N
p : PerfectPairing R M N
S : Type u_4
M' : Type u_5
N' : Type u_6
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra S R
inst✝⁹ : Module S M
inst✝⁸ : Module S N
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S R N
inst✝⁵ : NoZeroSMulDivisors S R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M'
inst✝² : Module S M'
inst✝¹ : AddCommGroup N'
inst✝ : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective ⇑i
hN : span R ↑(LinearMap.range j) = ⊤
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange j (Algebra.linearMap S R) ⋯ p.toLin hp
x : M'
hx : ∀ (n : N), (p (i x)) n = 0
⊢ p.toLin (i x) = 0

Tactic:
ext n

Result:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Module R M
inst✝¹³ : AddCommGroup N
inst✝¹² : Module R N
p : PerfectPairing R M N
S : Type u_4
M' : Type u_5
N' : Type u_6
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra S R
inst✝⁹ : Module S M
inst✝⁸ : Module S N
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S R N
inst✝⁵ : NoZeroSMulDivisors S R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M'
inst✝² : Module S M'
inst✝¹ : AddCommGroup N'
inst✝ : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective ⇑i
hN : span R ↑(LinearMap.range j) = ⊤
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange j (Algebra.linearMap S R) ⋯ p.toLin hp
x : M'
hx : ∀ (n : N), (p (i x)) n = 0
n : N
⊢ (p.toLin (i x)) n = 0 n

Proof state:
case smul
R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Module R M
inst✝¹³ : AddCommGroup N
inst✝¹² : Module R N
p : PerfectPairing R M N
S : Type u_4
M' : Type u_5
N' : Type u_6
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra S R
inst✝⁹ : Module S M
inst✝⁸ : Module S N
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S R N
inst✝⁵ : NoZeroSMulDivisors S R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M'
inst✝² : Module S M'
inst✝¹ : AddCommGroup N'
inst✝ : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective ⇑i
hN : span R ↑(LinearMap.range j) = ⊤
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange j (Algebra.linearMap S R) ⋯ p.toLin hp
x : M'
hx : f x = 0
n : N
a✝¹ : R
x✝ : N
hx✝ : x✝ ∈ span R ↑(LinearMap.range j)
a✝ : (p (i x)) x✝ = 0
⊢ a✝¹ • (p.toLin (i x)) x✝ = 0

Tactic:
aesop

Result:
no goals

Proof state:
case smul
R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Module R M
inst✝¹³ : AddCommGroup N
inst✝¹² : Module R N
p : PerfectPairing R M N
S : Type u_4
M' : Type u_5
N' : Type u_6
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra S R
inst✝⁹ : Module S M
inst✝⁸ : Module S N
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S R N
inst✝⁵ : NoZeroSMulDivisors S R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M'
inst✝² : Module S M'
inst✝¹ : AddCommGroup N'
inst✝ : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective ⇑i
hN : span R ↑(LinearMap.range j) = ⊤
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange j (Algebra.linearMap S R) ⋯ p.toLin hp
x : M'
hx : f x = 0
n : N
a✝¹ : R
x✝ : N
hx✝ : x✝ ∈ span R ↑(LinearMap.range j)
a✝ : (p (i x)) x✝ = 0
⊢ (p (i x)) (a✝¹ • x✝) = 0

Tactic:
rw [← p.toLin_apply, map_smul]

Result:
case smul
R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Module R M
inst✝¹³ : AddCommGroup N
inst✝¹² : Module R N
p : PerfectPairing R M N
S : Type u_4
M' : Type u_5
N' : Type u_6
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra S R
inst✝⁹ : Module S M
inst✝⁸ : Module S N
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S R N
inst✝⁵ : NoZeroSMulDivisors S R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M'
inst✝² : Module S M'
inst✝¹ : AddCommGroup N'
inst✝ : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective ⇑i
hN : span R ↑(LinearMap.range j) = ⊤
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange j (Algebra.linearMap S R) ⋯ p.toLin hp
x : M'
hx : f x = 0
n : N
a✝¹ : R
x✝ : N
hx✝ : x✝ ∈ span R ↑(LinearMap.range j)
a✝ : (p (i x)) x✝ = 0
⊢ a✝¹ • (p.toLin (i x)) x✝ = 0