awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  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)))) : Set M)
⊢ 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))))

Tactic:
rw [Submodule.span_le]

Premises used: Submodule.span_le
-- 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 ι
i : ι
y : M
hy : Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))) y
intro :
  ∀ (f : ι → R)
    (hy :
      Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
        (∑ i : ι, HSMul.hSMul (β := M) (f i) ((b : (a : ι) → M) i : M))),
    Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S) 1
      ((((B : (a : M) → M →ₗ[S] S) ((B.dualBasis hB b : (a : ι) → M) i) : M →ₗ[S] S) : (a : M) → S)
          (∑ i : ι, HSMul.hSMul (β := M) (f i) ((b : (a : ι) → M) i : M)) :
        S)
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S) 1
    ((((B : (a : M) → M →ₗ[S] S) ((B.dualBasis hB b : (a : ι) → M) i) : M →ₗ[S] S) : (a : M) → S) y : S)

Tactic:
obtain ⟨f, rfl⟩ := (Submodule.mem_span_range_iff_exists_fun _).mp hy

Premises used: Submodule.mem_span_range_iff_exists_fun, Iff.mp, 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 ι
i : ι
f : ι → R
hy :
  Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    (∑ i : ι, HSMul.hSMul (β := M) (f i) ((b : (a : ι) → M) i : M))
intro :
  Membership.mem (γ := Submodule R S) 1
    (∑ x : ι,
      (((B : (a : M) → M →ₗ[S] S) ((B.dualBasis hB b : (a : ι) → M) i) : M →ₗ[S] S) : (a : M) → S)
        (HSMul.hSMul (β := M) (f x) ((b : (a : ι) → M) x : M)))
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S) 1
    ((((B : (a : M) → M →ₗ[S] S) ((B.dualBasis hB b : (a : ι) → M) i) : M →ₗ[S] S) : (a : M) → S)
        (∑ i : ι, HSMul.hSMul (β := M) (f i) ((b : (a : ι) → M) i : M)) :
      S)

Tactic:
simp only [map_sum]

Premises used: map_sum
-- 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 ι
i : ι
f : ι → R
hy :
  Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    (∑ i : ι, HSMul.hSMul (β := M) (f i) ((b : (a : ι) → M) i : M))
intro :
  ∀ (c : ι),
    Membership.mem (γ := Finset ι) Finset.univ c →
      Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S) 1
        ((((B : (a : M) → M →ₗ[S] S) ((B.dualBasis hB b : (a : ι) → M) i) : M →ₗ[S] S) : (a : M) → S)
            (HSMul.hSMul (β := M) (f c) ((b : (a : ι) → M) c : M)) :
          S)
⊢ Membership.mem (γ := Submodule R S) 1
    (∑ x : ι,
      (((B : (a : M) → M →ₗ[S] S) ((B.dualBasis hB b : (a : ι) → M) i) : M →ₗ[S] S) : (a : M) → S)
        (HSMul.hSMul (β := M) (f x) ((b : (a : ι) → M) x : 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 ι
i : ι
f : ι → R
hy :
  Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    (∑ i : ι, HSMul.hSMul (β := M) (f i) ((b : (a : ι) → M) i : M))
j : ι
intro :
  Membership.mem (γ := Submodule R S) 1
    (HSMul.hSMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (f j) : S)
      ((((B : (a : M) → M →ₗ[S] S) ((B.dualBasis hB b : (a : ι) → M) i) : M →ₗ[S] S) : (a : M) → S)
          ((b : (a : ι) → M) j : M) :
        S))
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S) 1
    ((((B : (a : M) → M →ₗ[S] S) ((B.dualBasis hB b : (a : ι) → M) i) : M →ₗ[S] S) : (a : M) → S)
        (HSMul.hSMul (β := M) (f j) ((b : (a : ι) → M) j : M)) :
      S)

Tactic:
rw [← IsScalarTower.algebraMap_smul S (f j), map_smul]

Premises used: IsScalarTower.algebraMap_smul, map_smul
-- 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 ι
i : ι
f : ι → R
hy :
  Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    (∑ i : ι, HSMul.hSMul (β := M) (f i) ((b : (a : ι) → M) i : M))
j : ι
intro :
  Membership.mem (γ := Submodule R S) 1
    (HSMul.hSMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (f j) : S) (if j = i then 1 else 0))
