awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
Goal:
R : Type u_1
M : Type u_3
M' : Type u_4
N : Type u_5
N' : Type u_6
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : AddCommGroup M'
inst_3 : AddCommGroup N'
inst_4 : CommRing R
inst_5 : Module R M
inst_6 : Module R M'
inst_7 : Module R N
inst_8 : Module R N'
p : M →ₗ[R] N →ₗ[R] R
inst_9 : p.IsPerfPair
eM : M' ≃ₗ[R] M
eN : N' ≃ₗ[R] N
H : (p.compl₁₂ (↑eM : M' →ₗ[R] M) (↑eN : N' →ₗ[R] N)).compl₁₂ (↑eM.symm : M →ₗ[R] M') (↑eN.symm : N →ₗ[R] N') = p
⊢ (p.compl₁₂ (↑eM : M' →ₗ[R] M) (↑eN : N' →ₗ[R] N)).IsPerfPair

Tactic:
infer_instance
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
Goal:
R : Type u_1
M : Type u_3
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : CommRing R
inst_3 : Module R M
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : IsReflexive R N
h : Bijective (α := M) (β := N →ₗ[R] R) (⇑p : (a : M) → N →ₗ[R] R)
⊢ p.IsPerfPair

Tactic:
inferInstanceAs ((LinearMap.id (R := R) (M := Dual R N)).compl₁₂
    (LinearEquiv.ofBijective p h : M →ₗ[R] N →ₗ[R] R)
    (LinearEquiv.refl R N : N →ₗ[R] N)).IsPerfPair

Premises used: _private.0.LinearMap.IsPerfPair.of_bijective._proof_1
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
Goal:
K : Type u_2
M : Type u_3
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : Field K
inst_3 : Module K M
inst_4 : Module K N
p : M →ₗ[K] N →ₗ[K] K
inst_5 : FiniteDimensional K M
h : Injective (α := M) (β := N →ₗ[K] K) (⇑p : (a : M) → N →ₗ[K] K)
h' rwa rwa₁ rwa₂ rwa₃ : Injective (α := N) (β := M →ₗ[K] K) (⇑p.flip : (a : N) → M →ₗ[K] K)
⊢ Surjective (α := M) (β := N →ₗ[K] K) (⇑p : (a : M) → N →ₗ[K] K)

Tactic:
rwa [← p.flip_injective_iff₁]

Premises used: LinearMap.flip_injective_iff₁
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
Goal:
K : Type u_2
M : Type u_3
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : Field K
inst_3 : Module K M
inst_4 : Module K N
p : M →ₗ[K] N →ₗ[K] K
inst_5 : FiniteDimensional K M
h : Injective (α := M) (β := N →ₗ[K] K) (⇑p : (a : M) → N →ₗ[K] K)
h' : Injective (α := N) (β := M →ₗ[K] K) (⇑p.flip : (a : N) → M →ₗ[K] K)
⊢ FiniteDimensional K N

Tactic:
have : FiniteDimensional K N := FiniteDimensional.of_injective p.flip h'
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
Goal:
K : Type u_2
M : Type u_3
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : Field K
inst_3 : Module K M
inst_4 : Module K N
p : M →ₗ[K] N →ₗ[K] K
inst_5 : FiniteDimensional K M
h : Injective (α := M) (β := N →ₗ[K] K) (⇑p : (a : M) → N →ₗ[K] K)
h' : Injective (α := N) (β := M →ₗ[K] K) (⇑p.flip : (a : N) → M →ₗ[K] K)
this : FiniteDimensional K N
rwa : Injective (α := M) (β := N →ₗ[K] K) (⇑p.flip.flip : (a : M) → N →ₗ[K] K)
rwa₁ rwa₂ rwa₃ rwa₄ : Injective (α := M) (β := N →ₗ[K] K) (⇑p : (a : M) → N →ₗ[K] K)
⊢ Surjective (α := N) (β := M →ₗ[K] K) (⇑p.flip : (a : N) → M →ₗ[K] K)

Tactic:
rwa [← p.flip.flip_injective_iff₁, LinearMap.flip_flip]

