case refine_4
l : Type ?u.237230
m : Type ?u.237233
n : Type ?u.237236
o : Type ?u.237239
m' : o → Type ?u.237244
n' : o → Type ?u.237249
R✝ : Type ?u.237252
S : Type ?u.237255
α : Type v
β : Type w
γ : Type ?u.237262
R : Type u_1
inst✝ : CommRing R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (A ⬝ B) 1 1 = A 1 0 * B 0 1 + A 1 1 * B 1 1
case refine_4
l : Type ?u.237230
m : Type ?u.237233
n : Type ?u.237236
o : Type ?u.237239
m' : o → Type ?u.237244
n' : o → Type ?u.237249
R✝ : Type ?u.237252
S : Type ?u.237255
α : Type v
β : Type w
γ : Type ?u.237262
R : Type u_1
inst✝ : CommRing R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (A * B) 1 1 = A 1 0 * B 0 1 + A 1 1 * B 1 1
simp only [Matrix.mul_eq_mul]
case refine_4
l : Type ?u.237230
m : Type ?u.237233
n : Type ?u.237236
o : Type ?u.237239
m' : o → Type ?u.237244
n' : o → Type ?u.237249
R✝ : Type ?u.237252
S : Type ?u.237255
α : Type v
β : Type w
γ : Type ?u.237262
R : Type u_1
inst✝ : CommRing R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (((∑ x in Finset.range 0, if h : x < 2 then A 1 { val := x, isLt := h } * B { val := x, isLt := h } 1 else 0) +
        if h : 0 < 2 then A 1 { val := 0, isLt := h } * B { val := 0, isLt := h } 1 else 0) +
      if h : 1 < 2 then A 1 { val := 1, isLt := h } * B { val := 1, isLt := h } 1 else 0) =
    A 1 0 * B 0 1 + A 1 1 * B 1 1
case refine_4
l : Type ?u.237230
m : Type ?u.237233
n : Type ?u.237236
o : Type ?u.237239
m' : o → Type ?u.237244
n' : o → Type ?u.237249
R✝ : Type ?u.237252
S : Type ?u.237255
α : Type v
β : Type w
γ : Type ?u.237262
R : Type u_1
inst✝ : CommRing R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (A ⬝ B) 1 1 = A 1 0 * B 0 1 + A 1 1 * B 1 1
rw [Matrix.mul_apply, Finset.sum_fin_eq_sum_range, Finset.sum_range_succ, Finset.sum_range_succ]
no goals
case refine_4
l : Type ?u.237230
m : Type ?u.237233
n : Type ?u.237236
o : Type ?u.237239
m' : o → Type ?u.237244
n' : o → Type ?u.237249
R✝ : Type ?u.237252
S : Type ?u.237255
α : Type v
β : Type w
γ : Type ?u.237262
R : Type u_1
inst✝ : CommRing R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (((∑ x in Finset.range 0, if h : x < 2 then A 1 { val := x, isLt := h } * B { val := x, isLt := h } 1 else 0) +
        if h : 0 < 2 then A 1 { val := 0, isLt := h } * B { val := 0, isLt := h } 1 else 0) +
      if h : 1 < 2 then A 1 { val := 1, isLt := h } * B { val := 1, isLt := h } 1 else 0) =
    A 1 0 * B 0 1 + A 1 1 * B 1 1
simp