mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl.inl
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
val✝¹ val✝ : l
⊢ fromBlocks 1 0 0 1 (Sum.inl val✝¹) (Sum.inl val✝) = 1 (Sum.inl val✝¹) (Sum.inl val✝)

pp: case inl.inr
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
val✝¹ : l
val✝ : m
⊢ fromBlocks 1 0 0 1 (Sum.inl val✝¹) (Sum.inr val✝) = 1 (Sum.inl val✝¹) (Sum.inr val✝)

pp: case inr.inl
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
val✝¹ : m
val✝ : l
⊢ fromBlocks 1 0 0 1 (Sum.inr val✝¹) (Sum.inl val✝) = 1 (Sum.inr val✝¹) (Sum.inl val✝)

pp: case inr.inr
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
val✝¹ val✝ : m
⊢ fromBlocks 1 0 0 1 (Sum.inr val✝¹) (Sum.inr val✝) = 1 (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl.inl
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
val✝¹ val✝ : l
⊢ fromBlocks 1 0 0 1 (Sum.inl val✝¹) (Sum.inl val✝) = 1 (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
val✝¹ : l
val✝ : m
⊢ fromBlocks 1 0 0 1 (Sum.inl val✝¹) (Sum.inr val✝) = 1 (Sum.inl val✝¹) (Sum.inr val✝)

case inr.inl
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
val✝¹ : m
val✝ : l
⊢ fromBlocks 1 0 0 1 (Sum.inr val✝¹) (Sum.inl val✝) = 1 (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
val✝¹ val✝ : m
⊢ fromBlocks 1 0 0 1 (Sum.inr val✝¹) (Sum.inr val✝) = 1 (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case pos
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : o → Matrix m n α
i✝ : m × o
j✝ : n × o
h✝ : i✝.2 = j✝.2
⊢ M i✝.2 i✝.1 j✝.1 + N i✝.2 i✝.1 j✝.1 = M i✝.2 i✝.1 j✝.1 + N i✝.2 i✝.1 j✝.1

pp: case neg
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : o → Matrix m n α
i✝ : m × o
j✝ : n × o
h✝ : ¬i✝.2 = j✝.2
⊢ 0 = 0 + 0

Tactic:
<;>

Goal state after:
case pos
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : o → Matrix m n α
i✝ : m × o
j✝ : n × o
h✝ : i✝.2 = j✝.2
⊢ M i✝.2 i✝.1 j✝.1 + N i✝.2 i✝.1 j✝.1 = M i✝.2 i✝.1 j✝.1 + N i✝.2 i✝.1 j✝.1

case neg
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : o → Matrix m n α
i✝ : m × o
j✝ : n × o
h✝ : ¬i✝.2 = j✝.2
⊢ 0 = 0 + 0
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case pos
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
M : o → Matrix m n α
N : o → Matrix n p α
i : m
k : o
j : p
k' : o
h : k = k'
⊢ ∑ j_1, M k i j_1 * N k j_1 j = ∑ x, ∑ x_1, (if k = x_1 then M k i x else 0) * if x_1 = k' then N x_1 x j else 0

pp: case neg
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
M : o → Matrix m n α
N : o → Matrix n p α
i : m
k : o
j : p
k' : o
h : ¬k = k'
⊢ 0 = ∑ x, ∑ x_1, (if k = x_1 then M k i x else 0) * if x_1 = k' then N x_1 x j else 0

Tactic:
<;>

Goal state after:
case pos
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
M : o → Matrix m n α
N : o → Matrix n p α
i : m
k : o
j : p
k' : o
h : k = k'
⊢ ∑ j_1, M k i j_1 * N k j_1 j = ∑ x, ∑ x_1, (if k = x_1 then M k i x else 0) * if x_1 = k' then N x_1 x j else 0

case neg
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
M : o → Matrix m n α
N : o → Matrix n p α
i : m
k : o
j : p
k' : o
h : ¬k = k'
⊢ 0 = ∑ x, ∑ x_1, (if k = x_1 then M k i x else 0) * if x_1 = k' then N x_1 x j else 0
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case pos
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : DecidableEq o
R : Type u_14
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
x : R
M : o → Matrix m n α
i✝ : m × o
j✝ : n × o
h✝ : i✝.2 = j✝.2
⊢ x • M i✝.2 i✝.1 j✝.1 = x • M i✝.2 i✝.1 j✝.1

pp: case neg
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : DecidableEq o
R : Type u_14
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
x : R
M : o → Matrix m n α
i✝ : m × o
j✝ : n × o
h✝ : ¬i✝.2 = j✝.2
⊢ 0 = x • 0

Tactic:
<;>

Goal state after:
case pos
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : DecidableEq o
R : Type u_14
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
x : R
M : o → Matrix m n α
i✝ : m × o
j✝ : n × o
h✝ : i✝.2 = j✝.2
⊢ x • M i✝.2 i✝.1 j✝.1 = x • M i✝.2 i✝.1 j✝.1

case neg
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : DecidableEq o
R : Type u_14
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
x : R
M : o → Matrix m n α
i✝ : m × o
j✝ : n × o
h✝ : ¬i✝.2 = j✝.2
⊢ 0 = x • 0
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case pos
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
h✝¹ : ji = ii
h✝ : ii = ji
⊢ M ji jx (cast ⋯ ix) = M ii (cast ⋯ jx) ix

pp: case neg
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
h✝¹ : ji = ii
h✝ : ¬ii = ji
⊢ M ji jx (cast ⋯ ix) = 0

pp: case pos
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
h✝¹ : ¬ji = ii
h✝ : ii = ji
⊢ 0 = M ii (cast ⋯ jx) ix

pp: case neg
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
h✝¹ : ¬ji = ii
h✝ : ¬ii = ji
⊢ 0 = 0

Tactic:
<;>

Goal state after:
case pos
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
h✝¹ : ji = ii
h✝ : ii = ji
⊢ M ji jx (cast ⋯ ix) = M ii (cast ⋯ jx) ix

case neg
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
h✝¹ : ji = ii
h✝ : ¬ii = ji
⊢ M ji jx (cast ⋯ ix) = 0

case pos
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
h✝¹ : ¬ji = ii
h✝ : ii = ji
⊢ 0 = M ii (cast ⋯ jx) ix

case neg
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
h✝¹ : ¬ji = ii
h✝ : ¬ii = ji
⊢ 0 = 0
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case pos
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
h✝ : i✝.fst = j✝.fst
⊢ M i✝.fst i✝.snd (cast ⋯ j✝.snd) + N i✝.fst i✝.snd (cast ⋯ j✝.snd) =
    M i✝.fst i✝.snd (cast ⋯ j✝.snd) + N i✝.fst i✝.snd (cast ⋯ j✝.snd)

pp: case neg
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
h✝ : ¬i✝.fst = j✝.fst
⊢ 0 = 0 + 0

Tactic:
<;>

Goal state after:
case pos
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
h✝ : i✝.fst = j✝.fst
⊢ M i✝.fst i✝.snd (cast ⋯ j✝.snd) + N i✝.fst i✝.snd (cast ⋯ j✝.snd) =
    M i✝.fst i✝.snd (cast ⋯ j✝.snd) + N i✝.fst i✝.snd (cast ⋯ j✝.snd)

case neg
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
h✝ : ¬i✝.fst = j✝.fst
⊢ 0 = 0 + 0
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case pos
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
h✝ : k = k'
⊢ ∑ j_1, M k i j_1 * N k j_1 (cast ⋯ j) = ∑ x, M k i (cast ⋯ x) * N k x (cast ⋯ j)

pp: case neg
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
h✝ : ¬k = k'
⊢ 0 = ∑ x, M k i (cast ⋯ x) * 0

Tactic:
<;>

Goal state after:
case pos
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
h✝ : k = k'
⊢ ∑ j_1, M k i j_1 * N k j_1 (cast ⋯ j) = ∑ x, M k i (cast ⋯ x) * N k x (cast ⋯ j)

case neg
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
h✝ : ¬k = k'
⊢ 0 = ∑ x, M k i (cast ⋯ x) * 0
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case pos
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝² : DecidableEq o
R : Type u_14
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
x : R
M : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
h✝ : i✝.fst = j✝.fst
⊢ x • M i✝.fst i✝.snd (cast ⋯ j✝.snd) = x • M i✝.fst i✝.snd (cast ⋯ j✝.snd)

pp: case neg
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝² : DecidableEq o
R : Type u_14
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
x : R
M : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
h✝ : ¬i✝.fst = j✝.fst
⊢ 0 = x • 0

Tactic:
<;>

Goal state after:
case pos
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝² : DecidableEq o
R : Type u_14
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
x : R
M : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
h✝ : i✝.fst = j✝.fst
⊢ x • M i✝.fst i✝.snd (cast ⋯ j✝.snd) = x • M i✝.fst i✝.snd (cast ⋯ j✝.snd)

case neg
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝² : DecidableEq o
R : Type u_14
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
x : R
M : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
h✝ : ¬i✝.fst = j✝.fst
⊢ 0 = x • 0
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case refine_1
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
B : Fin m → n' → α
i : Fin m.succ
j : n'
⊢ vecCons v B 0 j = vecCons (v j) (fun i ↦ B i j) 0

pp: case refine_2
α : 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 ↦ B i j) i.succ

Tactic:
<;>

Goal state after:
case refine_1
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
B : Fin m → n' → α
i : Fin m.succ
j : n'
⊢ vecCons v B 0 j = vecCons (v j) (fun i ↦ B i j) 0

case refine_2
α : 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 ↦ B i j) i.succ
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case refine_1
α : Type u
m : ℕ
ι : Type u_1
x : α
u : Fin m → α
i : Fin m.succ
j : ι
⊢ replicateCol ι (vecCons x u) 0 j = of (vecCons (fun x_1 ↦ x) (replicateCol ι u)) 0 j

pp: case refine_2
α : 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 (vecCons (fun x_1 ↦ x) (replicateCol ι u)) i.succ j

Tactic:
<;>

Goal state after:
case refine_1
α : Type u
m : ℕ
ι : Type u_1
x : α
u : Fin m → α
i : Fin m.succ
j : ι
⊢ replicateCol ι (vecCons x u) 0 j = of (vecCons (fun x_1 ↦ x) (replicateCol ι u)) 0 j

case refine_2
α : 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 (vecCons (fun x_1 ↦ x) (replicateCol ι u)) i.succ j
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case refine_1
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
A : Matrix (Fin m) n' α
i : n'
j : Fin m.succ
⊢ (of (vecCons v A))ᵀ i 0 = of (fun i ↦ vecCons (v i) (Aᵀ i)) i 0

pp: case refine_2
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
A : Matrix (Fin m) n' α
i : n'
j : Fin m.succ
⊢ ∀ (i_1 : Fin m), (of (vecCons v A))ᵀ i i_1.succ = of (fun i ↦ vecCons (v i) (Aᵀ i)) i i_1.succ

Tactic:
<;>

Goal state after:
case refine_1
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
A : Matrix (Fin m) n' α
i : n'
j : Fin m.succ
⊢ (of (vecCons v A))ᵀ i 0 = of (fun i ↦ vecCons (v i) (Aᵀ i)) i 0

case refine_2
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
A : Matrix (Fin m) n' α
i : n'
j : Fin m.succ
⊢ ∀ (i_1 : Fin m), (of (vecCons v A))ᵀ i i_1.succ = of (fun i ↦ vecCons (v i) (Aᵀ i)) i i_1.succ
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case refine_1
α : Type u
m : ℕ
n' : Type uₙ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
w : n' → α
i : Fin m.succ
⊢ (of (vecCons v A) *ᵥ w) 0 = vecCons (v ⬝ᵥ w) (of A *ᵥ w) 0

pp: case refine_2
α : Type u
m : ℕ
n' : Type uₙ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
w : n' → α
i : Fin m.succ
⊢ ∀ (i : Fin m), (of (vecCons v A) *ᵥ w) i.succ = vecCons (v ⬝ᵥ w) (of A *ᵥ w) i.succ

Tactic:
<;>

Goal state after:
case refine_1
α : Type u
m : ℕ
n' : Type uₙ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
w : n' → α
i : Fin m.succ
⊢ (of (vecCons v A) *ᵥ w) 0 = vecCons (v ⬝ᵥ w) (of A *ᵥ w) 0

case refine_2
α : Type u
m : ℕ
n' : Type uₙ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
w : n' → α
i : Fin m.succ
⊢ ∀ (i : Fin m), (of (vecCons v A) *ᵥ w) i.succ = vecCons (v ⬝ᵥ w) (of A *ᵥ w) i.succ
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case refine_1
α : Type u
m : ℕ
n' : Type uₙ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
i : Fin m.succ
j✝ : n'
⊢ vecMulVec (vecCons x v) w 0 j✝ = vecCons (x • w) (vecMulVec v w) 0 j✝

pp: case refine_2
α : Type u
m : ℕ
n' : Type uₙ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
i : Fin m.succ
j✝ : n'
⊢ ∀ (i : Fin m), vecMulVec (vecCons x v) w i.succ j✝ = vecCons (x • w) (vecMulVec v w) i.succ j✝

Tactic:
<;>

Goal state after:
case refine_1
α : Type u
m : ℕ
n' : Type uₙ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
i : Fin m.succ
j✝ : n'
⊢ vecMulVec (vecCons x v) w 0 j✝ = vecCons (x • w) (vecMulVec v w) 0 j✝

case refine_2
α : Type u
m : ℕ
n' : Type uₙ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
i : Fin m.succ
j✝ : n'
⊢ ∀ (i : Fin m), vecMulVec (vecCons x v) w i.succ j✝ = vecCons (x • w) (vecMulVec v w) i.succ j✝
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case refine_1
α : Type u
m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
A : Matrix m' n' α
i✝ : m'
row : Fin m → m'
col : o' → n'
i : Fin m.succ
j : o'
⊢ A.submatrix (vecCons i✝ row) col 0 j = vecCons (fun j ↦ A i✝ (col j)) (A.submatrix row col) 0 j

pp: case refine_2
α : Type u
m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
A : Matrix m' n' α
i✝ : m'
row : Fin m → m'
col : o' → n'
i : Fin m.succ
j : o'
⊢ ∀ (i : Fin m),
    A.submatrix (vecCons i✝ row) col i.succ j = vecCons (fun j ↦ A i✝ (col j)) (A.submatrix row col) i.succ j

Tactic:
<;>

Goal state after:
case refine_1
α : Type u
m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
A : Matrix m' n' α
i✝ : m'
row : Fin m → m'
col : o' → n'
i : Fin m.succ
j : o'
⊢ A.submatrix (vecCons i✝ row) col 0 j = vecCons (fun j ↦ A i✝ (col j)) (A.submatrix row col) 0 j

case refine_2
α : Type u
m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
A : Matrix m' n' α
i✝ : m'
row : Fin m → m'
col : o' → n'
i : Fin m.succ
j : o'
⊢ ∀ (i : Fin m),
    A.submatrix (vecCons i✝ row) col i.succ j = vecCons (fun j ↦ A i✝ (col j)) (A.submatrix row col) i.succ j
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
j : Fin 2
⊢ 1 ((fun i ↦ i) ⟨0, ⋯⟩) j = !![1, 0; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) j

pp: case «1»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
j : Fin 2
⊢ 1 ((fun i ↦ i) ⟨1, ⋯⟩) j = !![1, 0; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
<;>

Goal state after:
case «0»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
j : Fin 2
⊢ 1 ((fun i ↦ i) ⟨0, ⋯⟩) j = !![1, 0; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
j : Fin 2
⊢ 1 ((fun i ↦ i) ⟨1, ⋯⟩) j = !![1, 0; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0».«0»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![1, 0; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «0».«1»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![1, 0; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «1».«0»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![1, 0; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1».«1»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![1, 0; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0».«0»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![1, 0; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![1, 0; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case «1».«0»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![1, 0; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«1»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![1, 0; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
j : Fin 3
⊢ 1 ((fun i ↦ i) ⟨0, ⋯⟩) j = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) j

pp: case «1»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
j : Fin 3
⊢ 1 ((fun i ↦ i) ⟨1, ⋯⟩) j = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) j

pp: case «2»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
j : Fin 3
⊢ 1 ((fun i ↦ i) ⟨2, ⋯⟩) j = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨2, ⋯⟩) j

Tactic:
<;>

Goal state after:
case «0»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
j : Fin 3
⊢ 1 ((fun i ↦ i) ⟨0, ⋯⟩) j = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
j : Fin 3
⊢ 1 ((fun i ↦ i) ⟨1, ⋯⟩) j = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) j

case «2»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
j : Fin 3
⊢ 1 ((fun i ↦ i) ⟨2, ⋯⟩) j = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨2, ⋯⟩) j
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
j : Fin 2
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) j = !![↑n, 0; 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) j

pp: case «1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
j : Fin 2
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) j = !![↑n, 0; 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
<;>

Goal state after:
case «0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
j : Fin 2
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) j = !![↑n, 0; 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
j : Fin 2
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) j = !![↑n, 0; 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0».«0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![↑n, 0; 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «0».«1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![↑n, 0; 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «1».«0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![↑n, 0; 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1».«1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![↑n, 0; 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0».«0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![↑n, 0; 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![↑n, 0; 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case «1».«0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![↑n, 0; 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![↑n, 0; 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
j : Fin 3
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) j = !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) j

pp: case «1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
j : Fin 3
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) j = !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) j

pp: case «2»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
j : Fin 3
⊢ ↑n ((fun i ↦ i) ⟨2, ⋯⟩) j = !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨2, ⋯⟩) j

Tactic:
<;>

Goal state after:
case «0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
j : Fin 3
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) j = !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
j : Fin 3
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) j = !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) j

case «2»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
j : Fin 3
⊢ ↑n ((fun i ↦ i) ⟨2, ⋯⟩) j = !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨2, ⋯⟩) j
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0»
α : Type u
A : Matrix (Fin 2) (Fin 2) α
j : Fin 2
⊢ A ((fun i ↦ i) ⟨0, ⋯⟩) j = !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun i ↦ i) ⟨0, ⋯⟩) j

pp: case «1»
α : Type u
A : Matrix (Fin 2) (Fin 2) α
j : Fin 2
⊢ A ((fun i ↦ i) ⟨1, ⋯⟩) j = !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
<;>

Goal state after:
case «0»
α : Type u
A : Matrix (Fin 2) (Fin 2) α
j : Fin 2
⊢ A ((fun i ↦ i) ⟨0, ⋯⟩) j = !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
α : Type u
A : Matrix (Fin 2) (Fin 2) α
j : Fin 2
⊢ A ((fun i ↦ i) ⟨1, ⋯⟩) j = !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun i ↦ i) ⟨1, ⋯⟩) j