awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
i j : ι
r : R
v : ι → M
i' : ι
hi : i ≠ i'
⊢ single i j r i' j • v j = Pi.single (M := fun (j : ι) ↦ M) i (r • v j) i'

Tactic:
simp [*]
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
i j : ι
r : R
v : ι → M
i' j' : ι
hj : j' ≠ j
⊢ single i j r i' j' • v j' = 0

Tactic:
simp [hj.symm]

Premises used: Ne.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
r : R
v : ι → M
h : ∀ (i : ι), HSMul.hSMul (α := Matrix ι ι R) (diagonal fun (x : ι) ↦ r) v i = (r • v) i
⊢ HSMul.hSMul (α := Matrix ι ι R) (diagonal fun (x : ι) ↦ r) v = r • v

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
r : R
v : ι → M
i : ι
⊢ HSMul.hSMul (α := Matrix ι ι R) (diagonal fun (x : ι) ↦ r) v i = (r • v) i

Tactic:
simp [Matrix.diagonal_apply]

Premises used: Matrix.diagonal_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
r : R
v : ι → M
⊢ HSMul.hSMul (α := Matrix ι ι R) ((scalar ι : (a : R) → Matrix ι ι R) r : Matrix ι ι R) v = r • v

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : AddCommGroup P
inst_8 : Module R P
S : Type u_6
inst_9 : Ring S
inst_10 : SMul R S
inst_11 : Module S M
inst_12 : IsScalarTower R S M
x : R
x_1 : Matrix ι ι S
x_2 : ι → M
h : ∀ (x_3 : ι), ((x • x_1) • x_2) x_3 = (x • x_1 • x_2) x_3
⊢ (x • x_1) • x_2 = x • x_1 • x_2

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : AddCommGroup P
inst_8 : Module R P
S : Type u_6
inst_9 : Ring S
inst_10 : SMul R S
inst_11 : Module S M
inst_12 : IsScalarTower R S M
x : R
x_1 : Matrix ι ι S
x_2 : ι → M
x_3 : ι
⊢ ((x • x_1) • x_2) x_3 = (x • x_1 • x_2) x_3

Tactic:
simp [Finset.smul_sum]

Premises used: Finset.smul_sum
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : AddCommGroup P
inst_8 : Module R P
f : M →ₗ[R] N
x : Matrix ι ι R
x_1 : ι → M
h :
  ∀ (x_2 : ι),
    (f.compLeft ι : (a : ι → M) → ι → N) (x • x_1) x_2 =
      HSMul.hSMul (α := Matrix ι ι R) (β := ι → N)
        ((RingHom.id (Matrix ι ι R) : (a : Matrix ι ι R) → Matrix ι ι R) x : Matrix ι ι R)
        ((f.compLeft ι : (a : ι → M) → ι → N) x_1 : ι → N) x_2
⊢ (f.compLeft ι : (a : ι → M) → ι → N) (x • x_1) =
    HSMul.hSMul (α := Matrix ι ι R) (β := ι → N)
      ((RingHom.id (Matrix ι ι R) : (a : Matrix ι ι R) → Matrix ι ι R) x : Matrix ι ι R)
      ((f.compLeft ι : (a : ι → M) → ι → N) x_1 : ι → N)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : AddCommGroup P
inst_8 : Module R P
f : M →ₗ[R] N
x : Matrix ι ι R
x_1 : ι → M
x_2 : ι
⊢ (f.compLeft ι : (a : ι → M) → ι → N) (x • x_1) x_2 =
    HSMul.hSMul (α := Matrix ι ι R) (β := ι → N)
      ((RingHom.id (Matrix ι ι R) : (a : Matrix ι ι R) → Matrix ι ι R) x : Matrix ι ι R)
      ((f.compLeft ι : (a : ι → M) → ι → N) x_1 : ι → N) x_2

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
h :
  ∀ (x : ι → M) (x_1 : ι),
    Eq.{u_3 + 1} (α := M) ((mapMatrixModule ι id : (a : ι → M) → ι → M) x x_1 : M)
      ((id : (a : ι → M) → ι → M) x x_1 : M)
