awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsReflexive R M
h :
  ∀ (x : Dual R M) (x_1 : Dual R (Dual R M)),
    Eq.{u_3 + 1} (α := R)
      (((((↑(LinearEquiv.dualMap (LinearEquiv.symm (evalEquiv R M))) : Dual R M →ₗ[R] Dual R (Dual R (Dual R M))) :
                  (a : Dual R M) → Dual R (Dual R (Dual R M)))
                x :
              Dual R (Dual R (Dual R M))) :
            (a : Dual R (Dual R M)) → R)
          x_1 :
        R)
      ((((Dual.eval R (Dual R M) : (a : Dual R M) → Dual R (Dual R (Dual R M))) x : Dual R (Dual R (Dual R M))) :
            (a : Dual R (Dual R M)) → R)
          x_1 :
        R)
⊢ Eq (α := Dual R M →ₗ[R] Dual R (Dual R (Dual R M)))
    (↑(LinearEquiv.dualMap (LinearEquiv.symm (evalEquiv R M))) : Dual R M →ₗ[R] Dual R (Dual R (Dual R M)))
    (Dual.eval R (Dual R M))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsReflexive R M
x : Dual R M
x_1 : Dual R (Dual R M)
⊢ Eq.{u_3 + 1} (α := R)
    (((((↑(LinearEquiv.dualMap (LinearEquiv.symm (evalEquiv R M))) : Dual R M →ₗ[R] Dual R (Dual R (Dual R M))) :
                (a : Dual R M) → Dual R (Dual R (Dual R M)))
              x :
            Dual R (Dual R (Dual R M))) :
          (a : Dual R (Dual R M)) → R)
        x_1 :
      R)
    ((((Dual.eval R (Dual R M) : (a : Dual R M) → Dual R (Dual R (Dual R M))) x : Dual R (Dual R (Dual R M))) :
          (a : Dual R (Dual R M)) → R)
        x_1 :
      R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsReflexive R M
M' : Type u_6
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
f : M →ₗ[R] M'
rw : (eval R M' ∘ₗ f) ∘ₗ (↑(LinearEquiv.symm (evalEquiv R M)) : Dual R (Dual R M) →ₗ[R] M) = f.dualMap.dualMap
rw₁ : eval R M' ∘ₗ f = f.dualMap.dualMap ∘ₗ (↑(evalEquiv R M) : M →ₗ[R] Dual R (Dual R M))
rw₂ : eval R M' ∘ₗ f = f.dualMap.dualMap ∘ₗ eval R M
rw₃ rw₄ : eval R M' ∘ₗ f = eval R M' ∘ₗ f
⊢ eval R M' ∘ₗ f ∘ₗ (↑(LinearEquiv.symm (evalEquiv R M)) : Dual R (Dual R M) →ₗ[R] M) = f.dualMap.dualMap

Tactic:
rw [← LinearMap.comp_assoc, LinearEquiv.comp_toLinearMap_symm_eq,
    evalEquiv_toLinearMap, eval_naturality]

Premises used: LinearEquiv.comp_toLinearMap_symm_eq, LinearMap.comp_assoc, Module.Dual.eval_naturality, Module.evalEquiv_toLinearMap
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsReflexive R M
M' : Type u_6
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
f g : M →ₗ[R] M'
h : Injective (α := M') (β := Dual R (Dual R M')) (⇑(Dual.eval R M') : (a : M') → Dual R (Dual R M'))
simp :
  Dual.eval R M' ∘ₗ f ∘ₗ (↑(LinearEquiv.symm (evalEquiv R M)) : Dual R (Dual R M) →ₗ[R] M) =
      Dual.eval R M' ∘ₗ g ∘ₗ (↑(LinearEquiv.symm (evalEquiv R M)) : Dual R (Dual R M) →ₗ[R] M) ↔
    f = g
⊢ f.dualMap.dualMap = g.dualMap.dualMap ↔ f = g

Tactic:
simp only [← Dual.eval_comp_comp_evalEquiv_eq]

Premises used: Module.Dual.eval_comp_comp_evalEquiv_eq
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsReflexive R M
M' : Type u_6
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
f g : M →ₗ[R] M'
h : Injective (α := M') (β := Dual R (Dual R M')) (⇑(Dual.eval R M') : (a : M') → Dual R (Dual R M'))
⊢ Dual.eval R M' ∘ₗ f ∘ₗ (↑(LinearEquiv.symm (evalEquiv R M)) : Dual R (Dual R M) →ₗ[R] M) =
      Dual.eval R M' ∘ₗ g ∘ₗ (↑(LinearEquiv.symm (evalEquiv R M)) : Dual R (Dual R M) →ₗ[R] M) ↔
    f = g

Tactic:
⟨fun hfg => ?_, fun a ↦ congrArg (Dual.eval R M').comp
    (congrFun (congrArg LinearMap.comp a) (evalEquiv R M).symm.toLinearMap)⟩

Premises used: LinearEquiv.symm, congrArg, LinearMap.comp, LinearEquiv.toLinearMap, congrFun, Iff.intro, Module.evalEquiv, Module.Dual.eval
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsReflexive R M
M' : Type u_6
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
f g : M →ₗ[R] M'
h : Injective (α := M') (β := Dual R (Dual R M')) (⇑(Dual.eval R M') : (a : M') → Dual R (Dual R M'))
refine :
  ∀
    (hfg :
      Dual.eval R M' ∘ₗ f ∘ₗ (↑(LinearEquiv.symm (evalEquiv R M)) : Dual R (Dual R M) →ₗ[R] M) =
        Dual.eval R M' ∘ₗ g ∘ₗ (↑(LinearEquiv.symm (evalEquiv R M)) : Dual R (Dual R M) →ₗ[R] M)),
    f = g
⊢ Dual.eval R M' ∘ₗ f ∘ₗ (↑(LinearEquiv.symm (evalEquiv R M)) : Dual R (Dual R M) →ₗ[R] M) =
      Dual.eval R M' ∘ₗ g ∘ₗ (↑(LinearEquiv.symm (evalEquiv R M)) : Dual R (Dual R M) →ₗ[R] M) ↔
    f = g

Tactic:
refine ⟨fun hfg => ?_, fun a ↦ congrArg (Dual.eval R M').comp
    (congrFun (congrArg LinearMap.comp a) (evalEquiv R M).symm.toLinearMap)⟩
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsReflexive R M
M' : Type u_6
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
f g : M →ₗ[R] M'
h : Injective (α := M') (β := Dual R (Dual R M')) (⇑(Dual.eval R M') : (a : M') → Dual R (Dual R M'))
hfg :
  Dual.eval R M' ∘ₗ f ∘ₗ (↑(LinearEquiv.symm (evalEquiv R M)) : Dual R (Dual R M) →ₗ[R] M) =
    Dual.eval R M' ∘ₗ g ∘ₗ (↑(LinearEquiv.symm (evalEquiv R M)) : Dual R (Dual R M) →ₗ[R] M)
⊢ f = g

Tactic:
rw [propext (cancel_left h), LinearEquiv.eq_comp_toLinearMap_iff] at hfg

Premises used: LinearEquiv.eq_comp_toLinearMap_iff, propext, LinearMap.cancel_left
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsReflexive R M
M' : Type u_6
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
f g : M →ₗ[R] M'
h : Injective (α := M') (β := Dual R (Dual R M')) (⇑(Dual.eval R M') : (a : M') → Dual R (Dual R M'))
hfg : f = g
⊢ f = g

Tactic:
hfg
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsReflexive R M
M' : Type u_6
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
f g : M →ₗ[R] M'
h : Injective (α := M') (β := Dual R (Dual R M')) (⇑(Dual.eval R M') : (a : M') → Dual R (Dual R M'))
hfg : f = g
⊢ f = g

Tactic:
exact hfg
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsReflexive R M
M' : Type u_6
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : IsReflexive R M'
f g : M →ₗ[R] M'
⊢ f.dualMap.dualMap = g.dualMap.dualMap ↔ f = g

Tactic:
dualMap_dualMap_eq_iff_of_injective _ _ (bijective_dual_eval R M').injective

Premises used: Function.Bijective.injective, Module.bijective_dual_eval, Module.dualMap_dualMap_eq_iff_of_injective
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
K : Type u_1
V : Type u_2
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
R : Type u_3
M : Type u_4
N : Type u_5
inst_3 : CommSemiring R
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : Module R M
inst_7 : Module R N
inst_8 : IsReflexive R M
⊢ Bijective (α := Dual R M) (β := Dual R (Dual R (Dual R M)))
    (⇑(eval R (Dual R M)) : (a : Dual R M) → Dual R (Dual R (Dual R M)))

Tactic:
simpa only [← symm_dualMap_evalEquiv] using (evalEquiv R M).dualMap.symm.bijective

Premises used: LinearEquiv.symm, LinearEquiv.bijective, Module.symm_dualMap_evalEquiv, LinearEquiv.dualMap, Module.evalEquiv
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsReflexive R M
W : Submodule R M
⊢ (mapEvalEquiv R M : (a : Submodule R M) → Submodule R (Dual R (Dual R M))) W = map (Dual.eval R M) W

Tactic:
rfl

Premises used: Submodule.map, rfl
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsReflexive R M
W'' : Submodule R (Dual R (Dual R M))
⊢ (OrderIso.symm (mapEvalEquiv R M) : (a : Submodule R (Dual R (Dual R M))) → Submodule R M) W'' =
    comap (Dual.eval R M) W''

Tactic:
rfl

Premises used: Submodule.comap, rfl
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsReflexive R M
e : M ≃ₗ[R] N
ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap
h :
  ∀ (m : N) (f : Dual R N),
    Eq.{u_3 + 1} (α := R)
      ((((Dual.eval R N : (a : N) → Dual R (Dual R N)) m : Dual R (Dual R N)) : (a : Dual R N) → R) f : R)
      (((((↑ed.symm : Dual R (Dual R M) →ₗ[R] Dual R (Dual R N)) ∘ₗ Dual.eval R M ∘ₗ (↑e.symm : N →ₗ[R] M) :
                  (a : N) → Dual R (Dual R N))
                m :
              Dual R (Dual R N)) :
            (a : Dual R N) → R)
          f :
        R)
⊢ Dual.eval R N = (↑ed.symm : Dual R (Dual R M) →ₗ[R] Dual R (Dual R N)) ∘ₗ Dual.eval R M ∘ₗ (↑e.symm : N →ₗ[R] M)

Tactic:
ext m f
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsReflexive R M
e : M ≃ₗ[R] N
ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap
m : N
f : Dual R N
⊢ Eq.{u_3 + 1} (α := R)
    ((((Dual.eval R N : (a : N) → Dual R (Dual R N)) m : Dual R (Dual R N)) : (a : Dual R N) → R) f : R)
    (((((↑ed.symm : Dual R (Dual R M) →ₗ[R] Dual R (Dual R N)) ∘ₗ Dual.eval R M ∘ₗ (↑e.symm : N →ₗ[R] M) :
                (a : N) → Dual R (Dual R N))
              m :
            Dual R (Dual R N)) :
          (a : Dual R N) → R)
        f :
      R)

Tactic:
DFunLike.congr_arg f (e.apply_symm_apply m).symm

Premises used: LinearEquiv.apply_symm_apply, Eq.symm, DFunLike.congr_arg
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsReflexive R M
e : M ≃ₗ[R] N
ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap
m : N
f : Dual R N
⊢ Eq.{u_3 + 1} (α := R)
    ((((Dual.eval R N : (a : N) → Dual R (Dual R N)) m : Dual R (Dual R N)) : (a : Dual R N) → R) f : R)
    (((((↑ed.symm : Dual R (Dual R M) →ₗ[R] Dual R (Dual R N)) ∘ₗ Dual.eval R M ∘ₗ (↑e.symm : N →ₗ[R] M) :
                (a : N) → Dual R (Dual R N))
              m :
            Dual R (Dual R N)) :
          (a : Dual R N) → R)
        f :
      R)

Tactic:
exact DFunLike.congr_arg f (e.apply_symm_apply m).symm

Premises used: LinearEquiv.apply_symm_apply, Eq.symm, DFunLike.congr_arg
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsReflexive R M
e : M ≃ₗ[R] N
ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap
⊢ Dual.eval R N = (↑ed.symm : Dual R (Dual R M) →ₗ[R] Dual R (Dual R N)) ∘ₗ Dual.eval R M ∘ₗ (↑e.symm : N →ₗ[R] M)

Tactic:
have : Dual.eval R N = ed.symm.comp ((Dual.eval R M).comp e.symm.toLinearMap) := by
      ext m f
      exact DFunLike.congr_arg f (e.apply_symm_apply m).symm
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsReflexive R M
e : M ≃ₗ[R] N
ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap
this : Dual.eval R N = (↑ed.symm : Dual R (Dual R M) →ₗ[R] Dual R (Dual R N)) ∘ₗ Dual.eval R M ∘ₗ (↑e.symm : N →ₗ[R] M)
simp :
  Bijective (α := N) (β := Dual R (Dual R M))
    (Function.comp (β := M) (⇑(Dual.eval R M) : (a : M) → Dual R (Dual R M)) (⇑e.symm : (a : N) → M))
⊢ Bijective (α := N) (β := Dual R (Dual R N)) (⇑(Dual.eval R N) : (a : N) → Dual R (Dual R N))

Tactic:
simp only [this,
      coe_comp, LinearEquiv.coe_coe, EquivLike.comp_bijective]

Premises used: EquivLike.comp_bijective, LinearMap.coe_comp, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsReflexive R M
e : M ≃ₗ[R] N
ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap
this : Dual.eval R N = (↑ed.symm : Dual R (Dual R M) →ₗ[R] Dual R (Dual R N)) ∘ₗ Dual.eval R M ∘ₗ (↑e.symm : N →ₗ[R] M)
⊢ Bijective (α := N) (β := Dual R (Dual R M))
    (Function.comp (β := M) (⇑(Dual.eval R M) : (a : M) → Dual R (Dual R M)) (⇑e.symm : (a : N) → M))

Tactic:
Bijective.comp (bijective_dual_eval R M) (LinearEquiv.bijective _)

Premises used: LinearEquiv.bijective, Module.bijective_dual_eval, Function.Bijective.comp
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsReflexive R M
e : M ≃ₗ[R] N
ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap
this : Dual.eval R N = (↑ed.symm : Dual R (Dual R M) →ₗ[R] Dual R (Dual R N)) ∘ₗ Dual.eval R M ∘ₗ (↑e.symm : N →ₗ[R] M)
⊢ Bijective (α := N) (β := Dual R (Dual R M))
    (Function.comp (β := M) (⇑(Dual.eval R M) : (a : M) → Dual R (Dual R M)) (⇑e.symm : (a : N) → M))

Tactic:
exact Bijective.comp (bijective_dual_eval R M) (LinearEquiv.bijective _)

Premises used: LinearEquiv.bijective, Module.bijective_dual_eval, Function.Bijective.comp
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
K : Type u_1
V : Type u_2
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
R : Type u_3
M : Type u_4
N : Type u_5
inst_3 : CommSemiring R
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : Module R M
inst_7 : Module R N
inst_8 : IsReflexive R M
⊢ IsReflexive.{u_3, u_4} R Mᵐᵒᵖ

Tactic:
equiv <| MulOpposite.opLinearEquiv _

Premises used: MulOpposite.opLinearEquiv, Module.equiv
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
K : Type u_1
V : Type u_2
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
R : Type u_3
M : Type u_4
N : Type u_5
inst_3 : CommSemiring R
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : Module R M
inst_7 : Module R N
inst_8 : IsReflexive R M
r : R
hr : IsRegular r
m₁ m₂ : M
hm : Eq.{u_4 + 1} (α := M) ((fun (x : M) ↦ r • x) m₁) ((fun (x : M) ↦ r • x) m₂)
h :
  ∀ (n : Dual R M),
    Eq.{u_3 + 1} (α := R)
      ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) m₁ : Dual R (Dual R M)) : (a : Dual R M) → R) n : R)
      ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) m₂ : Dual R (Dual R M)) : (a : Dual R M) → R) n : R)
⊢ Eq (α := Dual R (Dual R M)) ((Dual.eval R M : (a : M) → Dual R (Dual R M)) m₁ : Dual R (Dual R M))
    ((Dual.eval R M : (a : M) → Dual R (Dual R M)) m₂ : Dual R (Dual R M))

Tactic:
ext n
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
K : Type u_1
V : Type u_2
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
R : Type u_3
M : Type u_4
N : Type u_5
inst_3 : CommSemiring R
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : Module R M
inst_7 : Module R N
inst_8 : IsReflexive R M
r : R
hr : IsRegular r
m₁ m₂ : M
hm : Eq.{u_4 + 1} (α := M) ((fun (x : M) ↦ r • x) m₁) ((fun (x : M) ↦ r • x) m₂)
n : Dual R M
⊢ Eq.{u_3 + 1} (α := R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) m₁ : Dual R (Dual R M)) : (a : Dual R M) → R) n : R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) m₂ : Dual R (Dual R M)) : (a : Dual R M) → R) n : R)

