awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
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
have 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
Tactic: refine ⟨fun hfg => ?_, fun a ↦ congrArg (Dual.eval R M').comp
    (congrFun (congrArg LinearMap.comp a) (evalEquiv R M).symm.toLinearMap)⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
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)
have 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)
Tactic: ext m f
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (hypothesis)
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
⊢ Bijective (α := N) (β := Dual R (Dual R N)) (⇑(Dual.eval R N) : (a : N) → Dual R (Dual R N))
have 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)
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
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 N)) (⇑(Dual.eval R N) : (a : N) → Dual R (Dual R N))
have 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))
Tactic: simp only [this,
      coe_comp, LinearEquiv.coe_coe, EquivLike.comp_bijective]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
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₂)
⊢ 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))
have 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)
Tactic: ext n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
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
⊢ φ ∈ W.dualAnnihilator ↔ ∀ w ∈ W, Eq.{u_1 + 1} (α := R) ((φ : (a : M) → R) w : R) (0 : R)
have simp_rw : φ ∈ W.dualRestrict.ker ↔ ∀ 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
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)
⊢ φ ∈ W.dualAnnihilator ↔ ∀ w ∈ W, Eq.{u_1 + 1} (α := R) ((φ : (a : M) → R) w : R) (0 : R)
have 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)
Tactic: simp_rw [dualAnnihilator, LinearMap.mem_ker, LinearMap.ext_iff, dualRestrict_apply,
    Subtype.forall, LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
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)
⊢ φ ∈ W.dualAnnihilator ↔ ∀ w ∈ W, Eq.{u_1 + 1} (α := R) ((φ : (a : M) → R) w : R) (0 : R)
have 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)
Tactic: simp_rw [dualAnnihilator, LinearMap.mem_ker, LinearMap.ext_iff, dualRestrict_apply,
    Subtype.forall, LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
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)
⊢ φ ∈ W.dualAnnihilator ↔ ∀ w ∈ W, Eq.{u_1 + 1} (α := R) ((φ : (a : M) → R) w : R) (0 : R)
have 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)
Tactic: simp_rw [dualAnnihilator, LinearMap.mem_ker, LinearMap.ext_iff, dualRestrict_apply,
    Subtype.forall, LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
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)
⊢ φ ∈ W.dualAnnihilator ↔ ∀ w ∈ W, Eq.{u_1 + 1} (α := R) ((φ : (a : M) → R) w : R) (0 : R)
have 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)
Tactic: simp_rw [dualAnnihilator, LinearMap.mem_ker, LinearMap.ext_iff, dualRestrict_apply,
    Subtype.forall, LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
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
⊢ x ∈ Φ.dualCoannihilator ↔ ∀ φ ∈ Φ, Eq.{u_1 + 1} (α := R) ((φ : (a : M) → R) x : R) (0 : R)
have simp_rw : x ∈ comap (Dual.eval R M) Φ.dualAnnihilator ↔ ∀ φ ∈ Φ, Eq.{u_1 + 1} (α := R) ((φ : (a : M) → R) x : R) (0 : R)
Tactic: simp_rw [dualCoannihilator, mem_comap, mem_dualAnnihilator, Module.Dual.eval_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
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)
⊢ x ∈ Φ.dualCoannihilator ↔ ∀ φ ∈ Φ, Eq.{u_1 + 1} (α := R) ((φ : (a : M) → R) x : R) (0 : R)
have 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)
Tactic: simp_rw [dualCoannihilator, mem_comap, mem_dualAnnihilator, Module.Dual.eval_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
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)
⊢ x ∈ Φ.dualCoannihilator ↔ ∀ φ ∈ Φ, Eq.{u_1 + 1} (α := R) ((φ : (a : M) → R) x : R) (0 : R)
have 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)
Tactic: simp_rw [dualCoannihilator, mem_comap, mem_dualAnnihilator, Module.Dual.eval_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
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))ᵒᵈ
⊢ ((⇑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
have 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))ᵒᵈ)
Tactic: induction b using OrderDual.rec
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
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)
⊢ 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))ᵒᵈ)
have 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)
Tactic: simp only [Function.comp_apply, OrderDual.toDual_le_toDual, OrderDual.ofDual_toDual,
    SetLike.le_def, mem_dualAnnihilator, mem_dualCoannihilator]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
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.dualAnnihilator ⊔ V.dualAnnihilator ≤ (U ⊓ V).dualAnnihilator
have rw : U ⊓ V ≤ U.dualAnnihilator.dualCoannihilator ⊓ V.dualAnnihilator.dualCoannihilator
Tactic: rw [le_dualAnnihilator_iff_le_dualCoannihilator, dualCoannihilator_sup_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
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 ≤ U.dualAnnihilator.dualCoannihilator ⊓ V.dualAnnihilator.dualCoannihilator
have h₁ : U ≤ U.dualAnnihilator.dualCoannihilator
Tactic: apply inf_le_inf
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
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
⊢ U ⊓ V ≤ U.dualAnnihilator.dualCoannihilator ⊓ V.dualAnnihilator.dualCoannihilator
have h₂ : V ≤ V.dualAnnihilator.dualCoannihilator
Tactic: apply inf_le_inf
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
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
⊢ LE.le (α := Submodule R (Dual R M)) (⨆ (i : ι), (U i).dualAnnihilator) (dualAnnihilator (⨅ (i : ι), U i))
have rw : LE.le.{u_2} (α := Submodule R M) (⨅ (i : ι), U i) (⨅ (i : ι), (U i).dualAnnihilator.dualCoannihilator)
Tactic: rw [le_dualAnnihilator_iff_le_dualCoannihilator, dualCoannihilator_iSup_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
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
⊢ LE.le.{u_2} (α := Submodule R M) (⨅ (i : ι), U i) (⨅ (i : ι), (U i).dualAnnihilator.dualCoannihilator)
have h : ∀ (i : ι), U i ≤ (U i).dualAnnihilator.dualCoannihilator
Tactic: apply iInf_mono
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
⊢ (↑(dualAnnihilator (span R s)) : Set (Dual R M)) = {f : M →ₗ[R] R | s ⊆ (↑f.ker : Set M)}
have 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
Tactic: ext f
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
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
⊢ 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
have h : (∀ (w : M), Membership.mem (γ := Submodule R M) (span R s) w → w ∈ LinearMap.ker f) ↔ s ⊆ (↑(LinearMap.ker f) : Set M)
Tactic: simp only [SetLike.mem_coe, mem_dualAnnihilator, Set.mem_setOf_eq, ← LinearMap.mem_ker]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
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)
⊢ (↑(dualCoannihilator (span R s)) : Set M) = {x : M | ∀ f ∈ s, Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (0 : R)}
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (hypothesis)
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
⊢ 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
have 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)) φ
Tactic: have (φ : _) : x ∈ LinearMap.ker φ ↔ φ ∈ LinearMap.ker (Module.Dual.eval R M x) := by simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
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)) φ
⊢ 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
have 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
Tactic: simp only [SetLike.mem_coe, mem_dualCoannihilator, Set.mem_setOf_eq, ← LinearMap.mem_ker, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
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₂
⊢ f.dualMap.ker = f.range.dualAnnihilator
have h : ∀ (x : Dual R M₂), x ∈ f.dualMap.ker ↔ x ∈ f.range.dualAnnihilator
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
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 ∈ f.range.dualAnnihilator
have 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
Tactic: simp_rw [mem_ker, LinearMap.ext_iff, Submodule.mem_dualAnnihilator,
    ← SetLike.mem_coe, coe_range, Set.forall_mem_range, dualMap_apply, zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
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
⊢ x ∈ f.dualMap.ker ↔ x ∈ f.range.dualAnnihilator
have 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
Tactic: simp_rw [mem_ker, LinearMap.ext_iff, Submodule.mem_dualAnnihilator,
    ← SetLike.mem_coe, coe_range, Set.forall_mem_range, dualMap_apply, zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
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
⊢ x ∈ f.dualMap.ker ↔ x ∈ f.range.dualAnnihilator
have 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)
Tactic: simp_rw [mem_ker, LinearMap.ext_iff, Submodule.mem_dualAnnihilator,
    ← SetLike.mem_coe, coe_range, Set.forall_mem_range, dualMap_apply, zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
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)
⊢ x ∈ f.dualMap.ker ↔ x ∈ f.range.dualAnnihilator
have 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)
Tactic: simp_rw [mem_ker, LinearMap.ext_iff, Submodule.mem_dualAnnihilator,
    ← SetLike.mem_coe, coe_range, Set.forall_mem_range, dualMap_apply, zero_apply]