-- Mathlib/LinearAlgebra/Dual.lean
theorem range_dualMap_mkQ_eq (W : Submodule R M) :
    LinearMap.range W.mkQ.dualMap = W.dualAnnihilator

Proof state:
case h.mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
⊢ (∃ y, W.mkQ.dualMap y = φ) → φ ∈ W.dualAnnihilator

Tactic:
rintro ⟨ψ, rfl⟩

Result:
case h.mp.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
ψ : Dual R (M ⧸ W)
⊢ W.mkQ.dualMap ψ ∈ W.dualAnnihilator

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
⊢ φ ∈ LinearMap.range W.mkQ.dualMap ↔ φ ∈ W.dualAnnihilator

Tactic:
rw [LinearMap.mem_range]

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
⊢ (∃ y, W.mkQ.dualMap y = φ) ↔ φ ∈ W.dualAnnihilator

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
⊢ (∃ y, W.mkQ.dualMap y = φ) ↔ φ ∈ W.dualAnnihilator

Tactic:
constructor

Result:
case h.mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
⊢ (∃ y, W.mkQ.dualMap y = φ) → φ ∈ W.dualAnnihilator

case h.mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
⊢ φ ∈ W.dualAnnihilator → ∃ y, W.mkQ.dualMap y = φ

Proof state:
case h.mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
hφ : φ ∈ W.dualAnnihilator
⊢ ∃ y, W.mkQ.dualMap y = φ

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

Result:
no goals

Proof state:
case h.mp.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
ψ : Dual R (M ⧸ W)
⊢ W.mkQ.dualMap ψ ∈ W.dualAnnihilator

Tactic:
have := LinearMap.mem_range_self W.mkQ.dualMap ψ

Result:
case h.mp.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
ψ : Dual R (M ⧸ W)
this : W.mkQ.dualMap ψ ∈ LinearMap.range W.mkQ.dualMap
⊢ W.mkQ.dualMap ψ ∈ W.dualAnnihilator

Proof state:
case h.mp.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
ψ : Dual R (M ⧸ W)
this : W.mkQ.dualMap ψ ∈ LinearMap.range W.mkQ.dualMap
⊢ W.mkQ.dualMap ψ ∈ W.dualAnnihilator

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

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
⊢ LinearMap.range W.mkQ.dualMap = W.dualAnnihilator

Tactic:
ext φ

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
⊢ φ ∈ LinearMap.range W.mkQ.dualMap ↔ φ ∈ W.dualAnnihilator

Proof state:
case h.mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
⊢ φ ∈ W.dualAnnihilator → ∃ y, W.mkQ.dualMap y = φ

Tactic:
intro hφ

Result:
case h.mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
hφ : φ ∈ W.dualAnnihilator
⊢ ∃ y, W.mkQ.dualMap y = φ