case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 2) (Fin 2) α
i j : Fin 2
⊢ A i j = ↑of ![![A 0 0, A 0 1], ![A 1 0, A 1 1]] i j
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 2) (Fin 2) α
⊢ A = ↑of ![![A 0 0, A 0 1], ![A 1 0, A 1 1]]
ext (i j)
no goals
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 2) (Fin 2) α
i j : Fin 2
⊢ A i j = ↑of ![![A 0 0, A 0 1], ![A 1 0, A 1 1]] i j
fin_cases i <;> fin_cases j <;> rfl