awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
N : Submodule R M
r : R
a : M
ha :
  Membership.mem (γ := Set M)
    {x : M |
      ∀ y ∈ N,
        Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S) 1
          ((((B : (a : M) → M →ₗ[S] S) x : M →ₗ[S] S) : (a : M) → S) y : S)}
    a
y : M
hy : y ∈ N
h :
  (((B : (a : M) → M →ₗ[S] S) (r • a) : M →ₗ[S] S) : (a : M) → S) y =
    HSMul.hSMul (β := S) r ((((B : (a : M) → M →ₗ[S] S) a : M →ₗ[S] S) : (a : M) → S) y : S)
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S) 1
    ((((B : (a : M) → M →ₗ[S] S) (r • a) : M →ₗ[S] S) : (a : M) → S) y : S)

Tactic:
convert! (1 : Submodule R S).smul_mem r (ha y hy)

Premises used: OfNat.ofNat, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
N : Submodule R M
r : R
a : M
ha :
  Membership.mem (γ := Set M)
    {x : M |
      ∀ y ∈ N,
        Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S) 1
          ((((B : (a : M) → M →ₗ[S] S) x : M →ₗ[S] S) : (a : M) → S) y : S)}
    a
y : M
hy : y ∈ N
h :
  (((B : (a : M) → M →ₗ[S] S) (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) r : S) a) :
          M →ₗ[S] S) :
        (a : M) → S)
      y =
    HSMul.hSMul (β := S) r ((((B : (a : M) → M →ₗ[S] S) a : M →ₗ[S] S) : (a : M) → S) y : S)
⊢ (((B : (a : M) → M →ₗ[S] S) (r • a) : M →ₗ[S] S) : (a : M) → S) y =
    HSMul.hSMul (β := S) r ((((B : (a : M) → M →ₗ[S] S) a : M →ₗ[S] S) : (a : M) → S) y : S)

Tactic:
rw [← IsScalarTower.algebraMap_smul S r a]

Premises used: IsScalarTower.algebraMap_smul
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
N : Submodule R M
r : R
a : M
ha :
  Membership.mem (γ := Set M)
    {x : M |
      ∀ y ∈ N,
        Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S) 1
          ((((B : (a : M) → M →ₗ[S] S) x : M →ₗ[S] S) : (a : M) → S) y : S)}
    a
y : M
hy : y ∈ N
⊢ (((B : (a : M) → M →ₗ[S] S) (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) r : S) a) :
          M →ₗ[S] S) :
        (a : M) → S)
      y =
    HSMul.hSMul (β := S) r ((((B : (a : M) → M →ₗ[S] S) a : M →ₗ[S] S) : (a : M) → S) y : S)

Tactic:
simp only [algebraMap_smul, map_smul_of_tower, LinearMap.smul_apply]

Premises used: LinearMap.smul_apply, algebraMap_smul, LinearMap.map_smul_of_tower
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
Goal:
R : Type u_1
S : Type u_3
M : Type u_2
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
N : Submodule R M
x : M
⊢ x ∈ B.dualSubmodule N ↔
    ∀ y ∈ N,
      Membership.mem.{u_3, u_3} (α := S) (γ := Submodule R S) 1
        ((((B : (a : M) → M →ₗ[S] S) x : M →ₗ[S] S) : (a : M) → S) y : S)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
Goal:
R : Type u_1
S : Type u_3
M : Type u_2
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
N₁ N₂ : Submodule R M
simp :
  (∀ x ∈ N₁,
      ∀ y ∈ N₂,
        ∃ (y_1 : R),
          Eq.{u_3 + 1} (α := S) ((algebraMap R S : (a : R) → S) y_1 : S)
            ((((B : (a : M) → M →ₗ[S] S) y : M →ₗ[S] S) : (a : M) → S) x : S)) ↔
    ∀ x ∈ N₂,
      ∀ y ∈ N₁,
        ∃ (y_1 : R),
          Eq.{u_3 + 1} (α := S) ((algebraMap R S : (a : R) → S) y_1 : S)
            ((((B : (a : M) → M →ₗ[S] S) x : M →ₗ[S] S) : (a : M) → S) y : S)
