awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
simp [eq_bot_iff, SetLike.le_def, LinearMap.ext_iff]

Premises used: SetLike.le_def, LinearMap.ext_iff, eq_bot_iff
-- 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.{u_2 + 1} (α := Submodule R M) (dualCoannihilator ⊥) ⊤

Tactic:
(dualAnnihilator_gc R M).u_top

Premises used: Submodule.dualCoannihilator, Set.Mem, GaloisConnection.u_top, Submodule.dualAnnihilator_gc, Submodule.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
U V : Submodule R M
hUV : U ≤ V
⊢ V.dualAnnihilator ≤ U.dualAnnihilator

Tactic:
(dualAnnihilator_gc R M).monotone_l hUV

Premises used: Set.Mem, Submodule.dualAnnihilator_gc, GaloisConnection.monotone_l
-- 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 V : Submodule R (Dual R M)
hUV : U ≤ V
⊢ V.dualCoannihilator ≤ U.dualCoannihilator

Tactic:
(dualAnnihilator_gc R M).monotone_u hUV

Premises used: GaloisConnection.monotone_u, Set.Mem, 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
U : Submodule R M
⊢ U ≤ U.dualAnnihilator.dualCoannihilator

Tactic:
(dualAnnihilator_gc R M).le_u_l U

Premises used: Set.Mem, LinearMap.ker, Submodule.dualAnnihilator, GaloisConnection.le_u_l, Submodule.dualAnnihilator_gc, Submodule.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
U : Submodule R (Dual R M)
⊢ U ≤ U.dualCoannihilator.dualAnnihilator

Tactic:
(dualAnnihilator_gc R M).l_u_le U

Premises used: Submodule.dualCoannihilator, Set.Mem, Submodule.dualAnnihilator_gc, Submodule.comap, GaloisConnection.l_u_le
-- 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 M
⊢ U.dualAnnihilator.dualCoannihilator.dualAnnihilator = U.dualAnnihilator

Tactic:
(dualAnnihilator_gc R M).l_u_l_eq_l U

Premises used: Submodule.dualCoannihilator, Set.Mem, LinearMap.ker, GaloisConnection.l_u_l_eq_l, Submodule.dualAnnihilator, Submodule.dualAnnihilator_gc, Submodule.comap, OrderDual
-- 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)
⊢ U.dualCoannihilator.dualAnnihilator.dualCoannihilator = U.dualCoannihilator

Tactic:
(dualAnnihilator_gc R M).u_l_u_eq_u U

Premises used: Submodule.dualCoannihilator, Set.Mem, LinearMap.ker, Submodule.dualAnnihilator, Submodule.dualAnnihilator_gc, Submodule.comap, GaloisConnection.u_l_u_eq_u
-- 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 V : Submodule R M
⊢ (U ⊔ V).dualAnnihilator = U.dualAnnihilator ⊓ V.dualAnnihilator

Tactic:
(dualAnnihilator_gc R M).l_sup

Premises used: LinearMap.ker, Submodule.dualAnnihilator, Submodule.dualAnnihilator_gc, Submodule.comap, OrderDual, GaloisConnection.l_sup
-- 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 V : Submodule R (Dual R M)
⊢ (U ⊔ V).dualCoannihilator = U.dualCoannihilator ⊓ V.dualCoannihilator

Tactic:
(dualAnnihilator_gc R M).u_inf

Premises used: Submodule.dualCoannihilator, Set.Mem, Submodule.dualAnnihilator_gc, GaloisConnection.u_inf, Submodule.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
ι : Sort u_3
U : ι → Submodule R M
⊢ Eq (α := Submodule R (Dual R M)) (dualAnnihilator (⨆ (i : ι), U i)) (⨅ (i : ι), (U i).dualAnnihilator)

Tactic:
(dualAnnihilator_gc R M).l_iSup

Premises used: iInf, Set.Mem, LinearMap.ker, Submodule.dualAnnihilator, GaloisConnection.l_iSup, Submodule.dualAnnihilator_gc, Submodule.comap, OrderDual
-- 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
ι : Sort u_3
U : ι → Submodule R (Dual R M)
⊢ Eq.{u_2 + 1} (α := Submodule R M) (dualCoannihilator (⨆ (i : ι), U i)) (⨅ (i : ι), (U i).dualCoannihilator)

Tactic:
(dualAnnihilator_gc R M).u_iInf

