-- Mathlib/LinearAlgebra/PerfectPairing/Restrict.lean
private lemma restrict_aux :
    Bijective (p.toLin.compl₁₂ i j)

Proof state:
case refine_2
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
M' : Type u_4
N' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl (LinearMap.range i) (LinearMap.range j)
f : N' →ₗ[R] R
F : Dual R N :=
  f ∘ₗ LinearMap.linearProjOfIsCompl (Submodule.map p.toDualRight.symm (LinearMap.range i).dualAnnihilator) j hj ⋯
hF :
  F = f ∘ₗ LinearMap.linearProjOfIsCompl (Submodule.map p.toDualRight.symm (LinearMap.range i).dualAnnihilator) j hj ⋯
⊢ ∃ a, (p.toLin.compl₁₂ i j) a = f

Tactic:
have hF (n : N') : F (j n) = f n := by simp [hF]

Result:
case refine_2
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
M' : Type u_4
N' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl (LinearMap.range i) (LinearMap.range j)
f : N' →ₗ[R] R
F : Dual R N :=
  f ∘ₗ LinearMap.linearProjOfIsCompl (Submodule.map p.toDualRight.symm (LinearMap.range i).dualAnnihilator) j hj ⋯
hF✝ :
  F = f ∘ₗ LinearMap.linearProjOfIsCompl (Submodule.map p.toDualRight.symm (LinearMap.range i).dualAnnihilator) j hj ⋯
hF : ∀ (n : N'), F (j n) = f n
⊢ ∃ a, (p.toLin.compl₁₂ i j) a = f

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
M' : Type u_4
N' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl (LinearMap.range i) (LinearMap.range j)
m : M'
hm : i m ∈ Submodule.map p.toDualLeft.symm (LinearMap.range j).dualAnnihilator
this : i m ∈ ⊥
⊢ m ∈ ⊥

Tactic:
simpa [hi] using this

Result:
no goals

Proof state:
case refine_2.intro.intro.intro.intro.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
M' : Type u_4
N' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl (LinearMap.range i) (LinearMap.range j)
f : N' →ₗ[R] R
F : Dual R N :=
  f ∘ₗ LinearMap.linearProjOfIsCompl (Submodule.map p.toDualRight.symm (LinearMap.range i).dualAnnihilator) j hj ⋯
hF✝ :
  F = f ∘ₗ LinearMap.linearProjOfIsCompl (Submodule.map p.toDualRight.symm (LinearMap.range i).dualAnnihilator) j hj ⋯
hF : ∀ (n : N'), F (j n) = f n
m : M := p.toDualLeft.symm F
hm : m = p.toDualLeft.symm F
m₀ : M'
y : M
hy : y ∈ Submodule.map p.toDualLeft.symm (LinearMap.range j).dualAnnihilator
hm' : i m₀ + y = m
n : N'
⊢ ((p.toLin.compl₁₂ i j) m₀) n = f n

Tactic:
replace hy : (p y) (j n) = 0 := by
  simp only [Submodule.mem_map, Submodule.mem_dualAnnihilator] at hy
  obtain ⟨g, hg, rfl⟩ := hy
  simpa only [apply_toDualLeft_symm_apply] using hg _ (LinearMap.mem_range_self j n)

Result:
case refine_2.intro.intro.intro.intro.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
M' : Type u_4
N' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl (LinearMap.range i) (LinearMap.range j)
f : N' →ₗ[R] R
F : Dual R N :=
  f ∘ₗ LinearMap.linearProjOfIsCompl (Submodule.map p.toDualRight.symm (LinearMap.range i).dualAnnihilator) j hj ⋯
hF✝ :
  F = f ∘ₗ LinearMap.linearProjOfIsCompl (Submodule.map p.toDualRight.symm (LinearMap.range i).dualAnnihilator) j hj ⋯
hF : ∀ (n : N'), F (j n) = f n
m : M := p.toDualLeft.symm F
hm : m = p.toDualLeft.symm F
m₀ : M'
y : M
hm' : i m₀ + y = m
n : N'
hy : (p y) (j n) = 0
⊢ ((p.toLin.compl₁₂ i j) m₀) n = f 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
M' : Type u_4
N' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl (LinearMap.range i) (LinearMap.range j)
f : N' →ₗ[R] R
F : Dual R N :=
  f ∘ₗ LinearMap.linearProjOfIsCompl (Submodule.map p.toDualRight.symm (LinearMap.range i).dualAnnihilator) j hj ⋯
hF :
  F = f ∘ₗ LinearMap.linearProjOfIsCompl (Submodule.map p.toDualRight.symm (LinearMap.range i).dualAnnihilator) j hj ⋯
n : N'
⊢ F (j n) = f n

Tactic:
simp [hF]

Result:
no goals

Proof state:
case refine_2.intro.intro.intro.intro.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
M' : Type u_4
N' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl (LinearMap.range i) (LinearMap.range j)
f : N' →ₗ[R] R
F : Dual R N :=
  f ∘ₗ LinearMap.linearProjOfIsCompl (Submodule.map p.toDualRight.symm (LinearMap.range i).dualAnnihilator) j hj ⋯
hF✝ :
  F = f ∘ₗ LinearMap.linearProjOfIsCompl (Submodule.map p.toDualRight.symm (LinearMap.range i).dualAnnihilator) j hj ⋯
hF : ∀ (n : N'), F (j n) = f n
m : M := p.toDualLeft.symm F
hm : m = p.toDualLeft.symm F
m₀ : M'
y : M
hm' : i m₀ + y = m
n : N'
hy : (p y) (j n) = 0
⊢ ((p.toLin.compl₁₂ i j) m₀) n = f n

Tactic:
rw [hm, ← LinearEquiv.symm_apply_eq, map_add, LinearEquiv.symm_symm,
  toDualLeft_apply] at hm'

Result:
case refine_2.intro.intro.intro.intro.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
M' : Type u_4
N' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl (LinearMap.range i) (LinearMap.range j)
f : N' →ₗ[R] R
F : Dual R N :=
  f ∘ₗ LinearMap.linearProjOfIsCompl (Submodule.map p.toDualRight.symm (LinearMap.range i).dualAnnihilator) j hj ⋯
hF✝ :
  F = f ∘ₗ LinearMap.linearProjOfIsCompl (Submodule.map p.toDualRight.symm (LinearMap.range i).dualAnnihilator) j hj ⋯
hF : ∀ (n : N'), F (j n) = f n
m : M := p.toDualLeft.symm F
hm : m = p.toDualLeft.symm F
m₀ : M'
y : M
hm' : p (i m₀) + p.toDualLeft y = F
n : N'
hy : (p y) (j n) = 0
⊢ ((p.toLin.compl₁₂ i j) m₀) n = f n