awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
α : Type v
inst : CommRing α
inst_1 : Fintype m
inst_2 : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
rw : ((↑h.unit : Matrix m m α) * N * (↑h.unit : Matrix m m α)⁻¹).det = N.det
rw₁ : ((↑h.unit : Matrix m m α) * N * (↑h.unit⁻¹ : Matrix m m α)).det = N.det
rw₂ rw₃ : N.det = N.det
⊢ (M * N * M⁻¹).det = N.det

Tactic:
rw [← h.unit_spec, ← coe_units_inv, det_units_conj]

Premises used: Matrix.coe_units_inv, Matrix.det_units_conj, IsUnit.unit_spec
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
α : Type v
inst : CommRing α
inst_1 : Fintype m
inst_2 : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
rw : ((↑h.unit : Matrix m m α)⁻¹ * N * (↑h.unit : Matrix m m α)).det = N.det
rw₁ : ((↑h.unit⁻¹ : Matrix m m α) * N * (↑h.unit : Matrix m m α)).det = N.det
rw₂ rw₃ : N.det = N.det
⊢ (M⁻¹ * N * M).det = N.det

Tactic:
rw [← h.unit_spec, ← coe_units_inv, det_units_conj']

Premises used: Matrix.det_units_conj', Matrix.coe_units_inv, IsUnit.unit_spec
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
α : Type v
inst : CommRing α
inst_1 : Fintype m
inst_2 : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
rw : ((↑h.unit : Matrix m m α) * N * (↑h.unit : Matrix m m α)⁻¹).trace = N.trace
rw₁ : ((↑h.unit : Matrix m m α) * N * (↑h.unit⁻¹ : Matrix m m α)).trace = N.trace
rw₂ rw₃ : N.trace = N.trace
⊢ (M * N * M⁻¹).trace = N.trace

Tactic:
rw [← h.unit_spec, ← coe_units_inv, trace_units_conj]

Premises used: Matrix.trace_units_conj, Matrix.coe_units_inv, IsUnit.unit_spec
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
α : Type v
inst : CommRing α
inst_1 : Fintype m
inst_2 : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
rw : ((↑h.unit : Matrix m m α)⁻¹ * N * (↑h.unit : Matrix m m α)).trace = N.trace
rw₁ : ((↑h.unit⁻¹ : Matrix m m α) * N * (↑h.unit : Matrix m m α)).trace = N.trace
rw₂ rw₃ : N.trace = N.trace
⊢ (M⁻¹ * N * M).trace = N.trace

Tactic:
rw [← h.unit_spec, ← coe_units_inv, trace_units_conj']

Premises used: Matrix.coe_units_inv, Matrix.trace_units_conj', IsUnit.unit_spec
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
B : Fin m → n' → α
i : Fin m.succ
j : n'
⊢ vecCons v B i j = vecCons (v j) (fun (i : Fin m) ↦ B i j) i

Tactic:
Fin.cases ?_ ?_ i

Premises used: Fin.cases
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
B : Fin m → n' → α
i : Fin m.succ
j : n'
refine_1 : vecCons v B 0 j = vecCons (n := m) (v j) (fun (i : Fin m) ↦ B i j) 0
refine_2 : ∀ (i : Fin m), vecCons v B i.succ j = vecCons (v j) (fun (i : Fin m) ↦ B i j) i.succ
⊢ vecCons v B i j = vecCons (v j) (fun (i : Fin m) ↦ B i j) i

Tactic:
refine Fin.cases ?_ ?_ i
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
B : Fin m → n' → α
i : Fin m.succ
j : n'
⊢ vecCons v B 0 j = vecCons (n := m) (v j) (fun (i : Fin m) ↦ B i j) 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
B : Fin m → n' → α
i : Fin m.succ
j : n'
⊢ ∀ (i : Fin m), vecCons v B i.succ j = vecCons (v j) (fun (i : Fin m) ↦ B i j) i.succ

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
B : Fin m.succ → n' → α
j : n'
⊢ (vecHead (n := m) fun (i : Fin m.succ) ↦ B i j) = vecHead B j

Tactic:
rfl

Premises used: Matrix.vecHead, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
B : Fin m.succ → n' → α
j : n'
⊢ Eq.{u + 1} (α := Fin m → α) (vecTail fun (i : Fin m.succ) ↦ B i j) fun (i : Fin m) ↦ vecTail B i j

Tactic:
rfl

Premises used: Matrix.vecTail, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
n' : Type uₙ
inst : AddCommMonoid α
inst_1 : Mul α
inst_2 : Fintype n'
inst_3 : IsEmpty n'
v w : n' → α
⊢ v ⬝ᵥ w = 0

Tactic:
Finset.sum_of_isEmpty _

Premises used: dotProduct, Finset.sum_of_isEmpty
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
n : ℕ
inst : AddCommMonoid α
inst_1 : Mul α
x : α
v : Fin n → α
w : Fin n.succ → α
⊢ vecCons x v ⬝ᵥ w = x * vecHead w + v ⬝ᵥ vecTail w

Tactic:
simp [dotProduct, Fin.sum_univ_succ, vecHead, vecTail]

Premises used: dotProduct, Matrix.vecHead, Matrix.vecTail, Fin.sum_univ_succ
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
n : ℕ
inst : AddCommMonoid α
inst_1 : Mul α
v : Fin n.succ → α
x : α
w : Fin n → α
⊢ v ⬝ᵥ vecCons x w = vecHead v * x + vecTail v ⬝ᵥ w

Tactic:
simp [dotProduct, Fin.sum_univ_succ, vecHead, vecTail]

Premises used: dotProduct, Matrix.vecHead, Matrix.vecTail, Fin.sum_univ_succ
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
n : ℕ
inst : AddCommMonoid α
inst_1 : Mul α
x : α
v : Fin n → α
y : α
w : Fin n → α
⊢ vecCons x v ⬝ᵥ vecCons y w = x * y + v ⬝ᵥ w

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
d : Fin 1 → α
⊢ diagonal d = !![d 0]

Tactic:
simp [← Matrix.ext_iff]

Premises used: Matrix.ext_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
a : α
⊢ diagonal ![a] = !![a]

Tactic:
diagonal_fin_one ![a]

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Matrix.diagonal_fin_one, Fin.induction, Matrix.vecEmpty, Fin.cases, Matrix.vecCons
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
d : Fin 2 → α
⊢ diagonal d = !![d 0, 0; 0, d 1]

Tactic:
simp [← Matrix.ext_iff]

Premises used: Matrix.ext_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
a b : α
⊢ diagonal ![a, b] = !![a, 0; 0, b]

Tactic:
diagonal_fin_two ![a, b]

Premises used: Eq.mpr, Matrix.diagonal_fin_two, Fin.cons, Fin.induction.go, Fin.induction, Matrix.vecEmpty, Fin.cases, Matrix.vecCons
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
d : Fin 3 → α
⊢ diagonal d = !![d 0, 0, 0; 0, d 1, 0; 0, 0, d 2]

Tactic:
simp [← Matrix.ext_iff, Fin.forall_fin_succ]

Premises used: Fin.forall_fin_succ, Matrix.ext_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
a b c : α
⊢ diagonal ![a, b, c] = !![a, 0, 0; 0, b, 0; 0, 0, c]

Tactic:
diagonal_fin_three ![a, b, c]

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Fin.induction, Matrix.vecEmpty, Fin.cases, Matrix.diagonal_fin_three, Matrix.vecCons
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
ι : Type u_1
v : Fin 0 → α
⊢ replicateCol ι v = ![]

Tactic:
empty_eq _

Premises used: Matrix, Matrix.empty_eq
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
ι : Type u_1
x : α
u : Fin m → α
a :
  ∀ (i : Fin m.succ) (j : ι),
    replicateCol ι (vecCons x u) i j =
      (of : (a : Fin m.succ → ι → α) → Matrix (Fin m.succ) ι α) (vecCons (fun (x_1 : ι) ↦ x) (replicateCol ι u)) i j
⊢ replicateCol ι (vecCons x u) =
    (of : (a : Fin m.succ → ι → α) → Matrix (Fin m.succ) ι α) (vecCons (fun (x_1 : ι) ↦ x) (replicateCol ι u))

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
ι : Type u_1
x : α
u : Fin m → α
i : Fin m.succ
j : ι
⊢ replicateCol ι (vecCons x u) i j =
    (of : (a : Fin m.succ → ι → α) → Matrix (Fin m.succ) ι α) (vecCons (fun (x_1 : ι) ↦ x) (replicateCol ι u)) i j

Tactic:
Fin.cases ?_ ?_ i

Premises used: Fin.cases
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
ι : Type u_1
x : α
u : Fin m → α
i : Fin m.succ
j : ι
a :
  replicateCol ι (vecCons x u) 0 j =
    (of : (a : Fin m.succ → ι → α) → Matrix (Fin m.succ) ι α) (vecCons (fun (x_1 : ι) ↦ x) (replicateCol ι u)) 0 j
a₁ :
  ∀ (i : Fin m),
    replicateCol ι (vecCons x u) i.succ j =
      (of : (a : Fin m.succ → ι → α) → Matrix (Fin m.succ) ι α) (vecCons (fun (x_1 : ι) ↦ x) (replicateCol ι u)) i.succ
        j
⊢ replicateCol ι (vecCons x u) i j =
    (of : (a : Fin m.succ → ι → α) → Matrix (Fin m.succ) ι α) (vecCons (fun (x_1 : ι) ↦ x) (replicateCol ι u)) i j

Tactic:
refine Fin.cases ?_ ?_ i
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
ι : Type u_1
x : α
u : Fin m → α
i : Fin m.succ
j : ι
⊢ replicateCol ι (vecCons x u) 0 j =
    (of : (a : Fin m.succ → ι → α) → Matrix (Fin m.succ) ι α) (vecCons (fun (x_1 : ι) ↦ x) (replicateCol ι u)) 0 j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
ι : Type u_1
x : α
u : Fin m → α
i : Fin m.succ
j : ι
⊢ ∀ (i : Fin m),
    replicateCol ι (vecCons x u) i.succ j =
      (of : (a : Fin m.succ → ι → α) → Matrix (Fin m.succ) ι α) (vecCons (fun (x_1 : ι) ↦ x) (replicateCol ι u)) i.succ
        j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
ι : Type u_1
⊢ Eq (α := Matrix ι (Fin 0) α) (replicateRow ι ![]) ((of : (a : ι → Fin 0 → α) → Matrix ι (Fin 0) α) fun (x : ι) ↦ ![])

Tactic:
rfl

Premises used: Matrix.replicateRow, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
ι : Type u_1
x : α
u : Fin m → α
⊢ replicateRow ι (vecCons x u) = (of : (a : ι → Fin m.succ → α) → Matrix ι (Fin m.succ) α) fun (x_1 : ι) ↦ vecCons x u

Tactic:
rfl

Premises used: Matrix.replicateRow, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m' : Type uₘ
A : Matrix m' (Fin 0) α
⊢ Aᵀ = (of : (a : Fin 0 → m' → α) → Matrix (Fin 0) m' α) ![]

Tactic:
empty_eq _

Premises used: Matrix, Matrix.empty_eq, absurd, Matrix.vecEmpty, Fin.elim0
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m' : Type uₘ
A : Matrix (Fin 0) m' α
⊢ Aᵀ = (of : (a : m' → Fin 0 → α) → Matrix m' (Fin 0) α) fun (x : m') ↦ ![]

Tactic:
funext fun _ => empty_eq _

Premises used: Matrix, funext, Matrix.empty_eq, Matrix.transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
A : Matrix (Fin m) n' α
a :
  ∀ (i : n') (j : Fin m.succ),
    Eq.{u + 1} (α := α) (((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A))ᵀ i j : α)
      ((of : (a : n' → Fin m.succ → α) → Matrix n' (Fin m.succ) α) (fun (i : n') ↦ vecCons (v i) (Aᵀ i)) i j : α)
⊢ Eq (α := Matrix n' (Fin m.succ) α) ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A))ᵀ
    ((of : (a : n' → Fin m.succ → α) → Matrix n' (Fin m.succ) α) fun (i : n') ↦ vecCons (v i) (Aᵀ i))

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
A : Matrix (Fin m) n' α
i : n'
j : Fin m.succ
⊢ Eq.{u + 1} (α := α) (((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A))ᵀ i j : α)
    ((of : (a : n' → Fin m.succ → α) → Matrix n' (Fin m.succ) α) (fun (i : n') ↦ vecCons (v i) (Aᵀ i)) i j : α)

Tactic:
Fin.cases ?_ ?_ j

Premises used: Fin.cases
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
A : Matrix (Fin m) n' α
i : n'
j : Fin m.succ
a :
  Eq.{u + 1} (α := α)
    (transpose (m := Fin m.succ) ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A)) i 0 : α)
    ((of : (a : n' → Fin m.succ → α) → Matrix n' (Fin m.succ) α) (fun (i : n') ↦ vecCons (v i) (Aᵀ i)) i 0 : α)
a₁ :
  ∀ (i_1 : Fin m),
    Eq.{u + 1} (α := α) (((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A))ᵀ i i_1.succ : α)
      ((of : (a : n' → Fin m.succ → α) → Matrix n' (Fin m.succ) α) (fun (i : n') ↦ vecCons (v i) (Aᵀ i)) i i_1.succ : α)
⊢ Eq.{u + 1} (α := α) (((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A))ᵀ i j : α)
    ((of : (a : n' → Fin m.succ → α) → Matrix n' (Fin m.succ) α) (fun (i : n') ↦ vecCons (v i) (Aᵀ i)) i j : α)

Tactic:
refine Fin.cases ?_ ?_ j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
A : Matrix (Fin m) n' α
i : n'
j : Fin m.succ
⊢ Eq.{u + 1} (α := α)
    (transpose (m := Fin m.succ) ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A)) i 0 : α)
    ((of : (a : n' → Fin m.succ → α) → Matrix n' (Fin m.succ) α) (fun (i : n') ↦ vecCons (v i) (Aᵀ i)) i 0 : α)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
A : Matrix (Fin m) n' α
i : n'
j : Fin m.succ
⊢ ∀ (i_1 : Fin m),
    Eq.{u + 1} (α := α) (((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A))ᵀ i i_1.succ : α)
      ((of : (a : n' → Fin m.succ → α) → Matrix n' (Fin m.succ) α) (fun (i : n') ↦ vecCons (v i) (Aᵀ i)) i i_1.succ : α)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
n : ℕ
m' : Type uₘ
A : Matrix m' (Fin n.succ) α
⊢ Eq (α := m' → α) (vecHead (n := n) ((Equiv.symm of : (a : Matrix (Fin n.succ) m' α) → Fin n.succ → m' → α) Aᵀ))
    (Function.comp (β := Fin n.succ → α) vecHead
      ((Equiv.symm of : (a : Matrix m' (Fin n.succ) α) → m' → Fin n.succ → α) A))

Tactic:
rfl

Premises used: Matrix.vecHead, Matrix.transpose, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
n : ℕ
m' : Type uₘ
A : Matrix m' (Fin n.succ) α
h :
  ∀ (i : Fin n) (j : m'),
    vecTail ((Equiv.symm of : (a : Matrix (Fin n.succ) m' α) → Fin n.succ → m' → α) Aᵀ) i j = (vecTail ∘ A)ᵀ i j
⊢ vecTail ((Equiv.symm of : (a : Matrix (Fin n.succ) m' α) → Fin n.succ → m' → α) Aᵀ) = (vecTail ∘ A)ᵀ

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
n : ℕ
m' : Type uₘ
A : Matrix m' (Fin n.succ) α
i : Fin n
j : m'
⊢ vecTail ((Equiv.symm of : (a : Matrix (Fin n.succ) m' α) → Fin n.succ → m' → α) Aᵀ) i j = (vecTail ∘ A)ᵀ i j

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
n' : Type uₙ
o' : Type uₒ
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n'
A : Matrix (Fin 0) n' α
B : Matrix n' o' α
⊢ A * B = (of : (a : Fin 0 → o' → α) → Matrix (Fin 0) o' α) ![]

Tactic:
empty_eq _

Premises used: Matrix, Matrix.empty_eq, absurd, Matrix.vecEmpty, Fin.elim0
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m' : Type uₘ
o' : Type uₒ
inst : NonUnitalNonAssocSemiring α
A : Matrix m' (Fin 0) α
B : Matrix (Fin 0) o' α
⊢ A * B = 0

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, List.foldr, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m' : Type uₘ
n' : Type uₙ
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n'
A : Matrix m' n' α
B : Matrix n' (Fin 0) α
⊢ A * B = (of : (a : m' → Fin 0 → α) → Matrix m' (Fin 0) α) fun (x : m') ↦ ![]

Tactic:
funext fun _ => empty_eq _

Premises used: HMul.hMul, Matrix, funext, Matrix.empty_eq
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
o' : Type uₒ
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n'
A : Matrix (Fin m.succ) n' α
B : Matrix n' o' α
i : Fin m
j : o'
⊢ (A * B) i.succ j =
    HMul.hMul (α := Matrix (Fin m) n' α)
      ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α)
          (vecTail ((Equiv.symm of : (a : Matrix (Fin m.succ) n' α) → Fin m.succ → n' → α) A)) :
        Matrix (Fin m) n' α)
      B i j

Tactic:
rfl

Premises used: Matrix.vecTail, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
o' : Type uₒ
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
a :
  ∀ (i : Fin m.succ) (j : o'),
    HMul.hMul (α := Matrix (Fin m.succ) n' α)
        ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A) : Matrix (Fin m.succ) n' α) B i j =
      (of : (a : Fin m.succ → o' → α) → Matrix (Fin m.succ) o' α)
        (vecCons (v ᵥ* B)
          ((Equiv.symm of : (a : Matrix (Fin m) o' α) → Fin m → o' → α)
            (HMul.hMul (α := Matrix (Fin m) n' α)
              ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A : Matrix (Fin m) n' α) B)))
        i j
⊢ HMul.hMul (α := Matrix (Fin m.succ) n' α)
      ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A) : Matrix (Fin m.succ) n' α) B =
    (of : (a : Fin m.succ → o' → α) → Matrix (Fin m.succ) o' α)
      (vecCons (v ᵥ* B)
        ((Equiv.symm of : (a : Matrix (Fin m) o' α) → Fin m → o' → α)
          (HMul.hMul (α := Matrix (Fin m) n' α)
            ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A : Matrix (Fin m) n' α) B)))

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
o' : Type uₒ
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
i : Fin m.succ
j : o'
⊢ HMul.hMul (α := Matrix (Fin m.succ) n' α)
      ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A) : Matrix (Fin m.succ) n' α) B i j =
    (of : (a : Fin m.succ → o' → α) → Matrix (Fin m.succ) o' α)
      (vecCons (v ᵥ* B)
        ((Equiv.symm of : (a : Matrix (Fin m) o' α) → Fin m → o' → α)
          (HMul.hMul (α := Matrix (Fin m) n' α)
            ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A : Matrix (Fin m) n' α) B)))
      i j

Tactic:
Fin.cases ?_ ?_ i

Premises used: Fin.cases
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
o' : Type uₒ
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
i : Fin m.succ
j : o'
a :
  HMul.hMul (α := Matrix (Fin m.succ) n' α)
      ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A) : Matrix (Fin m.succ) n' α) B 0 j =
    (of : (a : Fin m.succ → o' → α) → Matrix (Fin m.succ) o' α)
      (vecCons (v ᵥ* B)
        ((Equiv.symm of : (a : Matrix (Fin m) o' α) → Fin m → o' → α)
          (HMul.hMul (α := Matrix (Fin m) n' α)
            ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A : Matrix (Fin m) n' α) B)))
      0 j
a₁ :
  ∀ (i : Fin m),
    HMul.hMul (α := Matrix (Fin m.succ) n' α)
        ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A) : Matrix (Fin m.succ) n' α) B i.succ
        j =
      (of : (a : Fin m.succ → o' → α) → Matrix (Fin m.succ) o' α)
        (vecCons (v ᵥ* B)
          ((Equiv.symm of : (a : Matrix (Fin m) o' α) → Fin m → o' → α)
            (HMul.hMul (α := Matrix (Fin m) n' α)
              ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A : Matrix (Fin m) n' α) B)))
        i.succ j
⊢ HMul.hMul (α := Matrix (Fin m.succ) n' α)
      ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A) : Matrix (Fin m.succ) n' α) B i j =
    (of : (a : Fin m.succ → o' → α) → Matrix (Fin m.succ) o' α)
      (vecCons (v ᵥ* B)
        ((Equiv.symm of : (a : Matrix (Fin m) o' α) → Fin m → o' → α)
          (HMul.hMul (α := Matrix (Fin m) n' α)
            ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A : Matrix (Fin m) n' α) B)))
      i j

Tactic:
refine Fin.cases ?_ ?_ i
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
o' : Type uₒ
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
i : Fin m.succ
j : o'
⊢ HMul.hMul (α := Matrix (Fin m.succ) n' α)
      ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A) : Matrix (Fin m.succ) n' α) B 0 j =
    (of : (a : Fin m.succ → o' → α) → Matrix (Fin m.succ) o' α)
      (vecCons (v ᵥ* B)
        ((Equiv.symm of : (a : Matrix (Fin m) o' α) → Fin m → o' → α)
          (HMul.hMul (α := Matrix (Fin m) n' α)
            ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A : Matrix (Fin m) n' α) B)))
      0 j

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
o' : Type uₒ
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
i : Fin m.succ
j : o'
⊢ ∀ (i : Fin m),
    HMul.hMul (α := Matrix (Fin m.succ) n' α)
        ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A) : Matrix (Fin m.succ) n' α) B i.succ
        j =
      (of : (a : Fin m.succ → o' → α) → Matrix (Fin m.succ) o' α)
        (vecCons (v ᵥ* B)
          ((Equiv.symm of : (a : Matrix (Fin m) o' α) → Fin m → o' → α)
            (HMul.hMul (α := Matrix (Fin m) n' α)
              ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A : Matrix (Fin m) n' α) B)))
        i.succ j

Tactic:
simp [mul_val_succ]

Premises used: Matrix.mul_val_succ
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
o' : Type uₒ
inst : NonUnitalNonAssocSemiring α
v : Fin 0 → α
B : Matrix (Fin 0) o' α
⊢ v ᵥ* B = 0

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.vecMul, List.foldr, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
n' : Type uₙ
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n'
v : n' → α
B : Matrix n' (Fin 0) α
⊢ v ᵥ* B = ![]

Tactic:
empty_eq _

Premises used: Matrix.empty_eq
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
n : ℕ
o' : Type uₒ
inst : NonUnitalNonAssocSemiring α
x : α
v : Fin n → α
B : Fin n.succ → o' → α
h :
  ∀ (i : o'),
    (vecCons x v ᵥ* (of : (a : Fin n.succ → o' → α) → Matrix (Fin n.succ) o' α) B) i =
      HAdd.hAdd (β := o' → α) (x • vecHead B) (v ᵥ* (of : (a : Fin n → o' → α) → Matrix (Fin n) o' α) (vecTail B)) i
⊢ vecCons x v ᵥ* (of : (a : Fin n.succ → o' → α) → Matrix (Fin n.succ) o' α) B =
    x • vecHead B + v ᵥ* (of : (a : Fin n → o' → α) → Matrix (Fin n) o' α) (vecTail B)

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
n : ℕ
o' : Type uₒ
inst : NonUnitalNonAssocSemiring α
x : α
v : Fin n → α
B : Fin n.succ → o' → α
i : o'
⊢ (vecCons x v ᵥ* (of : (a : Fin n.succ → o' → α) → Matrix (Fin n.succ) o' α) B) i =
    HAdd.hAdd (β := o' → α) (x • vecHead B) (v ᵥ* (of : (a : Fin n → o' → α) → Matrix (Fin n) o' α) (vecTail B)) i

Tactic:
simp [vecMul]

Premises used: Matrix.vecMul
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
n : ℕ
o' : Type uₒ
inst : NonUnitalNonAssocSemiring α
v : Fin n.succ → α
w : o' → α
B : Fin n → o' → α
h :
  ∀ (i : o'),
    (v ᵥ* (of : (a : Fin n.succ → o' → α) → Matrix (Fin n.succ) o' α) (vecCons w B)) i =
      HAdd.hAdd (β := o' → α) (vecHead v • w) (vecTail v ᵥ* (of : (a : Fin n → o' → α) → Matrix (Fin n) o' α) B) i
⊢ v ᵥ* (of : (a : Fin n.succ → o' → α) → Matrix (Fin n.succ) o' α) (vecCons w B) =
    vecHead v • w + vecTail v ᵥ* (of : (a : Fin n → o' → α) → Matrix (Fin n) o' α) B

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
n : ℕ
o' : Type uₒ
inst : NonUnitalNonAssocSemiring α
v : Fin n.succ → α
w : o' → α
B : Fin n → o' → α
i : o'
⊢ (v ᵥ* (of : (a : Fin n.succ → o' → α) → Matrix (Fin n.succ) o' α) (vecCons w B)) i =
    HAdd.hAdd (β := o' → α) (vecHead v • w) (vecTail v ᵥ* (of : (a : Fin n → o' → α) → Matrix (Fin n) o' α) B) i

Tactic:
simp [vecMul]

Premises used: Matrix.vecMul
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
n : ℕ
o' : Type uₒ
inst : NonUnitalNonAssocSemiring α
x : α
v : Fin n → α
w : o' → α
B : Fin n → o' → α
⊢ vecCons x v ᵥ* (of : (a : Fin n.succ → o' → α) → Matrix (Fin n.succ) o' α) (vecCons w B) =
    x • w + v ᵥ* (of : (a : Fin n → o' → α) → Matrix (Fin n) o' α) B

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
n' : Type uₙ
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n'
A : Matrix (Fin 0) n' α
v : n' → α
⊢ A *ᵥ v = ![]

Tactic:
empty_eq _

Premises used: Matrix.empty_eq
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m' : Type uₘ
inst : NonUnitalNonAssocSemiring α
A : Matrix m' (Fin 0) α
v : Fin 0 → α
⊢ A *ᵥ v = 0

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.mulVec, List.foldr, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n'
v : n' → α
A : Fin m → n' → α
w : n' → α
h :
  ∀ (i : Fin m.succ),
    ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A) *ᵥ w) i =
      vecCons (v ⬝ᵥ w) ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A *ᵥ w) i
⊢ Eq (α := Fin m.succ → α) ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A) *ᵥ w)
    (vecCons (v ⬝ᵥ w) ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A *ᵥ w))

Tactic:
ext i