awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : NonUnitalCommSemiring α
inst_1 : Fintype n
inst_2 : Fintype o
A : Matrix m n α
B : Matrix o n α
x : o → α
rw : A *ᵥ x ᵥ* B = A *ᵥ Bᵀ *ᵥ x
rw₁ rw₂ : A *ᵥ x ᵥ* B = A *ᵥ x ᵥ* B
⊢ A *ᵥ x ᵥ* B = (A * Bᵀ) *ᵥ x

Tactic:
rw [← mulVec_mulVec, mulVec_transpose]

Premises used: Matrix.mulVec_transpose, Matrix.mulVec_mulVec
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : NonUnitalCommSemiring α
inst_1 : Fintype m
inst_2 : Fintype n
A : Matrix m n α
B : Matrix m o α
x : n → α
rw : (A *ᵥ x) ᵥ* B = x ᵥ* Aᵀ ᵥ* B
rw₁ rw₂ : (A *ᵥ x) ᵥ* B = (A *ᵥ x) ᵥ* B
⊢ (A *ᵥ x) ᵥ* B = x ᵥ* (Aᵀ * B)

Tactic:
rw [← vecMul_vecMul, vecMul_transpose]

Premises used: Matrix.vecMul_vecMul, Matrix.vecMul_transpose
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
R : Type u_7
inst : Semiring R
inst_1 : Fintype m
inst_2 : DecidableEq m
A : Matrix m m R
ha : IsUnit A
⊢ Function.Injective A.mulVec

Tactic:
isLeftRegular_iff_mulVec_injective.1 ha.isRegular.left

Premises used: IsUnit.isRegular, Iff.mp, IsRegular.left, Matrix.isLeftRegular_iff_mulVec_injective
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
R : Type u_7
inst : Semiring R
inst_1 : Fintype m
inst_2 : DecidableEq m
A : Matrix m m R
ha : IsUnit A
⊢ Function.Injective (β := m → R) fun (v : m → R) ↦ v ᵥ* A

Tactic:
isRightRegular_iff_vecMul_injective.1 ha.isRegular.right

Premises used: IsRegular.right, Matrix.isRightRegular_iff_vecMul_injective, IsUnit.isRegular, Iff.mp
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
R : Type u_7
inst : Semiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : (M ^ k).row i = 0
h' : k ≤ l
⊢ l = k + (l - k)

Tactic:
lia
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
R : Type u_7
inst : Semiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : (M ^ k).row i = 0
h' : k ≤ l
⊢ l = k + (l - k)

