awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
W : Submodule R M
w : M
hw : w ∈ W
φ : Dual R M
hφ : φ ∈ W.dualAnnihilator
⊢ Eq.{u_1 + 1} (α := R)
    ((((W.dualAnnihilator.subtype.flip : (a : M) → ↥W.dualAnnihilator →ₗ[R] R) w : ↥W.dualAnnihilator →ₗ[R] R) :
          (a : ↥W.dualAnnihilator) → R)
        (Subtype.mk (p := fun (x : Dual R M) ↦ x ∈ W.dualAnnihilator) φ hφ) :
      R)
    ((0 : (a : ↥W.dualAnnihilator) → R) (Subtype.mk (p := fun (x : Dual R M) ↦ x ∈ W.dualAnnihilator) φ hφ) : R)

Tactic:
(mem_dualAnnihilator φ).mp hφ w hw

Premises used: Submodule.mem_dualAnnihilator, Iff.mp
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
W : Submodule R M
w : M
hw : w ∈ W
φ : Dual R M
hφ : φ ∈ W.dualAnnihilator
⊢ Eq.{u_1 + 1} (α := R)
    ((((W.dualAnnihilator.subtype.flip : (a : M) → ↥W.dualAnnihilator →ₗ[R] R) w : ↥W.dualAnnihilator →ₗ[R] R) :
          (a : ↥W.dualAnnihilator) → R)
        (Subtype.mk (p := fun (x : Dual R M) ↦ x ∈ W.dualAnnihilator) φ hφ) :
      R)
    ((0 : (a : ↥W.dualAnnihilator) → R) (Subtype.mk (p := fun (x : Dual R M) ↦ x ∈ W.dualAnnihilator) φ hφ) : R)

Tactic:
exact (mem_dualAnnihilator φ).mp hφ w hw

Premises used: Submodule.mem_dualAnnihilator, Iff.mp
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
W : Submodule R M
φ ψ : ↥W.dualAnnihilator
h :
  Eq (α := (a : M) → R) ((fun (φ : ↥W.dualAnnihilator) ↦ ((⇑(↑φ : Dual R M) : (a : M) → R) : (a : M) → R)) φ)
    ((fun (φ : ↥W.dualAnnihilator) ↦ ((⇑(↑φ : Dual R M) : (a : M) → R) : (a : M) → R)) ψ)
a : ∀ (x : M), Eq.{u_1 + 1} (α := R) (((↑φ : Dual R M) : (a : M) → R) x : R) (((↑ψ : Dual R M) : (a : M) → R) x : R)
⊢ φ = ψ

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
W : Submodule R M
φ ψ : ↥W.dualAnnihilator
h :
  Eq (α := (a : M) → R) ((fun (φ : ↥W.dualAnnihilator) ↦ ((⇑(↑φ : Dual R M) : (a : M) → R) : (a : M) → R)) φ)
    ((fun (φ : ↥W.dualAnnihilator) ↦ ((⇑(↑φ : Dual R M) : (a : M) → R) : (a : M) → R)) ψ)
x : M
⊢ ∀ (x : M), Eq.{u_1 + 1} (α := R) (((↑φ : Dual R M) : (a : M) → R) x : R) (((↑ψ : Dual R M) : (a : M) → R) x : R)

Tactic:
simp only [funext_iff] at h

Premises used: funext_iff
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
W : Submodule R M
φ ψ : ↥W.dualAnnihilator
x : M
h : ∀ (x : M), Eq.{u_1 + 1} (α := R) (((↑φ : Dual R M) : (a : M) → R) x : R) (((↑ψ : Dual R M) : (a : M) → R) x : R)
⊢ Eq.{u_1 + 1} (α := R) (((↑φ : Dual R M) : (a : M) → R) x : R) (((↑ψ : Dual R M) : (a : M) → R) x : R)

Tactic:
h _
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
W : Submodule R M
φ ψ : ↥W.dualAnnihilator
x : M
h : ∀ (x : M), Eq.{u_1 + 1} (α := R) (((↑φ : Dual R M) : (a : M) → R) x : R) (((↑ψ : Dual R M) : (a : M) → R) x : R)
⊢ Eq.{u_1 + 1} (α := R) (((↑φ : Dual R M) : (a : M) → R) x : R) (((↑ψ : Dual R M) : (a : M) → R) x : R)