⊢ Membership.mem (γ := Submodule R S) 1
    (HSMul.hSMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (f j) : S)
      ((((B : (a : M) → M →ₗ[S] S) ((B.dualBasis hB b : (a : ι) → M) i) : M →ₗ[S] S) : (a : M) → S)
          ((b : (a : ι) → M) j : M) :
        S))

Tactic:
simp_rw [apply_dualBasis_left]

Premises used: LinearMap.BilinForm.apply_dualBasis_left
-- 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 ι
i : ι
f : ι → R
hy :
  Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    (∑ i : ι, HSMul.hSMul (β := M) (f i) ((b : (a : ι) → M) i : M))
j : ι
intro :
  Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S) 1
    ((algebraMap R S : (a : R) → S) (if j = i then f j else 0) : S)
⊢ Membership.mem (γ := Submodule R S) 1
    (HSMul.hSMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (f j) : S) (if j = i then 1 else 0))

Tactic:
rw [smul_eq_mul, mul_ite, mul_one, mul_zero, ← (algebraMap R S).map_zero, ← apply_ite]

Premises used: Algebra.algebraMap, mul_ite, apply_ite, MulZeroClass.mul_zero, RingHom.map_zero, smul_eq_mul, mul_one
-- 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 ι
i : ι
f : ι → R
hy :
  Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    (∑ i : ι, HSMul.hSMul (β := M) (f i) ((b : (a : ι) → M) i : M))
j : ι
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S) 1
    ((algebraMap R S : (a : R) → S) (if j = i then f j else 0) : S)

Tactic:
Submodule.mem_one.mpr ⟨_, rfl⟩

Premises used: Iff.mpr, Set.Mem, Submodule.mem_one, Exists.intro, 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 ι
i : ι
f : ι → R
hy :
  Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    (∑ i : ι, HSMul.hSMul (β := M) (f i) ((b : (a : ι) → M) i : M))
j : ι
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S) 1
    ((algebraMap R S : (a : R) → S) (if j = i then f j else 0) : S)

Tactic:
exact Submodule.mem_one.mpr ⟨_, rfl⟩

Premises used: Iff.mpr, Submodule.mem_one, Exists.intro, 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 ι
hB : B.Nondegenerate
b : Basis ι S M
this : FiniteDimensional S M := ⋯
rw :
  Eq (α := Submodule R M)
    (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.flip.dualBasis ⋯ b) : (a : ι) → M))))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
rw₁ :
  Eq.{u_3 + 1} (α := Submodule R M)
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB (B.flip.dualBasis ⋯ b)) : (a : ι) → M)))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
rw₂ rw₃ :
  Eq.{u_3 + 1} (α := Submodule R M) (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
⊢ Eq (α := Submodule R M)
    (B.dualSubmodule (B.flip.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 : (a : ι) → M)))

Tactic:
rw [dualSubmodule_span_of_basis _ hB.flip, dualSubmodule_span_of_basis B hB,
    dualBasis_dualBasis_flip hB]

Premises used: LinearMap.BilinForm.dualSubmodule_span_of_basis, LinearMap.BilinForm.Nondegenerate.flip, LinearMap.BilinForm.dualBasis_dualBasis_flip
-- 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 ι
hB : B.Nondegenerate
b : Basis ι S M
letI letI₁ letI₂ :
  Eq (α := Submodule R M)
    (B.dualSubmodule (B.flip.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 : (a : ι) → M)))
⊢ Eq (α := Submodule R M)
    (B.dualSubmodule (B.flip.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 : (a : ι) → M)))

Tactic:
classical
  letI := b.finiteDimensional_of_finite
  rw [dualSubmodule_span_of_basis _ hB.flip, dualSubmodule_span_of_basis B hB,
    dualBasis_dualBasis_flip hB]

Premises used: LinearMap.BilinForm.dualSubmodule_span_of_basis, LinearMap.BilinForm.Nondegenerate.flip, LinearMap.BilinForm.dualBasis_dualBasis_flip
-- 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 ι
hB : B.Nondegenerate
b : Basis ι S M
this : FiniteDimensional S M := ⋯
rw :
  Eq (α := Submodule R M)
    (B.flip.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M))))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