Tactic:
simpa [hr.1.eq_iff] using congr(n $hm)

Premises used: Function.Injective.eq_iff, IsRegular.left
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
W : Submodule R M
⊢ W.dualRestrict = W.subtype.dualMap

Tactic:
rfl

Premises used: LinearMap.domRestrict, Submodule.dualRestrict, LinearMap.domRestrict', LinearMap.dualMap, rfl
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
W : Submodule R M
φ : Dual R M
x : ↥W
⊢ Eq.{u_1 + 1} (α := R)
    ((((W.dualRestrict : (a : Dual R M) → Dual R ↥W) φ : Dual.{u_1, u_2} R ↥W) : (a : ↥W) → R) x : R)
    ((φ : (a : M) → R) (↑x : M) : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
W : Submodule R M
φ : Dual R M
simp_rw : φ ∈ W.dualRestrict.ker ↔ ∀ w ∈ W, Eq.{u_1 + 1} (α := R) ((φ : (a : M) → R) w : R) (0 : R)
simp_rw₁ :
  Eq (α := Dual.{u_1, u_2} R ↥W) ((W.dualRestrict : (a : Dual R M) → Dual R ↥W) φ : Dual.{u_1, u_2} R ↥W)
      (0 : Dual.{u_1, u_2} R ↥W) ↔
    ∀ w ∈ W, Eq.{u_1 + 1} (α := R) ((φ : (a : M) → R) w : R) (0 : R)
simp_rw₂ :
  (∀ (x : ↥W),
      Eq.{u_1 + 1} (α := R)
        ((((W.dualRestrict : (a : Dual R M) → Dual R ↥W) φ : Dual.{u_1, u_2} R ↥W) : (a : ↥W) → R) x : R)
        ((0 : (a : ↥W) → R) x : R)) ↔
    ∀ w ∈ W, Eq.{u_1 + 1} (α := R) ((φ : (a : M) → R) w : R) (0 : R)
simp_rw₃ :
  (∀ (x : ↥W), Eq.{u_1 + 1} (α := R) ((φ : (a : M) → R) (↑x : M) : R) ((0 : (a : ↥W) → R) x : R)) ↔
    ∀ w ∈ W, Eq.{u_1 + 1} (α := R) ((φ : (a : M) → R) w : R) (0 : R)
simp_rw₄ :
  (∀ (a : M) (b : a ∈ W),
      Eq.{u_1 + 1} (α := R) ((φ : (a : M) → R) a : R)
        ((0 : (a : ↥W) → R) (Subtype.mk (p := fun (a : M) ↦ a ∈ W) a b) : R)) ↔
    ∀ w ∈ W, Eq.{u_1 + 1} (α := R) ((φ : (a : M) → R) w : R) (0 : R)
⊢ φ ∈ W.dualAnnihilator ↔ ∀ w ∈ W, Eq.{u_1 + 1} (α := R) ((φ : (a : M) → R) w : R) (0 : R)

Tactic:
simp_rw [dualAnnihilator, LinearMap.mem_ker, LinearMap.ext_iff, dualRestrict_apply,
    Subtype.forall, LinearMap.zero_apply]

Premises used: LinearMap.zero_apply, Submodule.dualAnnihilator, Subtype.forall, LinearMap.ext_iff, LinearMap.mem_ker, Submodule.dualRestrict_apply
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
W : Submodule R M
⊢ W.dualRestrict.ker = W.dualAnnihilator

Tactic:
rfl

Premises used: Submodule.dualAnnihilator, rfl
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Φ : Submodule R (Dual R M)
x : M
simp_rw : x ∈ comap (Dual.eval R M) Φ.dualAnnihilator ↔ ∀ φ ∈ Φ, Eq.{u_1 + 1} (α := R) ((φ : (a : M) → R) x : R) (0 : R)
simp_rw₁ :
  Membership.mem (α := Dual R (Dual R M)) Φ.dualAnnihilator
      ((Dual.eval R M : (a : M) → Dual R (Dual R M)) x : Dual R (Dual R M)) ↔
    ∀ φ ∈ Φ, Eq.{u_1 + 1} (α := R) ((φ : (a : M) → R) x : R) (0 : R)
simp_rw₂ :
  (∀ w ∈ Φ,
      Eq.{u_1 + 1} (α := R)
        ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) x : Dual R (Dual R M)) : (a : Dual R M) → R) w : R) (0 : R)) ↔
    ∀ φ ∈ Φ, Eq.{u_1 + 1} (α := R) ((φ : (a : M) → R) x : R) (0 : R)