Tactic:
exact h _
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
φ : ↥W.dualAnnihilator
x : M
⊢ Eq.{u_1 + 1} (α := R)
    ((((W.dualCopairing : (a : ↥W.dualAnnihilator) → M ⧸ W →ₗ[R] R) φ :
            LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (M ⧸ W) R) :
          (a : M ⧸ W) → R)
        (Quotient.mk x) :
      R)
    ((φ : (a : M) → R) x : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
φ : Dual R M
x : ↥W
⊢ Eq.{u_1 + 1} (α := R)
    ((((W.dualPairing : (a : Dual R M ⧸ W.dualAnnihilator) → ↥W →ₗ[R] R) (Quotient.mk φ) :
            LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥W) R) :
          (a : ↥W) → R)
        x :
      R)
    ((φ : (a : M) → R) (↑x : M) : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
h :
  ∀ (φ : Dual R M),
    Membership.mem (γ := Submodule R (Dual R M)) (LinearMap.range (M := Dual.{u_1, u_2} R (M ⧸ W)) W.mkQ.dualMap) φ ↔
      φ ∈ W.dualAnnihilator
⊢ LinearMap.range (M := Dual.{u_1, u_2} R (M ⧸ W)) W.mkQ.dualMap = W.dualAnnihilator

Tactic:
ext φ
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
φ : Dual R M
h : (∃ (y : Dual.{u_1, u_2} R (M ⧸ W)), (W.mkQ.dualMap : (a : Dual R (M ⧸ W)) → Dual R M) y = φ) → φ ∈ W.dualAnnihilator
h₁ : φ ∈ W.dualAnnihilator → ∃ (y : Dual.{u_1, u_2} R (M ⧸ W)), (W.mkQ.dualMap : (a : Dual R (M ⧸ W)) → Dual R M) y = φ
⊢ (∃ (y : Dual.{u_1, u_2} R (M ⧸ W)), (W.mkQ.dualMap : (a : Dual R (M ⧸ W)) → Dual R M) y = φ) ↔ φ ∈ W.dualAnnihilator

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
ψ : Dual.{u_1, u_2} R (M ⧸ W)
⊢ Membership.mem (α := Dual R M) (γ := Submodule R (Dual R M))
    (LinearMap.range (M := Dual.{u_1, u_2} R (M ⧸ W)) W.mkQ.dualMap)
    ((W.mkQ.dualMap : (a : Dual R (M ⧸ W)) → Dual R M) ψ : Dual R M)

Tactic:
have := LinearMap.mem_range_self W.mkQ.dualMap ψ
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
ψ : Dual.{u_1, u_2} R (M ⧸ W)
this :
  Membership.mem (α := Dual R M) (γ := Submodule R (Dual R M))
    (LinearMap.range (M := Dual.{u_1, u_2} R (M ⧸ W)) W.mkQ.dualMap)
    ((W.mkQ.dualMap : (a : Dual R (M ⧸ W)) → Dual R M) ψ : Dual R M)
⊢ Membership.mem (α := Dual R M) W.dualAnnihilator ((W.mkQ.dualMap : (a : Dual R (M ⧸ W)) → Dual R M) ψ : Dual R M)

Tactic:
simpa only [ker_mkQ] using W.mkQ.range_dualMap_le_dualAnnihilator_ker this

Premises used: LinearMap.range_dualMap_le_dualAnnihilator_ker, Submodule.mkQ, Submodule.ker_mkQ
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
φ : Dual R M
hφ : φ ∈ W.dualAnnihilator
h h₁ :
  (W.mkQ.dualMap : (a : Dual R (M ⧸ W)) → Dual R M)
      ((W.dualCopairing : (a : ↥W.dualAnnihilator) → M ⧸ W →ₗ[R] R)
        (Subtype.mk (p := fun (x : Dual R M) ↦ x ∈ W.dualAnnihilator) φ hφ)) =
    φ
⊢ ∃ (y : Dual.{u_1, u_2} R (M ⧸ W)), (W.mkQ.dualMap : (a : Dual R (M ⧸ W)) → Dual R M) y = φ

Tactic:
exists W.dualCopairing ⟨φ, hφ⟩

Premises used: Submodule.dualCopairing, Subtype.mk, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
W : Submodule R M
h :
  ∀ (x : ↥W.dualAnnihilator) (x_1 : M),
    Eq.{u_1 + 1} (α := R)
      (((↑((LinearMap.codRestrict W.dualAnnihilator W.mkQ.dualMap ⋯ ∘ₗ W.dualCopairing :
                    (a : ↥W.dualAnnihilator) → ↥W.dualAnnihilator)
                  x) :
              Dual R M) :
            (a : M) → R)
          x_1 :
        R)
      (((↑((LinearMap.id : (a : ↥W.dualAnnihilator) → ↥W.dualAnnihilator) x) : Dual R M) : (a : M) → R) x_1 : R)
⊢ LinearMap.codRestrict W.dualAnnihilator W.mkQ.dualMap ⋯ ∘ₗ W.dualCopairing = LinearMap.id

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
W : Submodule R M
x : ↥W.dualAnnihilator
x_1 : M
⊢ Eq.{u_1 + 1} (α := R)
    (((↑((LinearMap.codRestrict W.dualAnnihilator W.mkQ.dualMap ⋯ ∘ₗ W.dualCopairing :
                  (a : ↥W.dualAnnihilator) → ↥W.dualAnnihilator)
                x) :
            Dual R M) :
          (a : M) → R)
        x_1 :
      R)
    (((↑((LinearMap.id : (a : ↥W.dualAnnihilator) → ↥W.dualAnnihilator) x) : Dual R M) : (a : M) → R) x_1 : R)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
W : Submodule R M
h :
  ∀ (x : Dual.{u_1, u_2} R (M ⧸ W)) (x_1 : M),
    Eq.{u_1 + 1} (α := R)
      (((W.dualCopairing ∘ₗ LinearMap.codRestrict W.dualAnnihilator W.mkQ.dualMap ⋯ :
                  (a : Dual R (M ⧸ W)) → Dual R (M ⧸ W))
                x ∘ₗ
              W.mkQ :
            (a : M) → R)
          x_1 :
        R)
      (((LinearMap.id : (a : Dual R (M ⧸ W)) → Dual R (M ⧸ W)) x ∘ₗ W.mkQ : (a : M) → R) x_1 : R)
⊢ W.dualCopairing ∘ₗ LinearMap.codRestrict W.dualAnnihilator W.mkQ.dualMap ⋯ = LinearMap.id

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
W : Submodule R M
x : Dual.{u_1, u_2} R (M ⧸ W)
x_1 : M
⊢ Eq.{u_1 + 1} (α := R)
    (((W.dualCopairing ∘ₗ LinearMap.codRestrict W.dualAnnihilator W.mkQ.dualMap ⋯ :
                (a : Dual R (M ⧸ W)) → Dual R (M ⧸ W))
              x ∘ₗ
            W.mkQ :
          (a : M) → R)
        x_1 :
      R)
    (((LinearMap.id : (a : Dual R (M ⧸ W)) → Dual R (M ⧸ W)) x ∘ₗ W.mkQ : (a : M) → R) x_1 : R)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
φ : Dual.{u_1, u_2} R (M ⧸ W)
x : M
⊢ Eq.{u_1 + 1} (α := R)
    ((((W.dualQuotEquivDualAnnihilator : (a : Dual R (M ⧸ W)) → ↥W.dualAnnihilator) φ : ↥W.dualAnnihilator) :
          (a : M) → R)
        x :
      R)
    ((φ : (a : M ⧸ W) → R) (Quotient.mk x) : R)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, rfl
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
⊢ W.dualCopairing = (↑W.dualQuotEquivDualAnnihilator.symm : ↥W.dualAnnihilator →ₗ[R] Dual R (M ⧸ W))

Tactic:
rfl

Premises used: Set.Mem, LinearMap.mk₂'ₛₗ, Submodule.dualCopairing, LinearMap.flip, rfl
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
φ : ↥W.dualAnnihilator
x : M
⊢ Eq.{u_1 + 1} (α := R)
    ((((W.dualQuotEquivDualAnnihilator.symm : (a : ↥W.dualAnnihilator) → Dual R (M ⧸ W)) φ :
            Dual.{u_1, u_2} R (M ⧸ W)) :
          (a : M ⧸ W) → R)
        (Quotient.mk x) :
      R)
    ((φ : (a : M) → R) x : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
inst_3 : Free.{u_1, u_2} R (M ⧸ W)
⊢ Module.Finite R ↥W.dualAnnihilator ↔ Module.Finite.{u_1, u_2} R (M ⧸ W)

Tactic:
(Finite.equiv_iff W.dualQuotEquivDualAnnihilator.symm).trans (finite_dual_iff R)

Premises used: LinearEquiv.symm, Module.finite_dual_iff, Module.Finite.equiv_iff, Iff.trans, Submodule.dualQuotEquivDualAnnihilator
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
rw : W.dualAnnihilator = ⊥ ↔ Subsingleton ↥W.dualAnnihilator
rw₁ rw₂ : W.dualAnnihilator = ⊥ ↔ W.dualAnnihilator = ⊥
⊢ W.dualAnnihilator = ⊥ ↔ Subsingleton (Dual.{u_1, u_2} R (M ⧸ W))

Tactic:
rw [W.dualQuotEquivDualAnnihilator.toEquiv.subsingleton_congr, subsingleton_iff_eq_bot]

Premises used: Submodule.subsingleton_iff_eq_bot, Equiv.subsingleton_congr, LinearEquiv.toEquiv, Submodule.dualQuotEquivDualAnnihilator
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
inst_3 : Projective.{u_1, u_2} R (M ⧸ W)
rw : Subsingleton (Dual.{u_1, u_2} R (M ⧸ W)) ↔ W = ⊤
rw₁ : Subsingleton.{u_2 + 1} (M ⧸ W) ↔ W = ⊤
rw₂ rw₃ : W = ⊤ ↔ W = ⊤
⊢ W.dualAnnihilator = ⊥ ↔ W = ⊤

Tactic:
rw [dualAnnihilator_eq_bot_iff', subsingleton_dual_iff, Quotient.subsingleton_iff]

Premises used: Module.subsingleton_dual_iff, Submodule.Quotient.subsingleton_iff, Submodule.dualAnnihilator_eq_bot_iff'
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
inst_3 : Projective R M
⊢ W.dualAnnihilator = ⊤ ↔ W = ⊥

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

Premises used: Eq.rec, Iff.intro, Submodule.dualAnnihilator_bot, Eq.symm
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
inst_3 : Projective R M
refine : ∀ (h : W.dualAnnihilator = ⊤), W = ⊥
⊢ W.dualAnnihilator = ⊤ ↔ W = ⊥

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h ▸ dualAnnihilator_bot⟩
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
inst_3 : Projective R M
h : W.dualAnnihilator = ⊤
⊢ W = ⊥

Tactic:
W.eq_bot_iff.mpr fun v hv ↦ (forall_dual_apply_eq_zero_iff R v).mp fun f ↦ ?_

Premises used: Iff.mpr, Module.forall_dual_apply_eq_zero_iff, Iff.mp, Submodule.eq_bot_iff
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
inst_3 : Projective R M
h : W.dualAnnihilator = ⊤
refine : ∀ (v : M) (hv : v ∈ W) (f : Dual R M), Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) v : R) (0 : R)
⊢ W = ⊥

Tactic:
refine W.eq_bot_iff.mpr fun v hv ↦ (forall_dual_apply_eq_zero_iff R v).mp fun f ↦ ?_

Premises used: Iff.mpr, Module.forall_dual_apply_eq_zero_iff, Iff.mp, Submodule.eq_bot_iff
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
inst_3 : Projective R M
h : W.dualAnnihilator = ⊤
v : M
hv : v ∈ W
f : Dual R M
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) v : R) (0 : R)

