[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
M : Matrix (n ⊕ o) (l ⊕ m) α
⊢ fromBlocks (toBlocks₁₁ M) (toBlocks₁₂ M) (toBlocks₂₁ M) (toBlocks₂₂ M) = M
[PROOFSTEP]
ext i j
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
M : Matrix (n ⊕ o) (l ⊕ m) α
i : n ⊕ o
j : l ⊕ m
⊢ fromBlocks (toBlocks₁₁ M) (toBlocks₁₂ M) (toBlocks₂₁ M) (toBlocks₂₂ M) i j = M i j
[PROOFSTEP]
rcases i with ⟨⟩
[GOAL]
case a.h.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
M : Matrix (n ⊕ o) (l ⊕ m) α
j : l ⊕ m
val✝ : n
⊢ fromBlocks (toBlocks₁₁ M) (toBlocks₁₂ M) (toBlocks₂₁ M) (toBlocks₂₂ M) (Sum.inl val✝) j = M (Sum.inl val✝) j
[PROOFSTEP]
rcases j with ⟨⟩
[GOAL]
case a.h.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
M : Matrix (n ⊕ o) (l ⊕ m) α
j : l ⊕ m
val✝ : o
⊢ fromBlocks (toBlocks₁₁ M) (toBlocks₁₂ M) (toBlocks₂₁ M) (toBlocks₂₂ M) (Sum.inr val✝) j = M (Sum.inr val✝) j
[PROOFSTEP]
rcases j with ⟨⟩
[GOAL]
case a.h.inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
M : Matrix (n ⊕ o) (l ⊕ m) α
val✝¹ : n
val✝ : l
⊢ fromBlocks (toBlocks₁₁ M) (toBlocks₁₂ M) (toBlocks₂₁ M) (toBlocks₂₂ M) (Sum.inl val✝¹) (Sum.inl val✝) =
    M (Sum.inl val✝¹) (Sum.inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case a.h.inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
M : Matrix (n ⊕ o) (l ⊕ m) α
val✝¹ : n
val✝ : m
⊢ fromBlocks (toBlocks₁₁ M) (toBlocks₁₂ M) (toBlocks₂₁ M) (toBlocks₂₂ M) (Sum.inl val✝¹) (Sum.inr val✝) =
    M (Sum.inl val✝¹) (Sum.inr val✝)
[PROOFSTEP]
rfl
[GOAL]
case a.h.inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
M : Matrix (n ⊕ o) (l ⊕ m) α
val✝¹ : o
val✝ : l
⊢ fromBlocks (toBlocks₁₁ M) (toBlocks₁₂ M) (toBlocks₂₁ M) (toBlocks₂₂ M) (Sum.inr val✝¹) (Sum.inl val✝) =
    M (Sum.inr val✝¹) (Sum.inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case a.h.inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
M : Matrix (n ⊕ o) (l ⊕ m) α
val✝¹ : o
val✝ : m
⊢ fromBlocks (toBlocks₁₁ M) (toBlocks₁₂ M) (toBlocks₂₁ M) (toBlocks₂₂ M) (Sum.inr val✝¹) (Sum.inr val✝) =
    M (Sum.inr val✝¹) (Sum.inr val✝)
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A B : Matrix (n ⊕ o) (l ⊕ m) α
x✝ :
  toBlocks₁₁ A = toBlocks₁₁ B ∧ toBlocks₁₂ A = toBlocks₁₂ B ∧ toBlocks₂₁ A = toBlocks₂₁ B ∧ toBlocks₂₂ A = toBlocks₂₂ B
h₁₁ : toBlocks₁₁ A = toBlocks₁₁ B
h₁₂ : toBlocks₁₂ A = toBlocks₁₂ B
h₂₁ : toBlocks₂₁ A = toBlocks₂₁ B
h₂₂ : toBlocks₂₂ A = toBlocks₂₂ B
⊢ A = B
[PROOFSTEP]
rw [← fromBlocks_toBlocks A, ← fromBlocks_toBlocks B, h₁₁, h₁₂, h₂₁, h₂₂]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
⊢ map (fromBlocks A B C D) f = fromBlocks (map A f) (map B f) (map C f) (map D f)
[PROOFSTEP]
ext i j
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
i : n ⊕ o
j : l ⊕ m
⊢ map (fromBlocks A B C D) f i j = fromBlocks (map A f) (map B f) (map C f) (map D f) i j
[PROOFSTEP]
rcases i with ⟨⟩
[GOAL]
case a.h.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
j : l ⊕ m
val✝ : n
⊢ map (fromBlocks A B C D) f (Sum.inl val✝) j = fromBlocks (map A f) (map B f) (map C f) (map D f) (Sum.inl val✝) j
[PROOFSTEP]
rcases j with ⟨⟩
[GOAL]
case a.h.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
j : l ⊕ m
val✝ : o
⊢ map (fromBlocks A B C D) f (Sum.inr val✝) j = fromBlocks (map A f) (map B f) (map C f) (map D f) (Sum.inr val✝) j
[PROOFSTEP]
rcases j with ⟨⟩
[GOAL]
case a.h.inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
val✝¹ : n
val✝ : l
⊢ map (fromBlocks A B C D) f (Sum.inl val✝¹) (Sum.inl val✝) =
    fromBlocks (map A f) (map B f) (map C f) (map D f) (Sum.inl val✝¹) (Sum.inl val✝)
[PROOFSTEP]
simp [fromBlocks]
[GOAL]
case a.h.inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
val✝¹ : n
val✝ : m
⊢ map (fromBlocks A B C D) f (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks (map A f) (map B f) (map C f) (map D f) (Sum.inl val✝¹) (Sum.inr val✝)
[PROOFSTEP]
simp [fromBlocks]
[GOAL]
case a.h.inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
val✝¹ : o
val✝ : l
⊢ map (fromBlocks A B C D) f (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks (map A f) (map B f) (map C f) (map D f) (Sum.inr val✝¹) (Sum.inl val✝)
[PROOFSTEP]
simp [fromBlocks]
[GOAL]
case a.h.inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
val✝¹ : o
val✝ : m
⊢ map (fromBlocks A B C D) f (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks (map A f) (map B f) (map C f) (map D f) (Sum.inr val✝¹) (Sum.inr val✝)
[PROOFSTEP]
simp [fromBlocks]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
⊢ (fromBlocks A B C D)ᵀ = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ
[PROOFSTEP]
ext i j
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
i : l ⊕ m
j : n ⊕ o
⊢ (fromBlocks A B C D)ᵀ i j = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ i j
[PROOFSTEP]
rcases i with ⟨⟩
[GOAL]
case a.h.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
j : n ⊕ o
val✝ : l
⊢ (fromBlocks A B C D)ᵀ (Sum.inl val✝) j = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inl val✝) j
[PROOFSTEP]
rcases j with ⟨⟩
[GOAL]
case a.h.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
j : n ⊕ o
val✝ : m
⊢ (fromBlocks A B C D)ᵀ (Sum.inr val✝) j = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inr val✝) j
[PROOFSTEP]
rcases j with ⟨⟩
[GOAL]
case a.h.inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : l
val✝ : n
⊢ (fromBlocks A B C D)ᵀ (Sum.inl val✝¹) (Sum.inl val✝) = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inl val✝¹) (Sum.inl val✝)
[PROOFSTEP]
simp [fromBlocks]
[GOAL]
case a.h.inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : l
val✝ : o
⊢ (fromBlocks A B C D)ᵀ (Sum.inl val✝¹) (Sum.inr val✝) = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inl val✝¹) (Sum.inr val✝)
[PROOFSTEP]
simp [fromBlocks]
[GOAL]
case a.h.inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : m
val✝ : n
⊢ (fromBlocks A B C D)ᵀ (Sum.inr val✝¹) (Sum.inl val✝) = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inr val✝¹) (Sum.inl val✝)
[PROOFSTEP]
simp [fromBlocks]
[GOAL]
case a.h.inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : m
val✝ : o
⊢ (fromBlocks A B C D)ᵀ (Sum.inr val✝¹) (Sum.inr val✝) = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inr val✝¹) (Sum.inr val✝)
[PROOFSTEP]
simp [fromBlocks]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : Star α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
⊢ (fromBlocks A B C D)ᴴ = fromBlocks Aᴴ Cᴴ Bᴴ Dᴴ
[PROOFSTEP]
simp only [conjTranspose, fromBlocks_transpose, fromBlocks_map]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
⊢ submatrix (fromBlocks A B C D) Sum.swap f = submatrix (fromBlocks C D A B) id f
[PROOFSTEP]
ext i j
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
i : o ⊕ n
j : p
⊢ submatrix (fromBlocks A B C D) Sum.swap f i j = submatrix (fromBlocks C D A B) id f i j
[PROOFSTEP]
cases i
[GOAL]
case a.h.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝ : o
⊢ submatrix (fromBlocks A B C D) Sum.swap f (Sum.inl val✝) j = submatrix (fromBlocks C D A B) id f (Sum.inl val✝) j
[PROOFSTEP]
dsimp
[GOAL]
case a.h.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝ : n
⊢ submatrix (fromBlocks A B C D) Sum.swap f (Sum.inr val✝) j = submatrix (fromBlocks C D A B) id f (Sum.inr val✝) j
[PROOFSTEP]
dsimp
[GOAL]
case a.h.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝ : o
⊢ fromBlocks A B C D (Sum.inr val✝) (f j) = fromBlocks C D A B (Sum.inl val✝) (f j)
[PROOFSTEP]
cases f j
[GOAL]
case a.h.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝ : n
⊢ fromBlocks A B C D (Sum.inl val✝) (f j) = fromBlocks C D A B (Sum.inr val✝) (f j)
[PROOFSTEP]
cases f j
[GOAL]
case a.h.inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝¹ : o
val✝ : l
⊢ fromBlocks A B C D (Sum.inr val✝¹) (Sum.inl val✝) = fromBlocks C D A B (Sum.inl val✝¹) (Sum.inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case a.h.inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝¹ : o
val✝ : m
⊢ fromBlocks A B C D (Sum.inr val✝¹) (Sum.inr val✝) = fromBlocks C D A B (Sum.inl val✝¹) (Sum.inr val✝)
[PROOFSTEP]
rfl
[GOAL]
case a.h.inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝¹ : n
val✝ : l
⊢ fromBlocks A B C D (Sum.inl val✝¹) (Sum.inl val✝) = fromBlocks C D A B (Sum.inr val✝¹) (Sum.inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case a.h.inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝¹ : n
val✝ : m
⊢ fromBlocks A B C D (Sum.inl val✝¹) (Sum.inr val✝) = fromBlocks C D A B (Sum.inr val✝¹) (Sum.inr val✝)
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
⊢ submatrix (fromBlocks A B C D) f Sum.swap = submatrix (fromBlocks B A D C) f id
[PROOFSTEP]
ext i j
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
j : m ⊕ l
⊢ submatrix (fromBlocks A B C D) f Sum.swap i j = submatrix (fromBlocks B A D C) f id i j
[PROOFSTEP]
cases j
[GOAL]
case a.h.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝ : m
⊢ submatrix (fromBlocks A B C D) f Sum.swap i (Sum.inl val✝) = submatrix (fromBlocks B A D C) f id i (Sum.inl val✝)
[PROOFSTEP]
dsimp
[GOAL]
case a.h.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝ : l
⊢ submatrix (fromBlocks A B C D) f Sum.swap i (Sum.inr val✝) = submatrix (fromBlocks B A D C) f id i (Sum.inr val✝)
[PROOFSTEP]
dsimp
[GOAL]
case a.h.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝ : m
⊢ fromBlocks A B C D (f i) (Sum.inr val✝) = fromBlocks B A D C (f i) (Sum.inl val✝)
[PROOFSTEP]
cases f i
[GOAL]
case a.h.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝ : l
⊢ fromBlocks A B C D (f i) (Sum.inl val✝) = fromBlocks B A D C (f i) (Sum.inr val✝)
[PROOFSTEP]
cases f i
[GOAL]
case a.h.inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝¹ : m
val✝ : n
⊢ fromBlocks A B C D (Sum.inl val✝) (Sum.inr val✝¹) = fromBlocks B A D C (Sum.inl val✝) (Sum.inl val✝¹)
[PROOFSTEP]
rfl
[GOAL]
case a.h.inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝¹ : m
val✝ : o
⊢ fromBlocks A B C D (Sum.inr val✝) (Sum.inr val✝¹) = fromBlocks B A D C (Sum.inr val✝) (Sum.inl val✝¹)
[PROOFSTEP]
rfl
[GOAL]
case a.h.inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝¹ : l
val✝ : n
⊢ fromBlocks A B C D (Sum.inl val✝) (Sum.inl val✝¹) = fromBlocks B A D C (Sum.inl val✝) (Sum.inr val✝¹)
[PROOFSTEP]
rfl
[GOAL]
case a.h.inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝¹ : l
val✝ : o
⊢ fromBlocks A B C D (Sum.inr val✝) (Sum.inl val✝¹) = fromBlocks B A D C (Sum.inr val✝) (Sum.inr val✝¹)
[PROOFSTEP]
rfl
[GOAL]
l✝ : Type u_1
m✝ : Type u_2
n✝ : Type u_3
o✝ : Type u_4
p : Type u_5
q : Type u_6
m' : o✝ → Type u_7
n' : o✝ → Type u_8
p' : o✝ → Type u_9
R : Type u_10
S : Type u_11
α✝ : Type u_12
β : Type u_13
l : Type u_14
m : Type u_15
n : Type u_16
o : Type u_17
α : Type u_18
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
⊢ submatrix (fromBlocks A B C D) Sum.swap Sum.swap = fromBlocks D C B A
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
⊢ x • fromBlocks A B C D = fromBlocks (x • A) (x • B) (x • C) (x • D)
[PROOFSTEP]
ext i j
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
i : n ⊕ o
j : l ⊕ m
⊢ (x • fromBlocks A B C D) i j = fromBlocks (x • A) (x • B) (x • C) (x • D) i j
[PROOFSTEP]
rcases i with ⟨⟩
[GOAL]
case a.h.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
j : l ⊕ m
val✝ : n
⊢ (x • fromBlocks A B C D) (Sum.inl val✝) j = fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inl val✝) j
[PROOFSTEP]
rcases j with ⟨⟩
[GOAL]
case a.h.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
j : l ⊕ m
val✝ : o
⊢ (x • fromBlocks A B C D) (Sum.inr val✝) j = fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inr val✝) j
[PROOFSTEP]
rcases j with ⟨⟩
[GOAL]
case a.h.inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : n
val✝ : l
⊢ (x • fromBlocks A B C D) (Sum.inl val✝¹) (Sum.inl val✝) =
    fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inl val✝¹) (Sum.inl val✝)