⊢ x ∈ Φ.dualCoannihilator ↔ ∀ φ ∈ Φ, Eq.{u_1 + 1} (α := R) ((φ : (a : M) → R) x : R) (0 : R)

Tactic:
simp_rw [dualCoannihilator, mem_comap, mem_dualAnnihilator, Module.Dual.eval_apply]

Premises used: Submodule.dualCoannihilator, Submodule.mem_dualAnnihilator, Submodule.mem_comap, Module.Dual.eval_apply
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
W : Submodule R M
f : N →ₗ[R] M
x : Dual R N
⊢ x ∈ map f.dualMap W.dualAnnihilator → x ∈ (comap f W).dualAnnihilator

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Φ : Submodule R (Dual R M)
⊢ comap (Dual.eval R M) Φ.dualAnnihilator = Φ.dualCoannihilator

Tactic:
rfl

Premises used: Submodule.dualCoannihilator, rfl
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Φ : Submodule R (Dual R M)
⊢ map (Dual.eval R M) Φ.dualCoannihilator ≤ Φ.dualAnnihilator

Tactic:
map_le_iff_le_comap.mpr (comap_dualAnnihilator Φ).le

Premises used: Iff.mpr, Submodule.comap_dualAnnihilator, Eq.le, Submodule.map_le_iff_le_comap
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : Submodule R M
b : (Submodule R (Dual R M))ᵒᵈ
toDual :
  ∀ (a_1 : Submodule R (Dual R M)),
    LE.le (α := (Submodule R (Dual R M))ᵒᵈ)
        (((⇑OrderDual.toDual : (a : Submodule R (Dual R M)) → (Submodule R (Dual R M))ᵒᵈ) ∘ dualAnnihilator) a :
          (Submodule R (Dual R M))ᵒᵈ)
        ((OrderDual.toDual : (a : Submodule R (Dual R M)) → (Submodule R (Dual R M))ᵒᵈ) a_1 :
          (Submodule R (Dual R M))ᵒᵈ) ↔
      a ≤
        Function.comp (α := (Submodule R (Dual R M))ᵒᵈ) dualCoannihilator
          ((⇑OrderDual.ofDual : (a : (Submodule R (Dual R M))ᵒᵈ) → Submodule R (Dual R M)) :
            (a : (Submodule R (Dual R M))ᵒᵈ) → Submodule R (Dual R M))
          ((OrderDual.toDual : (a : Submodule R (Dual R M)) → (Submodule R (Dual R M))ᵒᵈ) a_1 :
            (Submodule R (Dual R M))ᵒᵈ)
