case a.h
l : Type ?u.266837
m✝ : Type ?u.266840
n✝ : Type ?u.266843
o : Type ?u.266846
p✝ : Type ?u.266849
q✝ : Type ?u.266852
m' : o → Type ?u.266857
n' : o → Type ?u.266862
p' : o → Type ?u.266867
R : Type u_4
S : Type ?u.266873
α : Type ?u.266876
β : Type ?u.266879
inst✝¹ : CommRing R
m : Type u_1
n : Type u_2
k✝ : Type u_3
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
l : Type ?u.266837
m✝ : Type ?u.266840
n✝ : Type ?u.266843
o : Type ?u.266846
p✝ : Type ?u.266849
q✝ : Type ?u.266852
m' : o → Type ?u.266857
n' : o → Type ?u.266862
p' : o → Type ?u.266867
R : Type u_4
S : Type ?u.266873
α : Type ?u.266876
β : Type ?u.266879
inst✝¹ : CommRing R
m : Type u_1
n : Type u_2
k : Type u_3
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
ext (i k)
case a.h
l : Type ?u.266837
m✝ : Type ?u.266840
n✝ : Type ?u.266843
o : Type ?u.266846
p✝ : Type ?u.266849
q✝ : Type ?u.266852
m' : o → Type ?u.266857
n' : o → Type ?u.266862
p' : o → Type ?u.266867
R : Type u_4
S : Type ?u.266873
α : Type ?u.266876
β : Type ?u.266879
inst✝¹ : CommRing R
m : Type u_1
n : Type u_2
k✝ : Type u_3
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
case a.h
l : Type ?u.266837
m✝ : Type ?u.266840
n✝ : Type ?u.266843
o : Type ?u.266846
p✝ : Type ?u.266849
q✝ : Type ?u.266852
m' : o → Type ?u.266857
n' : o → Type ?u.266862
p' : o → Type ?u.266867
R : Type u_4
S : Type ?u.266873
α : Type ?u.266876
β : Type ?u.266879
inst✝¹ : CommRing R
m : Type u_1
n : Type u_2
k✝ : Type u_3
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
simp only [toBlock_apply, mul_apply]
case a.h.h
l : Type ?u.266837
m✝ : Type ?u.266840
n✝ : Type ?u.266843
o : Type ?u.266846
p✝ : Type ?u.266849
q✝ : Type ?u.266852
m' : o → Type ?u.266857
n' : o → Type ?u.266862
p' : o → Type ?u.266867
R : Type u_4
S : Type ?u.266873
α : Type ?u.266876
β : Type ?u.266879
inst✝¹ : CommRing R
m : Type u_1
n : Type u_2
k✝ : Type u_3
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
case a.h
l : Type ?u.266837
m✝ : Type ?u.266840
n✝ : Type ?u.266843
o : Type ?u.266846
p✝ : Type ?u.266849
q✝ : Type ?u.266852
m' : o → Type ?u.266857
n' : o → Type ?u.266862
p' : o → Type ?u.266867
R : Type u_4
S : Type ?u.266873
α : Type ?u.266876
β : Type ?u.266879
inst✝¹ : CommRing R
m : Type u_1
n : Type u_2
k✝ : Type u_3
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
rw [Finset.sum_subtype]
no goals
case a.h.h
l : Type ?u.266837
m✝ : Type ?u.266840
n✝ : Type ?u.266843
o : Type ?u.266846
p✝ : Type ?u.266849
q✝ : Type ?u.266852
m' : o → Type ?u.266857
n' : o → Type ?u.266862
p' : o → Type ?u.266867
R : Type u_4
S : Type ?u.266873
α : Type ?u.266876
β : Type ?u.266879
inst✝¹ : CommRing R
m : Type u_1
n : Type u_2
k✝ : Type u_3
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
simp [Pi.top_apply, Prop.top_eq_true]