[PROOFSTEP]
simp [fromBlocks]
[GOAL]
case a.h.inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : n
val✝ : m
⊢ (x • fromBlocks A B C D) (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inl val✝¹) (Sum.inr val✝)
[PROOFSTEP]
simp [fromBlocks]
[GOAL]
case a.h.inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : o
val✝ : l
⊢ (x • fromBlocks A B C D) (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inr val✝¹) (Sum.inl val✝)
[PROOFSTEP]
simp [fromBlocks]
[GOAL]
case a.h.inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : o
val✝ : m
⊢ (x • fromBlocks A B C D) (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inr val✝¹) (Sum.inr val✝)
[PROOFSTEP]
simp [fromBlocks]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
⊢ -fromBlocks A B C D = fromBlocks (-A) (-B) (-C) (-D)
[PROOFSTEP]
ext i j
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
i : n ⊕ o
j : l ⊕ m
⊢ (-fromBlocks A B C D) i j = fromBlocks (-A) (-B) (-C) (-D) i j
[PROOFSTEP]
cases i
[GOAL]
case a.h.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
j : l ⊕ m
val✝ : n
⊢ (-fromBlocks A B C D) (Sum.inl val✝) j = fromBlocks (-A) (-B) (-C) (-D) (Sum.inl val✝) j
[PROOFSTEP]
cases j
[GOAL]
case a.h.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
j : l ⊕ m
val✝ : o
⊢ (-fromBlocks A B C D) (Sum.inr val✝) j = fromBlocks (-A) (-B) (-C) (-D) (Sum.inr val✝) j
[PROOFSTEP]
cases j
[GOAL]
case a.h.inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
val✝¹ : n
val✝ : l
⊢ (-fromBlocks A B C D) (Sum.inl val✝¹) (Sum.inl val✝) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inl val✝¹) (Sum.inl val✝)
[PROOFSTEP]
simp [fromBlocks]
[GOAL]
case a.h.inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
val✝¹ : n
val✝ : m
⊢ (-fromBlocks A B C D) (Sum.inl val✝¹) (Sum.inr val✝) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inl val✝¹) (Sum.inr val✝)
[PROOFSTEP]
simp [fromBlocks]
[GOAL]
case a.h.inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
val✝¹ : o
val✝ : l
⊢ (-fromBlocks A B C D) (Sum.inr val✝¹) (Sum.inl val✝) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inr val✝¹) (Sum.inl val✝)
[PROOFSTEP]
simp [fromBlocks]
[GOAL]
case a.h.inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
val✝¹ : o
val✝ : m
⊢ (-fromBlocks A B C D) (Sum.inr val✝¹) (Sum.inr val✝) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inr val✝¹) (Sum.inr val✝)
[PROOFSTEP]
simp [fromBlocks]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : Zero α
⊢ fromBlocks 0 0 0 0 = 0
[PROOFSTEP]
ext i j
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : Zero α
i : n ⊕ o
j : l ⊕ m
⊢ fromBlocks 0 0 0 0 i j = OfNat.ofNat 0 i j
[PROOFSTEP]
rcases i with ⟨⟩
[GOAL]
case a.h.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : Zero α
j : l ⊕ m
val✝ : n
⊢ fromBlocks 0 0 0 0 (Sum.inl val✝) j = OfNat.ofNat 0 (Sum.inl val✝) j
[PROOFSTEP]
rcases j with ⟨⟩
[GOAL]
case a.h.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : Zero α
j : l ⊕ m
val✝ : o
⊢ fromBlocks 0 0 0 0 (Sum.inr val✝) j = OfNat.ofNat 0 (Sum.inr val✝) j
[PROOFSTEP]
rcases j with ⟨⟩
[GOAL]
case a.h.inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : Zero α
val✝¹ : n
val✝ : l
⊢ fromBlocks 0 0 0 0 (Sum.inl val✝¹) (Sum.inl val✝) = OfNat.ofNat 0 (Sum.inl val✝¹) (Sum.inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case a.h.inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : Zero α
val✝¹ : n
val✝ : m
⊢ fromBlocks 0 0 0 0 (Sum.inl val✝¹) (Sum.inr val✝) = OfNat.ofNat 0 (Sum.inl val✝¹) (Sum.inr val✝)
[PROOFSTEP]
rfl
[GOAL]
case a.h.inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : Zero α
val✝¹ : o
val✝ : l
⊢ fromBlocks 0 0 0 0 (Sum.inr val✝¹) (Sum.inl val✝) = OfNat.ofNat 0 (Sum.inr val✝¹) (Sum.inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case a.h.inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : Zero α
val✝¹ : o
val✝ : m
⊢ fromBlocks 0 0 0 0 (Sum.inr val✝¹) (Sum.inr val✝) = OfNat.ofNat 0 (Sum.inr val✝¹) (Sum.inr val✝)
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
⊢ fromBlocks A B C D + fromBlocks A' B' C' D' = fromBlocks (A + A') (B + B') (C + C') (D + D')
[PROOFSTEP]
ext i j
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
i : n ⊕ o
j : l ⊕ m
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') i j = fromBlocks (A + A') (B + B') (C + C') (D + D') i j
[PROOFSTEP]
rcases i with ⟨⟩
[GOAL]
case a.h.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
j : l ⊕ m
val✝ : n
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inl val✝) j =
    fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inl val✝) j
