-- 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:
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)

Tactic:
refine ⟨m, ?_⟩

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
⊢ (PerfectPairing.restrictScalarsAux p i j hp) m = g

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

Tactic:
change Algebra.linearMap 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'
⊢ (Algebra.linearMap S R) (((PerfectPairing.restrictScalarsAux p i j hp) m) n) = (algebraMap S R) (g n)

Proof state:
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'
⊢ (Algebra.linearMap S R) (((PerfectPairing.restrictScalarsAux p i j hp) m) n) = (algebraMap S R) (g n)

Tactic:
simpa [restrictScalarsAux] using LinearMap.congr_fun hm 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
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) = ⊤

Tactic:
refine Submodule.eq_top_iff'.mpr fun g : Module.Dual S N' ↦ ?_

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
g : Dual S N'
⊢ g ∈ LinearMap.range (PerfectPairing.restrictScalarsAux p i j hp)