⊢ (∀ x ∈ N₁, x ∈ B.flip.dualSubmodule N₂) ↔ ∀ x ∈ N₂, x ∈ B.dualSubmodule N₁

Tactic:
simp only [mem_dualSubmodule, Submodule.mem_one, flip_apply]

Premises used: LinearMap.BilinForm.mem_dualSubmodule, LinearMap.BilinForm.flip_apply, Submodule.mem_one
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
Goal:
R : Type u_1
S : Type u_3
M : Type u_2
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
N₁ N₂ : Submodule R M
⊢ (∀ x ∈ N₁,
      ∀ y ∈ N₂,
        ∃ (y_1 : R),
          Eq.{u_3 + 1} (α := S) ((algebraMap R S : (a : R) → S) y_1 : S)
            ((((B : (a : M) → M →ₗ[S] S) y : M →ₗ[S] S) : (a : M) → S) x : S)) ↔
    ∀ x ∈ N₂,
      ∀ y ∈ N₁,
        ∃ (y_1 : R),
          Eq.{u_3 + 1} (α := S) ((algebraMap R S : (a : R) → S) y_1 : S)
            ((((B : (a : M) → M →ₗ[S] S) x : M →ₗ[S] S) : (a : M) → S) y : S)

Tactic:
forall₂_comm

Premises used: forall₂_comm
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
Goal:
R : Type u_1
S : Type u_3
M : Type u_2
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
N₁ N₂ : Submodule R M
⊢ (∀ x ∈ N₁,
      ∀ y ∈ N₂,
        ∃ (y_1 : R),
          Eq.{u_3 + 1} (α := S) ((algebraMap R S : (a : R) → S) y_1 : S)
            ((((B : (a : M) → M →ₗ[S] S) y : M →ₗ[S] S) : (a : M) → S) x : S)) ↔
    ∀ x ∈ N₂,
      ∀ y ∈ N₁,
        ∃ (y_1 : R),
          Eq.{u_3 + 1} (α := S) ((algebraMap R S : (a : R) → S) y_1 : S)
            ((((B : (a : M) → M →ₗ[S] S) x : M →ₗ[S] S) : (a : M) → S) y : S)

Tactic:
exact forall₂_comm

Premises used: forall₂_comm
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
Goal:
R : Type u_1
S : Type u_3
M : Type u_2
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
N : Submodule R M
x : ↥(B.dualSubmodule N)
y : ↥N
⊢ Eq.{u_3 + 1} (α := S) ((algebraMap R S : (a : R) → S) (B.dualSubmoduleParing x y) : S)
    ((((B : (a : M) → M →ₗ[S] S) (↑x : M) : M →ₗ[S] S) : (a : M) → S) (↑y : M) : S)

Tactic:
(Submodule.mem_one.mp <| x.prop y y.prop).choose_spec

Premises used: Exists.choose_spec, Submodule.mem_one, Subtype.prop, Iff.mp, Subtype.val, LinearMap.BilinForm.dualSubmoduleParing
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
inst_7 : IsDomain R
inst_8 : IsTorsionFree R S
N : Submodule R M
x_1 : ↥(B.dualSubmodule N)
x y : ↥N
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (B.dualSubmoduleParing x_1 (x + y)) : S)
    ((algebraMap R S : (a : R) → S) (B.dualSubmoduleParing x_1 x + B.dualSubmoduleParing x_1 y) : S)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
inst_7 : IsDomain R
inst_8 : IsTorsionFree R S
N : Submodule R M
x : ↥(B.dualSubmodule N)
r : R
m : ↥N
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (B.dualSubmoduleParing x (r • m)) : S)
    ((algebraMap R S : (a : R) → S)
        (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (B.dualSubmoduleParing x m)) :
      S)