Tactic:
replace h' : l = k + (l - k) := by lia
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
R : Type u_7
inst : Semiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : (M ^ k).row i = 0
h' : l = k + (l - k)
rw :
  ∀ (h : Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* M ^ k = 0) (h' : l = k + (l - k)),
    Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* M ^ l = 0
⊢ (M ^ l).row i = 0

Tactic:
rw [← single_one_vecMul] at h ⊢

Premises used: Matrix.single_one_vecMul
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
R : Type u_7
inst : Semiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* M ^ k = 0
h' : l = k + (l - k)
rw : Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* M ^ (k + (l - k)) = 0
rw₁ : Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* (M ^ k * M ^ (l - k)) = 0
rw₂ : Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* M ^ k ᵥ* M ^ (l - k) = 0
rw₃ : 0 ᵥ* M ^ (l - k) = 0
rw₄ rw₅ : Eq (α := n → R) 0 0
⊢ Pi.single (M := fun (a : n) ↦ R) i 1 ᵥ* M ^ l = 0

Tactic:
rw [h', pow_add, ← vecMul_vecMul, h, zero_vecMul]

Premises used: pow_add, Matrix.zero_vecMul, Matrix.vecMul_vecMul
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
R : Type u_7
inst : Semiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : (M ^ k).col i = 0
h' : k ≤ l
⊢ l = l - k + k

Tactic:
lia
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
R : Type u_7
inst : Semiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : (M ^ k).col i = 0
h' : k ≤ l
⊢ l = l - k + k

Tactic:
replace h' : l = (l - k) + k := by lia
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
R : Type u_7
inst : Semiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : (M ^ k).col i = 0
h' : l = l - k + k
rw :
  ∀ (h : M ^ k *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0) (h' : l = l - k + k),
    M ^ l *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
⊢ (M ^ l).col i = 0

Tactic:
rw [← mulVec_single_one] at h ⊢

Premises used: Matrix.mulVec_single_one
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
R : Type u_7
inst : Semiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : M ^ k *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
h' : l = l - k + k
rw : M ^ (l - k + k) *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
rw₁ : (M ^ (l - k) * M ^ k) *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
rw₂ : M ^ (l - k) *ᵥ M ^ k *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0
rw₃ : M ^ (l - k) *ᵥ 0 = 0
rw₄ rw₅ : Eq (α := n → R) 0 0
⊢ M ^ l *ᵥ Pi.single (M := fun (a : n) ↦ R) i 1 = 0

Tactic:
rw [h', pow_add, ← mulVec_mulVec, h, mulVec_zero]

Premises used: pow_add, Matrix.mulVec_zero, Matrix.mulVec_mulVec
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : NonAssocRing α
inst_1 : Fintype m
inst_2 : DecidableEq m
x : ℤ
v : m → α
⊢ (↑x : Matrix m m α) *ᵥ v = HSMul.hSMul (α := α) (↑x : α) v

Tactic:
diagonal_const_mulVec _ _

Premises used: Matrix.diagonal_const_mulVec
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : NonAssocRing α
inst_1 : Fintype m
inst_2 : DecidableEq m
x : ℤ
v : m → α
⊢ v ᵥ* (↑x : Matrix m m α) = HSMul.hSMul (α := αᵐᵒᵖ) (MulOpposite.op (↑x : α)) v

Tactic:
vecMul_diagonal_const _ _

Premises used: Matrix.vecMul_diagonal_const
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst : AddCommMonoid α
inst_1 : CommMagma α
inst_2 : Fintype n
M : Matrix m n α
N : Matrix n l α
a : ∀ (i : l) (j : m), (M * N)ᵀ i j = (Nᵀ * Mᵀ) i j
⊢ (M * N)ᵀ = Nᵀ * Mᵀ

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst : AddCommMonoid α
inst_1 : CommMagma α
inst_2 : Fintype n
M : Matrix m n α
N : Matrix n l α
i : l
j : m
⊢ (M * N)ᵀ i j = (Nᵀ * Mᵀ) i j

Tactic:
apply dotProduct_comm

Premises used: dotProduct_comm
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Fintype n
inst_1 : Fintype o
inst_2 : Mul α
inst_3 : AddCommMonoid α
p : Type u_10
q : Type u_11
M : Matrix m n α
N : Matrix n p α
e₁ : l → m
e₂ : o → n
e₃ : q → p
he₂ : Function.Bijective e₂
⊢ (M * N).submatrix e₁ e₃ = M.submatrix e₁ e₂ * N.submatrix e₂ e₃

Tactic:
ext fun _ _ => (he₂.sum_comp _).symm

Premises used: HMul.hMul, Function.Bijective.sum_comp, Eq.symm, Matrix.ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Fintype n
inst_1 : Fintype o
inst_2 : AddCommMonoid α
inst_3 : Mul α
p : Type u_10
q : Type u_11
M : Matrix m n α
N : Matrix n p α
e₁ : l → m
e₂ : o ≃ n
e₃ : q → p
⊢ M.submatrix e₁ (⇑e₂ : (a : o) → n) * N.submatrix (⇑e₂ : (a : o) → n) e₃ = (M * N).submatrix e₁ e₃

Tactic:
(submatrix_mul M N e₁ e₂ e₃ e₂.bijective).symm

Premises used: Equiv.bijective, Eq.symm, DFunLike.coe, Matrix.submatrix_mul
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Fintype n
inst_1 : Fintype o
inst_2 : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : o → α
e₁ : l → m
e₂ : o ≃ n
⊢ M.submatrix e₁ (⇑e₂ : (a : o) → n) *ᵥ v = (M *ᵥ v ∘ (⇑e₂.symm : (a : n) → o)) ∘ e₁

Tactic:
funext fun _ => Eq.symm (dotProduct_comp_equiv_symm _ _ _)

Premises used: dotProduct_comp_equiv_symm, funext, Eq.symm
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Fintype n
inst_1 : Fintype o
inst_2 : Mul α
inst_3 : AddCommMonoid α
p : Type u_10
M : Matrix m n α
N : Matrix o p α
e₁ : l → m
e₂ : n ≃ o
a :
  ∀ (i : l) (j : p),
    HMul.hMul (β := Matrix n p α) (M.submatrix e₁ id) (N.submatrix (⇑e₂ : (a : n) → o) id) i j =
      HMul.hMul (α := Matrix l o α) (M.submatrix e₁ (⇑e₂.symm : (a : o) → n)) N i j
⊢ HMul.hMul (β := Matrix n p α) (M.submatrix e₁ id) (N.submatrix (⇑e₂ : (a : n) → o) id) =
    HMul.hMul (α := Matrix l o α) (M.submatrix e₁ (⇑e₂.symm : (a : o) → n)) N

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Fintype n
inst_1 : Fintype o
inst_2 : Mul α
inst_3 : AddCommMonoid α
p : Type u_10
M : Matrix m n α
N : Matrix o p α
e₁ : l → m
e₂ : n ≃ o
i : l
j : p
⊢ HMul.hMul (β := Matrix n p α) (M.submatrix e₁ id) (N.submatrix (⇑e₂ : (a : n) → o) id) i j =
    HMul.hMul (α := Matrix l o α) (M.submatrix e₁ (⇑e₂.symm : (a : o) → n)) N i j

Tactic:
simp [mul_apply, ← e₂.bijective.sum_comp]

Premises used: Function.Bijective.sum_comp, Equiv.bijective, Matrix.mul_apply
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Fintype n
inst_1 : Fintype o
inst_2 : Mul α
inst_3 : AddCommMonoid α
p : Type u_10
M : Matrix m n α
N : Matrix o p α
e₁ : l → p
e₂ : o ≃ n
a :
  ∀ (i : m) (j : l),
    HMul.hMul (α := Matrix m o α) (M.submatrix id (⇑e₂ : (a : o) → n)) (N.submatrix id e₁) i j =
      HMul.hMul (β := Matrix n l α) M (N.submatrix (⇑e₂.symm : (a : n) → o) e₁) i j
⊢ HMul.hMul (α := Matrix m o α) (M.submatrix id (⇑e₂ : (a : o) → n)) (N.submatrix id e₁) =
    HMul.hMul (β := Matrix n l α) M (N.submatrix (⇑e₂.symm : (a : n) → o) e₁)

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Fintype n
inst_1 : Fintype o
inst_2 : Mul α
inst_3 : AddCommMonoid α
p : Type u_10
M : Matrix m n α
N : Matrix o p α
e₁ : l → p
e₂ : o ≃ n
i : m
j : l
⊢ HMul.hMul (α := Matrix m o α) (M.submatrix id (⇑e₂ : (a : o) → n)) (N.submatrix id e₁) i j =
    HMul.hMul (β := Matrix n l α) M (N.submatrix (⇑e₂.symm : (a : n) → o) e₁) i j

Tactic:
simp [mul_apply, ← e₂.bijective.sum_comp]

Premises used: Function.Bijective.sum_comp, Equiv.bijective, Matrix.mul_apply
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Fintype l
inst_1 : Fintype m
inst_2 : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : l → α
e₁ : l ≃ m
e₂ : o → n
⊢ v ᵥ* M.submatrix (⇑e₁ : (a : l) → m) e₂ = (v ∘ (⇑e₁.symm : (a : m) → l) ᵥ* M) ∘ e₂

Tactic:
funext fun _ => Eq.symm (comp_equiv_symm_dotProduct _ _ _)

Premises used: funext, Eq.symm, comp_equiv_symm_dotProduct
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Fintype n
inst_1 : Finite o
inst_2 : NonAssocSemiring α
inst_3 : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
intro :
  ∀ (val : Fintype o),
    HMul.hMul (β := Matrix n l α) M (submatrix (m := o) 1 (⇑e₁ : (a : n) → o) e₂) =
      M.submatrix id ((⇑e₁.symm : (a : o) → n) ∘ e₂)
⊢ HMul.hMul (β := Matrix n l α) M (submatrix (m := o) 1 (⇑e₁ : (a : n) → o) e₂) =
    M.submatrix id ((⇑e₁.symm : (a : o) → n) ∘ e₂)

Tactic:
cases nonempty_fintype o

Premises used: nonempty_fintype
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Fintype n
inst_1 : Finite o
inst_2 : NonAssocSemiring α
inst_3 : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
val : Fintype o
A : Matrix m o α := M.submatrix id (⇑e₁.symm : (a : o) → n)
⊢ M = A.submatrix id (⇑e₁ : (a : n) → o)

Tactic:
simp only [A, submatrix_submatrix, Function.comp_id, submatrix_id_id, Equiv.symm_comp_self]

Premises used: Function.comp_id, Equiv.symm_comp_self, Matrix.submatrix_id_id, Matrix.submatrix_submatrix
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Fintype n
inst_1 : Finite o
inst_2 : NonAssocSemiring α
inst_3 : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
val : Fintype o
A : Matrix m o α := M.submatrix id (⇑e₁.symm : (a : o) → n)
⊢ M = A.submatrix id (⇑e₁ : (a : n) → o)

Tactic:
have : M = A.submatrix id e₁ := by
    simp only [A, submatrix_submatrix, Function.comp_id, submatrix_id_id, Equiv.symm_comp_self]
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Fintype n
inst_1 : Finite o
inst_2 : NonAssocSemiring α
inst_3 : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
val : Fintype o
A : Matrix m o α := M.submatrix id (⇑e₁.symm : (a : o) → n)
this : M = A.submatrix id (⇑e₁ : (a : n) → o)
intro :
  (A * 1).submatrix id e₂ =
    submatrix.{v, u_2, u_2, u_3, u_1} (n := n) (A.submatrix id (⇑e₁ : (a : n) → o)) id ((⇑e₁.symm : (a : o) → n) ∘ e₂)
⊢ HMul.hMul (β := Matrix n l α) M (submatrix (m := o) 1 (⇑e₁ : (a : n) → o) e₂) =
    M.submatrix id ((⇑e₁.symm : (a : o) → n) ∘ e₂)

Tactic:
rw [this, submatrix_mul_equiv]

Premises used: Matrix.submatrix_mul_equiv
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Fintype n
inst_1 : Finite o
inst_2 : NonAssocSemiring α
inst_3 : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
val : Fintype o
A : Matrix m o α := M.submatrix id (⇑e₁.symm : (a : o) → n)
this : M = A.submatrix id (⇑e₁ : (a : n) → o)
⊢ (A * 1).submatrix id e₂ =
    submatrix.{v, u_2, u_2, u_3, u_1} (n := n) (A.submatrix id (⇑e₁ : (a : n) → o)) id ((⇑e₁.symm : (a : o) → n) ∘ e₂)

Tactic:
simp only [A, Matrix.mul_one, submatrix_submatrix, Function.comp_id, submatrix_id_id,
    Equiv.symm_comp_self]

Premises used: Function.comp_id, Equiv.symm_comp_self, Matrix.submatrix_id_id, Matrix.submatrix_submatrix, Matrix.mul_one
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Fintype m
inst_1 : Finite o
inst_2 : NonAssocSemiring α
inst_3 : DecidableEq o
e₁ : l → o
e₂ : m ≃ o
M : Matrix m n α
intro :
  ∀ (val : Fintype o),
    HMul.hMul (α := Matrix l m α) (submatrix (n := o) 1 e₁ (⇑e₂ : (a : m) → o)) M =
      M.submatrix ((⇑e₂.symm : (a : o) → m) ∘ e₁) id
⊢ HMul.hMul (α := Matrix l m α) (submatrix (n := o) 1 e₁ (⇑e₂ : (a : m) → o)) M =
    M.submatrix ((⇑e₂.symm : (a : o) → m) ∘ e₁) id

Tactic:
cases nonempty_fintype o

Premises used: nonempty_fintype
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Fintype m
inst_1 : Finite o
inst_2 : NonAssocSemiring α
inst_3 : DecidableEq o
e₁ : l → o
e₂ : m ≃ o
M : Matrix m n α
val : Fintype o
A : Matrix o n α := M.submatrix (⇑e₂.symm : (a : o) → m) id
⊢ M = A.submatrix (⇑e₂ : (a : m) → o) id

Tactic:
simp only [A, submatrix_submatrix, Function.comp_id, submatrix_id_id, Equiv.symm_comp_self]

Premises used: Function.comp_id, Equiv.symm_comp_self, Matrix.submatrix_id_id, Matrix.submatrix_submatrix
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Fintype m
inst_1 : Finite o
inst_2 : NonAssocSemiring α
inst_3 : DecidableEq o
e₁ : l → o
e₂ : m ≃ o
M : Matrix m n α
val : Fintype o
A : Matrix o n α := M.submatrix (⇑e₂.symm : (a : o) → m) id
⊢ M = A.submatrix (⇑e₂ : (a : m) → o) id

Tactic:
have : M = A.submatrix e₂ id := by
    simp only [A, submatrix_submatrix, Function.comp_id, submatrix_id_id, Equiv.symm_comp_self]
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Fintype m
inst_1 : Finite o
inst_2 : NonAssocSemiring α
inst_3 : DecidableEq o
e₁ : l → o
e₂ : m ≃ o
M : Matrix m n α
val : Fintype o
A : Matrix o n α := M.submatrix (⇑e₂.symm : (a : o) → m) id
this : M = A.submatrix (⇑e₂ : (a : m) → o) id
intro :
  (1 * A).submatrix e₁ id =
    submatrix.{v, u_1, u_2, u_3, u_3} (m := m) (A.submatrix (⇑e₂ : (a : m) → o) id) ((⇑e₂.symm : (a : o) → m) ∘ e₁) id
⊢ HMul.hMul (α := Matrix l m α) (submatrix (n := o) 1 e₁ (⇑e₂ : (a : m) → o)) M =
    M.submatrix ((⇑e₂.symm : (a : o) → m) ∘ e₁) id

Tactic:
rw [this, submatrix_mul_equiv]

Premises used: Matrix.submatrix_mul_equiv
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Fintype m
inst_1 : Finite o
inst_2 : NonAssocSemiring α
inst_3 : DecidableEq o
e₁ : l → o
e₂ : m ≃ o
M : Matrix m n α
val : Fintype o
A : Matrix o n α := M.submatrix (⇑e₂.symm : (a : o) → m) id
this : M = A.submatrix (⇑e₂ : (a : m) → o) id
⊢ (1 * A).submatrix e₁ id =
    submatrix.{v, u_1, u_2, u_3, u_3} (m := m) (A.submatrix (⇑e₂ : (a : m) → o) id) ((⇑e₂.symm : (a : o) → m) ∘ e₁) id

Tactic:
simp only [A, Matrix.one_mul, submatrix_submatrix, Function.comp_id, submatrix_id_id,
    Equiv.symm_comp_self]

Premises used: Function.comp_id, Equiv.symm_comp_self, Matrix.submatrix_id_id, Matrix.submatrix_submatrix, Matrix.one_mul
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Fintype m
inst_1 : Fintype n
inst_2 : AddCommMonoid α
inst_3 : Mul α
e : m ≃ n
M : Matrix m n α
rw : (M * Mᵀ).submatrix id id = M * Mᵀ
rw₁ rw₂ : M * Mᵀ = M * Mᵀ
⊢ M.submatrix id (⇑e : (a : m) → n) * Mᵀ.submatrix (⇑e : (a : m) → n) id = M * Mᵀ

Tactic:
rw [submatrix_mul_equiv, submatrix_id_id]

Premises used: Matrix.submatrix_id_id, Matrix.submatrix_mul_equiv
-- Module: Mathlib.Data.Matrix.Mul
Goal:
l : Type u_1
m_1 : Type u_2
n_1 : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R_1 : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
m : Type u_10
n : Type u_11
R : Type u_12
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : MulOne R
inst_5 : AddCommMonoid R
inst_6 : IsStablyFiniteRing R
⊢ IsDedekindFiniteMonoid (Matrix n n R)

Tactic:
let e := Fintype.equivFin n
  let f := MonoidHom.mk ⟨reindex (α := R) e e, submatrix_one_equiv _⟩
    fun _ _ ↦ (submatrix_mul_equiv ..).symm
  .of_injective f (reindex e e).injective

Premises used: OneHom.mk, MonoidHom.mk, Fintype.equivFin, Matrix.submatrix_one_equiv, IsDedekindFiniteMonoid.of_injective, Matrix.reindex, Equiv.injective, Matrix.submatrix_mul_equiv, Equiv.symm, Eq.symm, DFunLike.coe
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_10
n : Type u_11
R : Type u_12
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : MulOne R
inst_5 : AddCommMonoid R
inst_6 : IsStablyFiniteRing R
A : Matrix m n R
B : Matrix n m R
e : m ≃ n
rw :
  Eq (α := Matrix n n R) ((A * B).submatrix (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m))
      ((reindex e e : (a : Matrix m m R) → Matrix n n R) 1) ↔
    B * A = 1
rw₁ :
  Eq (α := Matrix n n R) ((A * B).submatrix (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m))
      (submatrix.{u_12, u_11, u_10, u_10, u_11} (m := m) (n := m) 1 (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m)) ↔
    B * A = 1
rw₂ : Eq (α := Matrix n n R) ((A * B).submatrix (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m)) 1 ↔ B * A = 1
rw₃ :
  HMul.hMul (α := Matrix n n R) (A.submatrix (⇑e.symm : (a : n) → m) (⇑(Equiv.refl n) : (a : n) → n))
        (B.submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑e.symm : (a : n) → m)) =
      1 ↔
    B * A = 1
rw₄ :
  HMul.hMul (α := Matrix n n R) (B.submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑e.symm : (a : n) → m))
        (A.submatrix (⇑e.symm : (a : n) → m) (⇑(Equiv.refl n) : (a : n) → n)) =
      1 ↔
    B * A = 1
rw₅ :
  Eq (α := Matrix n n R) ((B * A).submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑(Equiv.refl n) : (a : n) → n)) 1 ↔
    B * A = 1
rw₆ : (B * A).submatrix id id = 1 ↔ B * A = 1
rw₇ rw₈ : B * A = 1 ↔ B * A = 1
⊢ Eq (α := Matrix n n R) ((reindex e e : (a : Matrix m m R) → Matrix n n R) (A * B) : Matrix n n R)
      ((reindex e e : (a : Matrix m m R) → Matrix n n R) 1 : Matrix n n R) ↔
    B * A = 1

Tactic:
rw [reindex_apply, reindex_apply, submatrix_one_equiv, ← submatrix_mul_equiv _ _ _ (.refl _),
      mul_eq_one_comm, submatrix_mul_equiv, Equiv.coe_refl, submatrix_id_id]

Premises used: Matrix.reindex_apply, Matrix.submatrix_one_equiv, Equiv.coe_refl, Matrix.submatrix_id_id, Matrix.submatrix_mul_equiv, mul_eq_one_comm, Equiv.refl
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_10
n : Type u_11
R : Type u_12
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : MulOne R
inst_5 : AddCommMonoid R
inst_6 : IsStablyFiniteRing R
A : Matrix m n R
B : Matrix n m R
eq : Fintype.card m = Fintype.card n
⊢ A * B = 1 ↔ B * A = 1

Tactic:
mul_eq_one_comm_of_equiv (Fintype.card_eq.mp eq).some

Premises used: Fintype.card_eq, Nonempty.some, Matrix.mul_eq_one_comm_of_equiv, Iff.mp
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
β : Type w
inst : Fintype n
inst_1 : NonAssocSemiring α
inst_2 : NonAssocSemiring β
M : Matrix m n α
N : Matrix n o α
i : m
j : o
f : α →+* β
⊢ (f : (a : α) → β) ((M * N) i j) =
    HMul.hMul (α := Matrix m n β) (β := Matrix n o β) (M.map (⇑f : (a : α) → β)) (N.map (⇑f : (a : α) → β)) i j

Tactic:
simp [Matrix.mul_apply, map_sum]

Premises used: Matrix.mul_apply, map_sum
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
R : Type u_7
S : Type u_8
inst : Fintype n
inst_1 : NonAssocSemiring R
inst_2 : NonAssocSemiring S
f : R →+* S
v w : n → R
⊢ Eq.{u_8 + 1} (α := S) ((f : (a : R) → S) (v ⬝ᵥ w) : S) ((⇑f : (a : R) → S) ∘ v ⬝ᵥ (⇑f : (a : R) → S) ∘ w : S)

Tactic:
simp only [dotProduct, map_sum f, f.map_mul, Function.comp]

Premises used: dotProduct, Function.comp, map_sum, RingHom.map_mul
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
inst : Fintype n
inst_1 : NonAssocSemiring R
inst_2 : NonAssocSemiring S
f : R →+* S
M : Matrix n m R
v : n → R
i : m
⊢ Eq.{u_8 + 1} (α := S) ((f : (a : R) → S) ((v ᵥ* M) i) : S)
    (((⇑f : (a : R) → S) ∘ v ᵥ* M.map (⇑f : (a : R) → S)) i : S)

Tactic:
simp only [Matrix.vecMul, Matrix.map_apply, RingHom.map_dotProduct, Function.comp_def]

Premises used: Matrix.vecMul, Matrix.map_apply, Function.comp_def, RingHom.map_dotProduct
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
inst : Fintype n
inst_1 : NonAssocSemiring R
inst_2 : NonAssocSemiring S
f : R →+* S
M : Matrix m n R
v : n → R
i : m
⊢ Eq.{u_8 + 1} (α := S) ((f : (a : R) → S) ((M *ᵥ v) i) : S)
    ((M.map (⇑f : (a : R) → S) *ᵥ (⇑f : (a : R) → S) ∘ v) i : S)

Tactic:
simp only [Matrix.mulVec, Matrix.map_apply, RingHom.map_dotProduct, Function.comp_def]

Premises used: Matrix.map_apply, Function.comp_def, Matrix.mulVec, RingHom.map_dotProduct
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
f : m ≃. n
i : m
j : n
⊢ Eq.{u_5 + 1} (α := α) (f.toMatrix i j)
    (if Membership.mem (γ := Option n) ((f : (a : m) → Option n) i : Option n) j then 1 else 0)

Tactic:
rfl

Premises used: PEquiv.toMatrix, rfl, ite
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonAssocSemiring α
f : l ≃. m
i : l
j : n
M : Matrix m n α
dsimp :
  Eq.{u_5 + 1} (α := α)
    (∑ j_1 : m,
        (if Membership.mem (γ := Option m) ((f : (a : l) → Option m) i : Option m) j_1 then 1 else 0) * M j_1 j :
      α)
    (Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M val j) ((f : (a : l) → Option m) i) : α)
