-- 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 : f x = 0
n : N
⊢ (p (i x)) n = 0

Tactic:
have hn : n ∈ span R (LinearMap.range j : Set N) := hN ▸ Submodule.mem_top

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 : f x = 0
n : N
hn : n ∈ span R ↑(LinearMap.range j)
⊢ (p (i x)) n = 0

Proof state:
case mem.intro
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
n' : N'
⊢ (p (i x)) (j n') = 0

Tactic:
simpa [f] using LinearMap.congr_fun hx n'

Result:
no goals

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
⊢ Injective ⇑(PerfectPairing.restrictScalarsAux p i j hp)

Tactic:
rw [← LinearMap.ker_eq_bot]

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
⊢ LinearMap.ker (PerfectPairing.restrictScalarsAux p i j hp) = ⊥