awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst_6 : AddCommGroup M'
inst_7 : Module R M'
inst_8 : AddCommGroup N'
inst_9 : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective.{u_4 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hj : Injective.{u_5 + 1, u_3 + 1} (α := N') (β := N) (⇑j : (a : N') → N)
hij : p.IsPerfectCompl i.range j.range
m : M'
hm : m ∈ (p.compl₁₂ i j).ker
⊢ ∃ (y : Dual R N),
    (∀ w ∈ j.range, Eq.{u_1 + 1} (α := R) ((y : (a : N) → R) w : R) (0 : R)) ∧
      Eq.{u_2 + 1} (α := M) (((↑p.toPerfPair.symm : Dual R N →ₗ[R] M) : (a : Dual R N) → M) y : M)
        ((i : (a : M') → M) m : M)

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

Premises used: LinearEquiv.symm_apply_apply, LinearMap.toPerfPair, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst_6 : AddCommGroup M'
inst_7 : Module R M'
inst_8 : AddCommGroup N'
inst_9 : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective.{u_4 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hj : Injective.{u_5 + 1, u_3 + 1} (α := N') (β := N) (⇑j : (a : N') → N)
hij : p.IsPerfectCompl i.range j.range
m : M'
hm : m ∈ (p.compl₁₂ i j).ker
refine :
  ∀ w ∈ j.range,
    Eq.{u_1 + 1} (α := R)
      ((((p.toPerfPair : (a : M) → Dual R N) ((i : (a : M') → M) m) : Dual R N) : (a : N) → R) w : R) (0 : R)
⊢ ∃ (y : Dual R N),
    (∀ w ∈ j.range, Eq.{u_1 + 1} (α := R) ((y : (a : N) → R) w : R) (0 : R)) ∧
      Eq.{u_2 + 1} (α := M) (((↑p.toPerfPair.symm : Dual R N →ₗ[R] M) : (a : Dual R N) → M) y : M)
        ((i : (a : M') → M) m : M)

Tactic:
refine ⟨p.toPerfPair (i m), ?_, LinearEquiv.symm_apply_apply _ _⟩
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst_6 : AddCommGroup M'
inst_7 : Module R M'
inst_8 : AddCommGroup N'
inst_9 : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective.{u_4 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hj : Injective.{u_5 + 1, u_3 + 1} (α := N') (β := N) (⇑j : (a : N') → N)
hij : p.IsPerfectCompl i.range j.range
m : M'
hm : m ∈ (p.compl₁₂ i j).ker
n : N'
⊢ Eq.{u_1 + 1} (α := R)
    ((((p.toPerfPair : (a : M) → Dual R N) ((i : (a : M') → M) m) : Dual R N) : (a : N) → R)
        ((j : (a : N') → N) n : N) :
      R)
    (0 : R)

Tactic:
simpa using LinearMap.congr_fun hm n

Premises used: LinearMap.congr_fun
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst_6 : AddCommGroup M'
inst_7 : Module R M'
inst_8 : AddCommGroup N'
inst_9 : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective.{u_4 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hj : Injective.{u_5 + 1, u_3 + 1} (α := N') (β := N) (⇑j : (a : N') → N)
hij : p.IsPerfectCompl i.range j.range
m : M'
hm : m ∈ (p.compl₁₂ i j).ker
⊢ Membership.mem (α := M) (Submodule.map (↑p.toPerfPair.symm : Dual R N →ₗ[R] M) j.range.dualAnnihilator)
    ((i : (a : M') → M) m : M)

Tactic:
replace hm : i m ∈ j.range.dualAnnihilator.map (p.toPerfPair.symm : Dual R N →ₗ[R] M) := by
      simp only [Submodule.mem_map, Submodule.mem_dualAnnihilator]
      refine ⟨p.toPerfPair (i m), ?_, LinearEquiv.symm_apply_apply _ _⟩
      rintro - ⟨n, rfl⟩
      simpa using LinearMap.congr_fun hm n
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst_6 : AddCommGroup M'
inst_7 : Module R M'
inst_8 : AddCommGroup N'
inst_9 : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective.{u_4 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hj : Injective.{u_5 + 1, u_3 + 1} (α := N') (β := N) (⇑j : (a : N') → N)
hij : p.IsPerfectCompl i.range j.range
m : M'
hm :
  Membership.mem (α := M) (Submodule.map (↑p.toPerfPair.symm : Dual R N →ₗ[R] M) j.range.dualAnnihilator)
    ((i : (a : M') → M) m : M)
this : Membership.mem.{u_2, u_2} (α := M) (γ := Submodule R M) ⊥ ((i : (a : M') → M) m : M)
⊢ Membership.mem (γ := Submodule R M') ⊥ m

Tactic:
simpa [hi] using this
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst_6 : AddCommGroup M'
inst_7 : Module R M'
inst_8 : AddCommGroup N'
inst_9 : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective.{u_4 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hj : Injective.{u_5 + 1, u_3 + 1} (α := N') (β := N) (⇑j : (a : N') → N)
hij : p.IsPerfectCompl i.range j.range
m : M'
hm :
  Membership.mem (α := M) (Submodule.map (↑p.toPerfPair.symm : Dual R N →ₗ[R] M) j.range.dualAnnihilator)
    ((i : (a : M') → M) m : M)
refine_1 : Membership.mem.{u_2, u_2} (α := M) (γ := Submodule R M) ⊥ ((i : (a : M') → M) m : M)
⊢ Membership.mem (γ := Submodule R M') ⊥ m

Tactic:
suffices i m ∈ (⊥ : Submodule R M) by simpa [hi] using this
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst_6 : AddCommGroup M'
inst_7 : Module R M'
inst_8 : AddCommGroup N'
inst_9 : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective.{u_4 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hj : Injective.{u_5 + 1, u_3 + 1} (α := N') (β := N) (⇑j : (a : N') → N)
hij : p.IsPerfectCompl i.range j.range
m : M'
hm :
  Membership.mem (α := M) (Submodule.map (↑p.toPerfPair.symm : Dual R N →ₗ[R] M) j.range.dualAnnihilator)
    ((i : (a : M') → M) m : M)
⊢ Membership.mem.{u_2, u_2} (α := M) (γ := Submodule R M) ⊥ ((i : (a : M') → M) m : M)

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

Premises used: Submodule.mem_inf, IsCompl.inf_eq_bot, LinearMap.IsPerfectCompl.isCompl_left
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst_6 : AddCommGroup M'
inst_7 : Module R M'
inst_8 : AddCommGroup N'
inst_9 : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective.{u_4 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hj : Injective.{u_5 + 1, u_3 + 1} (α := N') (β := N) (⇑j : (a : N') → N)
hij : p.IsPerfectCompl i.range j.range
f : N' →ₗ[R] R
⊢ let F :=
    f ∘ₗ
      linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj ⋯;
  F =
    f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj ⋯

Tactic:
set F : Module.Dual R N := f ∘ₗ j.linearProjOfIsCompl _ hj hij.isCompl_right with hF

Premises used: LinearMap.IsPerfectCompl.isCompl_right, LinearMap.linearProjOfIsCompl, Module.Dual
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst_6 : AddCommGroup M'
inst_7 : Module R M'
inst_8 : AddCommGroup N'
inst_9 : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective.{u_4 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hj : Injective.{u_5 + 1, u_3 + 1} (α := N') (β := N) (⇑j : (a : N') → N)
hij : p.IsPerfectCompl i.range j.range
f : N' →ₗ[R] R
F : Dual R N :=
  f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj ⋯
hF :
  F =
    f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj ⋯
n : N'
⊢ Eq.{u_1 + 1} (α := R) ((F : (a : N) → R) ((j : (a : N') → N) n : N) : R) ((f : (a : N') → R) n : R)

Tactic:
simp [hF]
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst_6 : AddCommGroup M'
inst_7 : Module R M'
inst_8 : AddCommGroup N'
inst_9 : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective.{u_4 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hj : Injective.{u_5 + 1, u_3 + 1} (α := N') (β := N) (⇑j : (a : N') → N)
hij : p.IsPerfectCompl i.range j.range
f : N' →ₗ[R] R
F : Dual R N :=
  f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj ⋯
hF :
  F =
    f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj ⋯
⊢ ∀ (n : N'), Eq.{u_1 + 1} (α := R) ((F : (a : N) → R) ((j : (a : N') → N) n : N) : R) ((f : (a : N') → R) n : R)

Tactic:
have hF (n : N') : F (j n) = f n := by simp [hF]
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst_6 : AddCommGroup M'
inst_7 : Module R M'
inst_8 : AddCommGroup N'
inst_9 : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective.{u_4 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hj : Injective.{u_5 + 1, u_3 + 1} (α := N') (β := N) (⇑j : (a : N') → N)
hij : p.IsPerfectCompl i.range j.range
f : N' →ₗ[R] R
F : Dual R N :=
  f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj ⋯
hF_1 :
  F =
    f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj ⋯
hF : ∀ (n : N'), Eq.{u_1 + 1} (α := R) ((F : (a : N) → R) ((j : (a : N') → N) n : N) : R) ((f : (a : N') → R) n : R)
⊢ let m : M := (p.toPerfPair.symm : (a : Dual R N) → M) F;
  m = (p.toPerfPair.symm : (a : Dual R N) → M) F

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

Premises used: LinearEquiv.symm, LinearMap.toPerfPair, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst_6 : AddCommGroup M'
inst_7 : Module R M'
inst_8 : AddCommGroup N'
inst_9 : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective.{u_4 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hj : Injective.{u_5 + 1, u_3 + 1} (α := N') (β := N) (⇑j : (a : N') → N)
hij : p.IsPerfectCompl i.range j.range
f : N' →ₗ[R] R
F : Dual R N :=
  f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj ⋯
hF_1 :
  F =
    f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj ⋯
hF : ∀ (n : N'), Eq.{u_1 + 1} (α := R) ((F : (a : N) → R) ((j : (a : N') → N) n : N) : R) ((f : (a : N') → R) n : R)
m : M := (p.toPerfPair.symm : (a : Dual R N) → M) F
hm : m = (p.toPerfPair.symm : (a : Dual R N) → M) F
refine_2 :
  ∀ (y : M) (m₀ : M') (hy : y ∈ Submodule.map (↑p.toPerfPair.symm : Dual R N →ₗ[R] M) j.range.dualAnnihilator)
    (hm' : HAdd.hAdd (α := M) ((i : (a : M') → M) m₀ : M) y = m),
    ∃ (a : M'), (p.compl₁₂ i j : (a : M') → N' →ₗ[R] R) a = f
⊢ ∃ (a : M'), (p.compl₁₂ i j : (a : M') → N' →ₗ[R] R) a = f

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

Premises used: Submodule.codisjoint_iff_exists_add_eq, Iff.mp, IsCompl.codisjoint, LinearMap.IsPerfectCompl.isCompl_left, rfl
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst_6 : AddCommGroup M'
inst_7 : Module R M'
inst_8 : AddCommGroup N'
inst_9 : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective.{u_4 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hj : Injective.{u_5 + 1, u_3 + 1} (α := N') (β := N) (⇑j : (a : N') → N)
hij : p.IsPerfectCompl i.range j.range
f : N' →ₗ[R] R
F : Dual R N :=
  f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj ⋯
hF_1 :
  F =
    f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj ⋯
hF : ∀ (n : N'), Eq.{u_1 + 1} (α := R) ((F : (a : N) → R) ((j : (a : N') → N) n : N) : R) ((f : (a : N') → R) n : R)
m : M := (p.toPerfPair.symm : (a : Dual R N) → M) F
hm : m = (p.toPerfPair.symm : (a : Dual R N) → M) F
y : M
m₀ : M'
hy : y ∈ Submodule.map (↑p.toPerfPair.symm : Dual R N →ₗ[R] M) j.range.dualAnnihilator
hm' : HAdd.hAdd (α := M) ((i : (a : M') → M) m₀ : M) y = m
⊢ ∃ (a : M'), (p.compl₁₂ i j : (a : M') → N' →ₗ[R] R) a = f

Tactic:
⟨m₀, LinearMap.ext fun n ↦ ?_⟩

Premises used: LinearMap.ext, Exists.intro
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst_6 : AddCommGroup M'
inst_7 : Module R M'
inst_8 : AddCommGroup N'
inst_9 : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective.{u_4 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hj : Injective.{u_5 + 1, u_3 + 1} (α := N') (β := N) (⇑j : (a : N') → N)
hij : p.IsPerfectCompl i.range j.range
f : N' →ₗ[R] R
F : Dual R N :=
  f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj ⋯
hF_1 :
  F =
    f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj ⋯
hF : ∀ (n : N'), Eq.{u_1 + 1} (α := R) ((F : (a : N) → R) ((j : (a : N') → N) n : N) : R) ((f : (a : N') → R) n : R)
m : M := (p.toPerfPair.symm : (a : Dual R N) → M) F
hm : m = (p.toPerfPair.symm : (a : Dual R N) → M) F
y : M
m₀ : M'
hy : y ∈ Submodule.map (↑p.toPerfPair.symm : Dual R N →ₗ[R] M) j.range.dualAnnihilator
hm' : HAdd.hAdd (α := M) ((i : (a : M') → M) m₀ : M) y = m
refine_2 :
  ∀ (n : N'),
    Eq.{u_1 + 1} (α := R) ((((p.compl₁₂ i j : (a : M') → N' →ₗ[R] R) m₀ : N' →ₗ[R] R) : (a : N') → R) n : R)
      ((f : (a : N') → R) n : R)
⊢ ∃ (a : M'), (p.compl₁₂ i j : (a : M') → N' →ₗ[R] R) a = f

Tactic:
refine ⟨m₀, LinearMap.ext fun n ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst_6 : AddCommGroup M'
inst_7 : Module R M'
inst_8 : AddCommGroup N'
inst_9 : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective.{u_4 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hj : Injective.{u_5 + 1, u_3 + 1} (α := N') (β := N) (⇑j : (a : N') → N)
hij : p.IsPerfectCompl i.range j.range
f : N' →ₗ[R] R
F : Dual R N :=
  f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj ⋯
hF_1 :
  F =
    f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj ⋯
hF : ∀ (n : N'), Eq.{u_1 + 1} (α := R) ((F : (a : N) → R) ((j : (a : N') → N) n : N) : R) ((f : (a : N') → R) n : R)
m : M := (p.toPerfPair.symm : (a : Dual R N) → M) F
hm : m = (p.toPerfPair.symm : (a : Dual R N) → M) F
y : M
m₀ : M'
hy : y ∈ Submodule.map (↑p.toPerfPair.symm : Dual R N →ₗ[R] M) j.range.dualAnnihilator
hm' : HAdd.hAdd (α := M) ((i : (a : M') → M) m₀ : M) y = m
n : N'
⊢ ∃ (y_1 : Dual R N),
    (∀ w ∈ j.range, Eq.{u_1 + 1} (α := R) ((y_1 : (a : N) → R) w : R) (0 : R)) ∧
      ((↑p.toPerfPair.symm : Dual R N →ₗ[R] M) : (a : Dual R N) → M) y_1 = y

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

Premises used: Submodule.mem_dualAnnihilator, Submodule.mem_map
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst_6 : AddCommGroup M'
inst_7 : Module R M'
inst_8 : AddCommGroup N'
inst_9 : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective.{u_4 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hj : Injective.{u_5 + 1, u_3 + 1} (α := N') (β := N) (⇑j : (a : N') → N)
hij : p.IsPerfectCompl i.range j.range
f : N' →ₗ[R] R
F : Dual R N :=
  f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj ⋯
hF_1 :
  F =
    f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj ⋯
hF : ∀ (n : N'), Eq.{u_1 + 1} (α := R) ((F : (a : N) → R) ((j : (a : N') → N) n : N) : R) ((f : (a : N') → R) n : R)
m : M := (p.toPerfPair.symm : (a : Dual R N) → M) F
hm : m = (p.toPerfPair.symm : (a : Dual R N) → M) F
y : M
m₀ : M'
hm' : HAdd.hAdd (α := M) ((i : (a : M') → M) m₀ : M) y = m
n : N'
hy :
  ∃ (y_1 : Dual R N),
    (∀ w ∈ j.range, Eq.{u_1 + 1} (α := R) ((y_1 : (a : N) → R) w : R) (0 : R)) ∧
      ((↑p.toPerfPair.symm : Dual R N →ₗ[R] M) : (a : Dual R N) → M) y_1 = y
obtain :
  ∀ (g : Dual R N) (hg : ∀ w ∈ j.range, Eq.{u_1 + 1} (α := R) ((g : (a : N) → R) w : R) (0 : R))
    (hm' :
      HAdd.hAdd (α := M) (β := M) ((i : (a : M') → M) m₀ : M)
          (((↑p.toPerfPair.symm : Dual R N →ₗ[R] M) : (a : Dual R N) → M) g : M) =
        m),
    Eq.{u_1 + 1} (α := R)
      ((((p : (a : M) → N →ₗ[R] R) (((↑p.toPerfPair.symm : Dual R N →ₗ[R] M) : (a : Dual R N) → M) g) : N →ₗ[R] R) :
            (a : N) → R)
          ((j : (a : N') → N) n : N) :
        R)
      (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
    (0 : R)

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

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst_6 : AddCommGroup M'
inst_7 : Module R M'
inst_8 : AddCommGroup N'
inst_9 : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective.{u_4 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hj : Injective.{u_5 + 1, u_3 + 1} (α := N') (β := N) (⇑j : (a : N') → N)
hij : p.IsPerfectCompl i.range j.range
f : N' →ₗ[R] R
F : Dual R N :=
  f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj ⋯
hF_1 :
  F =
    f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj ⋯
hF : ∀ (n : N'), Eq.{u_1 + 1} (α := R) ((F : (a : N) → R) ((j : (a : N') → N) n : N) : R) ((f : (a : N') → R) n : R)
m : M := (p.toPerfPair.symm : (a : Dual R N) → M) F
hm : m = (p.toPerfPair.symm : (a : Dual R N) → M) F
m₀ : M'
n : N'
g : Dual R N
hg : ∀ w ∈ j.range, Eq.{u_1 + 1} (α := R) ((g : (a : N) → R) w : R) (0 : R)
hm' :
  HAdd.hAdd (α := M) (β := M) ((i : (a : M') → M) m₀ : M)
      (((↑p.toPerfPair.symm : Dual R N →ₗ[R] M) : (a : Dual R N) → M) g : M) =
    m
⊢ Eq.{u_1 + 1} (α := R)
    ((((p : (a : M) → N →ₗ[R] R) (((↑p.toPerfPair.symm : Dual R N →ₗ[R] M) : (a : Dual R N) → M) g) : N →ₗ[R] R) :
          (a : N) → R)
        ((j : (a : N') → N) n : N) :
      R)
    (0 : R)

Tactic:
simpa using hg _ (LinearMap.mem_range_self j n)

Premises used: LinearMap.mem_range_self
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst_6 : AddCommGroup M'
inst_7 : Module R M'
inst_8 : AddCommGroup N'
inst_9 : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective.{u_4 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hj : Injective.{u_5 + 1, u_3 + 1} (α := N') (β := N) (⇑j : (a : N') → N)
hij : p.IsPerfectCompl i.range j.range
f : N' →ₗ[R] R
F : Dual R N :=
  f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj ⋯
hF_1 :
  F =
    f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) i.range.dualAnnihilator) j hj ⋯
hF : ∀ (n : N'), Eq.{u_1 + 1} (α := R) ((F : (a : N) → R) ((j : (a : N') → N) n : N) : R) ((f : (a : N') → R) n : R)
m : M := (p.toPerfPair.symm : (a : Dual R N) → M) F
hm : m = (p.toPerfPair.symm : (a : Dual R N) → M) F
y : M
m₀ : M'
hy : y ∈ Submodule.map (↑p.toPerfPair.symm : Dual R N →ₗ[R] M) j.range.dualAnnihilator
hm' : HAdd.hAdd (α := M) ((i : (a : M') → M) m₀ : M) y = m
n : N'
⊢ Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) y : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
    (0 : R)

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 using hg _ (LinearMap.mem_range_self j n)