[PROOFSTEP]
rcases j with ⟨⟩
[GOAL]
case a.h.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
j : l ⊕ m
val✝ : o
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inr val✝) j =
    fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inr val✝) j
[PROOFSTEP]
rcases j with ⟨⟩
[GOAL]
case a.h.inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
val✝¹ : n
val✝ : l
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inl val✝¹) (Sum.inl val✝) =
    fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inl val✝¹) (Sum.inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case a.h.inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
val✝¹ : n
val✝ : m
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inl val✝¹) (Sum.inr val✝)
[PROOFSTEP]
rfl
[GOAL]
case a.h.inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
val✝¹ : o
val✝ : l
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inr val✝¹) (Sum.inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case a.h.inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
val✝¹ : o
val✝ : m
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inr val✝¹) (Sum.inr val✝)
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
⊢ fromBlocks A B C D * fromBlocks A' B' C' D' =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D')
[PROOFSTEP]
ext i j
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
i : n ⊕ o
j : p ⊕ q
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') i j =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') i j
[PROOFSTEP]
rcases i with ⟨⟩
[GOAL]
case a.h.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
j : p ⊕ q
val✝ : n
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inl val✝) j =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inl val✝) j
[PROOFSTEP]
rcases j with ⟨⟩
[GOAL]
case a.h.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
j : p ⊕ q
val✝ : o
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inr val✝) j =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inr val✝) j
[PROOFSTEP]
rcases j with ⟨⟩
[GOAL]
case a.h.inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
val✝¹ : n
val✝ : p
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inl val✝¹) (Sum.inl val✝) =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inl val✝¹) (Sum.inl val✝)
[PROOFSTEP]
simp only [fromBlocks, mul_apply, of_apply, Sum.elim_inr, Fintype.sum_sum_type, Sum.elim_inl, add_apply]
[GOAL]
case a.h.inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
val✝¹ : n
val✝ : q
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inl val✝¹) (Sum.inr val✝)
[PROOFSTEP]
simp only [fromBlocks, mul_apply, of_apply, Sum.elim_inr, Fintype.sum_sum_type, Sum.elim_inl, add_apply]
[GOAL]
case a.h.inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
val✝¹ : o
val✝ : p
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inr val✝¹) (Sum.inl val✝)
[PROOFSTEP]
simp only [fromBlocks, mul_apply, of_apply, Sum.elim_inr, Fintype.sum_sum_type, Sum.elim_inl, add_apply]
[GOAL]
case a.h.inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
val✝¹ : o
val✝ : q
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inr val✝¹) (Sum.inr val✝)
[PROOFSTEP]
simp only [fromBlocks, mul_apply, of_apply, Sum.elim_inr, Fintype.sum_sum_type, Sum.elim_inl, add_apply]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : l ⊕ m → α
⊢ mulVec (fromBlocks A B C D) x =
    Sum.elim (mulVec A (x ∘ Sum.inl) + mulVec B (x ∘ Sum.inr)) (mulVec C (x ∘ Sum.inl) + mulVec D (x ∘ Sum.inr))
[PROOFSTEP]
ext i
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : l ⊕ m → α
i : n ⊕ o
⊢ mulVec (fromBlocks A B C D) x i =
    Sum.elim (mulVec A (x ∘ Sum.inl) + mulVec B (x ∘ Sum.inr)) (mulVec C (x ∘ Sum.inl) + mulVec D (x ∘ Sum.inr)) i
[PROOFSTEP]
cases i
[GOAL]
case h.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : l ⊕ m → α
val✝ : n
⊢ mulVec (fromBlocks A B C D) x (Sum.inl val✝) =
    Sum.elim (mulVec A (x ∘ Sum.inl) + mulVec B (x ∘ Sum.inr)) (mulVec C (x ∘ Sum.inl) + mulVec D (x ∘ Sum.inr))
      (Sum.inl val✝)
