case zero
n : Type ?u.175750
p : Type ?u.175753
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k : ℕ
hk✝ : k ≤ r
hk : Nat.zero ≤ r
⊢ (M ⬝ List.prod (List.take Nat.zero (listTransvecRow M))) i (inr ()) = M i (inr ())

case succ
n : Type ?u.175750
p : Type ?u.175753
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k✝ : ℕ
hk✝ : k✝ ≤ r
k : ℕ
IH : k ≤ r → (M ⬝ List.prod (List.take k (listTransvecRow M))) i (inr ()) = M i (inr ())
hk : Nat.succ k ≤ r
⊢ (M ⬝ List.prod (List.take (Nat.succ k) (listTransvecRow M))) i (inr ()) = M i (inr ())
n : Type ?u.175750
p : Type ?u.175753
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k : ℕ
hk : k ≤ r
⊢ (M ⬝ List.prod (List.take k (listTransvecRow M))) i (inr ()) = M i (inr ())
induction' k with k IH
no goals
case zero
n : Type ?u.175750
p : Type ?u.175753
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k : ℕ
hk✝ : k ≤ r
hk : Nat.zero ≤ r
⊢ (M ⬝ List.prod (List.take Nat.zero (listTransvecRow M))) i (inr ()) = M i (inr ())
simp only [Matrix.mul_one, List.take_zero, List.prod_nil, List.take, Matrix.mul_one]
case succ
n : Type ?u.175750
p : Type ?u.175753
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k✝ : ℕ
hk✝ : k✝ ≤ r
k : ℕ
IH : k ≤ r → (M ⬝ List.prod (List.take k (listTransvecRow M))) i (inr ()) = M i (inr ())
hk : Nat.succ k ≤ r
hkr : k < r
⊢ (M ⬝ List.prod (List.take (Nat.succ k) (listTransvecRow M))) i (inr ()) = M i (inr ())
case succ
n : Type ?u.175750
p : Type ?u.175753
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k✝ : ℕ
hk✝ : k✝ ≤ r
k : ℕ
IH : k ≤ r → (M ⬝ List.prod (List.take k (listTransvecRow M))) i (inr ()) = M i (inr ())
hk : Nat.succ k ≤ r
⊢ (M ⬝ List.prod (List.take (Nat.succ k) (listTransvecRow M))) i (inr ()) = M i (inr ())
have hkr : k < r := hk
case succ
n : Type ?u.175750
p : Type ?u.175753
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k✝ : ℕ
hk✝ : k✝ ≤ r
k : ℕ
IH : k ≤ r → (M ⬝ List.prod (List.take k (listTransvecRow M))) i (inr ()) = M i (inr ())
hk : Nat.succ k ≤ r
hkr : k < r
k' : Fin r := { val := k, isLt := hkr }
⊢ (M ⬝ List.prod (List.take (Nat.succ k) (listTransvecRow M))) i (inr ()) = M i (inr ())
case succ
n : Type ?u.175750
p : Type ?u.175753
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k✝ : ℕ
hk✝ : k✝ ≤ r
k : ℕ
IH : k ≤ r → (M ⬝ List.prod (List.take k (listTransvecRow M))) i (inr ()) = M i (inr ())
hk : Nat.succ k ≤ r
hkr : k < r
⊢ (M ⬝ List.prod (List.take (Nat.succ k) (listTransvecRow M))) i (inr ()) = M i (inr ())
let k' : Fin r := ⟨k, hkr⟩
case succ
n : Type ?u.175750
p : Type ?u.175753
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k✝ : ℕ
hk✝ : k✝ ≤ r
k : ℕ
IH : k ≤ r → (M ⬝ List.prod (List.take k (listTransvecRow M))) i (inr ()) = M i (inr ())
hk : Nat.succ k ≤ r
hkr : k < r
k' : Fin r := { val := k, isLt := hkr }
this :
  List.get? (listTransvecRow M) k = some (transvection (inr ()) (inl k') (-M (inr ()) (inl k') / M (inr ()) (inr ())))
