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

Proof state:
case 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'
n : N'
g : Dual R N
hg : ∀ w ∈ LinearMap.range j, g w = 0
hm' : i m₀ + p.toDualLeft.symm g = m
⊢ (p (p.toDualLeft.symm g)) (j n) = 0

Tactic:
simpa only [apply_toDualLeft_symm_apply] using hg _ (LinearMap.mem_range_self j 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
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 : ∃ y_1, (∀ w ∈ LinearMap.range j, y_1 w = 0) ∧ p.toDualLeft.symm y_1 = y
⊢ (p y) (j n) = 0

Tactic:
obtain ⟨g, hg, rfl⟩ := hy

Result:
case 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'
n : N'
g : Dual R N
hg : ∀ w ∈ LinearMap.range j, g w = 0
hm' : i m₀ + p.toDualLeft.symm g = m
⊢ (p (p.toDualLeft.symm g)) (j n) = 0

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

Tactic:
rintro - ⟨n, rfl⟩

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
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)
n : N'
⊢ (p.toDualLeft (i m)) (j n) = 0

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' : p (i m₀) + p.toDualLeft y = F
n : N'
hy : (p y) (j n) = 0
⊢ ((p.toLin.compl₁₂ i j) m₀) n = f n

Tactic:
simpa [← hF, ← LinearMap.congr_fun hm' (j n)]

Result:
no goals

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

Tactic:
set m : M := p.toDualLeft.symm F with hm

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