[PROOFSTEP]
simp [mulVec, dotProduct]
[GOAL]
case h.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : l ⊕ m → α
val✝ : o
⊢ mulVec (fromBlocks A B C D) x (Sum.inr val✝) =
    Sum.elim (mulVec A (x ∘ Sum.inl) + mulVec B (x ∘ Sum.inr)) (mulVec C (x ∘ Sum.inl) + mulVec D (x ∘ Sum.inr))
      (Sum.inr val✝)
[PROOFSTEP]
simp [mulVec, dotProduct]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : n ⊕ o → α
⊢ vecMul x (fromBlocks A B C D) =
    Sum.elim (vecMul (x ∘ Sum.inl) A + vecMul (x ∘ Sum.inr) C) (vecMul (x ∘ Sum.inl) B + vecMul (x ∘ Sum.inr) D)
[PROOFSTEP]
ext i
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : n ⊕ o → α
i : l ⊕ m
⊢ vecMul x (fromBlocks A B C D) i =
    Sum.elim (vecMul (x ∘ Sum.inl) A + vecMul (x ∘ Sum.inr) C) (vecMul (x ∘ Sum.inl) B + vecMul (x ∘ Sum.inr) D) i
[PROOFSTEP]
cases i
[GOAL]
case h.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : n ⊕ o → α
val✝ : l
⊢ vecMul x (fromBlocks A B C D) (Sum.inl val✝) =
    Sum.elim (vecMul (x ∘ Sum.inl) A + vecMul (x ∘ Sum.inr) C) (vecMul (x ∘ Sum.inl) B + vecMul (x ∘ Sum.inr) D)
      (Sum.inl val✝)
[PROOFSTEP]
simp [vecMul, dotProduct]
[GOAL]
case h.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : n ⊕ o → α
val✝ : m
⊢ vecMul x (fromBlocks A B C D) (Sum.inr val✝) =
    Sum.elim (vecMul (x ∘ Sum.inl) A + vecMul (x ∘ Sum.inr) C) (vecMul (x ∘ Sum.inl) B + vecMul (x ∘ Sum.inr) D)
      (Sum.inr val✝)
[PROOFSTEP]
simp [vecMul, dotProduct]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p✝ : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
⊢ toBlock (diagonal d) p p = diagonal fun i => d ↑i
[PROOFSTEP]
ext i j
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p✝ : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
i j : { a // p a }
⊢ toBlock (diagonal d) p p i j = diagonal (fun i => d ↑i) i j
[PROOFSTEP]
by_cases i = j
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p✝ : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
i j : { a // p a }
⊢ toBlock (diagonal d) p p i j = diagonal (fun i => d ↑i) i j
[PROOFSTEP]
by_cases i = j
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p✝ : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
i j : { a // p a }
h : i = j
⊢ toBlock (diagonal d) p p i j = diagonal (fun i => d ↑i) i j
[PROOFSTEP]
simp [h]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p✝ : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
i j : { a // p a }
h : ¬i = j
⊢ toBlock (diagonal d) p p i j = diagonal (fun i => d ↑i) i j
[PROOFSTEP]
simp [One.one, h, Subtype.val_injective.ne h]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p✝ : Type u_5
q✝ : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p q : m → Prop
hpq : Disjoint p q
⊢ toBlock (diagonal d) p q = 0
[PROOFSTEP]
ext ⟨i, hi⟩ ⟨j, hj⟩
[GOAL]
case a.mk.h.mk
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p✝ : Type u_5
q✝ : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p q : m → Prop
hpq : Disjoint p q
i : m
hi : p i
j : m
hj : q j
⊢ toBlock (diagonal d) p q { val := i, property := hi } { val := j, property := hj } =
    OfNat.ofNat 0 { val := i, property := hi } { val := j, property := hj }
[PROOFSTEP]
have : i ≠ j := fun heq => hpq.le_bot i ⟨hi, heq.symm ▸ hj⟩
[GOAL]
case a.mk.h.mk
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p✝ : Type u_5
q✝ : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p q : m → Prop
hpq : Disjoint p q
i : m
hi : p i
j : m
hj : q j
this : i ≠ j
⊢ toBlock (diagonal d) p q { val := i, property := hi } { val := j, property := hj } =
    OfNat.ofNat 0 { val := i, property := hi } { val := j, property := hj }
[PROOFSTEP]
simp [diagonal_apply_ne d this]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) = diagonal (Sum.elim d₁ d₂)
[PROOFSTEP]
ext i j
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
i j : l ⊕ m
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) i j = diagonal (Sum.elim d₁ d₂) i j
[PROOFSTEP]
rcases i with ⟨⟩
[GOAL]
case a.h.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
j : l ⊕ m
val✝ : l
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inl val✝) j = diagonal (Sum.elim d₁ d₂) (Sum.inl val✝) j
[PROOFSTEP]
rcases j with ⟨⟩
[GOAL]
case a.h.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
j : l ⊕ m
val✝ : m
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inr val✝) j = diagonal (Sum.elim d₁ d₂) (Sum.inr val✝) j
[PROOFSTEP]
rcases j with ⟨⟩
[GOAL]
case a.h.inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
val✝¹ val✝ : l
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inl val✝¹) (Sum.inl val✝) =
    diagonal (Sum.elim d₁ d₂) (Sum.inl val✝¹) (Sum.inl val✝)
[PROOFSTEP]
simp [diagonal]
[GOAL]
case a.h.inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
val✝¹ : l
val✝ : m
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inl val✝¹) (Sum.inr val✝) =
    diagonal (Sum.elim d₁ d₂) (Sum.inl val✝¹) (Sum.inr val✝)
[PROOFSTEP]
simp [diagonal]
[GOAL]
case a.h.inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
val✝¹ : m
val✝ : l
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inr val✝¹) (Sum.inl val✝) =
    diagonal (Sum.elim d₁ d₂) (Sum.inr val✝¹) (Sum.inl val✝)
[PROOFSTEP]
simp [diagonal]
[GOAL]
case a.h.inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
val✝¹ val✝ : m
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inr val✝¹) (Sum.inr val✝) =
    diagonal (Sum.elim d₁ d₂) (Sum.inr val✝¹) (Sum.inr val✝)
