-- Mathlib/LinearAlgebra/PerfectPairing/Restrict.lean
private lemma restrictScalarsAux_surjective
    (h : ∀ g : Module.Dual S N', ∃ m,
      (p.toDualLeft (i m)).restrictScalars S ∘ₗ j = Algebra.linearMap S R ∘ₗ g)
    (hp : ∀ m n, p (i m) (j n) ∈ (algebraMap S R).range) :
    Surjective (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
h : ∀ (g : Dual S N'), ∃ m, ↑S (p.toDualLeft (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
g : Dual S N'
⊢ g ∈ LinearMap.range (PerfectPairing.restrictScalarsAux p i j hp)

Tactic:
obtain ⟨m, hm⟩ := h g

Result:
case 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
h : ∀ (g : Dual S N'), ∃ m, ↑S (p.toDualLeft (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
g : Dual S N'
m : M'
hm : ↑S (p.toDualLeft (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g
⊢ g ∈ LinearMap.range (PerfectPairing.restrictScalarsAux p i j hp)

Proof state:
case intro.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
h : ∀ (g : Dual S N'), ∃ m, ↑S (p.toDualLeft (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
g : Dual S N'
m : M'
hm : ↑S (p.toDualLeft (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g
n : N'
⊢ ((PerfectPairing.restrictScalarsAux p i j hp) m) n = g n

Tactic:
apply FaithfulSMul.algebraMap_injective S R

Result:
case intro.h.a
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
h : ∀ (g : Dual S N'), ∃ m, ↑S (p.toDualLeft (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
g : Dual S N'
m : M'
hm : ↑S (p.toDualLeft (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g
n : N'
⊢ (algebraMap S R) (((PerfectPairing.restrictScalarsAux p i j hp) m) n) = (algebraMap S R) (g n)

Proof state:
case 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
h : ∀ (g : Dual S N'), ∃ m, ↑S (p.toDualLeft (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
g : Dual S N'
m : M'
hm : ↑S (p.toDualLeft (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g
⊢ (PerfectPairing.restrictScalarsAux p i j hp) m = g

Tactic:
ext n

Result:
case intro.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
h : ∀ (g : Dual S N'), ∃ m, ↑S (p.toDualLeft (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
g : Dual S N'
m : M'
hm : ↑S (p.toDualLeft (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g
n : N'
⊢ ((PerfectPairing.restrictScalarsAux p i j hp) m) n = g n

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
h : ∀ (g : Dual S N'), ∃ m, ↑S (p.toDualLeft (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
⊢ Surjective ⇑(PerfectPairing.restrictScalarsAux p i j hp)

Tactic:
rw [← LinearMap.range_eq_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
h : ∀ (g : Dual S N'), ∃ m, ↑S (p.toDualLeft (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
⊢ LinearMap.range (PerfectPairing.restrictScalarsAux p i j hp) = ⊤