awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype n
inst_4 : StarOrderedRing R'
inst_5 : Finite m
inst_6 : DecidableEq n
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hD : D.PosDef
inst_7 : Invertible D
⊢ B = Bᴴᴴ

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ : Q.toMatrix'.PosDef
rw :
  QuadraticMap.PosDef.{0, u_1, 0} (M := n → ℝ) (N := ℝ)
    (LinearMap.BilinMap.toQuadraticMap
      (LinearEquiv.invFun (LinearMap.toMatrix₂' ℝ : ((n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ) ≃ₗ[ℝ] Matrix n n ℝ)
        (AddHom.toFun (M := (n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ)
          (LinearMap.toAddHom
            ((↑(LinearMap.toMatrix₂' ℝ) : ((n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ) →ₗ[ℝ] Matrix n n ℝ) :
              ((n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ) →ₗ[ℝ] Matrix n n ℝ))
          (((QuadraticMap.associatedHom ℝ : QuadraticMap ℝ (n → ℝ) ℝ →ₗ[ℝ] LinearMap.BilinMap ℝ (n → ℝ) ℝ) :
              (a : QuadraticMap ℝ (n → ℝ) ℝ) → LinearMap.BilinMap ℝ (n → ℝ) ℝ)
            Q))))
⊢ QuadraticMap.PosDef Q

Tactic:
rw [← Q.toQuadraticMap_associated ℝ,
    ← (LinearMap.toMatrix₂' ℝ).left_inv (Q.associatedHom ℝ)]

Premises used: Real, QuadraticMap.toQuadraticMap_associated, LinearEquiv.left_inv, LinearMap.toMatrix₂', DFunLike.coe, QuadraticMap.associatedHom
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ : Q.toMatrix'.PosDef
⊢ QuadraticMap.PosDef.{0, u_1, 0} (M := n → ℝ) (N := ℝ)
    (LinearMap.BilinMap.toQuadraticMap
      (LinearEquiv.invFun (LinearMap.toMatrix₂' ℝ : ((n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ) ≃ₗ[ℝ] Matrix n n ℝ)
        (AddHom.toFun (M := (n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ)
          (LinearMap.toAddHom
            ((↑(LinearMap.toMatrix₂' ℝ) : ((n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ) →ₗ[ℝ] Matrix n n ℝ) :
              ((n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ) →ₗ[ℝ] Matrix n n ℝ))
          (((QuadraticMap.associatedHom ℝ : QuadraticMap ℝ (n → ℝ) ℝ →ₗ[ℝ] LinearMap.BilinMap ℝ (n → ℝ) ℝ) :
              (a : QuadraticMap ℝ (n → ℝ) ℝ) → LinearMap.BilinMap ℝ (n → ℝ) ℝ)
            Q))))

Tactic:
hQ.toQuadraticForm'

Premises used: Matrix.toQuadraticForm', LinearMap.mk₂'ₛₗ, Matrix.toLinearMap₂'Aux, Matrix.PosDef.toQuadraticForm', QuadraticForm.toMatrix'
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ : Q.toMatrix'.PosDef
⊢ QuadraticMap.PosDef.{0, u_1, 0} (M := n → ℝ) (N := ℝ)
    (LinearMap.BilinMap.toQuadraticMap
      (LinearEquiv.invFun (LinearMap.toMatrix₂' ℝ : ((n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ) ≃ₗ[ℝ] Matrix n n ℝ)
        (AddHom.toFun (M := (n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ)
          (LinearMap.toAddHom
            ((↑(LinearMap.toMatrix₂' ℝ) : ((n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ) →ₗ[ℝ] Matrix n n ℝ) :
              ((n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ) →ₗ[ℝ] Matrix n n ℝ))
          (((QuadraticMap.associatedHom ℝ : QuadraticMap ℝ (n → ℝ) ℝ →ₗ[ℝ] LinearMap.BilinMap ℝ (n → ℝ) ℝ) :
              (a : QuadraticMap ℝ (n → ℝ) ℝ) → LinearMap.BilinMap ℝ (n → ℝ) ℝ)
            Q))))

Tactic:
exact hQ.toQuadraticForm'

Premises used: Matrix.PosDef.toQuadraticForm'
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ : QuadraticMap.PosDef Q
⊢ QuadraticMap.PosDef.{0, u_1, 0} (M := n → ℝ) (N := ℝ)
    (LinearMap.BilinMap.toQuadraticMap
      (LinearEquiv.invFun (LinearMap.toMatrix₂' ℝ : ((n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ) ≃ₗ[ℝ] Matrix n n ℝ)
        (AddHom.toFun (M := (n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ)
          (LinearMap.toAddHom
            ((↑(LinearMap.toMatrix₂' ℝ) : ((n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ) →ₗ[ℝ] Matrix n n ℝ) :
              ((n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ) →ₗ[ℝ] Matrix n n ℝ))
          (((QuadraticMap.associatedHom ℝ : QuadraticMap ℝ (n → ℝ) ℝ →ₗ[ℝ] LinearMap.BilinMap ℝ (n → ℝ) ℝ) :
              (a : QuadraticMap ℝ (n → ℝ) ℝ) → LinearMap.BilinMap ℝ (n → ℝ) ℝ)
            Q))))

Tactic:
rw [← Q.toQuadraticMap_associated ℝ,
    ← (LinearMap.toMatrix₂' ℝ).left_inv (Q.associatedHom ℝ)] at hQ

Premises used: Real, QuadraticMap.toQuadraticMap_associated, LinearEquiv.left_inv, LinearMap.toMatrix₂', DFunLike.coe, QuadraticMap.associatedHom
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ :
  QuadraticMap.PosDef.{0, u_1, 0} (M := n → ℝ) (N := ℝ)
    (LinearMap.BilinMap.toQuadraticMap
      (LinearEquiv.invFun (LinearMap.toMatrix₂' ℝ : ((n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ) ≃ₗ[ℝ] Matrix n n ℝ)
        (AddHom.toFun (M := (n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ)
          (LinearMap.toAddHom
            ((↑(LinearMap.toMatrix₂' ℝ) : ((n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ) →ₗ[ℝ] Matrix n n ℝ) :
              ((n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ) →ₗ[ℝ] Matrix n n ℝ))
          (((QuadraticMap.associatedHom ℝ : QuadraticMap ℝ (n → ℝ) ℝ →ₗ[ℝ] LinearMap.BilinMap ℝ (n → ℝ) ℝ) :
              (a : QuadraticMap ℝ (n → ℝ) ℝ) → LinearMap.BilinMap ℝ (n → ℝ) ℝ)
            Q))))
⊢ Q.toMatrix'.PosDef

Tactic:
.of_toQuadraticForm' (isSymm_toMatrix' Q) hQ

Premises used: Matrix.PosDef.of_toQuadraticForm', QuadraticForm.isSymm_toMatrix'
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ :
  QuadraticMap.PosDef.{0, u_1, 0} (M := n → ℝ) (N := ℝ)
    (LinearMap.BilinMap.toQuadraticMap
      (LinearEquiv.invFun (LinearMap.toMatrix₂' ℝ : ((n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ) ≃ₗ[ℝ] Matrix n n ℝ)
        (AddHom.toFun (M := (n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ)
          (LinearMap.toAddHom
            ((↑(LinearMap.toMatrix₂' ℝ) : ((n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ) →ₗ[ℝ] Matrix n n ℝ) :
              ((n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ) →ₗ[ℝ] Matrix n n ℝ))
          (((QuadraticMap.associatedHom ℝ : QuadraticMap ℝ (n → ℝ) ℝ →ₗ[ℝ] LinearMap.BilinMap ℝ (n → ℝ) ℝ) :
              (a : QuadraticMap ℝ (n → ℝ) ℝ) → LinearMap.BilinMap ℝ (n → ℝ) ℝ)
            Q))))
⊢ Q.toMatrix'.PosDef

Tactic:
exact .of_toQuadraticForm' (isSymm_toMatrix' Q) hQ
-- Module: Mathlib.LinearAlgebra.Matrix.Reindex
Goal:
m : Type u_2
n : Type u_3
m' : Type u_6
n' : Type u_7
R : Type u_11
A : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
eₘ : m ≃ m'
eₙ : n ≃ n'
M : Matrix m n A
⊢ Eq (α := Matrix m' n' A) ((reindexLinearEquiv R A eₘ eₙ : (a : Matrix m n A) → Matrix m' n' A) M : Matrix m' n' A)
    ((reindex eₘ eₙ : (a : Matrix m n A) → Matrix m' n' A) M : Matrix m' n' A)

Tactic:
rfl

Premises used: Matrix.submatrix, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Reindex
Goal:
m : Type u_2
n : Type u_3
m' : Type u_6
n' : Type u_7
R : Type u_11
A : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
eₘ : m ≃ m'
eₙ : n ≃ n'
⊢ Eq (α := Matrix m' n' A ≃ₗ[R] Matrix m n A) (LinearEquiv.symm (reindexLinearEquiv R A eₘ eₙ))
    (reindexLinearEquiv R A eₘ.symm eₙ.symm)

Tactic:
rfl

Premises used: LinearEquiv.symm, Matrix.submatrix, Matrix.reindexLinearEquiv, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Reindex
Goal:
m : Type u_2
n : Type u_3
R : Type u_11
A : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
⊢ Eq (α := Matrix m n A ≃ₗ[R] Matrix m n A) (reindexLinearEquiv R A (Equiv.refl m) (Equiv.refl n))
    (LinearEquiv.refl R (Matrix m n A))

Tactic:
LinearEquiv.ext fun _ => rfl

Premises used: LinearEquiv.ext, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Reindex
Goal:
m : Type u_2
n : Type u_3
m' : Type u_6
n' : Type u_7
m'' : Type u_9
n'' : Type u_10
R : Type u_11
A : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
e₁ : m ≃ m'
e₂ : n ≃ n'
e₁' : m' ≃ m''
e₂' : n' ≃ n''
h :
  ∀ (x : Matrix m n A) (i : m'') (j : n''),
    Eq.{u_12 + 1} (α := A)
      ((reindexLinearEquiv R A e₁ e₂ ≪≫ₗ reindexLinearEquiv R A e₁' e₂' : (a : Matrix m n A) → Matrix m'' n'' A) x i j :
        A)
      ((reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂') : (a : Matrix m n A) → Matrix m'' n'' A) x i j : A)
⊢ Eq (α := Matrix m n A ≃ₗ[R] Matrix m'' n'' A) (reindexLinearEquiv R A e₁ e₂ ≪≫ₗ reindexLinearEquiv R A e₁' e₂')
    (reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂'))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Reindex
Goal:
m : Type u_2
n : Type u_3
m' : Type u_6
n' : Type u_7
m'' : Type u_9
n'' : Type u_10
R : Type u_11
A : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
e₁ : m ≃ m'
e₂ : n ≃ n'
e₁' : m' ≃ m''
e₂' : n' ≃ n''
x : Matrix m n A
i : m''
j : n''
⊢ Eq.{u_12 + 1} (α := A)
    ((reindexLinearEquiv R A e₁ e₂ ≪≫ₗ reindexLinearEquiv R A e₁' e₂' : (a : Matrix m n A) → Matrix m'' n'' A) x i j :
      A)
    ((reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂') : (a : Matrix m n A) → Matrix m'' n'' A) x i j : A)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Reindex
Goal:
m : Type u_2
n : Type u_3
m' : Type u_6
n' : Type u_7
m'' : Type u_9
n'' : Type u_10
R : Type u_11
A : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
e₁ : m ≃ m'
e₂ : n ≃ n'
e₁' : m' ≃ m''
e₂' : n' ≃ n''
rw :
  Eq (α := Matrix m n A → Matrix m'' n'' A)
    (Function.comp (β := Matrix m' n' A) (⇑(reindexLinearEquiv R A e₁' e₂') : (a : Matrix m' n' A) → Matrix m'' n'' A)
      (⇑(reindexLinearEquiv R A e₁ e₂) : (a : Matrix m n A) → Matrix m' n' A))
    (⇑(reindexLinearEquiv R A e₁ e₂ ≪≫ₗ reindexLinearEquiv R A e₁' e₂') : (a : Matrix m n A) → Matrix m'' n'' A)
⊢ Eq (α := Matrix m n A → Matrix m'' n'' A)
    (Function.comp (β := Matrix m' n' A) (⇑(reindexLinearEquiv R A e₁' e₂') : (a : Matrix m' n' A) → Matrix m'' n'' A)
      (⇑(reindexLinearEquiv R A e₁ e₂) : (a : Matrix m n A) → Matrix m' n' A))
    (⇑(reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂')) : (a : Matrix m n A) → Matrix m'' n'' A)

Tactic:
rw [← reindexLinearEquiv_trans]

Premises used: Matrix.reindexLinearEquiv_trans
-- Module: Mathlib.LinearAlgebra.Matrix.Reindex
Goal:
m : Type u_2
n : Type u_3
m' : Type u_6
n' : Type u_7
m'' : Type u_9
n'' : Type u_10
R : Type u_11
A : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
e₁ : m ≃ m'
e₂ : n ≃ n'
e₁' : m' ≃ m''
e₂' : n' ≃ n''
⊢ Eq (α := Matrix m n A → Matrix m'' n'' A)
    (Function.comp (β := Matrix m' n' A) (⇑(reindexLinearEquiv R A e₁' e₂') : (a : Matrix m' n' A) → Matrix m'' n'' A)
      (⇑(reindexLinearEquiv R A e₁ e₂) : (a : Matrix m n A) → Matrix m' n' A))
    (⇑(reindexLinearEquiv R A e₁ e₂ ≪≫ₗ reindexLinearEquiv R A e₁' e₂') : (a : Matrix m n A) → Matrix m'' n'' A)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Reindex
Goal:
m : Type u_2
n : Type u_3
m' : Type u_6
n' : Type u_7
m'' : Type u_9
n'' : Type u_10
R : Type u_11
A : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
e₁ : m ≃ m'
e₂ : n ≃ n'
e₁' : m' ≃ m''
e₂' : n' ≃ n''
M : Matrix m n A
⊢ Eq (α := Matrix m'' n'' A)
    ((reindexLinearEquiv R A e₁' e₂' : (a : Matrix m' n' A) → Matrix m'' n'' A)
        ((reindexLinearEquiv R A e₁ e₂ : (a : Matrix m n A) → Matrix m' n' A) M) :
      Matrix m'' n'' A)
    ((reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂') : (a : Matrix m n A) → Matrix m'' n'' A) M :
      Matrix m'' n'' A)

Tactic:
submatrix_submatrix _ _ _ _ _

Premises used: Matrix.submatrix, Matrix.submatrix_submatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Reindex
Goal:
m : Type u_2
m' : Type u_6
R : Type u_11
A : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : DecidableEq m
inst_4 : DecidableEq m'
inst_5 : One A
e : m ≃ m'
⊢ Eq (α := Matrix m' m' A) ((reindexLinearEquiv R A e e : (a : Matrix m m A) → Matrix m' m' A) 1) 1

Tactic:
submatrix_one_equiv e.symm

Premises used: Matrix.submatrix, Matrix.submatrix_one_equiv, Equiv.symm, Matrix.diagonal, ite
-- Module: Mathlib.LinearAlgebra.Matrix.Reindex
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
m' : Type u_6
n' : Type u_7
o' : Type u_8
R : Type u_11
A : Type u_12
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : Fintype n
inst_4 : Fintype n'
eₘ : m ≃ m'
eₙ : n ≃ n'
eₒ : o ≃ o'
M : Matrix m n A
N : Matrix n o A
⊢ HMul.hMul (α := Matrix m' n' A) (β := Matrix n' o' A)
      ((reindexLinearEquiv R A eₘ eₙ : (a : Matrix m n A) → Matrix m' n' A) M : Matrix m' n' A)
      ((reindexLinearEquiv R A eₙ eₒ : (a : Matrix n o A) → Matrix n' o' A) N : Matrix n' o' A) =
    (reindexLinearEquiv R A eₘ eₒ : (a : Matrix m o A) → Matrix m' o' A) (M * N)

Tactic:
submatrix_mul_equiv M N _ _ _

Premises used: Multiset.sum, Multiset.foldr, Matrix.submatrix, dotProduct, Matrix.submatrix_mul_equiv, Finset.sum
-- Module: Mathlib.LinearAlgebra.Matrix.Reindex
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
n' : Type u_7
R : Type u_11
A : Type u_12
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : Fintype n
inst_4 : DecidableEq o
e₁ : o ≃ n
e₂ : o ≃ n'
M : Matrix m n A
⊢ M * (reindexLinearEquiv R A e₁ e₂ : (a : Matrix o o A) → Matrix n n' A) 1 =
    (reindexLinearEquiv R A (Equiv.refl m) (e₁.symm.trans e₂) : (a : Matrix m n A) → Matrix m n' A) M

Tactic:
haveI := Fintype.ofEquiv _ e₁.symm
  mul_submatrix_one _ _ _

Premises used: Matrix.submatrix, Matrix.mul_submatrix_one, Equiv.symm, DFunLike.coe, Matrix.diagonal, ite
-- Module: Mathlib.LinearAlgebra.Matrix.Reindex
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
l' : Type u_5
m' : Type u_6
n' : Type u_7
o' : Type u_8
m'' : Type u_9
n'' : Type u_10
R : Type u_11
A : Type u_12
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : DecidableEq n
inst_5 : Semiring A
inst_6 : Algebra R A
e : m ≃ n
x : R
⊢ AddHom.toFun (LinearMap.toAddHom (↑(reindexLinearEquiv A A e e) : Matrix m m A →ₗ[A] Matrix n n A))
      ((algebraMap R (Matrix m m A) : (a : R) → Matrix m m A) x) =
    (algebraMap R (Matrix n n A) : (a : R) → Matrix n n A) x

Tactic:
simp [algebraMap, Algebra.algebraMap]

Premises used: Algebra.algebraMap
-- Module: Mathlib.LinearAlgebra.Matrix.Reindex
Goal:
m : Type u_2
n : Type u_3
R : Type u_11
A : Type u_12
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : DecidableEq n
inst_5 : Semiring A
inst_6 : Algebra R A
e : m ≃ n
M : Matrix m m A
⊢ Eq (α := Matrix n n A) ((reindexAlgEquiv R A e : (a : Matrix m m A) → Matrix n n A) M : Matrix n n A)
    ((reindex e e : (a : Matrix m m A) → Matrix n n A) M : Matrix n n A)

Tactic:
rfl

Premises used: Matrix.submatrix, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Reindex
Goal:
m : Type u_2
n : Type u_3
R : Type u_11
A : Type u_12
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : DecidableEq n
inst_5 : Semiring A
inst_6 : Algebra R A
e : m ≃ n
⊢ Eq (α := Matrix n n A ≃ₐ[R] Matrix m m A) (AlgEquiv.symm (reindexAlgEquiv R A e)) (reindexAlgEquiv R A e.symm)

Tactic:
rfl

Premises used: Matrix.submatrix, AlgEquiv.symm, Matrix.reindexAlgEquiv, Equiv.symm, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Reindex
Goal:
m : Type u_2
R : Type u_11
A : Type u_12
inst : CommSemiring R
inst_1 : Fintype m
inst_2 : DecidableEq m
inst_3 : Semiring A
inst_4 : Algebra R A
⊢ Eq (α := Matrix m m A ≃ₐ[R] Matrix m m A) (reindexAlgEquiv R A (Equiv.refl m)) AlgEquiv.refl

Tactic:
AlgEquiv.ext fun _ => rfl

Premises used: AlgEquiv.ext, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Reindex
Goal:
m : Type u_2
n : Type u_3
R : Type u_11
A : Type u_12
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : DecidableEq n
inst_5 : Semiring A
inst_6 : Algebra R A
e : m ≃ n
M N : Matrix m m A
⊢ (reindexAlgEquiv R A e : (a : Matrix m m A) → Matrix n n A) (M * N) =
    HMul.hMul (α := Matrix n n A) (β := Matrix n n A)
      ((reindexAlgEquiv R A e : (a : Matrix m m A) → Matrix n n A) M : Matrix n n A)
      ((reindexAlgEquiv R A e : (a : Matrix m m A) → Matrix n n A) N : Matrix n n A)

Tactic:
map_mul ..

Premises used: map_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Reindex
Goal:
m : Type u_2
n : Type u_3
R : Type u_11
inst : CommRing R
inst_1 : Fintype m
inst_2 : DecidableEq m
inst_3 : Fintype n
inst_4 : DecidableEq n
e : m ≃ n
M : Matrix m m R
⊢ det.{u_11, u_3} (n := n) ((reindexLinearEquiv R R e e : (a : Matrix m m R) → Matrix n n R) M) = M.det

Tactic:
det_reindex_self e M

Premises used: Matrix.submatrix, Matrix.det_reindex_self
-- Module: Mathlib.LinearAlgebra.Matrix.Reindex
Goal:
m : Type u_2
n : Type u_3
R : Type u_11
B : Type u_13
inst : CommSemiring R
inst_1 : CommRing B
inst_2 : Algebra R B
inst_3 : Fintype m
inst_4 : DecidableEq m
inst_5 : Fintype n
inst_6 : DecidableEq n
e : m ≃ n
A : Matrix m m B
⊢ det.{u_13, u_3} (n := n) ((reindexAlgEquiv R B e : (a : Matrix m m B) → Matrix n n B) A) = A.det

Tactic:
det_reindex_self e A

Premises used: Matrix.submatrix, Matrix.det_reindex_self
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
α : Type v
ι : Type u_6
w : m → α
i : m
j : ι
⊢ replicateCol ι w i j = w i

Tactic:
rfl

Premises used: Matrix.replicateCol, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
n : Type u_3
α : Type v
ι : Type u_6
v : n → α
i : ι
j : n
⊢ replicateRow ι v i j = v j

Tactic:
rfl

Premises used: Matrix.replicateRow, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
inst : MulOneClass R
x : n → R
a : ∀ (i : n) (j : m), vecMulVec x 1 i j = replicateCol m x i j
⊢ vecMulVec x 1 = replicateCol m x

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
inst : MulOneClass R
x : n → R
i : n
j : m
⊢ vecMulVec x 1 i j = replicateCol m x i j

Tactic:
simp [vecMulVec_apply]

Premises used: Matrix.vecMulVec_apply
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
inst : MulOneClass R
x : n → R
a : ∀ (i : m) (j : n), vecMulVec 1 x i j = replicateRow m x i j
⊢ vecMulVec 1 x = replicateRow m x

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
inst : MulOneClass R
x : n → R
i : m
j : n
⊢ vecMulVec 1 x i j = replicateRow m x i j

Tactic:
simp [vecMulVec_apply]

Premises used: Matrix.vecMulVec_apply
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
α : Type v
ι : Type u_6
inst : Nonempty ι
inhabit : ∀ (inhabited_h : Inhabited ι), Function.Injective (α := m → α) (replicateCol ι)
⊢ Function.Injective (α := m → α) (replicateCol ι)

Tactic:
inhabit ι
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
α : Type v
ι : Type u_6
inst : Nonempty ι
inhabited_h : Inhabited ι
⊢ Function.Injective (α := m → α) (replicateCol ι)

Tactic:
fun _x _y h => funext fun i => congr_fun₂ h i default

Premises used: Inhabited.default, congr_fun₂, funext, Function.Injective
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
α : Type v
ι : Type u_6
inst : Nonempty ι
inhabited_h : Inhabited ι
⊢ Function.Injective (α := m → α) (replicateCol ι)

Tactic:
exact fun _x _y h => funext fun i => congr_fun₂ h i default

Premises used: Inhabited.default, congr_fun₂, funext
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
α : Type v
ι : Type u_6
inst : Nonempty ι
v w : m → α
⊢ replicateCol ι v = replicateCol ι w ↔ v = w

Tactic:
replicateCol_injective.eq_iff

Premises used: Matrix.replicateCol_injective, Function.Injective.eq_iff
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
α : Type v
ι : Type u_6
inst : Zero α
⊢ Eq (α := Matrix m ι α) (replicateCol ι 0) 0

Tactic:
rfl

Premises used: Matrix.replicateCol, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
α : Type v
ι : Type u_6
inst : Zero α
inst_1 : Nonempty ι
v : m → α
⊢ replicateCol ι v = 0 ↔ v = 0

Tactic:
replicateCol_inj

Premises used: Matrix.replicateCol, Matrix.replicateCol_inj
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
α : Type v
ι : Type u_6
inst : Add α
v w : m → α
a : ∀ (i : m) (j : ι), replicateCol ι (v + w) i j = (replicateCol ι v + replicateCol ι w) i j
⊢ replicateCol ι (v + w) = replicateCol ι v + replicateCol ι w

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
α : Type v
ι : Type u_6
inst : Add α
v w : m → α
i : m
j : ι
⊢ replicateCol ι (v + w) i j = (replicateCol ι v + replicateCol ι w) i j

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
R : Type u_5
α : Type v
ι : Type u_6
inst : SMul R α
x : R
v : m → α
a : ∀ (i : m) (j : ι), replicateCol ι (x • v) i j = (x • replicateCol ι v) i j
⊢ replicateCol ι (x • v) = x • replicateCol ι v

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
R : Type u_5
α : Type v
ι : Type u_6
inst : SMul R α
x : R
v : m → α
i : m
j : ι
⊢ replicateCol ι (x • v) i j = (x • replicateCol ι v) i j

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
n : Type u_3
α : Type v
ι : Type u_6
inst : Nonempty ι
inhabit : ∀ (inhabited_h : Inhabited ι), Function.Injective (α := n → α) (replicateRow ι)
⊢ Function.Injective (α := n → α) (replicateRow ι)

Tactic:
inhabit ι
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
n : Type u_3
α : Type v
ι : Type u_6
inst : Nonempty ι
inhabited_h : Inhabited ι
⊢ Function.Injective (α := n → α) (replicateRow ι)

Tactic:
fun _x _y h => funext fun j => congr_fun₂ h default j

Premises used: Inhabited.default, congr_fun₂, funext, Function.Injective
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
n : Type u_3
α : Type v
ι : Type u_6
inst : Nonempty ι
inhabited_h : Inhabited ι
⊢ Function.Injective (α := n → α) (replicateRow ι)

Tactic:
exact fun _x _y h => funext fun j => congr_fun₂ h default j

Premises used: Inhabited.default, congr_fun₂, funext
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
n : Type u_3
α : Type v
ι : Type u_6
inst : Nonempty ι
v w : n → α
⊢ replicateRow ι v = replicateRow ι w ↔ v = w

Tactic:
replicateRow_injective.eq_iff

Premises used: Function.Injective.eq_iff, Matrix.replicateRow_injective
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
n : Type u_3
α : Type v
ι : Type u_6
inst : Zero α
⊢ Eq (α := Matrix ι n α) (replicateRow ι 0) 0

Tactic:
rfl

Premises used: Matrix.replicateRow, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
n : Type u_3
α : Type v
ι : Type u_6
inst : Zero α
inst_1 : Nonempty ι
v : n → α
⊢ replicateRow ι v = 0 ↔ v = 0

Tactic:
replicateRow_inj

Premises used: Matrix.replicateRow_inj, Matrix.replicateRow
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
α : Type v
ι : Type u_6
inst : Add α
v w : m → α
a : ∀ (i : ι) (j : m), replicateRow ι (v + w) i j = (replicateRow ι v + replicateRow ι w) i j
⊢ replicateRow ι (v + w) = replicateRow ι v + replicateRow ι w

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
α : Type v
ι : Type u_6
inst : Add α
v w : m → α
i : ι
j : m
⊢ replicateRow ι (v + w) i j = (replicateRow ι v + replicateRow ι w) i j

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
R : Type u_5
α : Type v
ι : Type u_6
inst : SMul R α
x : R
v : m → α
a : ∀ (i : ι) (j : m), replicateRow ι (x • v) i j = (x • replicateRow ι v) i j
⊢ replicateRow ι (x • v) = x • replicateRow ι v

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
R : Type u_5
α : Type v
ι : Type u_6
inst : SMul R α
x : R
v : m → α
i : ι
j : m
⊢ replicateRow ι (x • v) i j = (x • replicateRow ι v) i j

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
α : Type v
ι : Type u_6
v : m → α
a : ∀ (i : ι) (j : m), (replicateCol ι v)ᵀ i j = replicateRow ι v i j
⊢ (replicateCol ι v)ᵀ = replicateRow ι v

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
α : Type v
ι : Type u_6
v : m → α
i : ι
j : m
⊢ (replicateCol ι v)ᵀ i j = replicateRow ι v i j

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
α : Type v
ι : Type u_6
v : m → α
a : ∀ (i : m) (j : ι), (replicateRow ι v)ᵀ i j = replicateCol ι v i j
⊢ (replicateRow ι v)ᵀ = replicateCol ι v

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
α : Type v
ι : Type u_6
v : m → α
i : m
j : ι
⊢ (replicateRow ι v)ᵀ i j = replicateCol ι v i j

Tactic:
rfl