rw₁ :
  Eq.{u_3 + 1} (α := Submodule R M)
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.flip.dualBasis ⋯ (B.dualBasis hB b)) : (a : ι) → M)))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
rw₂ rw₃ :
  Eq.{u_3 + 1} (α := Submodule R M) (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
⊢ Eq (α := Submodule R M)
    (B.flip.dualSubmodule (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 : (a : ι) → M)))

Tactic:
rw [dualSubmodule_span_of_basis B hB, dualSubmodule_span_of_basis _ hB.flip,
    dualBasis_flip_dualBasis hB]

Premises used: LinearMap.BilinForm.dualSubmodule_span_of_basis, LinearMap.BilinForm.Nondegenerate.flip, LinearMap.BilinForm.dualBasis_flip_dualBasis
-- 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 ι
hB : B.Nondegenerate
b : Basis ι S M
letI letI₁ letI₂ :
  Eq (α := Submodule R M)
    (B.flip.dualSubmodule (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 : (a : ι) → M)))
⊢ Eq (α := Submodule R M)
    (B.flip.dualSubmodule (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 : (a : ι) → M)))

Tactic:
classical
  letI := b.finiteDimensional_of_finite
  rw [dualSubmodule_span_of_basis B hB, dualSubmodule_span_of_basis _ hB.flip,
    dualBasis_flip_dualBasis hB]

Premises used: LinearMap.BilinForm.dualSubmodule_span_of_basis, LinearMap.BilinForm.Nondegenerate.flip, LinearMap.BilinForm.dualBasis_flip_dualBasis
-- 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 ι
hB : B.Nondegenerate
hB' : B.IsSymm
b : Basis ι S M
this : FiniteDimensional S M := ⋯
rw :
  Eq (α := Submodule R M)
    (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M))))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
rw₁ :
  Eq.{u_3 + 1} (α := Submodule R M)
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB (B.dualBasis hB b)) : (a : ι) → M)))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
rw₂ rw₃ :
  Eq.{u_3 + 1} (α := Submodule R M) (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
⊢ Eq (α := Submodule R M)
    (B.dualSubmodule (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 : (a : ι) → M)))

Tactic:
rw [dualSubmodule_span_of_basis B hB, dualSubmodule_span_of_basis B hB,
    dualBasis_dualBasis hB hB']

Premises used: LinearMap.BilinForm.dualSubmodule_span_of_basis, LinearMap.BilinForm.dualBasis_dualBasis
-- 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 ι
hB : B.Nondegenerate
hB' : B.IsSymm
b : Basis ι S M
letI letI₁ letI₂ :
  Eq (α := Submodule R M)
    (B.dualSubmodule (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 : (a : ι) → M)))
⊢ Eq (α := Submodule R M)
    (B.dualSubmodule (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 : (a : ι) → M)))

Tactic:
classical
  letI := b.finiteDimensional_of_finite
  rw [dualSubmodule_span_of_basis B hB, dualSubmodule_span_of_basis B hB,
    dualBasis_dualBasis hB hB']

Premises used: LinearMap.BilinForm.dualSubmodule_span_of_basis, LinearMap.BilinForm.dualBasis_dualBasis
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
α : Type u_7
t : Finset α
g : α → M
w : M
⊢ Eq.{u_1 + 1} (α := R) (((B : (a : M) → M →ₗ[R] R) (∑ i ∈ t, g i) : (a : M) → R) w : R)
    (∑ i ∈ t, (((B : (a : M) → M →ₗ[R] R) (g i) : M →ₗ[R] R) : (a : M) → R) w : R)

Tactic:
B.map_sum₂ t g w

Premises used: LinearMap.map_sum₂
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
α : Type u_7
t : Finset α
w : M
g : α → M
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) w : M →ₗ[R] R) : (a : M) → R) (∑ i ∈ t, g i) : R)
    (∑ i ∈ t, (((B : (a : M) → M →ₗ[R] R) w : M →ₗ[R] R) : (a : M) → R) (g i) : R)

Tactic:
map_sum _ _ _

