awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
h :
  SeparatingLeft (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
    RingHom.id R)
    (((toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
        (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
      M)
⊢ ∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0

Tactic:
exact fun v hv => h v fun w => (M.toLinearMap₂'_apply' _ _).trans <| hv w

Premises used: Matrix.toLinearMap₂'_apply', Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
⊢ SeparatingRight (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R)
      (((toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
          (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
        M) ↔
    M.SeparatingRight

Tactic:
⟨fun h ↦ separatingRight_def.mpr ?_, SeparatingRight.toLinearMap₂'⟩

Premises used: Iff.mpr, Matrix.SeparatingRight.toLinearMap₂', Iff.intro, Matrix.separatingRight_def
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
refine :
  ∀
    (h :
      SeparatingRight (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
        RingHom.id R)
        (((toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
            (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
          M))
    (w : n → R), (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0
⊢ SeparatingRight (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R)
      (((toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
          (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
        M) ↔
    M.SeparatingRight

Tactic:
refine ⟨fun h ↦ separatingRight_def.mpr ?_, SeparatingRight.toLinearMap₂'⟩
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
h :
  SeparatingRight (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
    RingHom.id R)
    (((toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
        (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
      M)
⊢ ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0

Tactic:
fun v hv => h v fun w => (M.toLinearMap₂'_apply' _ _).trans <| hv w

Premises used: Matrix.toLinearMap₂'_apply', Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
h :
  SeparatingRight (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
    RingHom.id R)
    (((toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
        (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
      M)
⊢ ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0

Tactic:
exact fun v hv => h v fun w => (M.toLinearMap₂'_apply' _ _).trans <| hv w

Premises used: Matrix.toLinearMap₂'_apply', Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
⊢ Nondegenerate (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R)
      (((toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
          (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
        M) ↔
    M.Nondegenerate

Tactic:
⟨fun h ↦ ⟨separatingLeft_toLinearMap₂'_iff.mp h.1, separatingRight_toLinearMap₂'_iff.mp h.2⟩,
   fun h ↦ ⟨separatingLeft_toLinearMap₂'_iff.mpr h.1, separatingRight_toLinearMap₂'_iff.mpr h.2⟩⟩

Premises used: Iff.mpr, Matrix.separatingRight_toLinearMap₂'_iff, Matrix.Nondegenerate.separatingRight, Matrix.Nondegenerate.mk, And.right, And.left, And.intro, Matrix.separatingLeft_toLinearMap₂'_iff, Iff.intro, Iff.mp, Matrix.Nondegenerate.separatingLeft
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
B : (m → R) →ₗ[R] (n → R) →ₗ[R] R
⊢ Matrix.SeparatingLeft.{u_12, u_11, u_1} (m := m) (n := n) (R := R)
      (((toMatrix₂' R : ((m → R) →ₗ[R] (n → R) →ₗ[R] R) ≃ₗ[R] Matrix m n R) :
          (a : (m → R) →ₗ[R] (n → R) →ₗ[R] R) → Matrix m n R)
        B) ↔
    B.SeparatingLeft

Tactic:
separatingLeft_toLinearMap₂'_iff.symm.trans <| (toLinearMap₂'_toMatrix' (R := R) B).symm ▸ Iff.rfl

Premises used: Matrix.separatingLeft_toLinearMap₂'_iff, Iff.trans, Iff.symm
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
B : (m → R) →ₗ[R] (n → R) →ₗ[R] R
⊢ Matrix.SeparatingRight.{u_12, u_11, u_1} (m := m) (n := n) (R := R)
      (((toMatrix₂' R : ((m → R) →ₗ[R] (n → R) →ₗ[R] R) ≃ₗ[R] Matrix m n R) :
          (a : (m → R) →ₗ[R] (n → R) →ₗ[R] R) → Matrix m n R)
        B) ↔
    B.SeparatingRight

Tactic:
separatingRight_toLinearMap₂'_iff.symm.trans
    <| (toLinearMap₂'_toMatrix' (R := R) B).symm ▸ Iff.rfl

Premises used: Matrix.separatingRight_toLinearMap₂'_iff, Iff.trans, Iff.symm
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
B : (m → R) →ₗ[R] (n → R) →ₗ[R] R
⊢ Matrix.Nondegenerate.{u_12, u_11, u_1} (m := m) (n := n) (R := R)
      (((toMatrix₂' R : ((m → R) →ₗ[R] (n → R) →ₗ[R] R) ≃ₗ[R] Matrix m n R) :
          (a : (m → R) →ₗ[R] (n → R) →ₗ[R] R) → Matrix m n R)
        B) ↔
    B.Nondegenerate

Tactic:
nondegenerate_toLinearMap₂'_iff.symm.trans <| (toLinearMap₂'_toMatrix' (R := R) B).symm ▸ Iff.rfl

Premises used: Iff.trans, Matrix.nondegenerate_toLinearMap₂'_iff, Iff.symm
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
B : (m → R) →ₗ[R] (n → R) →ₗ[R] R
h : B.SeparatingLeft
⊢ Matrix.SeparatingLeft.{u_12, u_11, u_1} (m := m) (n := n) (R := R)
    (((LinearMap.toMatrix₂' R : ((m → R) →ₗ[R] (n → R) →ₗ[R] R) ≃ₗ[R] Matrix m n R) :
        (a : (m → R) →ₗ[R] (n → R) →ₗ[R] R) → Matrix m n R)
      B)

Tactic:
separatingLeft_toMatrix₂'_iff.mpr h

Premises used: Iff.mpr, LinearMap.separatingLeft_toMatrix₂'_iff
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
B : (m → R) →ₗ[R] (n → R) →ₗ[R] R
h : B.SeparatingRight
⊢ Matrix.SeparatingRight.{u_12, u_11, u_1} (m := m) (n := n) (R := R)
    (((LinearMap.toMatrix₂' R : ((m → R) →ₗ[R] (n → R) →ₗ[R] R) ≃ₗ[R] Matrix m n R) :
        (a : (m → R) →ₗ[R] (n → R) →ₗ[R] R) → Matrix m n R)
      B)

Tactic:
separatingRight_toMatrix₂'_iff.mpr h

Premises used: Iff.mpr, LinearMap.separatingRight_toMatrix₂'_iff
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
B : (m → R) →ₗ[R] (n → R) →ₗ[R] R
h : B.Nondegenerate
⊢ Matrix.Nondegenerate.{u_12, u_11, u_1} (m := m) (n := n) (R := R)
    (((LinearMap.toMatrix₂' R : ((m → R) →ₗ[R] (n → R) →ₗ[R] R) ≃ₗ[R] Matrix m n R) :
        (a : (m → R) →ₗ[R] (n → R) →ₗ[R] R) → Matrix m n R)
      B)

Tactic:
nondegenerate_toMatrix₂'_iff.mpr h

Premises used: Iff.mpr, LinearMap.nondegenerate_toMatrix₂'_iff
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
inst_5 : AddCommMonoid M₁
inst_6 : Module R M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
⊢ SeparatingLeft (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R)
      (((toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
          (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
        M) ↔
    SeparatingLeft.{u_1, u_1, u_1, u_1, u_6, u_7} (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := M₁) (M₂ := M₂) (I₁ :=
      RingHom.id R) (I₂ := RingHom.id R) ((toLinearMap₂ b₁ b₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂ →ₗ[R] R) M)

Tactic:
(separatingLeft_congr_iff b₁.equivFun.symm b₂.equivFun.symm).symm

Premises used: Multiset.sum, Multiset.foldr, LinearEquiv.symm, LinearMap.separatingLeft_congr_iff, Finset.sum, Iff.symm, Module.Basis.equivFun
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
inst_5 : AddCommMonoid M₁
inst_6 : Module R M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
⊢ SeparatingRight (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R)
      (((toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
          (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
        M) ↔
    SeparatingRight.{u_1, u_1, u_1, u_1, u_6, u_7} (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := M₁) (M₂ := M₂) (I₁ :=
      RingHom.id R) (I₂ := RingHom.id R) ((toLinearMap₂ b₁ b₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂ →ₗ[R] R) M)

Tactic:
(separatingRight_congr_iff b₁.equivFun.symm b₂.equivFun.symm).symm

Premises used: Multiset.sum, Multiset.foldr, LinearEquiv.symm, LinearMap.separatingRight_congr_iff, Finset.sum, Iff.symm, Module.Basis.equivFun
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
inst_5 : AddCommMonoid M₁
inst_6 : Module R M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
⊢ Nondegenerate (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R)
      (((toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
          (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
        M) ↔
    Nondegenerate.{u_1, u_1, u_1, u_1, u_6, u_7} (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := M₁) (M₂ := M₂) (I₁ :=
      RingHom.id R) (I₂ := RingHom.id R) ((toLinearMap₂ b₁ b₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂ →ₗ[R] R) M)

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

Premises used: Multiset.sum, Multiset.foldr, LinearEquiv.symm, LinearMap.nondegenerate_congr_iff, Finset.sum, Iff.symm, Module.Basis.equivFun
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
inst_5 : AddCommMonoid M₁
inst_6 : Module R M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
rw :
  SeparatingLeft (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R)
      (((toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
          (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
        M) ↔
    M.SeparatingLeft
rw₁ rw₂ : M.SeparatingLeft ↔ M.SeparatingLeft
⊢ SeparatingLeft.{u_1, u_1, u_1, u_1, u_6, u_7} (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := M₁) (M₂ := M₂) (I₁ :=
      RingHom.id R) (I₂ := RingHom.id R) ((toLinearMap₂ b₁ b₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂ →ₗ[R] R) M) ↔
    M.SeparatingLeft

Tactic:
rw [← separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂,
    separatingLeft_toLinearMap₂'_iff]

Premises used: Matrix.separatingLeft_toLinearMap₂'_iff, Matrix.separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
inst_5 : AddCommMonoid M₁
inst_6 : Module R M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
rw :
  SeparatingRight (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R)
      (((toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
          (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
        M) ↔
    M.SeparatingRight
rw₁ rw₂ : M.SeparatingRight ↔ M.SeparatingRight
⊢ SeparatingRight.{u_1, u_1, u_1, u_1, u_6, u_7} (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := M₁) (M₂ := M₂) (I₁ :=
      RingHom.id R) (I₂ := RingHom.id R) ((toLinearMap₂ b₁ b₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂ →ₗ[R] R) M) ↔
    M.SeparatingRight

Tactic:
rw [← separatingRight_toLinearMap₂'_iff_separatingRight_toLinearMap₂,
    separatingRight_toLinearMap₂'_iff]

Premises used: Matrix.separatingRight_toLinearMap₂'_iff, Matrix.separatingRight_toLinearMap₂'_iff_separatingRight_toLinearMap₂
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
inst_5 : AddCommMonoid M₁
inst_6 : Module R M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
rw :
  Nondegenerate (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R)
      (((toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
          (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
        M) ↔
    M.Nondegenerate
rw₁ rw₂ : M.Nondegenerate ↔ M.Nondegenerate
⊢ Nondegenerate.{u_1, u_1, u_1, u_1, u_6, u_7} (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := M₁) (M₂ := M₂) (I₁ :=
      RingHom.id R) (I₂ := RingHom.id R) ((toLinearMap₂ b₁ b₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂ →ₗ[R] R) M) ↔
    M.Nondegenerate

Tactic:
rw [← nondegenerate_toLinearMap₂'_iff_nondegenerate_toLinearMap₂,
    nondegenerate_toLinearMap₂'_iff]

Premises used: Matrix.nondegenerate_toLinearMap₂'_iff_nondegenerate_toLinearMap₂, Matrix.nondegenerate_toLinearMap₂'_iff
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
inst_5 : AddCommMonoid M₁
inst_6 : Module R M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
h : M.SeparatingLeft
⊢ SeparatingLeft.{u_1, u_1, u_1, u_1, u_6, u_7} (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := M₁) (M₂ := M₂) (I₁ :=
    RingHom.id R) (I₂ := RingHom.id R) ((toLinearMap₂ b₁ b₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂ →ₗ[R] R) M)

Tactic:
(separatingLeft_toLinearMap₂_iff b₁ b₂).mpr h

Premises used: Iff.mpr, Matrix.separatingLeft_toLinearMap₂_iff
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
inst_5 : AddCommMonoid M₁
inst_6 : Module R M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
h : M.SeparatingRight
⊢ SeparatingRight.{u_1, u_1, u_1, u_1, u_6, u_7} (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := M₁) (M₂ := M₂) (I₁ :=
    RingHom.id R) (I₂ := RingHom.id R) ((toLinearMap₂ b₁ b₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂ →ₗ[R] R) M)

Tactic:
(separatingRight_toLinearMap₂_iff b₁ b₂).mpr h

Premises used: Iff.mpr, Matrix.separatingRight_toLinearMap₂_iff
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
inst_5 : AddCommMonoid M₁
inst_6 : Module R M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
h : M.Nondegenerate
⊢ Nondegenerate.{u_1, u_1, u_1, u_1, u_6, u_7} (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := M₁) (M₂ := M₂) (I₁ :=
    RingHom.id R) (I₂ := RingHom.id R) ((toLinearMap₂ b₁ b₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂ →ₗ[R] R) M)

Tactic:
(nondegenerate_toLinearMap₂_iff b₁ b₂).mpr h

Premises used: Iff.mpr, Matrix.nondegenerate_toLinearMap₂_iff
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
inst_5 : AddCommMonoid M₁
inst_6 : Module R M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
B : M₁ →ₗ[R] M₂ →ₗ[R] R
⊢ Matrix.SeparatingLeft.{u_12, u_11, u_1} (m := m) (n := n) (R := R)
      ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix m n R) B) ↔
    B.SeparatingLeft

Tactic:
(Matrix.separatingLeft_toLinearMap₂_iff b₁ b₂).symm.trans <|
    (Matrix.toLinearMap₂_toMatrix₂ b₁ b₂ B).symm ▸ Iff.rfl

Premises used: Matrix.toLinearMap₂_toMatrix₂, Iff.rfl, Eq.rec, Matrix.separatingLeft_toLinearMap₂_iff, Iff.trans, Eq.symm, Iff.symm
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
inst_5 : AddCommMonoid M₁
inst_6 : Module R M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
B : M₁ →ₗ[R] M₂ →ₗ[R] R
⊢ Matrix.SeparatingRight.{u_12, u_11, u_1} (m := m) (n := n) (R := R)
      ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix m n R) B) ↔
    B.SeparatingRight

Tactic:
(Matrix.separatingRight_toLinearMap₂_iff b₁ b₂).symm.trans <|
    (Matrix.toLinearMap₂_toMatrix₂ b₁ b₂ B).symm ▸ Iff.rfl

Premises used: Matrix.separatingRight_toLinearMap₂_iff, Matrix.toLinearMap₂_toMatrix₂, Iff.rfl, Eq.rec, Iff.trans, Eq.symm, Iff.symm
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
inst_5 : AddCommMonoid M₁
inst_6 : Module R M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
B : M₁ →ₗ[R] M₂ →ₗ[R] R
⊢ Matrix.Nondegenerate.{u_12, u_11, u_1} (m := m) (n := n) (R := R)
      ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix m n R) B) ↔
    B.Nondegenerate

Tactic:
(Matrix.nondegenerate_toLinearMap₂_iff b₁ b₂).symm.trans <|
    (Matrix.toLinearMap₂_toMatrix₂ b₁ b₂ B).symm ▸ Iff.rfl

Premises used: Matrix.toLinearMap₂_toMatrix₂, Iff.rfl, Eq.rec, Matrix.nondegenerate_toLinearMap₂_iff, Iff.trans, Eq.symm, Iff.symm
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
inst_5 : AddCommMonoid M₁
inst_6 : Module R M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
B : M₁ →ₗ[R] M₂ →ₗ[R] R
h : B.SeparatingLeft
⊢ Matrix.SeparatingLeft.{u_12, u_11, u_1} (m := m) (n := n) (R := R)
    ((LinearMap.toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix m n R) B)

Tactic:
(separatingLeft_toMatrix₂_iff b₁ b₂).mpr h

Premises used: Iff.mpr, LinearMap.separatingLeft_toMatrix₂_iff
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
inst_5 : AddCommMonoid M₁
inst_6 : Module R M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
B : M₁ →ₗ[R] M₂ →ₗ[R] R
h : B.SeparatingRight
⊢ Matrix.SeparatingRight.{u_12, u_11, u_1} (m := m) (n := n) (R := R)
    ((LinearMap.toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix m n R) B)

Tactic:
(separatingRight_toMatrix₂_iff b₁ b₂).mpr h

Premises used: Iff.mpr, LinearMap.separatingRight_toMatrix₂_iff
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
inst_5 : AddCommMonoid M₁
inst_6 : Module R M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
B : M₁ →ₗ[R] M₂ →ₗ[R] R
h : B.Nondegenerate
⊢ Matrix.Nondegenerate.{u_12, u_11, u_1} (m := m) (n := n) (R := R)
    ((LinearMap.toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix m n R) B)

Tactic:
(nondegenerate_toMatrix₂_iff b₁ b₂).mpr h

Premises used: Iff.mpr, LinearMap.nondegenerate_toMatrix₂_iff
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : IsDomain R
M : Matrix n n R
rw : M.Nondegenerate ↔ M.det ≠ 0
rw₁ rw₂ : M.det ≠ 0 ↔ M.det ≠ 0
⊢ Nondegenerate (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := n → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R)
      (((toLinearMap₂' R : Matrix n n R ≃ₗ[R] (n → R) →ₗ[R] (n → R) →ₗ[R] R) :
          (a : Matrix n n R) → (n → R) →ₗ[R] (n → R) →ₗ[R] R)
        M) ↔
    M.det ≠ 0

Tactic:
rw [nondegenerate_toLinearMap₂'_iff, Matrix.nondegenerate_iff_det_ne_zero]

Premises used: Matrix.nondegenerate_toLinearMap₂'_iff, Matrix.nondegenerate_iff_det_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : IsDomain R
M : Matrix n n R
⊢ SeparatingLeft (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := n → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R)
      (((toLinearMap₂' R : Matrix n n R ≃ₗ[R] (n → R) →ₗ[R] (n → R) →ₗ[R] R) :
          (a : Matrix n n R) → (n → R) →ₗ[R] (n → R) →ₗ[R] R)
        M) ↔
    M.det ≠ 0

Tactic:
simpa using separatingLeft_iff_det_ne_zero

Premises used: Matrix.separatingLeft_iff_det_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : IsDomain R
M : Matrix n n R
⊢ SeparatingRight (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := n → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R)
      (((toLinearMap₂' R : Matrix n n R ≃ₗ[R] (n → R) →ₗ[R] (n → R) →ₗ[R] R) :
          (a : Matrix n n R) → (n → R) →ₗ[R] (n → R) →ₗ[R] R)
        M) ↔
    M.det ≠ 0

Tactic:
simpa using separatingRight_iff_det_ne_zero

Premises used: Matrix.separatingRight_iff_det_ne_zero