⊢ HMul.hMul (α := Matrix l m α) f.toMatrix M i j =
    Option.casesOn (motive := fun (x : Option m) ↦ α) ((f : (a : l) → Option m) i) 0 fun (fi : m) ↦ M fi j

Tactic:
dsimp [toMatrix, Matrix.mul_apply]

Premises used: Matrix.mul_apply, PEquiv.toMatrix
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonAssocSemiring α
f : l ≃. m
i : l
j : n
M : Matrix m n α
none :
  ∀ (h : Eq.{u_3 + 1} (α := Option m) ((f : (a : l) → Option m) i : Option m) (Option.none : Option m)),
    Eq.{u_5 + 1} (α := α) (∑ j_1 : m, (if Membership.mem (γ := Option m) Option.none j_1 then 1 else 0) * M j_1 j : α)
      (Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M val j) Option.none : α)
some :
  ∀ (fi : m) (h : (f : (a : l) → Option m) i = Option.some fi),
    Eq.{u_5 + 1} (α := α) (∑ j_1 : m, (if j_1 ∈ Option.some fi then 1 else 0) * M j_1 j : α)
      (Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M val j) (Option.some fi) : α)
⊢ Eq.{u_5 + 1} (α := α)
    (∑ j_1 : m,
        (if Membership.mem (γ := Option m) ((f : (a : l) → Option m) i : Option m) j_1 then 1 else 0) * M j_1 j :
      α)
    (Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M val j) ((f : (a : l) → Option m) i) : α)

Tactic:
rcases h : f i with - | fi

Premises used: DFunLike.coe