Tactic:
simp [← Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
inst_7 : IsDomain R
inst_8 : IsTorsionFree R S
N : Submodule R M
x y : ↥(B.dualSubmodule N)
z : ↥N
⊢ Eq.{u_2 + 1} (α := S)
    ((algebraMap R S : (a : R) → S)
        (({ toFun := B.dualSubmoduleParing (x + y), map_add' := ⋯, map_smul' := ⋯ } : (a : ↥N) → R) z : R) :
      S)
    ((algebraMap R S : (a : R) → S)
        ((HAdd.hAdd (α := Dual.{u_1, u_3} R ↥N)
                { toFun := B.dualSubmoduleParing x, map_add' := ⋯, map_smul' := ⋯ :
                  LinearMap.{u_1, u_1, u_3, u_1} (RingHom.id R) (↥N) R }
                { toFun := B.dualSubmoduleParing y, map_add' := ⋯, map_smul' := ⋯ :
                  LinearMap.{u_1, u_1, u_3, u_1} (RingHom.id R) (↥N) R } :
              (a : ↥N) → R)
            z :
          R) :
      S)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
inst_7 : IsDomain R
inst_8 : IsTorsionFree R S
N : Submodule R M
r : R
x : ↥(B.dualSubmodule N)
y : ↥N
⊢ Eq.{u_2 + 1} (α := S)
    ((algebraMap R S : (a : R) → S)
        (({ toFun := B.dualSubmoduleParing (r • x), map_add' := ⋯, map_smul' := ⋯ } : (a : ↥N) → R) y : R) :
      S)
    ((algebraMap R S : (a : R) → S)
        ((HSMul.hSMul (α := R) (β := Dual.{u_1, u_3} R ↥N) ((RingHom.id R : (a : R) → R) r : R)
                { toFun := B.dualSubmoduleParing x, map_add' := ⋯, map_smul' := ⋯ :
                  LinearMap.{u_1, u_1, u_3, u_1} (RingHom.id R) (↥N) R } :
              (a : ↥N) → R)
            y :
          R) :
      S)

Tactic:
simp [← Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
inst_7 : IsDomain R
hB : B.Nondegenerate
inst_8 : IsTorsionFree R S
N : Submodule R M
hN : Eq (α := Submodule S M) (Submodule.span S (↑N : Set M)) ⊤
x y : ↥(B.dualSubmodule N)
e :
  Eq (α := Dual.{u_1, u_3} R ↥N)
    ((B.dualSubmoduleToDual N : (a : ↥(B.dualSubmodule N)) → Dual R ↥N) x : Dual.{u_1, u_3} R ↥N)
    ((B.dualSubmoduleToDual N : (a : ↥(B.dualSubmodule N)) → Dual R ↥N) y : Dual.{u_1, u_3} R ↥N)
a : (↑x : M) = (↑y : M)
⊢ x = y

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
inst_7 : IsDomain R
hB : B.Nondegenerate
inst_8 : IsTorsionFree R S
N : Submodule R M
hN : Eq (α := Submodule S M) (Submodule.span S (↑N : Set M)) ⊤
x y : ↥(B.dualSubmodule N)
e :
  Eq (α := Dual.{u_1, u_3} R ↥N)
    ((B.dualSubmoduleToDual N : (a : ↥(B.dualSubmodule N)) → Dual R ↥N) x : Dual.{u_1, u_3} R ↥N)
    ((B.dualSubmoduleToDual N : (a : ↥(B.dualSubmodule N)) → Dual R ↥N) y : Dual.{u_1, u_3} R ↥N)
a :
  Eq (α := M →ₗ[S] S) ((B : (a : M) → M →ₗ[S] S) (↑x : M) : M →ₗ[S] S) ((B : (a : M) → M →ₗ[S] S) (↑y : M) : M →ₗ[S] S)
⊢ (↑x : M) = (↑y : M)

Tactic:
apply LinearMap.ker_eq_bot.mp hB.ker_eq_bot

Premises used: LinearMap.ker_eq_bot, Iff.mp, LinearMap.BilinForm.Nondegenerate.ker_eq_bot
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
inst_7 : IsDomain R
hB : B.Nondegenerate
inst_8 : IsTorsionFree R S
N : Submodule R M
hN : Eq (α := Submodule S M) (Submodule.span S (↑N : Set M)) ⊤
x y : ↥(B.dualSubmodule N)
e :
  Eq (α := Dual.{u_1, u_3} R ↥N)
    ((B.dualSubmoduleToDual N : (a : ↥(B.dualSubmodule N)) → Dual R ↥N) x : Dual.{u_1, u_3} R ↥N)
    ((B.dualSubmoduleToDual N : (a : ↥(B.dualSubmodule N)) → Dual R ↥N) y : Dual.{u_1, u_3} R ↥N)
a :
  Set.EqOn.{u_3, u_2} (β := S) (⇑((B : (a : M) → M →ₗ[S] S) (↑x : M) : M →ₗ[S] S) : (a : M) → S)
    (⇑((B : (a : M) → M →ₗ[S] S) (↑y : M) : M →ₗ[S] S) : (a : M) → S) (↑N : Set M)
⊢ Eq (α := M →ₗ[S] S) ((B : (a : M) → M →ₗ[S] S) (↑x : M) : M →ₗ[S] S) ((B : (a : M) → M →ₗ[S] S) (↑y : M) : M →ₗ[S] S)

Tactic:
apply LinearMap.ext_on hN

Premises used: LinearMap.ext_on
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
inst_7 : IsDomain R
hB : B.Nondegenerate
inst_8 : IsTorsionFree R S
N : Submodule R M
hN : Eq (α := Submodule S M) (Submodule.span S (↑N : Set M)) ⊤
x y : ↥(B.dualSubmodule N)
e :
  Eq (α := Dual.{u_1, u_3} R ↥N)
    ((B.dualSubmoduleToDual N : (a : ↥(B.dualSubmodule N)) → Dual R ↥N) x : Dual.{u_1, u_3} R ↥N)
    ((B.dualSubmoduleToDual N : (a : ↥(B.dualSubmodule N)) → Dual R ↥N) y : Dual.{u_1, u_3} R ↥N)
z : M
hz : z ∈ (↑N : Set M)
⊢ Eq.{u_2 + 1} (α := S) ((((B : (a : M) → M →ₗ[S] S) (↑x : M) : M →ₗ[S] S) : (a : M) → S) z : S)
    ((((B : (a : M) → M →ₗ[S] S) (↑y : M) : M →ₗ[S] S) : (a : M) → S) z : S)

Tactic:
simpa using congr_arg (algebraMap R S) (LinearMap.congr_fun e ⟨z, hz⟩)

Premises used: Algebra.algebraMap, Subtype.mk, congr_arg, LinearMap.congr_fun, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
inst_8 : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
intro :
  ∀ (val : Fintype ι),
    Eq (α := Submodule R M) (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))))
      (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
⊢ Eq (α := Submodule R M) (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
inst_8 : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val : Fintype ι
intro :
  LE.le (α := Submodule R M) (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
intro₁ :
  LE.le (α := Submodule R M) (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
    (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))))
⊢ Eq (α := Submodule R M) (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
inst_8 : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val : Fintype ι
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))) x
intro :
  Membership.mem (γ := Submodule R M)
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
    (∑ i : ι,
      HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := M)
        (((((B.dualBasis hB b).repr : (a : M) → ι →₀ S) x : ι →₀ S) : (a : ι) → S) i : S)
        ((B.dualBasis hB b : (a : ι) → M) i : M))