⊢ ((⇑OrderDual.toDual : (a : Submodule R (Dual R M)) → (Submodule R (Dual R M))ᵒᵈ) ∘ dualAnnihilator) a ≤ b ↔
    a ≤ (dualCoannihilator ∘ (⇑OrderDual.ofDual : (a : (Submodule R (Dual R M))ᵒᵈ) → Submodule R (Dual R M))) b

Tactic:
induction b using OrderDual.rec
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : Submodule R M
a_1 : Submodule R (Dual R M)
toDual :
  (∀ ⦃x : Dual R M⦄, x ∈ a_1 → ∀ w ∈ a, Eq.{u_1 + 1} (α := R) ((x : (a : M) → R) w : R) (0 : R)) ↔
    ∀ ⦃x : M⦄, x ∈ a → ∀ φ ∈ a_1, Eq.{u_1 + 1} (α := R) ((φ : (a : M) → R) x : R) (0 : R)
⊢ LE.le (α := (Submodule R (Dual R M))ᵒᵈ)
      (((⇑OrderDual.toDual : (a : Submodule R (Dual R M)) → (Submodule R (Dual R M))ᵒᵈ) ∘ dualAnnihilator) a :
        (Submodule R (Dual R M))ᵒᵈ)
      ((OrderDual.toDual : (a : Submodule R (Dual R M)) → (Submodule R (Dual R M))ᵒᵈ) a_1 :
        (Submodule R (Dual R M))ᵒᵈ) ↔
    a ≤
      Function.comp (α := (Submodule R (Dual R M))ᵒᵈ) dualCoannihilator
        ((⇑OrderDual.ofDual : (a : (Submodule R (Dual R M))ᵒᵈ) → Submodule R (Dual R M)) :
          (a : (Submodule R (Dual R M))ᵒᵈ) → Submodule R (Dual R M))
        ((OrderDual.toDual : (a : Submodule R (Dual R M)) → (Submodule R (Dual R M))ᵒᵈ) a_1 :
          (Submodule R (Dual R M))ᵒᵈ)