Premises used: map_sum
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_7
t : Finset α
B : α → BilinForm R M
v w : M
⊢ Eq.{u_1 + 1} (α := R) ((((∑ i ∈ t, B i : (a : M) → M →ₗ[R] R) v : M →ₗ[R] R) : (a : M) → R) w : R)
    (∑ i ∈ t, (((B i : (a : M) → M →ₗ[R] R) v : M →ₗ[R] R) : (a : M) → R) w : R)

Tactic:
simp only [coe_sum, Finset.sum_apply]

Premises used: Finset.sum_apply, LinearMap.coe_sum
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : BilinForm R M
x : M
⊢ Eq (α := (a : M) → R)
    (⇑((((toLinHomFlip : (a : BilinForm R M) → M →ₗ[R] M →ₗ[R] R) A : M →ₗ[R] M →ₗ[R] R) : (a : M) → M →ₗ[R] R) x :
          M →ₗ[R] R) :
      (a : M) → R)
    fun (y : M) ↦ (((A : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type w
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
M'' : Type u_7
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
B : BilinForm R M''
l r : M →ₗ[R] M'
l' r' : M' →ₗ[R] M''
⊢ (B.comp l' r').comp l r = B.comp (l' ∘ₗ l) (r' ∘ₗ r)

Tactic:
rfl

Premises used: LinearMap.BilinForm.comp, LinearMap.compl₁₂, rfl, LinearMap.compl₂
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
l r : M →ₗ[R] M
⊢ (B.compLeft l).compRight r = B.comp l r

Tactic:
rfl

Premises used: LinearMap.BilinForm.comp, LinearMap.BilinForm.compLeft, LinearMap.compl₁₂, rfl, LinearMap.compl₂, LinearMap.BilinForm.compRight
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
l r : M →ₗ[R] M
⊢ (B.compRight r).compLeft l = B.comp l r

Tactic:
rfl

Premises used: LinearMap.BilinForm.comp, LinearMap.BilinForm.compLeft, LinearMap.compl₁₂, rfl, LinearMap.compl₂, LinearMap.BilinForm.compRight
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type w
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
B : BilinForm R M'
l r : M →ₗ[R] M'
v w : M
⊢ Eq.{u_1 + 1} (α := R) ((((B.comp l r : (a : M) → M →ₗ[R] R) v : M →ₗ[R] R) : (a : M) → R) w : R)
    ((((B : (a : M') → M' →ₗ[R] R) ((l : (a : M) → M') v) : M' →ₗ[R] R) : (a : M') → R) ((r : (a : M) → M') w : M') : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
f : M →ₗ[R] M
v w : M
⊢ Eq.{u_1 + 1} (α := R) ((((B.compLeft f : (a : M) → M →ₗ[R] R) v : M →ₗ[R] R) : (a : M) → R) w : R)
    ((((B : (a : M) → M →ₗ[R] R) ((f : (a : M) → M) v) : M →ₗ[R] R) : (a : M) → R) w : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
f : M →ₗ[R] M
v w : M
⊢ Eq.{u_1 + 1} (α := R) ((((B.compRight f : (a : M) → M →ₗ[R] R) v : M →ₗ[R] R) : (a : M) → R) w : R)
    ((((B : (a : M) → M →ₗ[R] R) v : M →ₗ[R] R) : (a : M) → R) ((f : (a : M) → M) w : M) : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
r : M →ₗ[R] M
H :
  ∀ (x y : M),
    Eq.{u_1 + 1} (α := R) ((((B.comp id r : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B.compRight r : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
⊢ B.comp id r = B.compRight r

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
r : M →ₗ[R] M
x y : M
⊢ Eq.{u_1 + 1} (α := R) ((((B.comp id r : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
    ((((B.compRight r : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
l : M →ₗ[R] M
H :
  ∀ (x y : M),
    Eq.{u_1 + 1} (α := R) ((((B.comp l id : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B.compLeft l : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
⊢ B.comp l id = B.compLeft l

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
l : M →ₗ[R] M
x y : M
⊢ Eq.{u_1 + 1} (α := R) ((((B.comp l id : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
    ((((B.compLeft l : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
H :
  ∀ (x y : M),
    Eq.{u_1 + 1} (α := R) ((((B.compLeft id : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
⊢ B.compLeft id = B

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.BilinearForm.Hom
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
x y : M
⊢ Eq.{u_1 + 1} (α := R) ((((B.compLeft id : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
    ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
rfl