-- Mathlib/LinearAlgebra/Dual.lean
theorem dualAnnihilator_gc :
    GaloisConnection
      (OrderDual.toDual ∘ (dualAnnihilator : Submodule R M → Submodule R (Module.Dual R M)))
      (dualCoannihilator ∘ OrderDual.ofDual)

Proof state:
case h₂.mpr
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Dual R M)
h : a ≤ a✝.dualCoannihilator
x : Dual R M
hx : x ∈ a✝
⊢ x ∈ a.dualAnnihilator

Tactic:
simp only [mem_dualAnnihilator, mem_dualCoannihilator]

Result:
case h₂.mpr
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Dual R M)
h : a ≤ a✝.dualCoannihilator
x : Dual R M
hx : x ∈ a✝
⊢ ∀ w ∈ a, x w = 0

Proof state:
case h₂.mpr
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Dual R M)
h : a ≤ a✝.dualCoannihilator
x : Dual R M
hx : x ∈ a✝
⊢ ∀ w ∈ a, x w = 0

Tactic:
intro y hy

Result:
case h₂.mpr
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Dual R M)
h : a ≤ a✝.dualCoannihilator
x : Dual R M
hx : x ∈ a✝
y : M
hy : y ∈ a
⊢ x y = 0

Proof state:
case h₂.mpr
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Dual R M)
h : a ≤ a✝.dualCoannihilator
x : Dual R M
hx : x ∈ a✝
y : M
hy : y ∈ a
this : ∀ φ ∈ a✝, φ y = 0
⊢ x y = 0

Tactic:
exact this x hx

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
b : (Submodule R (Dual R M))ᵒᵈ
⊢ (⇑OrderDual.toDual ∘ dualAnnihilator) a ≤ b ↔ a ≤ (dualCoannihilator ∘ ⇑OrderDual.ofDual) b

Tactic:
induction b using OrderDual.rec

Result:
case h₂
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Dual R M)
⊢ (⇑OrderDual.toDual ∘ dualAnnihilator) a ≤ OrderDual.toDual a✝ ↔
    a ≤ (dualCoannihilator ∘ ⇑OrderDual.ofDual) (OrderDual.toDual a✝)

Proof state:
case h₂
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Dual R M)
⊢ (⇑OrderDual.toDual ∘ dualAnnihilator) a ≤ OrderDual.toDual a✝ ↔
    a ≤ (dualCoannihilator ∘ ⇑OrderDual.ofDual) (OrderDual.toDual a✝)

Tactic:
simp only [Function.comp_apply, OrderDual.toDual_le_toDual, OrderDual.ofDual_toDual]

Result:
case h₂
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Dual R M)
⊢ a✝ ≤ a.dualAnnihilator ↔ a ≤ a✝.dualCoannihilator

Proof state:
case h₂.mpr
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Dual R M)
⊢ a ≤ a✝.dualCoannihilator → a✝ ≤ a.dualAnnihilator

Tactic:
intro h x hx

Result:
case h₂.mpr
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Dual R M)
h : a ≤ a✝.dualCoannihilator
x : Dual R M
hx : x ∈ a✝
⊢ x ∈ a.dualAnnihilator

Proof state:
case h₂.mpr
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Dual R M)
h : a ≤ a✝.dualCoannihilator
x : Dual R M
hx : x ∈ a✝
y : M
hy : y ∈ a
this : y ∈ a✝.dualCoannihilator
⊢ x y = 0

Tactic:
simp only [mem_dualAnnihilator, mem_dualCoannihilator] at this

Result:
case h₂.mpr
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Dual R M)
h : a ≤ a✝.dualCoannihilator
x : Dual R M
hx : x ∈ a✝
y : M
hy : y ∈ a
this : ∀ φ ∈ a✝, φ y = 0
⊢ x y = 0

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ GaloisConnection (⇑OrderDual.toDual ∘ dualAnnihilator) (dualCoannihilator ∘ ⇑OrderDual.ofDual)

Tactic:
intro a b

Result:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
b : (Submodule R (Dual R M))ᵒᵈ
⊢ (⇑OrderDual.toDual ∘ dualAnnihilator) a ≤ b ↔ a ≤ (dualCoannihilator ∘ ⇑OrderDual.ofDual) b

Proof state:
case h₂.mpr
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Dual R M)
h : a ≤ a✝.dualCoannihilator
x : Dual R M
hx : x ∈ a✝
y : M
hy : y ∈ a
⊢ x y = 0

Tactic:
have := h hy

Result:
case h₂.mpr
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Dual R M)
h : a ≤ a✝.dualCoannihilator
x : Dual R M
hx : x ∈ a✝
y : M
hy : y ∈ a
this : y ∈ a✝.dualCoannihilator
⊢ x y = 0