[PROOFSTEP]
simp [diagonal]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
⊢ fromBlocks 1 0 0 1 = 1
[PROOFSTEP]
ext i j
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
i j : l ⊕ m
⊢ fromBlocks 1 0 0 1 i j = OfNat.ofNat 1 i j
[PROOFSTEP]
rcases i with ⟨⟩
[GOAL]
case a.h.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
j : l ⊕ m
val✝ : l
⊢ fromBlocks 1 0 0 1 (Sum.inl val✝) j = OfNat.ofNat 1 (Sum.inl val✝) j
[PROOFSTEP]
rcases j with ⟨⟩
[GOAL]
case a.h.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
j : l ⊕ m
val✝ : m
⊢ fromBlocks 1 0 0 1 (Sum.inr val✝) j = OfNat.ofNat 1 (Sum.inr val✝) j
[PROOFSTEP]
rcases j with ⟨⟩
[GOAL]
case a.h.inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
val✝¹ val✝ : l
⊢ fromBlocks 1 0 0 1 (Sum.inl val✝¹) (Sum.inl val✝) = OfNat.ofNat 1 (Sum.inl val✝¹) (Sum.inl val✝)
[PROOFSTEP]
simp [one_apply]
[GOAL]
case a.h.inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
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✝) = OfNat.ofNat 1 (Sum.inl val✝¹) (Sum.inr val✝)
[PROOFSTEP]
simp [one_apply]
[GOAL]
case a.h.inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
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✝) = OfNat.ofNat 1 (Sum.inr val✝¹) (Sum.inl val✝)
[PROOFSTEP]
simp [one_apply]
[GOAL]
case a.h.inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
val✝¹ val✝ : m
⊢ fromBlocks 1 0 0 1 (Sum.inr val✝¹) (Sum.inr val✝) = OfNat.ofNat 1 (Sum.inr val✝¹) (Sum.inr val✝)
[PROOFSTEP]
simp [one_apply]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
ik : m × o
jk : n × o
⊢ blockDiagonal M ik jk = if ik.snd = jk.snd then M ik.snd ik.fst jk.fst else 0
[PROOFSTEP]
cases ik
[GOAL]
case mk
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
jk : n × o
fst✝ : m
snd✝ : o
⊢ blockDiagonal M (fst✝, snd✝) jk = if (fst✝, snd✝).snd = jk.snd then M (fst✝, snd✝).snd (fst✝, snd✝).fst jk.fst else 0
[PROOFSTEP]
cases jk
[GOAL]
case mk.mk
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
fst✝¹ : m
snd✝¹ : o
fst✝ : n
snd✝ : o
⊢ blockDiagonal M (fst✝¹, snd✝¹) (fst✝, snd✝) =
    if (fst✝¹, snd✝¹).snd = (fst✝, snd✝).snd then M (fst✝¹, snd✝¹).snd (fst✝¹, snd✝¹).fst (fst✝, snd✝).fst else 0
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
f : α → β
hf : f 0 = 0
⊢ map (blockDiagonal M) f = blockDiagonal fun k => map (M k) f
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
f : α → β
hf : f 0 = 0
i✝ : m × o
x✝ : n × o
⊢ map (blockDiagonal M) f i✝ x✝ = blockDiagonal (fun k => map (M k) f) i✝ x✝
[PROOFSTEP]
simp only [map_apply, blockDiagonal_apply, eq_comm]
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
f : α → β
hf : f 0 = 0
i✝ : m × o
x✝ : n × o
⊢ f (if i✝.snd = x✝.snd then M i✝.snd i✝.fst x✝.fst else 0) = if i✝.snd = x✝.snd then f (M i✝.snd i✝.fst x✝.fst) else 0
[PROOFSTEP]
rw [apply_ite f, hf]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
⊢ (blockDiagonal M)ᵀ = blockDiagonal fun k => (M k)ᵀ
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
i✝ : n × o
x✝ : m × o
⊢ (blockDiagonal M)ᵀ i✝ x✝ = blockDiagonal (fun k => (M k)ᵀ) i✝ x✝
[PROOFSTEP]
simp only [transpose_apply, blockDiagonal_apply, eq_comm]
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
i✝ : n × o
x✝ : m × o
⊢ (if i✝.snd = x✝.snd then M i✝.snd x✝.fst i✝.fst else 0) = if i✝.snd = x✝.snd then M x✝.snd x✝.fst i✝.fst else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
i✝ : n × o
x✝ : m × o
h : i✝.snd = x✝.snd
⊢ M i✝.snd x✝.fst i✝.fst = M x✝.snd x✝.fst i✝.fst
[PROOFSTEP]
rw [h]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
i✝ : n × o
x✝ : m × o
h : ¬i✝.snd = x✝.snd
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α✝ : Type u_12
β : Type u_13
inst✝⁴ : DecidableEq o
inst✝³ : Zero α✝
inst✝² : Zero β
α : Type u_14
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : o → Matrix m n α
⊢ (blockDiagonal M)ᴴ = blockDiagonal fun k => (M k)ᴴ
[PROOFSTEP]
simp only [conjTranspose, blockDiagonal_transpose]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α✝ : Type u_12
β : Type u_13
inst✝⁴ : DecidableEq o
inst✝³ : Zero α✝
inst✝² : Zero β
α : Type u_14
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : o → Matrix m n α
⊢ map (blockDiagonal fun k => (M k)ᵀ) star = blockDiagonal fun k => map (M k)ᵀ star
[PROOFSTEP]
rw [blockDiagonal_map _ star (star_zero α)]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
⊢ blockDiagonal 0 = 0
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
i✝ : m × o
x✝ : n × o
⊢ blockDiagonal 0 i✝ x✝ = OfNat.ofNat 0 i✝ x✝
[PROOFSTEP]
simp [blockDiagonal_apply]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : DecidableEq m
d : o → m → α
⊢ (blockDiagonal fun k => diagonal (d k)) = diagonal fun ik => d ik.snd ik.fst
[PROOFSTEP]
ext ⟨i, k⟩ ⟨j, k'⟩
[GOAL]
case a.mk.h.mk
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : DecidableEq m
d : o → m → α
i : m
k : o
j : m
k' : o
⊢ blockDiagonal (fun k => diagonal (d k)) (i, k) (j, k') = diagonal (fun ik => d ik.snd ik.fst) (i, k) (j, k')
[PROOFSTEP]
simp only [blockDiagonal_apply, diagonal_apply, Prod.mk.inj_iff, ← ite_and]
[GOAL]
case a.mk.h.mk
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : DecidableEq m
d : o → m → α
i : m
k : o
j : m
k' : o
⊢ (if k = k' ∧ i = j then d k i else 0) = if i = j ∧ k = k' then d k i else 0
[PROOFSTEP]
congr 1
[GOAL]
case a.mk.h.mk.e_c
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : DecidableEq m
d : o → m → α
i : m
k : o
j : m
k' : o
⊢ (k = k' ∧ i = j) = (i = j ∧ k = k')
[PROOFSTEP]
rw [and_comm]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝⁴ : DecidableEq o
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : DecidableEq m
inst✝ : One α
⊢ (blockDiagonal fun x => diagonal fun x => 1) = diagonal fun x => 1
[PROOFSTEP]
rw [blockDiagonal_diagonal]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : o → Matrix m n α
⊢ blockDiagonal (M + N) = blockDiagonal M + blockDiagonal N
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : o → Matrix m n α
i✝ : m × o
x✝ : n × o
⊢ blockDiagonal (M + N) i✝ x✝ = (blockDiagonal M + blockDiagonal N) i✝ x✝
[PROOFSTEP]
simp only [blockDiagonal_apply, Pi.add_apply, add_apply]
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : o → Matrix m n α
i✝ : m × o
x✝ : n × o
⊢ (if i✝.snd = x✝.snd then M i✝.snd i✝.fst x✝.fst + N i✝.snd i✝.fst x✝.fst else 0) =
    (if i✝.snd = x✝.snd then M i✝.snd i✝.fst x✝.fst else 0) + if i✝.snd = x✝.snd then N i✝.snd i✝.fst x✝.fst else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : o → Matrix m n α
i✝ : m × o
x✝ : n × o
h✝ : i✝.snd = x✝.snd
⊢ M i✝.snd i✝.fst x✝.fst + N i✝.snd i✝.fst x✝.fst = M i✝.snd i✝.fst x✝.fst + N i✝.snd i✝.fst x✝.fst
[PROOFSTEP]
simp
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : o → Matrix m n α
i✝ : m × o
x✝ : n × o
h✝ : ¬i✝.snd = x✝.snd
⊢ 0 = 0 + 0
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : DecidableEq o
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
M : o → Matrix m n α
N : o → Matrix n p α
⊢ (blockDiagonal fun k => M k * N k) = blockDiagonal M * blockDiagonal N
[PROOFSTEP]
ext ⟨i, k⟩ ⟨j, k'⟩
[GOAL]
case a.mk.h.mk
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
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
⊢ blockDiagonal (fun k => M k * N k) (i, k) (j, k') = (blockDiagonal M * blockDiagonal N) (i, k) (j, k')
[PROOFSTEP]
simp only [blockDiagonal_apply, mul_apply, ← Finset.univ_product_univ, Finset.sum_product]
[GOAL]
case a.mk.h.mk
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
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
⊢ (if k = k' then ∑ j_1 : n, M k i j_1 * N k j_1 j else 0) =
    ∑ x : n, ∑ x_1 : o, (if k = x_1 then M k i x else 0) * if x_1 = k' then N x_1 x j else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
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 : n, M k i j_1 * N k j_1 j =
    ∑ x : n, ∑ x_1 : o, (if k = x_1 then M k i x else 0) * if x_1 = k' then N x_1 x j else 0
[PROOFSTEP]
simp [h]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
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 : n, ∑ x_1 : o, (if k = x_1 then M k i x else 0) * if x_1 = k' then N x_1 x j else 0
[PROOFSTEP]
simp [h]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R✝ : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : DecidableEq o
R : Type u_14
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
x : R
M : o → Matrix m n α
⊢ blockDiagonal (x • M) = x • blockDiagonal M
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R✝ : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : DecidableEq o
R : Type u_14
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
x : R
M : o → Matrix m n α
i✝ : m × o
x✝ : n × o
⊢ blockDiagonal (x • M) i✝ x✝ = (x • blockDiagonal M) i✝ x✝
[PROOFSTEP]
simp only [blockDiagonal_apply, Pi.smul_apply, smul_apply]
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R✝ : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : DecidableEq o
R : Type u_14
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
x : R
M : o → Matrix m n α
i✝ : m × o
x✝ : n × o
⊢ (if i✝.snd = x✝.snd then x • M i✝.snd i✝.fst x✝.fst else 0) =
    x • if i✝.snd = x✝.snd then M i✝.snd i✝.fst x✝.fst else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R✝ : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : DecidableEq o
R : Type u_14
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
x : R
M : o → Matrix m n α
i✝ : m × o
x✝ : n × o
h✝ : i✝.snd = x✝.snd
⊢ x • M i✝.snd i✝.fst x✝.fst = x • M i✝.snd i✝.fst x✝.fst
[PROOFSTEP]
simp
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R✝ : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : DecidableEq o
R : Type u_14
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
x : R
M : o → Matrix m n α
i✝ : m × o
x✝ : n × o
h✝ : ¬i✝.snd = x✝.snd
⊢ 0 = x • 0
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
⊢ blockDiag (diagonal d) k i j = diagonal (fun i => d (i, k)) i j
[PROOFSTEP]
obtain rfl | hij := Decidable.eq_or_ne i j
[GOAL]
case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i : m
⊢ blockDiag (diagonal d) k i i = diagonal (fun i => d (i, k)) i i
[PROOFSTEP]
rw [blockDiag_apply, diagonal_apply_eq, diagonal_apply_eq]
[GOAL]
case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ blockDiag (diagonal d) k i j = diagonal (fun i => d (i, k)) i j
[PROOFSTEP]
rw [blockDiag_apply, diagonal_apply_ne _ hij, diagonal_apply_ne _ (mt _ hij)]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ (i, k) = (j, k) → i = j
[PROOFSTEP]
exact Prod.fst_eq_iff.mpr
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
ik : (i : o) × m' i
jk : (i : o) × n' i
⊢ blockDiagonal' M ik jk = if h : ik.fst = jk.fst then M ik.fst ik.snd (cast (_ : n' jk.fst = n' ik.fst) jk.snd) else 0
[PROOFSTEP]
cases ik
[GOAL]
case mk
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
jk : (i : o) × n' i
fst✝ : o
snd✝ : m' fst✝
⊢ blockDiagonal' M { fst := fst✝, snd := snd✝ } jk =
    if h : { fst := fst✝, snd := snd✝ }.fst = jk.fst then
      M { fst := fst✝, snd := snd✝ }.fst { fst := fst✝, snd := snd✝ }.snd
        (cast (_ : n' jk.fst = n' { fst := fst✝, snd := snd✝ }.fst) jk.snd)
    else 0
[PROOFSTEP]
cases jk
[GOAL]
case mk.mk
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
fst✝¹ : o
snd✝¹ : m' fst✝¹
fst✝ : o
snd✝ : n' fst✝
⊢ blockDiagonal' M { fst := fst✝¹, snd := snd✝¹ } { fst := fst✝, snd := snd✝ } =
    if h : { fst := fst✝¹, snd := snd✝¹ }.fst = { fst := fst✝, snd := snd✝ }.fst then
      M { fst := fst✝¹, snd := snd✝¹ }.fst { fst := fst✝¹, snd := snd✝¹ }.snd
        (cast (_ : n' { fst := fst✝, snd := snd✝ }.fst = n' { fst := fst✝¹, snd := snd✝¹ }.fst)
          { fst := fst✝, snd := snd✝ }.snd)
    else 0
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
f : α → β
hf : f 0 = 0
⊢ map (blockDiagonal' M) f = blockDiagonal' fun k => map (M k) f
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
f : α → β
hf : f 0 = 0
i✝ : (i : o) × m' i
x✝ : (i : o) × n' i
⊢ map (blockDiagonal' M) f i✝ x✝ = blockDiagonal' (fun k => map (M k) f) i✝ x✝
[PROOFSTEP]
simp only [map_apply, blockDiagonal'_apply, eq_comm]
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
f : α → β
hf : f 0 = 0
i✝ : (i : o) × m' i
x✝ : (i : o) × n' i
⊢ f (if h : i✝.fst = x✝.fst then M i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd) else 0) =
    if h : i✝.fst = x✝.fst then f (M i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd)) else 0
[PROOFSTEP]
rw [apply_dite f, hf]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
⊢ (blockDiagonal' M)ᵀ = blockDiagonal' fun k => (M k)ᵀ
[PROOFSTEP]
ext ⟨ii, ix⟩ ⟨ji, jx⟩
[GOAL]
case a.mk.h.mk
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
⊢ (blockDiagonal' M)ᵀ { fst := ii, snd := ix } { fst := ji, snd := jx } =
    blockDiagonal' (fun k => (M k)ᵀ) { fst := ii, snd := ix } { fst := ji, snd := jx }
[PROOFSTEP]
simp only [transpose_apply, blockDiagonal'_apply]
[GOAL]
case a.mk.h.mk
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
⊢ (if h : ji = ii then M ji jx (cast (_ : n' { fst := ii, snd := ix }.fst = n' { fst := ji, snd := jx }.fst) ix)
    else 0) =
    if h : ii = ji then M ii (cast (_ : m' { fst := ji, snd := jx }.fst = m' { fst := ii, snd := ix }.fst) jx) ix else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
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 (_ : n' { fst := ii, snd := ix }.fst = n' { fst := ji, snd := jx }.fst) ix) =
    M ii (cast (_ : m' { fst := ji, snd := jx }.fst = m' { fst := ii, snd := ix }.fst) jx) ix
[PROOFSTEP]
subst h
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
ji : o
jx : m' ji
ix : n' ji
h✝ : ji = ji
⊢ M ji jx (cast (_ : n' { fst := ji, snd := ix }.fst = n' { fst := ji, snd := jx }.fst) ix) =
    M ji (cast (_ : m' { fst := ji, snd := jx }.fst = m' { fst := ji, snd := ix }.fst) jx) ix
[PROOFSTEP]
rfl
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
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 (_ : n' { fst := ii, snd := ix }.fst = n' { fst := ji, snd := jx }.fst) ix) = 0
[PROOFSTEP]
simp_all only [not_true]
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
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 (_ : m' { fst := ji, snd := jx }.fst = m' { fst := ii, snd := ix }.fst) jx) ix
[PROOFSTEP]
simp_all only [not_true]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
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
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α✝ : Type u_12
β : Type u_13
inst✝⁴ : DecidableEq o
inst✝³ : Zero α✝
inst✝² : Zero β
α : Type u_14
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : (i : o) → Matrix (m' i) (n' i) α
⊢ (blockDiagonal' M)ᴴ = blockDiagonal' fun k => (M k)ᴴ
[PROOFSTEP]
simp only [conjTranspose, blockDiagonal'_transpose]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α✝ : Type u_12
β : Type u_13
inst✝⁴ : DecidableEq o
inst✝³ : Zero α✝
inst✝² : Zero β
α : Type u_14
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : (i : o) → Matrix (m' i) (n' i) α
⊢ map (blockDiagonal' fun k => (M k)ᵀ) star = blockDiagonal' fun k => map (M k)ᵀ star
[PROOFSTEP]
exact blockDiagonal'_map _ star (star_zero α)
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
⊢ blockDiagonal' 0 = 0
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
i✝ : (i : o) × m' i
x✝ : (i : o) × n' i
⊢ blockDiagonal' 0 i✝ x✝ = OfNat.ofNat 0 i✝ x✝
[PROOFSTEP]
simp [blockDiagonal'_apply]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
⊢ (blockDiagonal' fun k => diagonal (d k)) = diagonal fun ik => d ik.fst ik.snd
[PROOFSTEP]
ext ⟨i, k⟩ ⟨j, k'⟩
[GOAL]
case a.mk.h.mk
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k : m' i
j : o
k' : m' j
⊢ blockDiagonal' (fun k => diagonal (d k)) { fst := i, snd := k } { fst := j, snd := k' } =
    diagonal (fun ik => d ik.fst ik.snd) { fst := i, snd := k } { fst := j, snd := k' }
[PROOFSTEP]
simp only [blockDiagonal'_apply, diagonal]
[GOAL]
case a.mk.h.mk
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k : m' i
j : o
k' : m' j
⊢ (if h : i = j then
      ↑of (fun i_1 j => if i_1 = j then d i i_1 else 0) k
        (cast (_ : m' { fst := j, snd := k' }.fst = m' { fst := i, snd := k }.fst) k')
    else 0) =
    ↑of (fun i j => if i = j then d i.fst i.snd else 0) { fst := i, snd := k } { fst := j, snd := k' }
[PROOFSTEP]
obtain rfl | hij := Decidable.eq_or_ne i j
[GOAL]
case a.mk.h.mk.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k k' : m' i
⊢ (if h : i = i then
      ↑of (fun i_1 j => if i_1 = j then d i i_1 else 0) k
        (cast (_ : m' { fst := i, snd := k' }.fst = m' { fst := i, snd := k }.fst) k')
    else 0) =
    ↑of (fun i j => if i = j then d i.fst i.snd else 0) { fst := i, snd := k } { fst := i, snd := k' }
[PROOFSTEP]
simp
[GOAL]
case a.mk.h.mk.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k : m' i
j : o
k' : m' j
hij : i ≠ j
⊢ (if h : i = j then
      ↑of (fun i_1 j => if i_1 = j then d i i_1 else 0) k
        (cast (_ : m' { fst := j, snd := k' }.fst = m' { fst := i, snd := k }.fst) k')
    else 0) =
    ↑of (fun i j => if i = j then d i.fst i.snd else 0) { fst := i, snd := k } { fst := j, snd := k' }
[PROOFSTEP]
simp [hij]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝⁴ : DecidableEq o
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : (i : o) → DecidableEq (m' i)
inst✝ : One α
⊢ (blockDiagonal' fun i => diagonal fun x => 1) = diagonal fun x => 1
[PROOFSTEP]
rw [blockDiagonal'_diagonal]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : (i : o) → Matrix (m' i) (n' i) α
⊢ blockDiagonal' (M + N) = blockDiagonal' M + blockDiagonal' N
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
x✝ : (i : o) × n' i
⊢ blockDiagonal' (M + N) i✝ x✝ = (blockDiagonal' M + blockDiagonal' N) i✝ x✝
[PROOFSTEP]
simp only [blockDiagonal'_apply, Pi.add_apply, add_apply]
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
x✝ : (i : o) × n' i
⊢ (if h : i✝.fst = x✝.fst then
      M i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd) +
        N i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd)
    else 0) =
    (if h : i✝.fst = x✝.fst then M i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd) else 0) +
      if h : i✝.fst = x✝.fst then N i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd) else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
x✝ : (i : o) × n' i
h✝ : i✝.fst = x✝.fst
⊢ M i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd) +
      N i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd) =
    M i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd) +
      N i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd)
[PROOFSTEP]
simp
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
x✝ : (i : o) × n' i
h✝ : ¬i✝.fst = x✝.fst
⊢ 0 = 0 + 0
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
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) α
⊢ (blockDiagonal' fun k => M k * N k) = blockDiagonal' M * blockDiagonal' N
[PROOFSTEP]
ext ⟨k, i⟩ ⟨k', j⟩
[GOAL]
case a.mk.h.mk
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
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'
⊢ blockDiagonal' (fun k => M k * N k) { fst := k, snd := i } { fst := k', snd := j } =
    (blockDiagonal' M * blockDiagonal' N) { fst := k, snd := i } { fst := k', snd := j }
[PROOFSTEP]
simp only [blockDiagonal'_apply, mul_apply, ← Finset.univ_sigma_univ, Finset.sum_sigma]
[GOAL]
case a.mk.h.mk
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
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'
⊢ (if h : k = k' then
      ∑ j_1 : n' k, M k i j_1 * N k j_1 (cast (_ : p' { fst := k', snd := j }.fst = p' { fst := k, snd := i }.fst) j)
    else 0) =
    ∑ x : o,
      ∑ x_1 : n' x,
        (if h : k = x then M k i (cast (_ : n' { fst := x, snd := x_1 }.fst = n' { fst := k, snd := i }.fst) x_1)
          else 0) *
          if h : x = k' then N x x_1 (cast (_ : p' { fst := k', snd := j }.fst = p' { fst := x, snd := x_1 }.fst) j)
          else 0
[PROOFSTEP]
rw [Fintype.sum_eq_single k]
[GOAL]
case a.mk.h.mk
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
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'
⊢ (if h : k = k' then
      ∑ j_1 : n' k, M k i j_1 * N k j_1 (cast (_ : p' { fst := k', snd := j }.fst = p' { fst := k, snd := i }.fst) j)
    else 0) =
    ∑ x : n' k,
      (if h : k = k then M k i (cast (_ : n' { fst := k, snd := x }.fst = n' { fst := k, snd := i }.fst) x) else 0) *
        if h : k = k' then N k x (cast (_ : p' { fst := k', snd := j }.fst = p' { fst := k, snd := x }.fst) j) else 0
[PROOFSTEP]
simp only [if_pos, dif_pos]
  -- porting note: added
[GOAL]
case a.mk.h.mk
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
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'
⊢ (if h : k = k' then
      ∑ j_1 : n' k, M k i j_1 * N k j_1 (cast (_ : p' { fst := k', snd := j }.fst = p' { fst := k, snd := i }.fst) j)
    else 0) =
    ∑ x : n' k,
      M k i (cast (_ : n' { fst := k, snd := x }.fst = n' { fst := k, snd := i }.fst) x) *
        if h : k = k' then N k x (cast (_ : p' { fst := k', snd := j }.fst = p' { fst := k, snd := x }.fst) j) else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
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 : n' k, M k i j_1 * N k j_1 (cast (_ : p' { fst := k', snd := j }.fst = p' { fst := k, snd := i }.fst) j) =
    ∑ x : n' k,
      M k i (cast (_ : n' { fst := k, snd := x }.fst = n' { fst := k, snd := i }.fst) x) *
        N k x (cast (_ : p' { fst := k', snd := j }.fst = p' { fst := k, snd := x }.fst) j)
[PROOFSTEP]
simp
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
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 : n' k, M k i (cast (_ : n' { fst := k, snd := x }.fst = n' { fst := k, snd := i }.fst) x) * 0
[PROOFSTEP]
simp
[GOAL]
case a.mk.h.mk
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
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'
⊢ ∀ (x : o),
    x ≠ k →
      (∑ x_2 : n' x,
          (if h : k = x then M k i (cast (_ : n' { fst := x, snd := x_2 }.fst = n' { fst := k, snd := i }.fst) x_2)
            else 0) *
            if h : x = k' then N x x_2 (cast (_ : p' { fst := k', snd := j }.fst = p' { fst := x, snd := x_2 }.fst) j)
            else 0) =
        0
[PROOFSTEP]
intro j' hj'
[GOAL]
case a.mk.h.mk
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
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'
j' : o
hj' : j' ≠ k
⊢ (∑ x : n' j',
      (if h : k = j' then M k i (cast (_ : n' { fst := j', snd := x }.fst = n' { fst := k, snd := i }.fst) x) else 0) *
        if h : j' = k' then N j' x (cast (_ : p' { fst := k', snd := j }.fst = p' { fst := j', snd := x }.fst) j)
        else 0) =
    0
[PROOFSTEP]
exact Finset.sum_eq_zero fun _ _ => by rw [dif_neg hj'.symm, zero_mul]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
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'
j' : o
hj' : j' ≠ k
x✝¹ : n' j'
x✝ : x✝¹ ∈ Finset.univ
⊢ ((if h : k = j' then M k i (cast (_ : n' { fst := j', snd := x✝¹ }.fst = n' { fst := k, snd := i }.fst) x✝¹) else 0) *
      if h : j' = k' then N j' x✝¹ (cast (_ : p' { fst := k', snd := j }.fst = p' { fst := j', snd := x✝¹ }.fst) j)
      else 0) =
    0
[PROOFSTEP]
rw [dif_neg hj'.symm, zero_mul]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R✝ : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : DecidableEq o
R : Type u_14
inst✝² : Semiring R
inst✝¹ : AddCommMonoid α
inst✝ : Module R α
x : R
M : (i : o) → Matrix (m' i) (n' i) α
⊢ blockDiagonal' (x • M) = x • blockDiagonal' M
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R✝ : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : DecidableEq o
R : Type u_14
inst✝² : Semiring R
inst✝¹ : AddCommMonoid α
inst✝ : Module R α
x : R
M : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
x✝ : (i : o) × n' i
⊢ blockDiagonal' (x • M) i✝ x✝ = (x • blockDiagonal' M) i✝ x✝
[PROOFSTEP]
simp only [blockDiagonal'_apply, Pi.smul_apply, smul_apply]
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R✝ : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : DecidableEq o
R : Type u_14
inst✝² : Semiring R
inst✝¹ : AddCommMonoid α
inst✝ : Module R α
x : R
M : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
x✝ : (i : o) × n' i
⊢ (if h : i✝.fst = x✝.fst then x • M i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd) else 0) =
    x • if h : i✝.fst = x✝.fst then M i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd) else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R✝ : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : DecidableEq o
R : Type u_14
inst✝² : Semiring R
inst✝¹ : AddCommMonoid α
inst✝ : Module R α
x : R
M : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
x✝ : (i : o) × n' i
h✝ : i✝.fst = x✝.fst
⊢ x • M i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd) =
    x • M i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd)
[PROOFSTEP]
simp
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R✝ : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : DecidableEq o
R : Type u_14
inst✝² : Semiring R
inst✝¹ : AddCommMonoid α
inst✝ : Module R α
x : R
M : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
x✝ : (i : o) × n' i
h✝ : ¬i✝.fst = x✝.fst
⊢ 0 = x • 0
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
⊢ blockDiag' (diagonal d) k i j = diagonal (fun i => d { fst := k, snd := i }) i j
[PROOFSTEP]
obtain rfl | hij := Decidable.eq_or_ne i j
[GOAL]
case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i : m' k
⊢ blockDiag' (diagonal d) k i i = diagonal (fun i => d { fst := k, snd := i }) i i
[PROOFSTEP]
rw [blockDiag'_apply, diagonal_apply_eq, diagonal_apply_eq]
[GOAL]
case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
hij : i ≠ j
⊢ blockDiag' (diagonal d) k i j = diagonal (fun i => d { fst := k, snd := i }) i j
[PROOFSTEP]
rw [blockDiag'_apply, diagonal_apply_ne _ hij, diagonal_apply_ne _ (mt (fun h => ?_) hij)]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
hij : i ≠ j
h : { fst := k, snd := i } = { fst := k, snd := j }
⊢ i = j
[PROOFSTEP]
cases h
[GOAL]
case refl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i : m' k
hij : i ≠ i
⊢ i = i
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m✝ : Type u_2
n✝ : Type u_3
o : Type u_4
p✝ : Type u_5
q✝ : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝¹ : CommRing R
m : Type u_14
n : Type u_15
k : Type u_16
inst✝ : Fintype n
p : m → Prop
q : k → Prop
A : Matrix m n R
B : Matrix n k R
⊢ toBlock (A * B) p q = toBlock A p ⊤ * toBlock B ⊤ q
[PROOFSTEP]
ext i k
[GOAL]
case a.h
l : Type u_1
m✝ : Type u_2
n✝ : Type u_3
o : Type u_4
p✝ : Type u_5
q✝ : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝¹ : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝ : Fintype n
p : m → Prop
q : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // q a }
⊢ toBlock (A * B) p q i k = (toBlock A p ⊤ * toBlock B ⊤ q) i k
[PROOFSTEP]
simp only [toBlock_apply, mul_apply]
[GOAL]
case a.h
l : Type u_1
m✝ : Type u_2
n✝ : Type u_3
o : Type u_4
p✝ : Type u_5
q✝ : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝¹ : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝ : Fintype n
p : m → Prop
q : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // q a }
⊢ ∑ j : n, A (↑i) j * B j ↑k = ∑ x : { a // ⊤ a }, A ↑i ↑x * B ↑x ↑k
[PROOFSTEP]
rw [Finset.sum_subtype]
[GOAL]
case a.h.h
l : Type u_1
m✝ : Type u_2
n✝ : Type u_3
o : Type u_4
p✝ : Type u_5
q✝ : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝¹ : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝ : Fintype n
p : m → Prop
q : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // q a }
⊢ ∀ (x : n), x ∈ Finset.univ ↔ ⊤ x
[PROOFSTEP]
simp [Pi.top_apply, Prop.top_eq_true]
[GOAL]
l : Type u_1
m✝ : Type u_2
n✝ : Type u_3
o : Type u_4
p✝ : Type u_5
q✝ : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : CommRing R
m : Type u_14
n : Type u_15
k : Type u_16
inst✝¹ : Fintype n
p : m → Prop
q : n → Prop
inst✝ : DecidablePred q
r : k → Prop
A : Matrix m n R
B : Matrix n k R
⊢ toBlock (A * B) p r = toBlock A p q * toBlock B q r + (toBlock A p fun i => ¬q i) * toBlock B (fun i => ¬q i) r
[PROOFSTEP]
classical
ext i k
simp only [toBlock_apply, mul_apply, Pi.add_apply]
exact (Fintype.sum_subtype_add_sum_subtype q fun x => A (↑i) x * B x ↑k).symm
[GOAL]
l : Type u_1
m✝ : Type u_2
n✝ : Type u_3
o : Type u_4
p✝ : Type u_5
q✝ : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : CommRing R
m : Type u_14
n : Type u_15
k : Type u_16
inst✝¹ : Fintype n
p : m → Prop
q : n → Prop
inst✝ : DecidablePred q
r : k → Prop
A : Matrix m n R
B : Matrix n k R
⊢ toBlock (A * B) p r = toBlock A p q * toBlock B q r + (toBlock A p fun i => ¬q i) * toBlock B (fun i => ¬q i) r
[PROOFSTEP]
ext i k
[GOAL]
case a.h
l : Type u_1
m✝ : Type u_2
n✝ : Type u_3
o : Type u_4
p✝ : Type u_5
q✝ : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝¹ : Fintype n
p : m → Prop
q : n → Prop
inst✝ : DecidablePred q
r : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // r a }
⊢ toBlock (A * B) p r i k =
    (toBlock A p q * toBlock B q r + (toBlock A p fun i => ¬q i) * toBlock B (fun i => ¬q i) r) i k
[PROOFSTEP]
simp only [toBlock_apply, mul_apply, Pi.add_apply]
[GOAL]
case a.h
l : Type u_1
m✝ : Type u_2
n✝ : Type u_3
o : Type u_4
p✝ : Type u_5
q✝ : Type u_6
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
R : Type u_10
S : Type u_11
α : Type u_12
β : Type u_13
inst✝² : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝¹ : Fintype n
p : m → Prop
q : n → Prop
inst✝ : DecidablePred q
r : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // r a }
⊢ ∑ j : n, A (↑i) j * B j ↑k =
    (toBlock A p q * toBlock B q r + (toBlock A p fun i => ¬q i) * toBlock B (fun i => ¬q i) r) i k
[PROOFSTEP]
exact (Fintype.sum_subtype_add_sum_subtype q fun x => A (↑i) x * B x ↑k).symm