Premises used: iInf, Submodule.dualCoannihilator, Set.Mem, iSup, setOf, GaloisConnection.u_iInf, Submodule.dualAnnihilator_gc, Submodule.comap, OrderDual
-- 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 V : Submodule R M
rw : U ⊓ V ≤ U.dualAnnihilator.dualCoannihilator ⊓ V.dualAnnihilator.dualCoannihilator
⊢ U.dualAnnihilator ⊔ V.dualAnnihilator ≤ (U ⊓ V).dualAnnihilator

Tactic:
rw [le_dualAnnihilator_iff_le_dualCoannihilator, dualCoannihilator_sup_eq]

Premises used: Submodule.dualCoannihilator_sup_eq, Submodule.le_dualAnnihilator_iff_le_dualCoannihilator
-- 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 V : Submodule R M
h₁ : U ≤ U.dualAnnihilator.dualCoannihilator
h₂ : V ≤ V.dualAnnihilator.dualCoannihilator
⊢ U ⊓ V ≤ U.dualAnnihilator.dualCoannihilator ⊓ V.dualAnnihilator.dualCoannihilator

Tactic:
apply inf_le_inf

Premises used: inf_le_inf
-- 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 V : Submodule R M
⊢ U ≤ U.dualAnnihilator.dualCoannihilator

Tactic:
le_dualAnnihilator_dualCoannihilator _

Premises used: Submodule.le_dualAnnihilator_dualCoannihilator
-- 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 V : Submodule R M
⊢ U ≤ U.dualAnnihilator.dualCoannihilator

Tactic:
exact le_dualAnnihilator_dualCoannihilator _

Premises used: Submodule.le_dualAnnihilator_dualCoannihilator
-- 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 V : Submodule R M
⊢ V ≤ V.dualAnnihilator.dualCoannihilator

Tactic:
le_dualAnnihilator_dualCoannihilator _

Premises used: Submodule.le_dualAnnihilator_dualCoannihilator
-- 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 V : Submodule R M
⊢ V ≤ V.dualAnnihilator.dualCoannihilator

Tactic:
exact le_dualAnnihilator_dualCoannihilator _

Premises used: Submodule.le_dualAnnihilator_dualCoannihilator
-- 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
ι : Sort u_3
U : ι → Submodule R M
rw : LE.le.{u_2} (α := Submodule R M) (⨅ (i : ι), U i) (⨅ (i : ι), (U i).dualAnnihilator.dualCoannihilator)
⊢ LE.le (α := Submodule R (Dual R M)) (⨆ (i : ι), (U i).dualAnnihilator) (dualAnnihilator (⨅ (i : ι), U i))

Tactic:
rw [le_dualAnnihilator_iff_le_dualCoannihilator, dualCoannihilator_iSup_eq]

Premises used: Submodule.dualCoannihilator_iSup_eq, Submodule.le_dualAnnihilator_iff_le_dualCoannihilator
-- 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
ι : Sort u_3
U : ι → Submodule R M
h : ∀ (i : ι), U i ≤ (U i).dualAnnihilator.dualCoannihilator
⊢ LE.le.{u_2} (α := Submodule R M) (⨅ (i : ι), U i) (⨅ (i : ι), (U i).dualAnnihilator.dualCoannihilator)

Tactic:
apply iInf_mono

Premises used: iInf_mono
-- 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
ι : Sort u_3
U : ι → Submodule R M
⊢ ∀ (i : ι), U i ≤ (U i).dualAnnihilator.dualCoannihilator

Tactic:
fun i : ι => le_dualAnnihilator_dualCoannihilator (U i)

Premises used: Submodule.le_dualAnnihilator_dualCoannihilator
-- 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
ι : Sort u_3
U : ι → Submodule R M
⊢ ∀ (i : ι), U i ≤ (U i).dualAnnihilator.dualCoannihilator

Tactic:
exact fun i : ι => le_dualAnnihilator_dualCoannihilator (U i)

Premises used: Submodule.le_dualAnnihilator_dualCoannihilator
-- 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
s : Set M
h :
  ∀ (f : Dual R M),
    f ∈ (↑(dualAnnihilator (span R s)) : Set (Dual R M)) ↔
      Membership.mem (γ := Set (Dual R M)) {f : M →ₗ[R] R | s ⊆ (↑f.ker : Set M)} f
⊢ (↑(dualAnnihilator (span R s)) : Set (Dual R M)) = {f : M →ₗ[R] R | s ⊆ (↑f.ker : Set M)}

