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

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)
⊢ Bijective ⇑(p.toLin.compl₁₂ i j)

Tactic:
refine ⟨LinearMap.ker_eq_bot.mp <| eq_bot_iff.mpr fun m hm ↦ ?_, fun f ↦ ?_⟩

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 : m ∈ LinearMap.ker (p.toLin.compl₁₂ i j)
⊢ m ∈ ⊥

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

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)
⊢ i m ∈ Submodule.map p.toDualLeft.symm (LinearMap.range j).dualAnnihilator

Tactic:
simp only [Submodule.mem_map, Submodule.mem_dualAnnihilator]

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

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
⊢ i m ∈ ⊥

Tactic:
simpa only [← hij.isCompl_left.inf_eq_bot, Submodule.mem_inf]
  using ⟨LinearMap.mem_range_self i m, hm⟩

Result:
no goals

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

Tactic:
simpa 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
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 y) (j n) = 0

Tactic:
simp only [Submodule.mem_map, Submodule.mem_dualAnnihilator] at hy

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

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 : m ∈ LinearMap.ker (p.toLin.compl₁₂ i j)
⊢ m ∈ ⊥

Tactic:
replace hm : i m ∈ (LinearMap.range j).dualAnnihilator.map p.toDualLeft.symm := by
  simp only [Submodule.mem_map, Submodule.mem_dualAnnihilator]
  refine ⟨p.toDualLeft (i m), ?_, LinearEquiv.symm_apply_apply _ _⟩
  rintro - ⟨n, rfl⟩
  simpa using LinearMap.congr_fun hm n

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
⊢ m ∈ ⊥