Tactic:
simp only [Function.comp_apply, OrderDual.toDual_le_toDual, OrderDual.ofDual_toDual,
    SetLike.le_def, mem_dualAnnihilator, mem_dualCoannihilator]

Premises used: OrderDual.toDual_le_toDual, Submodule.mem_dualAnnihilator, SetLike.le_def, Submodule.mem_dualCoannihilator, Function.comp_apply, OrderDual.ofDual_toDual
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : Submodule R M
a_1 : Submodule R (Dual R M)
⊢ (∀ ⦃x : Dual R M⦄, x ∈ a_1 → ∀ w ∈ a, Eq.{u_1 + 1} (α := R) ((x : (a : M) → R) w : R) (0 : R)) ↔
    ∀ ⦃x : M⦄, x ∈ a → ∀ φ ∈ a_1, Eq.{u_1 + 1} (α := R) ((φ : (a : M) → R) x : R) (0 : R)

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
U : Submodule R (Dual R M)
V : Submodule R M
⊢ U ≤ V.dualAnnihilator ↔ V ≤ U.dualCoannihilator

Tactic:
(dualAnnihilator_gc R M).le_iff_le

Premises used: Set.Mem, GaloisConnection.le_iff_le, Submodule.dualAnnihilator_gc
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := Submodule R (Dual R M)) (dualAnnihilator ⊥) ⊤

Tactic:
(dualAnnihilator_gc R M).l_bot

Premises used: Set.Mem, LinearMap.ker, Submodule.dualAnnihilator, Submodule.dualAnnihilator_gc, Submodule.comap, GaloisConnection.l_bot, OrderDual