Tactic:
ext f
-- 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
s : Set M
f : Dual R M
h :
  (∀ (w : M), Membership.mem (γ := Submodule R M) (span R s) w → w ∈ LinearMap.ker f) ↔ s ⊆ (↑(LinearMap.ker f) : Set M)
⊢ f ∈ (↑(dualAnnihilator (span R s)) : Set (Dual R M)) ↔
    Membership.mem (γ := Set (Dual R M)) {f : M →ₗ[R] R | s ⊆ (↑f.ker : Set M)} f

Tactic:
simp only [SetLike.mem_coe, mem_dualAnnihilator, Set.mem_setOf_eq, ← LinearMap.mem_ker]

Premises used: Submodule.mem_dualAnnihilator, Set.mem_setOf_eq, LinearMap.mem_ker, SetLike.mem_coe
-- 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
s : Set M
f : Dual R M
⊢ (∀ (w : M), Membership.mem (γ := Submodule R M) (span R s) w → w ∈ LinearMap.ker f) ↔ s ⊆ (↑(LinearMap.ker f) : Set M)

Tactic:
span_le

Premises used: Submodule.span_le
-- 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
s : Set M
f : Dual R M
⊢ (∀ (w : M), Membership.mem (γ := Submodule R M) (span R s) w → w ∈ LinearMap.ker f) ↔ s ⊆ (↑(LinearMap.ker f) : Set M)

Tactic:
exact span_le

Premises used: Submodule.span_le
-- 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
s : Set (Dual R M)
h :
  ∀ (x : M),
    x ∈ (↑(dualCoannihilator (span R s)) : Set M) ↔
      Membership.mem (γ := Set M) {x : M | ∀ f ∈ s, Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (0 : R)} x
⊢ (↑(dualCoannihilator (span R s)) : Set M) = {x : M | ∀ f ∈ s, Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (0 : R)}

Tactic:
ext x
-- 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
s : Set (Dual R M)
x : M
φ : M →ₗ[R] R
⊢ x ∈ φ.ker ↔
    Membership.mem (γ := Submodule R (Dual R M))
      (LinearMap.ker (R₂ := R) (M₂ := R) (τ₁₂ := RingHom.id R) ((Dual.eval R M : (a : M) → Dual R (Dual R M)) x)) φ

Tactic:
simp
-- 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
s : Set (Dual R M)
x : M
⊢ ∀ (φ : M →ₗ[R] R),
    x ∈ φ.ker ↔
      Membership.mem (γ := Submodule R (Dual R M))
        (LinearMap.ker (R₂ := R) (M₂ := R) (τ₁₂ := RingHom.id R) ((Dual.eval R M : (a : M) → Dual R (Dual R M)) x)) φ

Tactic:
have (φ : _) : x ∈ LinearMap.ker φ ↔ φ ∈ LinearMap.ker (Module.Dual.eval R M x) := by simp
-- 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
s : Set (Dual R M)
x : M
this :
  ∀ (φ : M →ₗ[R] R),
    x ∈ φ.ker ↔
      Membership.mem (γ := Submodule R (Dual R M))
        (LinearMap.ker (R₂ := R) (M₂ := R) (τ₁₂ := RingHom.id R) ((Dual.eval R M : (a : M) → Dual R (Dual R M)) x)) φ
h :
  (∀ (φ : Dual R M),
      Membership.mem (γ := Submodule R (Dual R M)) (span R s) φ →
        Membership.mem (γ := Submodule R (Dual R M))
          (LinearMap.ker (R₂ := R) (M₂ := R) (τ₁₂ := RingHom.id R) ((Dual.eval R M : (a : M) → Dual R (Dual R M)) x))
          φ) ↔
    ∀ f ∈ s,
      Membership.mem (γ := Submodule R (Dual R M))
        (LinearMap.ker (R₂ := R) (M₂ := R) (τ₁₂ := RingHom.id R) ((Dual.eval R M : (a : M) → Dual R (Dual R M)) x)) f
⊢ x ∈ (↑(dualCoannihilator (span R s)) : Set M) ↔
    Membership.mem (γ := Set M) {x : M | ∀ f ∈ s, Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (0 : R)} x

Tactic:
simp only [SetLike.mem_coe, mem_dualCoannihilator, Set.mem_setOf_eq, ← LinearMap.mem_ker, this]