Premises used: LinearMap.flip_injective_iff₁, LinearMap.flip_flip
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
Goal:
K : Type u_2
M : Type u_3
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : Field K
inst_3 : Module K M
inst_4 : Module K N
p : M →ₗ[K] N →ₗ[K] K
inst_5 : FiniteDimensional K N
h : Injective (α := M) (β := N →ₗ[K] K) (⇑p : (a : M) → N →ₗ[K] K)
h' : Injective (α := N) (β := M →ₗ[K] K) (⇑p.flip : (a : N) → M →ₗ[K] K)
⊢ p.IsPerfPair

Tactic:
.flip <| .of_injective h' h

Premises used: LinearMap.IsPerfPair.of_injective, LinearMap.mk₂'ₛₗ, LinearMap.flip, LinearMap.IsPerfPair.flip
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
U : Submodule R M
V : Submodule R N
⊢ p.flip.IsPerfectCompl V U ↔ p.IsPerfectCompl U V

Tactic:
⟨fun h ↦ h.flip, fun h ↦ h.flip⟩

Premises used: Iff.intro, LinearMap.IsPerfectCompl.flip
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
V : Submodule R N
⊢ p.IsPerfectCompl ⊤ V ↔ V = ⊤

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
V : Submodule R N
refine_1 : ∀ (h : p.IsPerfectCompl ⊤ V), V = ⊤
refine_2 : ∀ (h : V = ⊤), p.IsPerfectCompl ⊤ V
⊢ p.IsPerfectCompl ⊤ V ↔ V = ⊤

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
V : Submodule R N
h : p.IsPerfectCompl ⊤ V
⊢ IsCompl V ⊥

Tactic:
simpa using h.isCompl_right

Premises used: LinearMap.IsPerfectCompl.isCompl_right
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
V : Submodule R N
h : p.IsPerfectCompl ⊤ V
⊢ V = ⊤

Tactic:
exact eq_top_of_isCompl_bot <| by simpa using h.isCompl_right

Premises used: eq_top_of_isCompl_bot
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
V : Submodule R N
h : V = ⊤
refine_2 : p.IsPerfectCompl ⊤ ⊤
⊢ p.IsPerfectCompl ⊤ V

Tactic:
rw [h]
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
V : Submodule R N
h : V = ⊤
⊢ IsCompl ⊤ (Submodule.map (↑p.toPerfPair.symm : Dual R N →ₗ[R] M) (Submodule.dualAnnihilator ⊤))

Tactic:
simpa using isCompl_top_bot

Premises used: isCompl_top_bot
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
V : Submodule R N
h : V = ⊤
⊢ IsCompl ⊤ (Submodule.map (↑p.flip.toPerfPair.symm : Dual R M →ₗ[R] N) (Submodule.dualAnnihilator ⊤))

Tactic:
simpa using isCompl_top_bot

Premises used: isCompl_top_bot
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
V : Submodule R N
h : V = ⊤
⊢ p.IsPerfectCompl ⊤ ⊤

Tactic:
exact
      { isCompl_left := by simpa using isCompl_top_bot
        isCompl_right := by simpa using isCompl_top_bot }
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
U : Submodule R M
rw : p.flip.IsPerfectCompl ⊤ U ↔ U = ⊤
⊢ p.IsPerfectCompl U ⊤ ↔ U = ⊤

Tactic:
rw [← IsPerfectCompl.flip_iff]

Premises used: LinearMap.IsPerfectCompl.flip_iff
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
U : Submodule R M
⊢ p.flip.IsPerfectCompl ⊤ U ↔ U = ⊤

Tactic:
left_top_iff

Premises used: LinearMap.IsPerfectCompl.left_top_iff
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
U : Submodule R M
⊢ p.flip.IsPerfectCompl ⊤ U ↔ U = ⊤

Tactic:
exact left_top_iff

Premises used: LinearMap.IsPerfectCompl.left_top_iff
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
inst_5 : IsReflexive R M
e : N ≃ₗ[R] Dual R M
⊢ (↑e.flip : M →ₗ[R] Dual R N) = (↑e : N →ₗ[R] Dual R M).flip

Tactic:
rfl

