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

Proof state:
case refine_1
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
⊢ m ∈ ⊥

Tactic:
suffices i m ∈ (⊥ : Submodule R M) by simpa [hi] using this

Result:
case refine_1
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
⊢ i m ∈ ⊥

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 : m ∈ LinearMap.ker (p.toLin.compl₁₂ i j)
⊢ ∃ y, (∀ w ∈ LinearMap.range j, y w = 0) ∧ p.toDualLeft.symm y = i m

Tactic:
refine ⟨p.toDualLeft (i m), ?_, LinearEquiv.symm_apply_apply _ _⟩

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
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 : m ∈ LinearMap.ker (p.toLin.compl₁₂ i j)
⊢ ∀ w ∈ LinearMap.range j, (p.toDualLeft (i m)) w = 0

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 ⋯
hF : ∀ (n : N'), F (j n) = f n
m : M := p.toDualLeft.symm F
hm : m = p.toDualLeft.symm F
⊢ ∃ a, (p.toLin.compl₁₂ i j) a = f

Tactic:
obtain ⟨-, ⟨m₀, rfl⟩, y, hy, hm'⟩ :=
  Submodule.exists_add_eq_of_codisjoint hij.isCompl_left.codisjoint m

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
hy : y ∈ Submodule.map p.toDualLeft.symm (LinearMap.range j).dualAnnihilator
hm' : i m₀ + y = m
⊢ ∃ a, (p.toLin.compl₁₂ i j) a = f

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
⊢ ∃ a, (p.toLin.compl₁₂ i j) a = f

Tactic:
set F : Module.Dual R N := f ∘ₗ j.linearProjOfIsCompl _ hj hij.isCompl_right with 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 ⋯
⊢ ∃ a, (p.toLin.compl₁₂ i j) a = f

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
⊢ ∃ a, (p.toLin.compl₁₂ i j) a = f

Tactic:
refine ⟨m₀, LinearMap.ext fun 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
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