Premises used: Set.mem_setOf_eq, LinearMap.mem_ker, Submodule.mem_dualCoannihilator, SetLike.mem_coe
-- 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
s : Set (Dual R M)
x : M
this :
  ∀ (φ : M →ₗ[R] R),
    x ∈ φ.ker ↔
      Membership.mem (γ := Submodule R (Dual R M))
        (LinearMap.ker (R₂ := R) (M₂ := R) (τ₁₂ := RingHom.id R) ((Dual.eval R M : (a : M) → Dual R (Dual R M)) x)) φ
⊢ (∀ (φ : Dual R M),
      Membership.mem (γ := Submodule R (Dual R M)) (span R s) φ →
        Membership.mem (γ := Submodule R (Dual R M))
          (LinearMap.ker (R₂ := R) (M₂ := R) (τ₁₂ := RingHom.id R) ((Dual.eval R M : (a : M) → Dual R (Dual R M)) x))
          φ) ↔
    ∀ f ∈ s,
      Membership.mem (γ := Submodule R (Dual R M))
        (LinearMap.ker (R₂ := R) (M₂ := R) (τ₁₂ := RingHom.id R) ((Dual.eval R M : (a : M) → Dual R (Dual R M)) x)) f

Tactic:
span_le

Premises used: Set.Mem, Set.Subset, Submodule.span_le
-- 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
s : Set (Dual R M)
x : M
this :
  ∀ (φ : M →ₗ[R] R),
    x ∈ φ.ker ↔
      Membership.mem (γ := Submodule R (Dual R M))
        (LinearMap.ker (R₂ := R) (M₂ := R) (τ₁₂ := RingHom.id R) ((Dual.eval R M : (a : M) → Dual R (Dual R M)) x)) φ
⊢ (∀ (φ : Dual R M),
      Membership.mem (γ := Submodule R (Dual R M)) (span R s) φ →
        Membership.mem (γ := Submodule R (Dual R M))
          (LinearMap.ker (R₂ := R) (M₂ := R) (τ₁₂ := RingHom.id R) ((Dual.eval R M : (a : M) → Dual R (Dual R M)) x))
          φ) ↔
    ∀ f ∈ s,
      Membership.mem (γ := Submodule R (Dual R M))
        (LinearMap.ker (R₂ := R) (M₂ := R) (τ₁₂ := RingHom.id R) ((Dual.eval R M : (a : M) → Dual R (Dual R M)) x)) f

Tactic:
exact span_le

Premises used: Submodule.span_le
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
f : M₁ →ₗ[R] M₂
h : ∀ (x : Dual R M₂), x ∈ f.dualMap.ker ↔ x ∈ f.range.dualAnnihilator
⊢ f.dualMap.ker = f.range.dualAnnihilator

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
f : M₁ →ₗ[R] M₂
x : Dual R M₂
h :
  Eq (α := Dual R M₁) ((f.dualMap : (a : Dual R M₂) → Dual R M₁) x : Dual R M₁) (0 : Dual R M₁) ↔
    x ∈ f.range.dualAnnihilator
h₁ :
  (∀ (x_1 : M₁),
      Eq.{u_1 + 1} (α := R) ((((f.dualMap : (a : Dual R M₂) → Dual R M₁) x : Dual R M₁) : (a : M₁) → R) x_1 : R)
        ((0 : (a : M₁) → R) x_1 : R)) ↔
    x ∈ f.range.dualAnnihilator
h₂ :
  (∀ (x_1 : M₁),
      Eq.{u_1 + 1} (α := R) ((((f.dualMap : (a : Dual R M₂) → Dual R M₁) x : Dual R M₁) : (a : M₁) → R) x_1 : R)
        ((0 : (a : M₁) → R) x_1 : R)) ↔
    ∀ w ∈ f.range, Eq.{u_1 + 1} (α := R) ((x : (a : M₂) → R) w : R) (0 : R)
h₃ :
  (∀ (x_1 : M₁),
      Eq.{u_1 + 1} (α := R) ((((f.dualMap : (a : Dual R M₂) → Dual R M₁) x : Dual R M₁) : (a : M₁) → R) x_1 : R)
        ((0 : (a : M₁) → R) x_1 : R)) ↔
    ∀ w ∈ (↑f.range : Set M₂), Eq.{u_1 + 1} (α := R) ((x : (a : M₂) → R) w : R) (0 : R)