⊢ Eq (α := LinearMap (R := Matrix ι ι R) (RingHom.id (Matrix ι ι R)) (ι → M) (ι → M)) (mapMatrixModule ι id) id

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
x : ι → M
x_1 : ι
⊢ Eq.{u_3 + 1} (α := M) ((mapMatrixModule ι id : (a : ι → M) → ι → M) x x_1 : M) ((id : (a : ι → M) → ι → M) x x_1 : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
v : ι → M
⊢ (mapMatrixModule ι id : (a : ι → M) → ι → M) v = v

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : AddCommGroup P
inst_8 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h :
  ∀ (x : ι → M) (x_1 : ι),
    Eq.{u_5 + 1} (α := P) ((mapMatrixModule ι (g ∘ₗ f) : (a : ι → M) → ι → P) x x_1 : P)
      ((mapMatrixModule ι g ∘ₗ mapMatrixModule ι f : (a : ι → M) → ι → P) x x_1 : P)
⊢ mapMatrixModule ι (g ∘ₗ f) = mapMatrixModule ι g ∘ₗ mapMatrixModule ι f

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : AddCommGroup P
inst_8 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
x : ι → M
x_1 : ι
⊢ Eq.{u_5 + 1} (α := P) ((mapMatrixModule ι (g ∘ₗ f) : (a : ι → M) → ι → P) x x_1 : P)
    ((mapMatrixModule ι g ∘ₗ mapMatrixModule ι f : (a : ι → M) → ι → P) x x_1 : P)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : AddCommGroup P
inst_8 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
v : ι → M
⊢ Eq (α := ι → P) ((mapMatrixModule ι (g ∘ₗ f) : (a : ι → M) → ι → P) v : ι → P)
    ((mapMatrixModule ι g : (a : ι → N) → ι → P) ((mapMatrixModule ι f : (a : ι → M) → ι → N) v : ι → N) : ι → P)

Tactic:
simp [mapMatrixModule_comp]

Premises used: LinearMap.mapMatrixModule_comp
-- Module: Mathlib.LinearAlgebra.Matrix.MvPolynomial
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : CommSemiring R
i : m
j : n
⊢ Eq (α := MvPolynomial (m × n) R) (mvPolynomialX m n R i j) (MvPolynomial.X (i, j))

Tactic:
rfl

Premises used: MvPolynomial.X, Matrix.mvPolynomialX, rfl, Finsupp.single
-- Module: Mathlib.LinearAlgebra.Matrix.MvPolynomial
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
A : Matrix m n S
⊢ map (mvPolynomialX m n R) (MvPolynomial.eval₂ f fun (p : m × n) ↦ A p.1 p.2) = A

Tactic:
ext fun i j => MvPolynomial.eval₂_X _ (fun p : m × n => A p.1 p.2) (i, j)

Premises used: MvPolynomial.eval₂_X, Prod.mk, Prod.fst, Prod.snd, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.MvPolynomial
Goal:
m : Type u_1
R : Type u_3
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommSemiring R
A : Matrix m m R
⊢ (RingHom.mapMatrix (MvPolynomial.eval fun (p : m × m) ↦ A p.1 p.2) :
        (a : Matrix m m (MvPolynomial (m × m) R)) → Matrix m m R)
      (mvPolynomialX m m R) =
    A

Tactic:
mvPolynomialX_map_eval₂ _ A

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, Matrix.map, Matrix.mvPolynomialX_map_eval₂, Finset.sum
-- Module: Mathlib.LinearAlgebra.Matrix.MvPolynomial
Goal:
m : Type u_1
R : Type u_3
S : Type u_4
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
A : Matrix m m S
⊢ (AlgHom.mapMatrix (MvPolynomial.aeval fun (p : m × m) ↦ A p.1 p.2) :
        (a : Matrix m m (MvPolynomial (m × m) R)) → Matrix m m S)
      (mvPolynomialX m m R) =
    A

Tactic:
mvPolynomialX_map_eval₂ _ A

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, Matrix.map, Matrix.mvPolynomialX_map_eval₂, Finset.sum
-- Module: Mathlib.LinearAlgebra.Matrix.MvPolynomial
Goal:
m : Type u_1
R : Type u_3
inst : DecidableEq m
inst_1 : Fintype m
inst_2 : CommRing R
inst_3 : Nontrivial R
h_det : Eq (α := MvPolynomial.{u_1, u_3} (m × m) R) (det (mvPolynomialX m m R)) 0
⊢ Eq.{u_3 + 1} (α := R)
    (det.{u_3, u_1} (n := m)
      ((RingHom.mapMatrix (MvPolynomial.eval fun (p : m × m) ↦ 1 p.1 p.2) :
          (a : Matrix m m (MvPolynomial (m × m) R)) → Matrix m m R)
        (mvPolynomialX m m R)))
    (det.{u_3, u_1} (n := m) 1)

Tactic:
have := congr_arg Matrix.det (mvPolynomialX_mapMatrix_eval (1 : Matrix m m R))
-- Module: Mathlib.LinearAlgebra.Matrix.MvPolynomial
Goal:
m : Type u_1
R : Type u_3
inst : DecidableEq m
inst_1 : Fintype m
inst_2 : CommRing R
inst_3 : Nontrivial R
h_det : Eq (α := MvPolynomial.{u_1, u_3} (m × m) R) (det (mvPolynomialX m m R)) 0
this :
  Eq.{u_3 + 1} (α := R)
    (det.{u_3, u_1} (n := m)
      ((RingHom.mapMatrix (MvPolynomial.eval fun (p : m × m) ↦ 1 p.1 p.2) :
          (a : Matrix m m (MvPolynomial (m × m) R)) → Matrix m m R)
        (mvPolynomialX m m R)))
    (det.{u_3, u_1} (n := m) 1)
⊢ Eq.{u_3 + 1} (α := R) 0 1

Tactic:
rw [det_one, ← RingHom.map_det, h_det, map_zero] at this

Premises used: map_zero, RingHom.map_det, Matrix.det_one
-- Module: Mathlib.LinearAlgebra.Matrix.MvPolynomial
Goal:
m : Type u_1
R : Type u_3
inst : DecidableEq m
inst_1 : Fintype m
inst_2 : CommRing R
inst_3 : Nontrivial R
h_det : Eq (α := MvPolynomial.{u_1, u_3} (m × m) R) (det (mvPolynomialX m m R)) 0
this : Eq.{u_3 + 1} (α := R) 0 1
⊢ False

Tactic:
zero_ne_one this

Premises used: zero_ne_one
-- Module: Mathlib.LinearAlgebra.Matrix.MvPolynomial
Goal:
m : Type u_1
R : Type u_3
inst : DecidableEq m
inst_1 : Fintype m
inst_2 : CommRing R
inst_3 : Nontrivial R
h_det : Eq (α := MvPolynomial.{u_1, u_3} (m × m) R) (det (mvPolynomialX m m R)) 0
this : Eq.{u_3 + 1} (α := R) 0 1
⊢ False

Tactic:
exact zero_ne_one this

Premises used: zero_ne_one
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : CommRing R
inst_1 : Fintype m
inst_2 : Fintype n
M : Matrix m n R
⊢ M.SeparatingRight ↔ ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0

Tactic:
forall_congr' fun w ↦ ⟨fun hM hw ↦ hM ?_, fun hM hw ↦ hM ?_⟩

Premises used: Matrix.SeparatingRight, Iff.intro, forall_congr'
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : CommRing R
inst_1 : Fintype m
inst_2 : Fintype n
M : Matrix m n R
refine_1 :
  ∀ (w : n → R) (hM : (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0) (hw : ∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) (v : m → R),
    v ⬝ᵥ M *ᵥ w = 0
refine_2 :
  ∀ (w : n → R) (hM : (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0) (hw : ∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) (v : m → R),
    v ⬝ᵥ M *ᵥ w = 0
⊢ M.SeparatingRight ↔ ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0

Tactic:
refine forall_congr' fun w ↦ ⟨fun hM hw ↦ hM ?_, fun hM hw ↦ hM ?_⟩

Premises used: Iff.intro, forall_congr'
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : CommRing R
inst_1 : Fintype m
inst_2 : Fintype n
M : Matrix m n R
w : n → R
hM : (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0
hw : ∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0
⊢ ∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0

Tactic:
hw
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : CommRing R
inst_1 : Fintype m
inst_2 : Fintype n
M : Matrix m n R
w : n → R
hM : (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0
hw : ∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0
⊢ ∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0

Tactic:
convert! hw
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : CommRing R
inst_1 : Fintype m
inst_2 : Fintype n
M : Matrix m n R
⊢ M.SeparatingLeft ↔ ∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0

Tactic:
forall_congr' fun v ↦ ⟨fun hM hv ↦ hM ?_, fun hM hv ↦ hM ?_⟩

Premises used: Matrix.SeparatingLeft, Iff.intro, forall_congr'
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : CommRing R
inst_1 : Fintype m
inst_2 : Fintype n
M : Matrix m n R
refine_1 :
  ∀ (v : m → R) (hM : (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0) (hv : ∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) (w : n → R),
    v ⬝ᵥ M *ᵥ w = 0
refine_2 :
  ∀ (v : m → R) (hM : (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0) (hv : ∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) (w : n → R),
    v ⬝ᵥ M *ᵥ w = 0
⊢ M.SeparatingLeft ↔ ∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0

Tactic:
refine forall_congr' fun v ↦ ⟨fun hM hv ↦ hM ?_, fun hM hv ↦ hM ?_⟩

Premises used: Iff.intro, forall_congr'
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : CommRing R
inst_1 : Fintype m
inst_2 : Fintype n
M : Matrix m n R
v : m → R
hM : (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0
hv : ∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0
⊢ ∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0

Tactic:
hv
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : CommRing R
inst_1 : Fintype m
inst_2 : Fintype n
M : Matrix m n R
v : m → R
hM : (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0
hv : ∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0
⊢ ∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0

Tactic:
convert! hv
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : CommRing R
inst_1 : Fintype m
inst_2 : Fintype n
M : Matrix m n R
mp :
  M.Nondegenerate →
    (∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0) ∧ ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0
mpr :
  ((∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0) ∧
      ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0) →
    M.Nondegenerate
⊢ M.Nondegenerate ↔
    (∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0) ∧ ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : CommRing R
inst_1 : Fintype m
inst_2 : Fintype n
M : Matrix m n R
⊢ M.Nondegenerate →
    (∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0) ∧ ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0

Tactic:
fun h ↦ ⟨separatingLeft_def.mp h.1, separatingRight_def.mp h.2⟩

Premises used: Matrix.Nondegenerate.separatingRight, Matrix.separatingLeft_def, And.intro, Iff.mp, Matrix.Nondegenerate.separatingLeft, Matrix.separatingRight_def
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : CommRing R
inst_1 : Fintype m
inst_2 : Fintype n
M : Matrix m n R
⊢ M.Nondegenerate →
    (∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0) ∧ ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0

Tactic:
exact fun h ↦ ⟨separatingLeft_def.mp h.1, separatingRight_def.mp h.2⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : CommRing R
inst_1 : Fintype m
inst_2 : Fintype n
M : Matrix m n R
⊢ ((∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0) ∧
      ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0) →
    M.Nondegenerate

Tactic:
fun h ↦ ⟨separatingLeft_def.mpr h.1, separatingRight_def.mpr h.2⟩

Premises used: Iff.mpr, Matrix.separatingLeft_def, Matrix.Nondegenerate.mk, And.right, And.left, Matrix.separatingRight_def
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : CommRing R
inst_1 : Fintype m
inst_2 : Fintype n
M : Matrix m n R
⊢ ((∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0) ∧
      ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0) →
    M.Nondegenerate

Tactic:
exact fun h ↦ ⟨separatingLeft_def.mpr h.1, separatingRight_def.mpr h.2⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : CommRing R
inst_1 : Fintype m
inst_2 : Fintype n
M : Matrix m n R
hM : M.Nondegenerate
v : m → R
hv : ∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0
⊢ v = 0

Tactic:
(nondegenerate_def.mp hM).1 v hv

Premises used: And.left, Iff.mp, Matrix.nondegenerate_def
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : CommRing R
inst_1 : Fintype m
inst_2 : Fintype n
M : Matrix m n R
hM : M.Nondegenerate
v : m → R
hv : v ≠ 0
⊢ ∃ (w : n → R), v ⬝ᵥ M *ᵥ w ≠ 0

Tactic:
not_forall.mp (mt hM.eq_zero_of_ortho hv)

Premises used: Matrix.Nondegenerate.eq_zero_of_ortho, mt, Iff.mp, Classical.not_forall
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : CommRing R
inst_1 : Fintype m
inst_2 : Fintype n
M : Matrix m n R
hM : M.Nondegenerate
w : n → R
hw : ∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0
⊢ w = 0

Tactic:
(nondegenerate_def.mp hM).2 w hw

Premises used: And.right, Iff.mp, Matrix.nondegenerate_def
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : CommRing R
inst_1 : Fintype m
inst_2 : Fintype n
M : Matrix m n R
hM : M.Nondegenerate
w : n → R
hw : w ≠ 0
⊢ ∃ (v : m → R), v ⬝ᵥ M *ᵥ w ≠ 0

Tactic:
not_forall.mp (mt hM.eq_zero_of_ortho' hw)

Premises used: mt, Iff.mp, Matrix.Nondegenerate.eq_zero_of_ortho', Classical.not_forall
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
A : Type u_4
inst : Fintype m
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
⊢ M.Nondegenerate

Tactic:
nondegenerate_def.mpr ⟨fun v h ↦ ?_, fun w h ↦ ?_⟩

Premises used: Iff.mpr, And.intro, Matrix.nondegenerate_def
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
A : Type u_4
inst : Fintype m
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
refine_1 : ∀ (v : m → A) (h : ∀ (w : m → A), v ⬝ᵥ M *ᵥ w = 0), v = 0
refine_2 : ∀ (w : m → A) (h : ∀ (v : m → A), v ⬝ᵥ M *ᵥ w = 0), w = 0
⊢ M.Nondegenerate

Tactic:
refine nondegenerate_def.mpr ⟨fun v h ↦ ?_, fun w h ↦ ?_⟩

Premises used: Iff.mpr, And.intro, Matrix.nondegenerate_def
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
A : Type u_4
inst : Fintype m
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
h : ∀ (w : m → A), v ⬝ᵥ M *ᵥ w = 0
refine_1 : ∀ (i : m), v i = 0 i
⊢ v = 0

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
A : Type u_4
inst : Fintype m
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
h : ∀ (w : m → A), v ⬝ᵥ M *ᵥ w = 0
i : m
⊢ v ⬝ᵥ M *ᵥ (M.cramer : (a : m → A) → m → A) (Pi.single (M := fun (a : m) ↦ A) i 1) = 0

Tactic:
specialize h (M.cramer (Pi.single i 1))

Premises used: Matrix.cramer, Pi.single, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
A : Type u_4
inst : Fintype m
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
i : m
h : v ⬝ᵥ M *ᵥ (M.cramer : (a : m → A) → m → A) (Pi.single (M := fun (a : m) ↦ A) i 1) = 0
⊢ v i = 0 i

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
A : Type u_4
inst : Fintype m
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
w : m → A
h : ∀ (v : m → A), v ⬝ᵥ M *ᵥ w = 0
refine_2 : ∀ (i : m), w i = 0 i
⊢ w = 0

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
A : Type u_4
inst : Fintype m
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
w : m → A
h : ∀ (v : m → A), v ⬝ᵥ M *ᵥ w = 0
i : m
refine_2 : ∀ (h : w i ≠ 0 i), ∃ (v : m → A), v ⬝ᵥ M *ᵥ w ≠ 0
⊢ w i = 0 i

Tactic:
contrapose! h
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
A : Type u_4
inst : Fintype m
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
w : m → A
i : m
h : w i ≠ 0 i
h₁ : Pi.single (M := fun (a : m) ↦ A) i 1 ᵥ* M.adjugate ⬝ᵥ M *ᵥ w ≠ 0
⊢ ∃ (v : m → A), v ⬝ᵥ M *ᵥ w ≠ 0

Tactic:
use Pi.single i 1 ᵥ* M.adjugate

Premises used: Pi.single, Matrix.adjugate, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
A : Type u_4
inst : Fintype m
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
w : m → A
i : m
h : w i ≠ 0 i
h₁ : Pi.single (M := fun (a : m) ↦ A) i 1 ᵥ* HSMul.hSMul (β := Matrix m m A) M.det 1 ⬝ᵥ w ≠ 0
⊢ Pi.single (M := fun (a : m) ↦ A) i 1 ᵥ* M.adjugate ⬝ᵥ M *ᵥ w ≠ 0

Tactic:
rw [dotProduct_mulVec, vecMul_vecMul, adjugate_mul]

Premises used: Matrix.vecMul_vecMul, Matrix.adjugate_mul, Matrix.dotProduct_mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
A : Type u_4
inst : Fintype m
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
w : m → A
i : m
h : w i ≠ 0 i
⊢ Pi.single (M := fun (a : m) ↦ A) i 1 ᵥ* HSMul.hSMul (β := Matrix m m A) M.det 1 ⬝ᵥ w ≠ 0

Tactic:
simp_all [dotProduct, smul_apply, smul_eq_mul, Matrix.one_apply]

Premises used: dotProduct, Matrix.one_apply, Matrix.smul_apply, smul_eq_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
A : Type u_4
inst : Fintype m
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
hv : v ᵥ* M = 0
w : m → A
rw : v ᵥ* M ⬝ᵥ w = 0
rw₁ : 0 ⬝ᵥ w = 0
rw₂ rw₃ : Eq.{u_4 + 1} (α := A) 0 0
⊢ v ⬝ᵥ M *ᵥ w = 0

Tactic:
rw [dotProduct_mulVec, hv, zero_dotProduct]

Premises used: zero_dotProduct, Matrix.dotProduct_mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
m : Type u_1
A : Type u_4
inst : Fintype m
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
hv : M *ᵥ v = 0
rwa rwa₁ rwa₂ rwa₃ : M.det ≠ 0
⊢ Mᵀ.det ≠ 0

Tactic:
rwa [det_transpose]

Premises used: Matrix.det_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst : Fintype ι
inst_1 : Finite κ
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
v : ι → M
hv : LinearIndependent R v
A : Matrix κ ι R
hA : A.Nondegenerate
have : ∀ (this : Fintype κ), LinearIndependent.{u_2, u_3, u_4} R (M := M) fun (i : κ) ↦ ∑ j : ι, A i j • v j
⊢ LinearIndependent.{u_2, u_3, u_4} R (M := M) fun (i : κ) ↦ ∑ j : ι, A i j • v j

Tactic:
have : Fintype κ := Fintype.ofFinite _
-- Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst : Fintype ι
inst_1 : Finite κ
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
v : ι → M
hv : LinearIndependent R v
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
rw :
  ∀ (hv : ∀ (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0 → ∀ (i : ι), g i = 0) {A : Matrix κ ι R}
    (hA : A.Nondegenerate) (this : Fintype κ) (g : κ → R),
    Eq.{u_4 + 1} (α := M) (∑ i : κ, HSMul.hSMul (β := M) (g i) (∑ j : ι, A i j • v j)) 0 → ∀ (i : κ), g i = 0
⊢ LinearIndependent.{u_2, u_3, u_4} R (M := M) fun (i : κ) ↦ ∑ j : ι, A i j • v j

Tactic:
rw [Fintype.linearIndependent_iff] at hv ⊢

Premises used: Fintype.linearIndependent_iff