awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R₁
i i_1 : n
⊢ Eq (α := R₁)
    ((((((toBilin (Pi.basisFun R₁ n) : (a : Matrix n n R₁) → BilinForm R₁ (n → R₁)) M ∘ₗ
                      LinearMap.single R₁ (fun (i : n) ↦ R₁) i :
                    R₁ →ₗ[R₁] (n → R₁) →ₗ[R₁] R₁) :
                  (a : R₁) → (n → R₁) →ₗ[R₁] R₁)
                1 ∘ₗ
              LinearMap.single R₁ (fun (i : n) ↦ R₁) i_1 :
            R₁ →ₗ[R₁] R₁) :
          (a : R₁) → R₁)
        1 :
      R₁)
    ((((((toBilin' : (a : Matrix n n R₁) → BilinForm R₁ (n → R₁)) M ∘ₗ LinearMap.single R₁ (fun (i : n) ↦ R₁) i :
                    R₁ →ₗ[R₁] (n → R₁) →ₗ[R₁] R₁) :
                  (a : R₁) → (n → R₁) →ₗ[R₁] R₁)
                1 ∘ₗ
              LinearMap.single R₁ (fun (i : n) ↦ R₁) i_1 :
            R₁ →ₗ[R₁] R₁) :
          (a : R₁) → R₁)
        1 :
      R₁)

Tactic:
simp only [coe_comp, coe_single, Function.comp_apply, toBilin_apply, Pi.basisFun_repr,
    toBilin'_apply]

Premises used: Matrix.toBilin_apply, Matrix.toBilin'_apply, LinearMap.coe_comp, LinearMap.coe_single, Function.comp_apply, Pi.basisFun_repr
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
rw : Eq (α := BilinForm R₁ (n → R₁) ≃ₗ[R₁] Matrix n n R₁) (toMatrix₂ (Pi.basisFun R₁ n) (Pi.basisFun R₁ n)) toMatrix'
rw₁ :
  Eq (α := BilinForm R₁ (n → R₁) ≃ₗ[R₁] Matrix n n R₁) (toMatrix₂ (Pi.basisFun R₁ n) (Pi.basisFun R₁ n)) (toMatrix₂' R₁)
rw₂ rw₃ :
  Eq (α := BilinForm R₁ (n → R₁) ≃ₗ[R₁] Matrix n n R₁)
    (toMatrix₂' R₁ : ((n → R₁) →ₗ[R₁] (n → R₁) →ₗ[R₁] R₁) ≃ₗ[R₁] Matrix n n R₁)
    (toMatrix₂' R₁ : ((n → R₁) →ₗ[R₁] (n → R₁) →ₗ[R₁] R₁) ≃ₗ[R₁] Matrix n n R₁)
⊢ Eq (α := BilinForm R₁ (n → R₁) ≃ₗ[R₁] Matrix n n R₁) (toMatrix (Pi.basisFun R₁ n)) toMatrix'

Tactic:
rw [BilinForm.toMatrix, BilinForm.toMatrix', LinearMap.toMatrix₂_basisFun]

Premises used: LinearMap.BilinForm.toMatrix, LinearMap.toMatrix₂_basisFun, LinearMap.BilinForm.toMatrix'
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
M₁ : Type u_2
inst : CommSemiring R₁
inst_1 : AddCommMonoid M₁
inst_2 : Module R₁ M₁
n : Type u_5
inst_3 : Fintype n
inst_4 : DecidableEq n
b : Basis n R₁ M₁
B : BilinForm R₁ M₁
⊢ (toBilin b : (a : Matrix n n R₁) → BilinForm R₁ M₁)
      ((LinearMap.BilinForm.toMatrix b : (a : BilinForm R₁ M₁) → Matrix n n R₁) B) =
    B

Tactic:
(Matrix.toBilin b).apply_symm_apply B

Premises used: Matrix.toBilin, LinearEquiv.apply_symm_apply
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
M₁ : Type u_2
inst : CommSemiring R₁
inst_1 : AddCommMonoid M₁
inst_2 : Module R₁ M₁
n : Type u_5
inst_3 : Fintype n
inst_4 : DecidableEq n
b : Basis n R₁ M₁
M : Matrix n n R₁
⊢ (toMatrix b : (a : BilinForm R₁ M₁) → Matrix n n R₁) ((toBilin b : (a : Matrix n n R₁) → BilinForm R₁ M₁) M) = M

Tactic:
(BilinForm.toMatrix b).apply_symm_apply M

Premises used: LinearMap.BilinForm.toMatrix, LinearEquiv.apply_symm_apply
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
M₁ : Type u_2
inst : CommSemiring R₁
inst_1 : AddCommMonoid M₁
inst_2 : Module R₁ M₁
n : Type u_5
o : Type u_6
inst_3 : Fintype n
inst_4 : Fintype o
inst_5 : DecidableEq n
b : Basis n R₁ M₁
M₂' : Type u_7
inst_6 : AddCommMonoid M₂'
inst_7 : Module R₁ M₂'
c : Basis o R₁ M₂'
inst_8 : DecidableEq o
B : BilinForm R₁ M₁
l r : M₂' →ₗ[R₁] M₁
⊢ (toMatrix c : (a : BilinForm R₁ M₂') → Matrix o o R₁) (B.comp l r) =
    HMul.hMul (β := Matrix n o R₁)
      (HMul.hMul (α := Matrix o n R₁) (β := Matrix n n R₁)
        ((LinearMap.toMatrix c b : (a : M₂' →ₗ[R₁] M₁) → Matrix n o R₁) l)ᵀ
        ((toMatrix b : (a : BilinForm R₁ M₁) → Matrix n n R₁) B : Matrix n n R₁))
      ((LinearMap.toMatrix c b : (a : M₂' →ₗ[R₁] M₁) → Matrix n o R₁) r : Matrix n o R₁)

Tactic:
LinearMap.toMatrix₂_compl₁₂ _ _ _ _ B _ _

Premises used: LinearMap.toMatrix₂_compl₁₂
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
M₁ : Type u_2
inst : CommSemiring R₁
inst_1 : AddCommMonoid M₁
inst_2 : Module R₁ M₁
n : Type u_5
inst_3 : Fintype n
inst_4 : DecidableEq n
b : Basis n R₁ M₁
B : BilinForm R₁ M₁
f : M₁ →ₗ[R₁] M₁
⊢ (toMatrix b : (a : BilinForm R₁ M₁) → Matrix n n R₁) (B.compLeft f) =
    HMul.hMul (α := Matrix n n R₁) (β := Matrix n n R₁)
      ((LinearMap.toMatrix b b : (a : M₁ →ₗ[R₁] M₁) → Matrix n n R₁) f)ᵀ
      ((toMatrix b : (a : BilinForm R₁ M₁) → Matrix n n R₁) B : Matrix n n R₁)

Tactic:
LinearMap.toMatrix₂_comp _ _ _ B _

Premises used: LinearMap.toMatrix₂_comp
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
M₁ : Type u_2
inst : CommSemiring R₁
inst_1 : AddCommMonoid M₁
inst_2 : Module R₁ M₁
n : Type u_5
inst_3 : Fintype n
inst_4 : DecidableEq n
b : Basis n R₁ M₁
B : BilinForm R₁ M₁
f : M₁ →ₗ[R₁] M₁
⊢ (toMatrix b : (a : BilinForm R₁ M₁) → Matrix n n R₁) (B.compRight f) =
    HMul.hMul (α := Matrix n n R₁) (β := Matrix n n R₁)
      ((toMatrix b : (a : BilinForm R₁ M₁) → Matrix n n R₁) B : Matrix n n R₁)
      ((LinearMap.toMatrix b b : (a : M₁ →ₗ[R₁] M₁) → Matrix n n R₁) f : Matrix n n R₁)

Tactic:
LinearMap.toMatrix₂_compl₂ _ _ _ B _

Premises used: LinearMap.toMatrix₂_compl₂
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
M₁ : Type u_2
inst : CommSemiring R₁
inst_1 : AddCommMonoid M₁
inst_2 : Module R₁ M₁
n : Type u_5
o : Type u_6
inst_3 : Fintype n
inst_4 : Fintype o
inst_5 : DecidableEq n
b : Basis n R₁ M₁
inst_6 : DecidableEq o
c : Basis o R₁ M₁
B : BilinForm R₁ M₁
⊢ HMul.hMul (β := Matrix n o R₁)
      (HMul.hMul (α := Matrix o n R₁) (β := Matrix n n R₁) (b.toMatrix (⇑c : (a : o) → M₁))ᵀ
        ((toMatrix b : (a : BilinForm R₁ M₁) → Matrix n n R₁) B : Matrix n n R₁))
      (b.toMatrix (⇑c : (a : o) → M₁)) =
    (toMatrix c : (a : BilinForm R₁ M₁) → Matrix o o R₁) B

Tactic:
LinearMap.toMatrix₂_mul_basis_toMatrix _ _ _ _ B

Premises used: LinearMap.toMatrix₂_mul_basis_toMatrix
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
M₁ : Type u_2
inst : CommSemiring R₁
inst_1 : AddCommMonoid M₁
inst_2 : Module R₁ M₁
n : Type u_5
o : Type u_6
inst_3 : Fintype n
inst_4 : Fintype o
inst_5 : DecidableEq n
b : Basis n R₁ M₁
M₂' : Type u_7
inst_6 : AddCommMonoid M₂'
inst_7 : Module R₁ M₂'
c : Basis o R₁ M₂'
inst_8 : DecidableEq o
B : BilinForm R₁ M₁
M : Matrix o n R₁
N : Matrix n o R₁
⊢ HMul.hMul (β := Matrix n n R₁) M ((toMatrix b : (a : BilinForm R₁ M₁) → Matrix n n R₁) B : Matrix n n R₁) * N =
    (toMatrix c : (a : BilinForm R₁ M₂') → Matrix o o R₁)
      (B.comp ((toLin c b : (a : Matrix n o R₁) → M₂' →ₗ[R₁] M₁) Mᵀ)
        ((toLin c b : (a : Matrix n o R₁) → M₂' →ₗ[R₁] M₁) N))

Tactic:
LinearMap.mul_toMatrix₂_mul _ _ _ _ B _ _

Premises used: LinearMap.mul_toMatrix₂_mul
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
M₁ : Type u_2
inst : CommSemiring R₁
inst_1 : AddCommMonoid M₁
inst_2 : Module R₁ M₁
n : Type u_5
inst_3 : Fintype n
inst_4 : DecidableEq n
b : Basis n R₁ M₁
B : BilinForm R₁ M₁
M : Matrix n n R₁
⊢ HMul.hMul (β := Matrix n n R₁) M ((toMatrix b : (a : BilinForm R₁ M₁) → Matrix n n R₁) B : Matrix n n R₁) =
    (toMatrix b : (a : BilinForm R₁ M₁) → Matrix n n R₁)
      (B.compLeft ((toLin b b : (a : Matrix n n R₁) → M₁ →ₗ[R₁] M₁) Mᵀ))

Tactic:
LinearMap.mul_toMatrix₂ _ _ _ B _

Premises used: LinearMap.mul_toMatrix₂
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
M₁ : Type u_2
inst : CommSemiring R₁
inst_1 : AddCommMonoid M₁
inst_2 : Module R₁ M₁
n : Type u_5
inst_3 : Fintype n
inst_4 : DecidableEq n
b : Basis n R₁ M₁
B : BilinForm R₁ M₁
M : Matrix n n R₁
⊢ HMul.hMul (α := Matrix n n R₁) ((toMatrix b : (a : BilinForm R₁ M₁) → Matrix n n R₁) B : Matrix n n R₁) M =
    (toMatrix b : (a : BilinForm R₁ M₁) → Matrix n n R₁)
      (B.compRight ((toLin b b : (a : Matrix n n R₁) → M₁ →ₗ[R₁] M₁) M))

Tactic:
LinearMap.toMatrix₂_mul _ _ _ B _

Premises used: LinearMap.toMatrix₂_mul
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
M₁ : Type u_2
inst : CommSemiring R₁
inst_1 : AddCommMonoid M₁
inst_2 : Module R₁ M₁
n : Type u_5
o : Type u_6
inst_3 : Fintype n
inst_4 : Fintype o
inst_5 : DecidableEq n
b : Basis n R₁ M₁
M₂' : Type u_7
inst_6 : AddCommMonoid M₂'
inst_7 : Module R₁ M₂'
c : Basis o R₁ M₂'
inst_8 : DecidableEq o
M : Matrix n n R₁
P Q : Matrix n o R₁
H :
  ∀ (x y : M₂'),
    Eq.{u_1 + 1} (α := R₁)
      ((((BilinForm.comp.{u_2, u_1, u_7} (M' := M₁) ((toBilin b : (a : Matrix n n R₁) → BilinForm R₁ M₁) M)
                    ((toLin c b : (a : Matrix n o R₁) → M₂' →ₗ[R₁] M₁) P)
                    ((toLin c b : (a : Matrix n o R₁) → M₂' →ₗ[R₁] M₁) Q) :
                  (a : M₂') → M₂' →ₗ[R₁] R₁)
                x :
              M₂' →ₗ[R₁] R₁) :
            (a : M₂') → R₁)
          y :
        R₁)
      ((((((toBilin c : (a : Matrix o o R₁) → BilinForm R₁ M₂') (Pᵀ * M * Q) : BilinForm R₁ M₂') :
                  (a : M₂') → M₂' →ₗ[R₁] R₁)
                x :
              M₂' →ₗ[R₁] R₁) :
            (a : M₂') → R₁)
          y :
        R₁)
⊢ Eq (α := BilinForm R₁ M₂')
    (BilinForm.comp.{u_2, u_1, u_7} (M' := M₁) ((toBilin b : (a : Matrix n n R₁) → BilinForm R₁ M₁) M)
      ((toLin c b : (a : Matrix n o R₁) → M₂' →ₗ[R₁] M₁) P) ((toLin c b : (a : Matrix n o R₁) → M₂' →ₗ[R₁] M₁) Q))
    ((toBilin c : (a : Matrix o o R₁) → BilinForm R₁ M₂') (Pᵀ * M * Q))

Tactic:
ext x y
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
M₁ : Type u_2
inst : CommSemiring R₁
inst_1 : AddCommMonoid M₁
inst_2 : Module R₁ M₁
n : Type u_5
o : Type u_6
inst_3 : Fintype n
inst_4 : Fintype o
inst_5 : DecidableEq n
b : Basis n R₁ M₁
M₂' : Type u_7
inst_6 : AddCommMonoid M₂'
inst_7 : Module R₁ M₂'
c : Basis o R₁ M₂'
inst_8 : DecidableEq o
M : Matrix n n R₁
P Q : Matrix n o R₁
x y : M₂'
H :
  Eq.{u_1 + 1} (α := R₁)
    ((((BilinForm.comp.{u_2, u_1, u_7} (M' := M₁) ((toLinearMap₂ b b : (a : Matrix n n R₁) → BilinForm R₁ M₁) M)
                  ((toLin c b : (a : Matrix n o R₁) → M₂' →ₗ[R₁] M₁) P)
                  ((toLin c b : (a : Matrix n o R₁) → M₂' →ₗ[R₁] M₁) Q) :
                (a : M₂') → M₂' →ₗ[R₁] R₁)
              x :
            M₂' →ₗ[R₁] R₁) :
          (a : M₂') → R₁)
        y :
      R₁)
    ((((compl₁₂.{u_1, u_1, u_2, u_2, u_1, u_7, u_7} (Mₗ := M₁) (N := M₁)
                  ((toLinearMap₂ b b : (a : Matrix n n R₁) → M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁) M)
                  ((toLin c b : (a : Matrix n o R₁) → M₂' →ₗ[R₁] M₁) P)
                  ((toLin c b : (a : Matrix n o R₁) → M₂' →ₗ[R₁] M₁) Q) :
                (a : M₂') → M₂' →ₗ[R₁] R₁)
              x :
            M₂' →ₗ[R₁] R₁) :
          (a : M₂') → R₁)
        y :
      R₁)
⊢ Eq.{u_1 + 1} (α := R₁)
    ((((BilinForm.comp.{u_2, u_1, u_7} (M' := M₁) ((toBilin b : (a : Matrix n n R₁) → BilinForm R₁ M₁) M)
                  ((toLin c b : (a : Matrix n o R₁) → M₂' →ₗ[R₁] M₁) P)
                  ((toLin c b : (a : Matrix n o R₁) → M₂' →ₗ[R₁] M₁) Q) :
                (a : M₂') → M₂' →ₗ[R₁] R₁)
              x :
            M₂' →ₗ[R₁] R₁) :
          (a : M₂') → R₁)
        y :
      R₁)
    ((((((toBilin c : (a : Matrix o o R₁) → BilinForm R₁ M₂') (Pᵀ * M * Q) : BilinForm R₁ M₂') :
                (a : M₂') → M₂' →ₗ[R₁] R₁)
              x :
            M₂' →ₗ[R₁] R₁) :
          (a : M₂') → R₁)
        y :
      R₁)

Tactic:
rw [Matrix.toBilin, LinearMap.BilinForm.toMatrix, Matrix.toBilin, LinearMap.BilinForm.toMatrix,
    toMatrix₂_symm, toMatrix₂_symm, ← Matrix.toLinearMap₂_compl₁₂ b b c c]

Premises used: Matrix.toLinearMap₂_compl₁₂, LinearMap.BilinForm.toMatrix, LinearMap.toMatrix₂_symm, Matrix.toBilin
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
M₁ : Type u_2
inst : CommSemiring R₁
inst_1 : AddCommMonoid M₁
inst_2 : Module R₁ M₁
n : Type u_5
o : Type u_6
inst_3 : Fintype n
inst_4 : Fintype o
inst_5 : DecidableEq n
b : Basis n R₁ M₁
M₂' : Type u_7
inst_6 : AddCommMonoid M₂'
inst_7 : Module R₁ M₂'
c : Basis o R₁ M₂'
inst_8 : DecidableEq o
M : Matrix n n R₁
P Q : Matrix n o R₁
x y : M₂'
⊢ Eq.{u_1 + 1} (α := R₁)
    ((((BilinForm.comp.{u_2, u_1, u_7} (M' := M₁) ((toLinearMap₂ b b : (a : Matrix n n R₁) → BilinForm R₁ M₁) M)
                  ((toLin c b : (a : Matrix n o R₁) → M₂' →ₗ[R₁] M₁) P)
                  ((toLin c b : (a : Matrix n o R₁) → M₂' →ₗ[R₁] M₁) Q) :
                (a : M₂') → M₂' →ₗ[R₁] R₁)
              x :
            M₂' →ₗ[R₁] R₁) :
          (a : M₂') → R₁)
        y :
      R₁)
    ((((compl₁₂.{u_1, u_1, u_2, u_2, u_1, u_7, u_7} (Mₗ := M₁) (N := M₁)
                  ((toLinearMap₂ b b : (a : Matrix n n R₁) → M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁) M)
                  ((toLin c b : (a : Matrix n o R₁) → M₂' →ₗ[R₁] M₁) P)
                  ((toLin c b : (a : Matrix n o R₁) → M₂' →ₗ[R₁] M₁) Q) :
                (a : M₂') → M₂' →ₗ[R₁] R₁)
              x :
            M₂' →ₗ[R₁] R₁) :
          (a : M₂') → R₁)
        y :
      R₁)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
inst : CommRing R₂
n : Type u_5
inst_1 : Fintype n
J A A' : Matrix n n R₂
inst_2 : DecidableEq n
P : Matrix n n R₂
h : IsUnit P
⊢ (Pᵀ * J * P).IsAdjointPair (Pᵀ * J * P) A A' ↔ J.IsAdjointPair J (P * A * P⁻¹) (P * A' * P⁻¹)

Tactic:
Matrix.isAdjointPair_equiv _ _ _ _ h

Premises used: Matrix.isAdjointPair_equiv
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
inst : CommRing R₂
n : Type u_5
inst_1 : Fintype n
J J₃ A : Matrix n n R₂
inst_2 : DecidableEq n
⊢ Membership.mem (γ := Submodule R₂ (Matrix n n R₂)) (pairSelfAdjointMatricesSubmodule J J₃) A ↔ J.IsAdjointPair J₃ A A

Tactic:
simp only [mem_pairSelfAdjointMatricesSubmodule]

Premises used: mem_pairSelfAdjointMatricesSubmodule
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
inst : CommRing R₂
n : Type u_5
inst_1 : Fintype n
J A : Matrix n n R₂
inst_2 : DecidableEq n
⊢ Membership.mem (γ := Submodule R₂ (Matrix n n R₂)) (selfAdjointMatricesSubmodule J) A ↔ J.IsSelfAdjoint A

Tactic:
simp only [mem_selfAdjointMatricesSubmodule]

Premises used: mem_selfAdjointMatricesSubmodule
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
inst : CommRing R₂
n : Type u_5
inst_1 : Fintype n
J A : Matrix n n R₂
inst_2 : DecidableEq n
⊢ Membership.mem (γ := Submodule R₂ (Matrix n n R₂)) (skewAdjointMatricesSubmodule J) A ↔ J.IsSkewAdjoint A

Tactic:
simp only [mem_skewAdjointMatricesSubmodule]

Premises used: mem_skewAdjointMatricesSubmodule
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₁ : Type u_1
M₁ : Type u_2
inst : CommSemiring R₁
inst_1 : AddCommMonoid M₁
inst_2 : Module R₁ M₁
ι : Type u_6
inst_3 : DecidableEq ι
inst_4 : Fintype ι
M : Matrix ι ι R₁
b : Basis ι R₁ M₁
⊢ Nondegenerate (R := R₁) (M := ι → R₁) ((toBilin' : (a : Matrix ι ι R₁) → BilinForm R₁ (ι → R₁)) M) ↔
    Nondegenerate.{u_1, u_2} (R := R₁) (M := M₁) ((toBilin b : (a : Matrix ι ι R₁) → BilinForm R₁ M₁) M)

Tactic:
(nondegenerate_congr_iff b.equivFun.symm).symm

Premises used: Multiset.sum, Multiset.foldr, LinearEquiv.symm, LinearMap.BilinForm.nondegenerate_congr_iff, Finset.sum, Iff.symm, Module.Basis.equivFun
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
inst : CommRing R₂
ι : Type u_6
inst_1 : DecidableEq ι
inst_2 : Fintype ι
M : Matrix ι ι R₂
h : M.Nondegenerate
⊢ Nondegenerate (R := R₂) (M := ι → R₂) ((toBilin' : (a : Matrix ι ι R₂) → BilinForm R₂ (ι → R₂)) M)

Tactic:
h.toLinearMap₂'

Premises used: Matrix.Nondegenerate.toLinearMap₂'
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
inst : CommRing R₂
ι : Type u_6
inst_1 : DecidableEq ι
inst_2 : Fintype ι
M : Matrix ι ι R₂
⊢ Nondegenerate (R := R₂) (M := ι → R₂) ((toBilin' : (a : Matrix ι ι R₂) → BilinForm R₂ (ι → R₂)) M) ↔ M.Nondegenerate

Tactic:
Matrix.nondegenerate_toLinearMap₂'_iff

Premises used: Matrix.nondegenerate_toLinearMap₂'_iff
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
M₂ : Type u_4
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
ι : Type u_6
inst_3 : DecidableEq ι
inst_4 : Fintype ι
M : Matrix ι ι R₂
h : M.Nondegenerate
b : Basis ι R₂ M₂
⊢ Nondegenerate.{u_3, u_4} (R := R₂) (M := M₂) ((toBilin b : (a : Matrix ι ι R₂) → BilinForm R₂ M₂) M)

Tactic:
h.toLinearMap₂ b b

Premises used: Matrix.Nondegenerate.toLinearMap₂
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
M₂ : Type u_4
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
ι : Type u_6
inst_3 : DecidableEq ι
inst_4 : Fintype ι
M : Matrix ι ι R₂
b : Basis ι R₂ M₂
⊢ Nondegenerate.{u_3, u_4} (R := R₂) (M := M₂) ((toBilin b : (a : Matrix ι ι R₂) → BilinForm R₂ M₂) M) ↔ M.Nondegenerate

Tactic:
Matrix.nondegenerate_toLinearMap₂_iff b b

Premises used: Matrix.nondegenerate_toLinearMap₂_iff
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
inst : CommRing R₂
ι : Type u_6
inst_1 : DecidableEq ι
inst_2 : Fintype ι
M : Matrix ι ι R₂
h : M.SeparatingLeft
⊢ SeparatingLeft (R := R₂) (R₁ := R₂) (R₂ := R₂) (M := R₂) (M₁ := ι → R₂) (M₂ := ι → R₂) (I₁ := RingHom.id R₂) (I₂ :=
    RingHom.id R₂) ((toBilin' : (a : Matrix ι ι R₂) → BilinForm R₂ (ι → R₂)) M)

Tactic:
h.toLinearMap₂'

Premises used: Matrix.SeparatingLeft.toLinearMap₂'
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
inst : CommRing R₂
ι : Type u_6
inst_1 : DecidableEq ι
inst_2 : Fintype ι
M : Matrix ι ι R₂
⊢ SeparatingLeft (R := R₂) (R₁ := R₂) (R₂ := R₂) (M := R₂) (M₁ := ι → R₂) (M₂ := ι → R₂) (I₁ := RingHom.id R₂) (I₂ :=
      RingHom.id R₂) ((toBilin' : (a : Matrix ι ι R₂) → BilinForm R₂ (ι → R₂)) M) ↔
    M.SeparatingLeft

Tactic:
Matrix.separatingLeft_toLinearMap₂'_iff

Premises used: Matrix.separatingLeft_toLinearMap₂'_iff
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
M₂ : Type u_4
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
ι : Type u_6
inst_3 : DecidableEq ι
inst_4 : Fintype ι
M : Matrix ι ι R₂
h : M.SeparatingLeft
b : Basis ι R₂ M₂
⊢ SeparatingLeft.{u_3, u_3, u_3, u_3, u_4, u_4} (R := R₂) (R₁ := R₂) (R₂ := R₂) (M := R₂) (M₁ := M₂) (M₂ := M₂) (I₁ :=
    RingHom.id R₂) (I₂ := RingHom.id R₂) ((toBilin b : (a : Matrix ι ι R₂) → BilinForm R₂ M₂) M)

Tactic:
h.toLinearMap₂ b b

Premises used: Matrix.SeparatingLeft.toLinearMap₂
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
M₂ : Type u_4
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
ι : Type u_6
inst_3 : DecidableEq ι
inst_4 : Fintype ι
M : Matrix ι ι R₂
b : Basis ι R₂ M₂
⊢ SeparatingLeft.{u_3, u_3, u_3, u_3, u_4, u_4} (R := R₂) (R₁ := R₂) (R₂ := R₂) (M := R₂) (M₁ := M₂) (M₂ := M₂) (I₁ :=
      RingHom.id R₂) (I₂ := RingHom.id R₂) ((toBilin b : (a : Matrix ι ι R₂) → BilinForm R₂ M₂) M) ↔
    M.SeparatingLeft

Tactic:
Matrix.separatingLeft_toLinearMap₂_iff b b

Premises used: Matrix.separatingLeft_toLinearMap₂_iff
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
inst : CommRing R₂
ι : Type u_6
inst_1 : DecidableEq ι
inst_2 : Fintype ι
M : Matrix ι ι R₂
h : M.SeparatingRight
⊢ SeparatingRight (R := R₂) (R₁ := R₂) (R₂ := R₂) (M := R₂) (M₁ := ι → R₂) (M₂ := ι → R₂) (I₁ := RingHom.id R₂) (I₂ :=
    RingHom.id R₂) ((toBilin' : (a : Matrix ι ι R₂) → BilinForm R₂ (ι → R₂)) M)

Tactic:
h.toLinearMap₂'

Premises used: Matrix.SeparatingRight.toLinearMap₂'
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
inst : CommRing R₂
ι : Type u_6
inst_1 : DecidableEq ι
inst_2 : Fintype ι
M : Matrix ι ι R₂
⊢ SeparatingRight (R := R₂) (R₁ := R₂) (R₂ := R₂) (M := R₂) (M₁ := ι → R₂) (M₂ := ι → R₂) (I₁ := RingHom.id R₂) (I₂ :=
      RingHom.id R₂) ((toBilin' : (a : Matrix ι ι R₂) → BilinForm R₂ (ι → R₂)) M) ↔
    M.SeparatingRight

Tactic:
Matrix.separatingRight_toLinearMap₂'_iff

Premises used: Matrix.separatingRight_toLinearMap₂'_iff
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
M₂ : Type u_4
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
ι : Type u_6
inst_3 : DecidableEq ι
inst_4 : Fintype ι
M : Matrix ι ι R₂
h : M.SeparatingRight
b : Basis ι R₂ M₂
⊢ SeparatingRight.{u_3, u_3, u_3, u_3, u_4, u_4} (R := R₂) (R₁ := R₂) (R₂ := R₂) (M := R₂) (M₁ := M₂) (M₂ := M₂) (I₁ :=
    RingHom.id R₂) (I₂ := RingHom.id R₂) ((toBilin b : (a : Matrix ι ι R₂) → BilinForm R₂ M₂) M)

Tactic:
h.toLinearMap₂ b b

Premises used: Matrix.SeparatingRight.toLinearMap₂
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
M₂ : Type u_4
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
ι : Type u_6
inst_3 : DecidableEq ι
inst_4 : Fintype ι
M : Matrix ι ι R₂
b : Basis ι R₂ M₂
⊢ SeparatingRight.{u_3, u_3, u_3, u_3, u_4, u_4} (R := R₂) (R₁ := R₂) (R₂ := R₂) (M := R₂) (M₁ := M₂) (M₂ := M₂) (I₁ :=
      RingHom.id R₂) (I₂ := RingHom.id R₂) ((toBilin b : (a : Matrix ι ι R₂) → BilinForm R₂ M₂) M) ↔
    M.SeparatingRight

Tactic:
Matrix.separatingRight_toLinearMap₂_iff b b

Premises used: Matrix.separatingRight_toLinearMap₂_iff
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
inst : CommRing R₂
ι : Type u_6
inst_1 : DecidableEq ι
inst_2 : Fintype ι
B : BilinForm R₂ (ι → R₂)
⊢ Matrix.Nondegenerate.{u_6, u_6, u_3} (m := ι) (n := ι) (R := R₂)
      ((toMatrix' : (a : BilinForm R₂ (ι → R₂)) → Matrix ι ι R₂) B) ↔
    B.Nondegenerate

Tactic:
LinearMap.nondegenerate_toMatrix₂'_iff

Premises used: LinearMap.nondegenerate_toMatrix₂'_iff
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
inst : CommRing R₂
ι : Type u_6
inst_1 : DecidableEq ι
inst_2 : Fintype ι
B : BilinForm R₂ (ι → R₂)
h : B.Nondegenerate
⊢ Matrix.Nondegenerate.{u_6, u_6, u_3} (m := ι) (n := ι) (R := R₂)
    ((BilinForm.toMatrix' : (a : BilinForm R₂ (ι → R₂)) → Matrix ι ι R₂) B)

Tactic:
h.toMatrix₂'

Premises used: LinearMap.Nondegenerate.toMatrix₂'
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
M₂ : Type u_4
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
ι : Type u_6
inst_3 : DecidableEq ι
inst_4 : Fintype ι
B : BilinForm R₂ M₂
b : Basis ι R₂ M₂
⊢ Matrix.Nondegenerate.{u_6, u_6, u_3} (m := ι) (n := ι) (R := R₂)
      ((toMatrix b : (a : BilinForm R₂ M₂) → Matrix ι ι R₂) B) ↔
    B.Nondegenerate

Tactic:
(Matrix.nondegenerate_toBilin_iff b).symm.trans <| (Matrix.toBilin_toMatrix b B).symm ▸ Iff.rfl

Premises used: Iff.rfl, Eq.rec, Matrix.nondegenerate_toBilin_iff, Matrix.toBilin_toMatrix, Iff.trans, Eq.symm, Iff.symm
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
M₂ : Type u_4
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
ι : Type u_6
inst_3 : DecidableEq ι
inst_4 : Fintype ι
B : BilinForm R₂ M₂
h : B.Nondegenerate
b : Basis ι R₂ M₂
⊢ Matrix.Nondegenerate.{u_6, u_6, u_3} (m := ι) (n := ι) (R := R₂)
    ((BilinForm.toMatrix b : (a : BilinForm R₂ M₂) → Matrix ι ι R₂) B)

Tactic:
(nondegenerate_toMatrix_iff b).mpr h

Premises used: Iff.mpr, LinearMap.BilinForm.nondegenerate_toMatrix_iff
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
inst : CommRing R₂
ι : Type u_6
inst_1 : DecidableEq ι
inst_2 : Fintype ι
B : BilinForm R₂ (ι → R₂)
⊢ Matrix.SeparatingLeft.{u_6, u_6, u_3} (m := ι) (n := ι) (R := R₂)
      ((toMatrix' : (a : BilinForm R₂ (ι → R₂)) → Matrix ι ι R₂) B) ↔
    SeparatingLeft B

Tactic:
Matrix.separatingLeft_toBilin'_iff.symm.trans <| (Matrix.toBilin'_toMatrix' B).symm ▸ Iff.rfl

Premises used: Matrix.separatingLeft_toBilin'_iff, Iff.trans, Iff.symm
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
inst : CommRing R₂
ι : Type u_6
inst_1 : DecidableEq ι
inst_2 : Fintype ι
B : BilinForm R₂ (ι → R₂)
h : SeparatingLeft B
⊢ Matrix.SeparatingLeft.{u_6, u_6, u_3} (m := ι) (n := ι) (R := R₂)
    ((BilinForm.toMatrix' : (a : BilinForm R₂ (ι → R₂)) → Matrix ι ι R₂) B)

Tactic:
separatingLeft_toMatrix'_iff.mpr h

Premises used: Iff.mpr, LinearMap.BilinForm.separatingLeft_toMatrix'_iff