Tactic:
(mem_dualAnnihilator f).mp ?_ v hv

Premises used: Submodule.mem_dualAnnihilator, Iff.mp
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
inst_3 : Projective R M
h : W.dualAnnihilator = ⊤
v : M
hv : v ∈ W
f : Dual R M
refine : f ∈ W.dualAnnihilator
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) v : R) (0 : R)

Tactic:
refine (mem_dualAnnihilator f).mp ?_ v hv

Premises used: Submodule.mem_dualAnnihilator, Iff.mp
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
inst_3 : Projective R M
h : W.dualAnnihilator = ⊤
v : M
hv : v ∈ W
f : Dual R M
⊢ f ∈ W.dualAnnihilator

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R (Dual R M)
m : M
w : ↥W
⊢ Eq.{u_1 + 1} (α := R)
    ((((W.quotDualCoannihilatorToDual : (a : M ⧸ W.dualCoannihilator) → Dual R ↥W) (Quotient.mk m) : Dual R ↥W) :
          (a : ↥W) → R)
        w :
      R)
    (((↑w : Dual R M) : (a : M) → R) m : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R (Dual R M)
⊢ Function.Injective (α := M ⧸ W.dualCoannihilator) (β := Dual R ↥W)
    (⇑W.quotDualCoannihilatorToDual : (a : M ⧸ W.dualCoannihilator) → Dual R ↥W)

Tactic:
LinearMap.ker_eq_bot.mp (ker_liftQ_eq_bot _ _ _ le_rfl)

Premises used: le_rfl, LinearMap.ker_eq_bot, Submodule.ker_liftQ_eq_bot, Iff.mp
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R (Dual R M)
⊢ Function.Injective (α := ↥W) (β := LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (M ⧸ W.dualCoannihilator) R)
    (⇑W.quotDualCoannihilatorToDual.flip : (a : ↥W) → M ⧸ W.dualCoannihilator →ₗ[R] R)

Tactic:
fun _ _ he ↦ Subtype.ext <| LinearMap.ext fun m ↦ DFunLike.congr_fun he ⟦m⟧

Premises used: DFunLike.congr_fun, Submodule.dualCoannihilator, LinearMap.ext, Quotient.mk, Submodule.quotientRel, Function.Injective, Subtype.ext
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R (Dual R M)
rw : W.quotDualCoannihilatorToDual.ker = ⊥ ∧ W.quotDualCoannihilatorToDual.flip.ker = ⊥
⊢ W.quotDualCoannihilatorToDual.Nondegenerate

Tactic:
rw [Nondegenerate, separatingLeft_iff_ker_eq_bot, separatingRight_iff_flip_ker_eq_bot]

Premises used: LinearMap.separatingRight_iff_flip_ker_eq_bot, LinearMap.separatingLeft_iff_ker_eq_bot, LinearMap.Nondegenerate
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R (Dual R M)
simp_rw :
  Function.Injective (α := M ⧸ W.dualCoannihilator) (β := ↥W →ₗ[R] R)
      (⇑W.quotDualCoannihilatorToDual : (a : M ⧸ W.dualCoannihilator) → ↥W →ₗ[R] R) ∧
    W.quotDualCoannihilatorToDual.flip.ker = ⊥
⊢ W.quotDualCoannihilatorToDual.ker = ⊥ ∧ W.quotDualCoannihilatorToDual.flip.ker = ⊥

Tactic:
simp_rw [ker_eq_bot]

Premises used: LinearMap.ker_eq_bot
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R (Dual R M)
⊢ Function.Injective (α := M ⧸ W.dualCoannihilator) (β := ↥W →ₗ[R] R)
      (⇑W.quotDualCoannihilatorToDual : (a : M ⧸ W.dualCoannihilator) → ↥W →ₗ[R] R) ∧
    W.quotDualCoannihilatorToDual.flip.ker = ⊥

Tactic:
⟨W.quotDualCoannihilatorToDual_injective, W.flip_quotDualCoannihilatorToDual_injective⟩

Premises used: Unit.unit, sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Bool.true, Submodule.quotDualCoannihilatorToDual_injective, And.intro, Function.const, Lean.Name, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R (Dual R M)
⊢ Function.Injective (α := M ⧸ W.dualCoannihilator) (β := ↥W →ₗ[R] R)
      (⇑W.quotDualCoannihilatorToDual : (a : M ⧸ W.dualCoannihilator) → ↥W →ₗ[R] R) ∧
    W.quotDualCoannihilatorToDual.flip.ker = ⊥

Tactic:
exact ⟨W.quotDualCoannihilatorToDual_injective, W.flip_quotDualCoannihilatorToDual_injective⟩
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
⊢ f.dualMap.range = f.ker.dualAnnihilator

Tactic:
((f.quotKerEquivOfSurjective hf).dualMap.range_comp _).trans
    (LinearMap.ker f).range_dualMap_mkQ_eq

Premises used: LinearEquiv.range_comp, Quotient.liftOn', AddCon.liftOn, LinearMap.ker, LinearMap.quotKerEquivOfSurjective, LinearEquiv.dualMap, Submodule.range_dualMap_mkQ_eq, LinearMap.dualMap, Eq.trans
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf :
  Function.Surjective (α := Dual R M') (β := Dual.{u_1, u_3} R ↥f.range)
    (⇑f.range.subtype.dualMap : (a : Dual R M') → Dual R ↥f.range)
rw : Eq (α := Submodule R ↥f.range) (range f.rangeRestrict) ⊤
rw₁ rw₂ : Eq.{u_3 + 1} (α := Submodule R ↥f.range) ⊤ ⊤
⊢ Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := ↥f.range) (⇑f.rangeRestrict : (a : M) → ↥f.range)

Tactic:
rw [← range_eq_top, range_rangeRestrict]

Premises used: LinearMap.range_rangeRestrict, LinearMap.range_eq_top
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf :
  Function.Surjective (α := Dual R M') (β := Dual.{u_1, u_3} R ↥f.range)
    (⇑f.range.subtype.dualMap : (a : Dual R M') → Dual R ↥f.range)
⊢ Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := ↥f.range) (⇑f.rangeRestrict : (a : M) → ↥f.range)

Tactic:
have rr_surj : Function.Surjective f.rangeRestrict := by
    rw [← range_eq_top, range_rangeRestrict]
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf :
  Function.Surjective (α := Dual R M') (β := Dual.{u_1, u_3} R ↥f.range)
    (⇑f.range.subtype.dualMap : (a : Dual R M') → Dual R ↥f.range)
rr_surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := ↥f.range) (⇑f.rangeRestrict : (a : M) → ↥f.range)
⊢ range (M := Dual.{u_1, u_3} R ↥f.range) (dualMap f.rangeRestrict) =
    (ker (M₂ := ↥f.range) f.rangeRestrict).dualAnnihilator

Tactic:
have := range_dualMap_eq_dualAnnihilator_ker_of_surjective f.rangeRestrict rr_surj
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf :
  Function.Surjective (α := Dual R M') (β := Dual.{u_1, u_3} R ↥f.range)
    (⇑f.range.subtype.dualMap : (a : Dual R M') → Dual R ↥f.range)
rr_surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := ↥f.range) (⇑f.rangeRestrict : (a : M) → ↥f.range)
this :
  range (M := Dual.{u_1, u_3} R ↥f.range) (dualMap f.rangeRestrict) =
    (ker (M₂ := ↥f.range) f.rangeRestrict).dualAnnihilator
⊢ range (M := Dual.{u_1, u_3} R ↥f.range) (dualMap f.rangeRestrict) =
    (ker (M₂ := ↥f.range) f.rangeRestrict).dualAnnihilator

Tactic:
this
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf :
  Function.Surjective (α := Dual R M') (β := Dual.{u_1, u_3} R ↥f.range)
    (⇑f.range.subtype.dualMap : (a : Dual R M') → Dual R ↥f.range)
rr_surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := ↥f.range) (⇑f.rangeRestrict : (a : M) → ↥f.range)
this :
  range (M := Dual.{u_1, u_3} R ↥f.range) (dualMap f.rangeRestrict) =
    (ker (M₂ := ↥f.range) f.rangeRestrict).dualAnnihilator
h : f.dualMap.range = range (M := Dual.{u_1, u_3} R ↥f.range) (dualMap f.rangeRestrict)
h₁ : f.ker.dualAnnihilator = (ker (M₂ := ↥f.range) f.rangeRestrict).dualAnnihilator
⊢ f.dualMap.range = f.ker.dualAnnihilator

Tactic:
convert! this using 1
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf :
  Function.Surjective (α := Dual R M') (β := Dual.{u_1, u_3} R ↥f.range)
    (⇑f.range.subtype.dualMap : (a : Dual R M') → Dual R ↥f.range)
rr_surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := ↥f.range) (⇑f.rangeRestrict : (a : M) → ↥f.range)
this :
  range (M := Dual.{u_1, u_3} R ↥f.range) (dualMap f.rangeRestrict) =
    (ker (M₂ := ↥f.range) f.rangeRestrict).dualAnnihilator
⊢ f.dualMap.range = (f.range.subtype ∘ₗ f.rangeRestrict).dualMap.range

Tactic:
simp