h₄ :
  (∀ (x_1 : M₁),
      Eq.{u_1 + 1} (α := R) ((((f.dualMap : (a : Dual R M₂) → Dual R M₁) x : Dual R M₁) : (a : M₁) → R) x_1 : R)
        ((0 : (a : M₁) → R) x_1 : R)) ↔
    ∀ (w : M₂),
      Membership.mem (γ := Set M₂) (Set.range.{u_3, u_2 + 1} (ι := M₁) (⇑f : (a : M₁) → M₂)) w →
        Eq.{u_1 + 1} (α := R) ((x : (a : M₂) → R) w : R) (0 : R)
h₅ :
  (∀ (x_1 : M₁),
      Eq.{u_1 + 1} (α := R) ((((f.dualMap : (a : Dual R M₂) → Dual R M₁) x : Dual R M₁) : (a : M₁) → R) x_1 : R)
        ((0 : (a : M₁) → R) x_1 : R)) ↔
    ∀ (i : M₁), Eq.{u_1 + 1} (α := R) ((x : (a : M₂) → R) ((f : (a : M₁) → M₂) i : M₂) : R) (0 : R)
h₆ :
  (∀ (x_1 : M₁),
      Eq.{u_1 + 1} (α := R) ((x : (a : M₂) → R) ((f : (a : M₁) → M₂) x_1 : M₂) : R) ((0 : (a : M₁) → R) x_1 : R)) ↔
    ∀ (i : M₁), Eq.{u_1 + 1} (α := R) ((x : (a : M₂) → R) ((f : (a : M₁) → M₂) i : M₂) : R) (0 : R)
⊢ x ∈ f.dualMap.ker ↔ x ∈ f.range.dualAnnihilator

Tactic:
simp_rw [mem_ker, LinearMap.ext_iff, Submodule.mem_dualAnnihilator,
    ← SetLike.mem_coe, coe_range, Set.forall_mem_range, dualMap_apply, zero_apply]

Premises used: LinearMap.zero_apply, Set.forall_mem_range, Submodule.mem_dualAnnihilator, LinearMap.ext_iff, LinearMap.coe_range, LinearMap.mem_ker, SetLike.mem_coe, LinearMap.dualMap_apply
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
f : M₁ →ₗ[R] M₂
ψ : Dual R M₂
⊢ Membership.mem (α := Dual R M₁) f.ker.dualAnnihilator ((f.dualMap : (a : Dual R M₂) → Dual R M₁) ψ : Dual R M₁)