⊢ (M ⬝ List.prod (List.take (Nat.succ k) (listTransvecRow M))) i (inr ()) = M i (inr ())
case succ
n : Type ?u.175750
p : Type ?u.175753
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k✝ : ℕ
hk✝ : k✝ ≤ r
k : ℕ
IH : k ≤ r → (M ⬝ List.prod (List.take k (listTransvecRow M))) i (inr ()) = M i (inr ())
hk : Nat.succ k ≤ r
hkr : k < r
k' : Fin r := { val := k, isLt := hkr }
⊢ (M ⬝ List.prod (List.take (Nat.succ k) (listTransvecRow M))) i (inr ()) = M i (inr ())
have :
  (listTransvecRow M).get? k =
    ↑(transvection (inr Unit.unit) (inl k')
        (-M (inr Unit.unit) (inl k') / M (inr Unit.unit) (inr Unit.unit))) := by
  simp only [listTransvecRow, List.ofFnNthVal, hkr, dif_pos, List.get?_ofFn]
case succ
n : Type ?u.175750
p : Type ?u.175753
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k✝ : ℕ
hk✝ : k✝ ≤ r
k : ℕ
IH : k ≤ r → (M ⬝ List.prod (List.take k (listTransvecRow M))) i (inr ()) = M i (inr ())
hk : Nat.succ k ≤ r
hkr : k < r
k' : Fin r := { val := k, isLt := hkr }
this :
  List.get? (listTransvecRow M) k = some (transvection (inr ()) (inl k') (-M (inr ()) (inl k') / M (inr ()) (inr ())))
⊢ (M ⬝ List.prod (List.take k (listTransvecRow M)) ⬝
        transvection (inr ()) (inl { val := k, isLt := hkr })
          (-M (inr ()) (inl { val := k, isLt := hkr }) / M (inr ()) (inr ())))
      i (inr ()) =
    M i (inr ())
case succ
n : Type ?u.175750
p : Type ?u.175753
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k✝ : ℕ
hk✝ : k✝ ≤ r
k : ℕ
IH : k ≤ r → (M ⬝ List.prod (List.take k (listTransvecRow M))) i (inr ()) = M i (inr ())
hk : Nat.succ k ≤ r
hkr : k < r
k' : Fin r := { val := k, isLt := hkr }
this :
  List.get? (listTransvecRow M) k = some (transvection (inr ()) (inl k') (-M (inr ()) (inl k') / M (inr ()) (inr ())))
⊢ (M ⬝ List.prod (List.take (Nat.succ k) (listTransvecRow M))) i (inr ()) = M i (inr ())
simp only [List.take_succ, ← Matrix.mul_assoc, this, List.prod_append, Matrix.mul_one,
  Matrix.mul_eq_mul, List.prod_cons, List.prod_nil, Option.to_list_some]
case succ.hb
n : Type ?u.175750
p : Type ?u.175753
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k✝ : ℕ
hk✝ : k✝ ≤ r
k : ℕ
IH : k ≤ r → (M ⬝ List.prod (List.take k (listTransvecRow M))) i (inr ()) = M i (inr ())
hk : Nat.succ k ≤ r
hkr : k < r
k' : Fin r := { val := k, isLt := hkr }
this :
  List.get? (listTransvecRow M) k = some (transvection (inr ()) (inl k') (-M (inr ()) (inl k') / M (inr ()) (inr ())))
⊢ inr () ≠ inl { val := k, isLt := hkr }
case succ
n : Type ?u.175750
p : Type ?u.175753
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k✝ : ℕ
hk✝ : k✝ ≤ r
k : ℕ
IH : k ≤ r → (M ⬝ List.prod (List.take k (listTransvecRow M))) i (inr ()) = M i (inr ())
hk : Nat.succ k ≤ r
hkr : k < r
k' : Fin r := { val := k, isLt := hkr }
this :
  List.get? (listTransvecRow M) k = some (transvection (inr ()) (inl k') (-M (inr ()) (inl k') / M (inr ()) (inr ())))
⊢ (M ⬝ List.prod (List.take k (listTransvecRow M)) ⬝
        transvection (inr ()) (inl { val := k, isLt := hkr })
          (-M (inr ()) (inl { val := k, isLt := hkr }) / M (inr ()) (inr ())))
      i (inr ()) =
    M i (inr ())
rw [mul_transvection_apply_of_ne, IH hkr.le]
no goals
case succ.hb
n : Type ?u.175750
p : Type ?u.175753
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k✝ : ℕ
hk✝ : k✝ ≤ r
k : ℕ
IH : k ≤ r → (M ⬝ List.prod (List.take k (listTransvecRow M))) i (inr ()) = M i (inr ())
hk : Nat.succ k ≤ r
hkr : k < r
k' : Fin r := { val := k, isLt := hkr }
this :
  List.get? (listTransvecRow M) k = some (transvection (inr ()) (inl k') (-M (inr ()) (inl k') / M (inr ()) (inr ())))
⊢ inr () ≠ inl { val := k, isLt := hkr }
simp only [Ne.def, not_false_iff]
no goals
n : Type ?u.175750
p : Type ?u.175753
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k✝ : ℕ
hk✝ : k✝ ≤ r
k : ℕ
IH : k ≤ r → (M ⬝ List.prod (List.take k (listTransvecRow M))) i (inr ()) = M i (inr ())
hk : Nat.succ k ≤ r
hkr : k < r
k' : Fin r := { val := k, isLt := hkr }
⊢ List.get? (listTransvecRow M) k = some (transvection (inr ()) (inl k') (-M (inr ()) (inl k') / M (inr ()) (inr ())))
simp only [listTransvecRow, List.ofFnNthVal, hkr, dif_pos, List.get?_ofFn]