case a.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
i j : Fin 2
⊢ adjugate A i j = ↑of ![![A 1 1, -A 0 1], ![-A 1 0, A 0 0]] i j
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
⊢ adjugate A = ↑of ![![A 1 1, -A 0 1], ![-A 1 0, A 0 0]]
ext (i j)
case a.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
i j : Fin 2
⊢ updateRow A j (Pi.single i 1) 0 0 * updateRow A j (Pi.single i 1) 1 1 -
      updateRow A j (Pi.single i 1) 0 1 * updateRow A j (Pi.single i 1) 1 0 =
    ↑of ![![A 1 1, -A 0 1], ![-A 1 0, A 0 0]] i j
case a.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
i j : Fin 2
⊢ adjugate A i j = ↑of ![![A 1 1, -A 0 1], ![-A 1 0, A 0 0]] i j
rw [adjugate_apply, det_fin_two]
no goals
case a.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
i j : Fin 2
⊢ updateRow A j (Pi.single i 1) 0 0 * updateRow A j (Pi.single i 1) 1 1 -
      updateRow A j (Pi.single i 1) 0 1 * updateRow A j (Pi.single i 1) 1 0 =
    ↑of ![![A 1 1, -A 0 1], ![-A 1 0, A 0 0]] i j
fin_cases i <;> fin_cases j <;>
  simp [one_mul, Fin.one_eq_zero_iff, Pi.single_eq_same, MulZeroClass.mul_zero, sub_zero,
    Pi.single_eq_of_ne, Ne.def, not_false_iff, updateRow_self, updateRow_ne, cons_val_zero,
    of_apply, Nat.succ_succ_ne_one, Pi.single_eq_of_ne, updateRow_self, Pi.single_eq_of_ne,
    Ne.def, Fin.zero_eq_one_iff, Nat.succ_succ_ne_one, not_false_iff, updateRow_ne,
    Fin.one_eq_zero_iff, MulZeroClass.zero_mul, Pi.single_eq_same, one_mul, zero_sub, of_apply,
    cons_val', cons_val_fin_one, cons_val_one, head_fin_const, neg_inj, eq_self_iff_true,
    cons_val_zero, head_cons, mul_one]