⊢ Membership.mem (γ := Submodule R M)
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M))) x

Tactic:
rw [← (B.dualBasis hB b).sum_repr x]

Premises used: LinearMap.BilinForm.dualBasis, Module.Basis.sum_repr
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
inst_8 : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val : Fintype ι
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))) x
intro :
  ∀ (c : ι),
    Membership.mem (γ := Finset ι) Finset.univ c →
      Membership.mem (γ := Submodule R M)
        (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
        (HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := M)
          (((((B.dualBasis hB b).repr : (a : M) → ι →₀ S) x : ι →₀ S) : (a : ι) → S) c : S)
          ((B.dualBasis hB b : (a : ι) → M) c : M))
⊢ Membership.mem (γ := Submodule R M)
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
    (∑ i : ι,
      HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := M)
        (((((B.dualBasis hB b).repr : (a : M) → ι →₀ S) x : ι →₀ S) : (a : ι) → S) i : S)
        ((B.dualBasis hB b : (a : ι) → M) i : M))

Tactic:
apply sum_mem

Premises used: sum_mem
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
inst_8 : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val : Fintype ι
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))) x
i : ι
intro :
  ∀ (r : R)
    (hr :
      Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) r : S)
        ((((B : (a : M) → M →ₗ[S] S) x : M →ₗ[S] S) : (a : M) → S) ((b : (a : ι) → M) i : M) : S)),
    Membership.mem (γ := Submodule R M)
      (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
      (HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := M)
        (((((B.dualBasis hB b).repr : (a : M) → ι →₀ S) x : ι →₀ S) : (a : ι) → S) i : S)
        ((B.dualBasis hB b : (a : ι) → M) i : M))
