-- 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:
case add
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 x✝ y✝ : N
hx✝ : x✝ ∈ span R ↑(LinearMap.range j)
hy✝ : y✝ ∈ span R ↑(LinearMap.range j)
a✝¹ : (p (i x)) x✝ = 0
a✝ : (p (i x)) y✝ = 0
⊢ (p (i x)) (x✝ + y✝) = 0

Tactic:
rw [← p.toLin_apply, map_add]

Result:
case add
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 x✝ y✝ : N
hx✝ : x✝ ∈ span R ↑(LinearMap.range j)
hy✝ : y✝ ∈ span R ↑(LinearMap.range j)
a✝¹ : (p (i x)) x✝ = 0
a✝ : (p (i x)) y✝ = 0
⊢ (p.toLin (i x)) x✝ + (p.toLin (i x)) y✝ = 0

Proof state:
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

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

Tactic:
induction hn using Submodule.span_induction with
| mem z hz =>
  obtain ⟨n', rfl⟩ := hz
  simpa [f] using LinearMap.congr_fun hx n'
| zero => simp
| add => rw [← p.toLin_apply, map_add]; aesop
| smul => rw [← p.toLin_apply, map_smul]; aesop

Result:
no goals

Proof state:
case zero
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)) 0 = 0

Tactic:
simp

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

Tactic:
let f := LinearMap.restrictScalarsRange i j (Algebra.linearMap S R)
    (FaithfulSMul.algebraMap_injective S R) p.toLin hp

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