Premises used: LinearMap.mk₂'ₛₗ, LinearMap.flip, rfl
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
inst_5 : IsReflexive R M
e : N ≃ₗ[R] Dual R M
m : M
n : N
⊢ Eq.{u_1 + 1} (α := R) ((((e.flip : (a : M) → Dual R N) m : Dual R N) : (a : N) → R) n : R)
    ((((e : (a : N) → Dual R M) n : Dual R M) : (a : M) → R) m : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
inst_5 : IsReflexive R M
e : N ≃ₗ[R] Dual R M
⊢ e.flip.symm = e.symm.dualMap ≪≫ₗ symm (evalEquiv R M)

Tactic:
rfl

Premises used: LinearEquiv.symm, Classical.choose, LinearEquiv.trans, rfl
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
inst_5 : IsReflexive R M
e : N ≃ₗ[R] Dual R M
h :
  ∀ (x : N) (x_1 : Dual R N),
    Eq.{u_1 + 1} (α := R)
      (((((↑(e ≪≫ₗ e.flip.symm.dualMap) : N →ₗ[R] Dual R (Dual R N)) : (a : N) → Dual R (Dual R N)) x :
              Dual R (Dual R N)) :
            (a : Dual R N) → R)
          x_1 :
        R)
      ((((Dual.eval R N : (a : N) → Dual R (Dual R N)) x : Dual R (Dual R N)) : (a : Dual R N) → R) x_1 : R)
⊢ (↑(e ≪≫ₗ e.flip.symm.dualMap) : N →ₗ[R] Dual R (Dual R N)) = Dual.eval R N

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
inst_5 : IsReflexive R M
e : N ≃ₗ[R] Dual R M
x : N
x_1 : Dual R N
⊢ Eq.{u_1 + 1} (α := R)
    (((((↑(e ≪≫ₗ e.flip.symm.dualMap) : N →ₗ[R] Dual R (Dual R N)) : (a : N) → Dual R (Dual R N)) x :
            Dual R (Dual R N)) :
          (a : Dual R N) → R)
        x_1 :
      R)
    ((((Dual.eval R N : (a : N) → Dual R (Dual R N)) x : Dual R (Dual R N)) : (a : Dual R N) → R) x_1 : R)

Tactic:
simp [symm_flip]

Premises used: LinearEquiv.symm_flip
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
inst_5 : IsReflexive R M
e : N ≃ₗ[R] Dual R M
bijective_dual_eval' : Bijective (α := N) (β := Dual R (Dual R N)) (⇑(Dual.eval R N) : (a : N) → Dual R (Dual R N))
⊢ IsReflexive R N

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
inst_5 : IsReflexive R M
e : N ≃ₗ[R] Dual R M
bijective_dual_eval' :
  Bijective (α := N) (β := Dual R (Dual R N))
    (⇑(↑(e ≪≫ₗ e.flip.symm.dualMap) : N →ₗ[R] Dual R (Dual R N)) : (a : N) → Dual R (Dual R N))
⊢ Bijective (α := N) (β := Dual R (Dual R N)) (⇑(Dual.eval R N) : (a : N) → Dual R (Dual R N))

Tactic:
rw [← trans_dualMap_symm_flip e]

Premises used: LinearEquiv.trans_dualMap_symm_flip
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
inst_5 : IsReflexive R M
e : N ≃ₗ[R] Dual R M
⊢ Bijective (α := N) (β := Dual R (Dual R N))
    (⇑(↑(e ≪≫ₗ e.flip.symm.dualMap) : N →ₗ[R] Dual R (Dual R N)) : (a : N) → Dual R (Dual R N))

Tactic:
LinearEquiv.bijective _

Premises used: LinearEquiv.bijective
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
inst_5 : IsReflexive R M
e : N ≃ₗ[R] Dual R M
⊢ Bijective (α := N) (β := Dual R (Dual R N))
    (⇑(↑(e ≪≫ₗ e.flip.symm.dualMap) : N →ₗ[R] Dual R (Dual R N)) : (a : N) → Dual R (Dual R N))

Tactic:
exact LinearEquiv.bijective _

Premises used: LinearEquiv.bijective
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
inst_5 : IsReflexive R M
e : N ≃ₗ[R] Dual R M
h : IsReflexive R N
h₁ :
  ∀ (x : N) (x_1 : M),
    Eq.{u_1 + 1} (α := R) ((((e.flip.flip : (a : N) → Dual R M) x : Dual R M) : (a : M) → R) x_1 : R)
      ((((e : (a : N) → Dual R M) x : Dual R M) : (a : M) → R) x_1 : R)
⊢ e.flip.flip = e

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
inst_5 : IsReflexive R M
e : N ≃ₗ[R] Dual R M
h : IsReflexive R N
x : N
x_1 : M
⊢ Eq.{u_1 + 1} (α := R) ((((e.flip.flip : (a : N) → Dual R M) x : Dual R M) : (a : M) → R) x_1 : R)
    ((((e : (a : N) → Dual R M) x : Dual R M) : (a : M) → R) x_1 : R)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
e : N ≃ₗ[R] Dual R M
p : Submodule R M
h :
  ∀ (x : N),
    x ∈ (map (↑e : N →ₗ[R] Dual R M).flip p).dualCoannihilator ↔ x ∈ map (↑e.symm : Dual R M →ₗ[R] N) p.dualAnnihilator
⊢ (map (↑e : N →ₗ[R] Dual R M).flip p).dualCoannihilator = map (↑e.symm : Dual R M →ₗ[R] N) p.dualAnnihilator

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
e : N ≃ₗ[R] Dual R M
p : Submodule R M
x : N
⊢ x ∈ (map (↑e : N →ₗ[R] Dual R M).flip p).dualCoannihilator ↔ x ∈ map (↑e.symm : Dual R M →ₗ[R] N) p.dualAnnihilator

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
inst_5 : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R N
⊢ IsReflexive R N

Tactic:
have : IsReflexive R N := e.isReflexive_of_equiv_dual_of_isReflexive
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
inst_5 : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R N
this : IsReflexive R N
rw : (map (↑e.flip : M →ₗ[R] Dual R N).flip p).dualCoannihilator = (map (↑e : N →ₗ[R] Dual R M) p).dualCoannihilator
rw₁ : (map (↑e.flip.flip : N →ₗ[R] Dual R M) p).dualCoannihilator = (map (↑e : N →ₗ[R] Dual R M) p).dualCoannihilator
rw₂ rw₃ : (map (↑e : N →ₗ[R] Dual R M) p).dualCoannihilator = (map (↑e : N →ₗ[R] Dual R M) p).dualCoannihilator
⊢ map (↑e.flip.symm : Dual R N →ₗ[R] M) p.dualAnnihilator = (map (↑e : N →ₗ[R] Dual R M) p).dualCoannihilator

Tactic:
rw [← dualCoannihilator_map_linearEquiv_flip, ← LinearEquiv.coe_toLinearMap_flip,
    LinearEquiv.flip_flip]

Premises used: LinearEquiv.coe_toLinearMap_flip, LinearEquiv.isReflexive_of_equiv_dual_of_isReflexive, LinearEquiv.flip_flip, Submodule.dualCoannihilator_map_linearEquiv_flip
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
inst_5 : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R (Dual R M)
⊢ IsReflexive R N

Tactic:
have : IsReflexive R N := e.isReflexive_of_equiv_dual_of_isReflexive
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
inst_5 : IsReflexive R M
e : N ≃ₗ[R] Module.Dual R M
p : Submodule R (Module.Dual R M)
this : IsReflexive R N
Dual :
  map (↑e.flip.symm : Module.Dual R N →ₗ[R] M) (map (↑e.symm : Module.Dual R M →ₗ[R] N) p).dualAnnihilator =
    map (↑e.flip.symm : Module.Dual R N →ₗ[R] M) (map (↑e.flip : M →ₗ[R] Module.Dual R N) p.dualCoannihilator)
⊢ map (↑e : N →ₗ[R] Module.Dual R M).flip p.dualCoannihilator =
    (map (↑e.symm : Module.Dual R M →ₗ[R] N) p).dualAnnihilator

Tactic:
suffices
      (p.map (e.symm : Dual R M →ₗ[R] N)).dualAnnihilator.map (e.flip.symm : Dual R N →ₗ[R] M) =
        (p.dualCoannihilator.map (e.flip : M →ₗ[R] Dual R N)).map (e.flip.symm : Dual R N →ₗ[R] M)
    from (Submodule.map_injective_of_injective e.flip.symm.injective this).symm
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
inst_5 : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R (Dual R M)
this : IsReflexive R N
rw :
  (map ((↑e : N →ₗ[R] Dual R M) ∘ₗ (↑e.symm : Dual R M →ₗ[R] N)) p).dualCoannihilator =
    map ((↑e.flip.symm : Dual R N →ₗ[R] M) ∘ₗ (↑e.flip : M →ₗ[R] Dual R N)) p.dualCoannihilator
⊢ map (↑e.flip.symm : Dual R N →ₗ[R] M) (map (↑e.symm : Dual R M →ₗ[R] N) p).dualAnnihilator =
    map (↑e.flip.symm : Dual R N →ₗ[R] M) (map (↑e.flip : M →ₗ[R] Dual R N) p.dualCoannihilator)

Tactic:
rw [← dualCoannihilator_map_linearEquiv_flip, ← LinearEquiv.coe_toLinearMap_flip,
    LinearEquiv.flip_flip, ← map_comp, ← map_comp]

Premises used: LinearEquiv.coe_toLinearMap_flip, LinearEquiv.isReflexive_of_equiv_dual_of_isReflexive, LinearEquiv.flip_flip, Submodule.dualCoannihilator_map_linearEquiv_flip, Submodule.map_comp
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
inst_5 : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R (Dual R M)
this : IsReflexive R N
⊢ (map ((↑e : N →ₗ[R] Dual R M) ∘ₗ (↑e.symm : Dual R M →ₗ[R] N)) p).dualCoannihilator =
    map ((↑e.flip.symm : Dual R N →ₗ[R] M) ∘ₗ (↑e.flip : M →ₗ[R] Dual R N)) p.dualCoannihilator

Tactic:
simp [-coe_toLinearMap_flip]

Premises used: LinearEquiv.coe_toLinearMap_flip
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
inst_5 : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R (Dual R N)
⊢ IsReflexive R N

Tactic:
have : IsReflexive R N := e.isReflexive_of_equiv_dual_of_isReflexive
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Basic
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
inst_5 : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R (Dual R N)
this : IsReflexive R N
rw : map (↑e.flip : M →ₗ[R] Dual R N).flip p.dualCoannihilator = map (↑e : N →ₗ[R] Dual R M) p.dualCoannihilator
rw₁ : map (↑e.flip.flip : N →ₗ[R] Dual R M) p.dualCoannihilator = map (↑e : N →ₗ[R] Dual R M) p.dualCoannihilator
rw₂ rw₃ : map (↑e : N →ₗ[R] Dual R M) p.dualCoannihilator = map (↑e : N →ₗ[R] Dual R M) p.dualCoannihilator
⊢ (map (↑e.flip.symm : Dual R N →ₗ[R] M) p).dualAnnihilator = map (↑e : N →ₗ[R] Dual R M) p.dualCoannihilator

Tactic:
rw [← map_dualCoannihilator_linearEquiv_flip, ← LinearEquiv.coe_toLinearMap_flip,
    LinearEquiv.flip_flip]

Premises used: LinearEquiv.coe_toLinearMap_flip, LinearEquiv.isReflexive_of_equiv_dual_of_isReflexive, LinearEquiv.flip_flip, Submodule.map_dualCoannihilator_linearEquiv_flip
-- 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
⊢ Bijective (α := M') (β := N' →ₗ[R] R) (⇑(p.compl₁₂ i j) : (a : M') → N' →ₗ[R] R)

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

Premises used: Iff.mpr, LinearMap.ker_eq_bot, And.intro, Iff.mp, Function.Bijective, eq_bot_iff
-- 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
refine_1 : ∀ (m : M') (hm : m ∈ (p.compl₁₂ i j).ker), Membership.mem (γ := Submodule R M') ⊥ m
refine_2 : ∀ (f : N' →ₗ[R] R), ∃ (a : M'), (p.compl₁₂ i j : (a : M') → N' →ₗ[R] R) a = f
⊢ Bijective (α := M') (β := N' →ₗ[R] R) (⇑(p.compl₁₂ i j) : (a : M') → N' →ₗ[R] R)

Tactic:
refine ⟨LinearMap.ker_eq_bot.mp <| eq_bot_iff.mpr fun m hm ↦ ?_, fun f ↦ ?_⟩
-- 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
simp :
  ∃ (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)
⊢ Membership.mem (α := M) (Submodule.map (↑p.toPerfPair.symm : Dual R N →ₗ[R] M) j.range.dualAnnihilator)
    ((i : (a : M') → M) m : M)

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

Premises used: Submodule.mem_dualAnnihilator, Submodule.mem_map