⊢ Membership.mem (γ := Submodule R M)
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
    (HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := M)
      (((((B.dualBasis hB b).repr : (a : M) → ι →₀ S) x : ι →₀ S) : (a : ι) → S) i : S)
      ((B.dualBasis hB b : (a : ι) → M) i : M))

Tactic:
obtain ⟨r, hr⟩ := Submodule.mem_one.mp <| hx (b i) (Submodule.subset_span ⟨_, rfl⟩)

Premises used: Submodule.mem_one, Exists.intro, Iff.mp, Submodule.subset_span, DFunLike.coe, rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
inst_8 : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val : Fintype ι
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))) x
i : ι
r : R
hr :
  Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) r : S)
    ((((B : (a : M) → M →ₗ[S] S) x : M →ₗ[S] S) : (a : M) → S) ((b : (a : ι) → M) i : M) : S)
intro :
  Membership.mem (γ := Submodule R M)
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
    (HSMul.hSMul (β := M) r ((B.dualBasis hB b : (a : ι) → M) i : M))
⊢ Membership.mem (γ := Submodule R M)
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
    (HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := M)
      (((((B.dualBasis hB b).repr : (a : M) → ι →₀ S) x : ι →₀ S) : (a : ι) → S) i : S)
      ((B.dualBasis hB b : (a : ι) → M) i : M))

Tactic:
simp only [dualBasis_repr_apply, ← hr, algebraMap_smul]

Premises used: algebraMap_smul, LinearMap.BilinForm.dualBasis_repr_apply
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
inst_8 : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val : Fintype ι
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))) x
i : ι
r : R
hr :
  Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) r : S)
    ((((B : (a : M) → M →ₗ[S] S) x : M →ₗ[S] S) : (a : M) → S) ((b : (a : ι) → M) i : M) : S)
intro :
  Membership.mem.{u_3, u_3} (α := M) (γ := Submodule R M)
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
    ((B.dualBasis hB b : (a : ι) → M) i : M)
⊢ Membership.mem (γ := Submodule R M)
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
    (HSMul.hSMul (β := M) r ((B.dualBasis hB b : (a : ι) → M) i : M))

Tactic:
apply Submodule.smul_mem

Premises used: Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
inst_8 : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val : Fintype ι
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))) x
i : ι
r : R
hr :
  Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) r : S)
    ((((B : (a : M) → M →ₗ[S] S) x : M →ₗ[S] S) : (a : M) → S) ((b : (a : ι) → M) i : M) : S)
⊢ Membership.mem.{u_3, u_3} (α := M) (γ := Submodule R M)
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
    ((B.dualBasis hB b : (a : ι) → M) i : M)

Tactic:
Submodule.subset_span ⟨_, rfl⟩

Premises used: Exists.intro, Submodule.subset_span, rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
inst_8 : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val : Fintype ι
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))) x
i : ι
r : R
hr :
  Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) r : S)
    ((((B : (a : M) → M →ₗ[S] S) x : M →ₗ[S] S) : (a : M) → S) ((b : (a : ι) → M) i : M) : S)
⊢ Membership.mem.{u_3, u_3} (α := M) (γ := Submodule R M)
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
    ((B.dualBasis hB b : (a : ι) → M) i : M)

Tactic:
exact Submodule.subset_span ⟨_, rfl⟩