Tactic:
simp +contextual
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
h : ∀ (x : Dual R M'), x ∈ f.dualMap.ker ↔ x ∈ (Dual.eval R M' ∘ₗ f).range.dualCoannihilator
⊢ f.dualMap.ker = (Dual.eval R M' ∘ₗ f).range.dualCoannihilator

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
x : Dual R M'
⊢ x ∈ f.dualMap.ker ↔ x ∈ (Dual.eval R M' ∘ₗ f).range.dualCoannihilator

Tactic:
simp [LinearMap.ext_iff (f := dualMap f x)]

Premises used: LinearMap.ext_iff
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
B : M →ₗ[R] M' →ₗ[R] R
h : ∀ (x : M'), x ∈ B.range.dualCoannihilator ↔ x ∈ B.flip.ker
⊢ B.range.dualCoannihilator = B.flip.ker

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
B : M →ₗ[R] M' →ₗ[R] R
x : M'
⊢ x ∈ B.range.dualCoannihilator ↔ x ∈ B.flip.ker

Tactic:
simp [LinearMap.ext_iff (f := B.flip x)]

Premises used: LinearMap.ext_iff
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_4
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
φ : Dual R M
ψ : Dual R M'
⊢ (dualProdDualEquivDual R M M' : (a : Dual R M × Dual R M') → Dual R (M × M')) (φ, ψ) = LinearMap.coprod φ ψ

Tactic:
rfl

Premises used: LinearMap.coprod, rfl
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
⊢ Nonempty (V ≃ₗ[K] Dual K V) ↔ FiniteDimensional K V

Tactic:
⟨fun ⟨e⟩ ↦ ?_, fun h ↦ ⟨(Module.Free.chooseBasis K V).toDualEquiv⟩⟩

Premises used: _private.0.Basis.linearEquiv_dual_iff_finiteDimensional.match_1, Nonempty.intro, FiniteDimensional, Iff.intro, Module.Free.chooseBasis, Module.Basis.toDualEquiv
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
refine : Nonempty (V ≃ₗ[K] Dual K V) → ∀ (e : V ≃ₗ[K] Dual K V), FiniteDimensional K V
⊢ Nonempty (V ≃ₗ[K] Dual K V) ↔ FiniteDimensional K V

Tactic:
refine ⟨fun ⟨e⟩ ↦ ?_, fun h ↦ ⟨(Module.Free.chooseBasis K V).toDualEquiv⟩⟩
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : Nonempty (V ≃ₗ[K] Dual K V)
e : V ≃ₗ[K] Dual K V
rw : Module.rank K V < ℵ₀
⊢ FiniteDimensional K V

Tactic:
rw [FiniteDimensional, ← Module.rank_lt_aleph0_iff]

Premises used: Module.rank_lt_aleph0_iff, FiniteDimensional
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : Nonempty (V ≃ₗ[K] Dual K V)
e : V ≃ₗ[K] Dual K V
by_contra! : ∀ (this : ℵ₀ ≤ Module.rank K V), False
⊢ Module.rank K V < ℵ₀

Tactic:
by_contra!
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : Nonempty (V ≃ₗ[K] Dual K V)
e : V ≃ₗ[K] Dual K V
this : ℵ₀ ≤ Module.rank K V
apply : lift.{uK, uV} (Module.rank K V) = Module.rank K (V →ₗ[K] K)
⊢ False

Tactic:
apply (lift_rank_lt_rank_dual this).ne

Premises used: lift_rank_lt_rank_dual, LT.lt.ne
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : Nonempty (V ≃ₗ[K] Dual K V)
e : V ≃ₗ[K] Dual K V
this : ℵ₀ ≤ Module.rank K V
⊢ lift.{max uK uV, uV} (Module.rank K V) = lift.{uV, max uK uV} (Module.rank K (Dual K V))

Tactic:
have := e.lift_rank_eq
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : Nonempty (V ≃ₗ[K] Dual K V)
e : V ≃ₗ[K] Dual K V
this_1 : ℵ₀ ≤ Module.rank K V
this : lift.{max uK uV, uV} (Module.rank K V) = lift.{uV, max uK uV} (Module.rank K (Dual K V))
rwa :
  ∀ (this : lift.{uK, uV} (Module.rank K V) = lift.{uV, max uK uV} (Module.rank K (Dual K V))),
    lift.{uK, uV} (Module.rank K V) = Module.rank K (V →ₗ[K] K)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : lift.{uK, uV} (Module.rank K V) = Module.rank K (Dual K V)),
    lift.{uK, uV} (Module.rank K V) = Module.rank K (V →ₗ[K] K)
⊢ lift.{uK, uV} (Module.rank K V) = Module.rank K (V →ₗ[K] K)

Tactic:
rwa [lift_umax, lift_id'.{uV}] at this

Premises used: Cardinal.lift_umax
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type uR
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite ι
b : Basis ι R M
rw : Module.rank R (Dual R M) = lift.{max uM uR, uM} (Module.rank R M)
rw₁ : Module.rank R (Dual R M) = lift.{uM, max uM uR} (Module.rank R (Dual R M))
rw₂ rw₃ : Module.rank R (Dual R M) = Module.rank R (Dual R M)
⊢ Module.rank R (Dual R M) = lift.{uR, uM} (Module.rank R M)

Tactic:
rw [← lift_umax.{uM, uR}, b.toDualEquiv.lift_rank_eq, lift_id'.{uM, uR}]

Premises used: LinearEquiv.lift_rank_eq, Module.Basis.toDualEquiv
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type uR
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite ι
b : Basis ι R M
classical : Module.rank R (Dual R M) = lift.{max uM uR, uM} (Module.rank R M)
classical₁ : Module.rank R (Dual R M) = lift.{uM, max uM uR} (Module.rank R (Dual R M))
classical₂ classical₃ : Module.rank R (Dual R M) = Module.rank R (Dual R M)
⊢ Module.rank R (Dual R M) = lift.{uR, uM} (Module.rank R M)

Tactic:
classical rw [← lift_umax.{uM, uR}, b.toDualEquiv.lift_rank_eq, lift_id'.{uM, uR}]
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type uR
M : Type uM
K : Type uK
V : Type uV
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Free R M
⊢ Free R (Dual R M)

Tactic:
Free.of_basis (Free.chooseBasis R M).dualBasis

Premises used: Module.Free.of_basis, Module.Basis.dualBasis, Module.Free.chooseBasis