n : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
H :
  ∀ (k : ℕ),
    k ≤ r →
      (List.prod (List.drop k (listTransvecCol M)) ⬝ M) (inl i) (inr ()) = if k ≤ ↑i then 0 else M (inl i) (inr ())
⊢ (List.prod (listTransvecCol M) ⬝ M) (inl i) (inr ()) = 0

case H
n : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
⊢ ∀ (k : ℕ),
    k ≤ r →
      (List.prod (List.drop k (listTransvecCol M)) ⬝ M) (inl i) (inr ()) = if k ≤ ↑i then 0 else M (inl i) (inr ())
n : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
⊢ (List.prod (listTransvecCol M) ⬝ M) (inl i) (inr ()) = 0
suffices H :
  ∀ k : ℕ,
    k ≤ r →
      (((listTransvecCol M).drop k).prod ⬝ M) (inl i) (inr unit) =
        if k ≤ i then 0 else M (inl i) (inr unit)
case H
n : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk : k ≤ r
⊢ (List.prod (List.drop k (listTransvecCol M)) ⬝ M) (inl i) (inr ()) = if k ≤ ↑i then 0 else M (inl i) (inr ())
case H
n : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
⊢ ∀ (k : ℕ),
    k ≤ r →
      (List.prod (List.drop k (listTransvecCol M)) ⬝ M) (inl i) (inr ()) = if k ≤ ↑i then 0 else M (inl i) (inr ())
intro k hk
case H.refine'_1
n : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk : k ≤ r
⊢ ∀ (k_1 : ℕ),
    k_1 < r →
      k ≤ k_1 →
        ((List.prod (List.drop (k_1 + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
            if k_1 + 1 ≤ ↑i then 0 else M (inl i) (inr ())) →
          (List.prod (List.drop k_1 (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
            if k_1 ≤ ↑i then 0 else M (inl i) (inr ())

case H.refine'_2
n : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk : k ≤ r
⊢ (List.prod (List.drop r (listTransvecCol M)) ⬝ M) (inl i) (inr ()) = if r ≤ ↑i then 0 else M (inl i) (inr ())
case H
n : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk : k ≤ r
⊢ (List.prod (List.drop k (listTransvecCol M)) ⬝ M) (inl i) (inr ()) = if k ≤ ↑i then 0 else M (inl i) (inr ())
refine' Nat.decreasingInduction' _ hk _
no goals
n : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
H :
  ∀ (k : ℕ),
    k ≤ r →
      (List.prod (List.drop k (listTransvecCol M)) ⬝ M) (inl i) (inr ()) = if k ≤ ↑i then 0 else M (inl i) (inr ())
⊢ (List.prod (listTransvecCol M) ⬝ M) (inl i) (inr ()) = 0
simpa only [List.drop, _root_.zero_le, ite_true] using H 0 (zero_le _)
case H.refine'_1
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
⊢ (List.prod (List.drop n (listTransvecCol M)) ⬝ M) (inl i) (inr ()) = if n ≤ ↑i then 0 else M (inl i) (inr ())
case H.refine'_1
n : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk : k ≤ r
⊢ ∀ (k_1 : ℕ),
    k_1 < r →
      k ≤ k_1 →
        ((List.prod (List.drop (k_1 + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
            if k_1 + 1 ≤ ↑i then 0 else M (inl i) (inr ())) →
          (List.prod (List.drop k_1 (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
            if k_1 ≤ ↑i then 0 else M (inl i) (inr ())
intro n hn hk IH
case H.refine'_1
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
⊢ (List.prod (List.drop n (listTransvecCol M)) ⬝ M) (inl i) (inr ()) = if n ≤ ↑i then 0 else M (inl i) (inr ())
case H.refine'_1
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
⊢ (List.prod (List.drop n (listTransvecCol M)) ⬝ M) (inl i) (inr ()) = if n ≤ ↑i then 0 else M (inl i) (inr ())
have hn' : n < (listTransvecCol M).length := by simpa [listTransvecCol] using hn
case H.refine'_1
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
⊢ (List.prod (List.drop n (listTransvecCol M)) ⬝ M) (inl i) (inr ()) = if n ≤ ↑i then 0 else M (inl i) (inr ())
case H.refine'_1
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
⊢ (List.prod (List.drop n (listTransvecCol M)) ⬝ M) (inl i) (inr ()) = if n ≤ ↑i then 0 else M (inl i) (inr ())
let n' : Fin r := ⟨n, hn⟩
case H.refine'_1
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
⊢ (List.prod
          (List.get (listTransvecCol M) { val := n, isLt := hn' } ::
            List.drop (↑{ val := n, isLt := hn' } + 1) (listTransvecCol M)) ⬝
        M)
      (inl i) (inr ()) =
    if n ≤ ↑i then 0 else M (inl i) (inr ())
case H.refine'_1
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
⊢ (List.prod (List.drop n (listTransvecCol M)) ⬝ M) (inl i) (inr ()) = if n ≤ ↑i then 0 else M (inl i) (inr ())
rw [← @List.cons_get_drop_succ _ _ ⟨n, hn'⟩]
case H.refine'_1
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
⊢ (List.prod
          (List.get (listTransvecCol M) { val := n, isLt := hn' } ::
            List.drop (↑{ val := n, isLt := hn' } + 1) (listTransvecCol M)) ⬝
        M)
      (inl i) (inr ()) =
    if n ≤ ↑i then 0 else M (inl i) (inr ())
case H.refine'_1
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
⊢ (List.prod
          (List.get (listTransvecCol M) { val := n, isLt := hn' } ::
            List.drop (↑{ val := n, isLt := hn' } + 1) (listTransvecCol M)) ⬝
        M)
      (inl i) (inr ()) =
    if n ≤ ↑i then 0 else M (inl i) (inr ())
have A :
  (listTransvecCol M).get ⟨n, hn'⟩ =
    transvection (inl n') (inr unit) (-M (inl n') (inr unit) / M (inr unit) (inr unit)) :=
  by simp [listTransvecCol]
case H.refine'_1
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
⊢ (transvection (inl { val := n, isLt := hn }) (inr ())
          (-M (inl { val := n, isLt := hn }) (inr ()) / M (inr ()) (inr ())) ⬝
        (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M))
      (inl i) (inr ()) =
    if n ≤ ↑i then 0 else M (inl i) (inr ())
case H.refine'_1
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
⊢ (List.prod
          (List.get (listTransvecCol M) { val := n, isLt := hn' } ::
            List.drop (↑{ val := n, isLt := hn' } + 1) (listTransvecCol M)) ⬝
        M)
      (inl i) (inr ()) =
    if n ≤ ↑i then 0 else M (inl i) (inr ())
simp only [Matrix.mul_assoc, A, Matrix.mul_eq_mul, List.prod_cons]
case pos
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : n' = i
⊢ (transvection (inl { val := n, isLt := hn }) (inr ())
          (-M (inl { val := n, isLt := hn }) (inr ()) / M (inr ()) (inr ())) ⬝
        (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M))
      (inl i) (inr ()) =
    if n ≤ ↑i then 0 else M (inl i) (inr ())

case neg
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
⊢ (transvection (inl { val := n, isLt := hn }) (inr ())
          (-M (inl { val := n, isLt := hn }) (inr ()) / M (inr ()) (inr ())) ⬝
        (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M))
      (inl i) (inr ()) =
    if n ≤ ↑i then 0 else M (inl i) (inr ())
case H.refine'_1
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
⊢ (transvection (inl { val := n, isLt := hn }) (inr ())
          (-M (inl { val := n, isLt := hn }) (inr ()) / M (inr ()) (inr ())) ⬝
        (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M))
      (inl i) (inr ()) =
    if n ≤ ↑i then 0 else M (inl i) (inr ())
by_cases h : n' = i
no goals
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
⊢ n < List.length (listTransvecCol M)
simpa [listTransvecCol] using hn
no goals
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
⊢ List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
simp [listTransvecCol]
case pos
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : n' = i
hni : n = ↑i
⊢ (transvection (inl { val := n, isLt := hn }) (inr ())
          (-M (inl { val := n, isLt := hn }) (inr ()) / M (inr ()) (inr ())) ⬝
        (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M))
      (inl i) (inr ()) =
    if n ≤ ↑i then 0 else M (inl i) (inr ())
case pos
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : n' = i
⊢ (transvection (inl { val := n, isLt := hn }) (inr ())
          (-M (inl { val := n, isLt := hn }) (inr ()) / M (inr ()) (inr ())) ⬝
        (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M))
      (inl i) (inr ()) =
    if n ≤ ↑i then 0 else M (inl i) (inr ())
have hni : n = i := by
  cases i
  simp only [Fin.mk_eq_mk] at h
  simp [h]
case pos
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : n' = i
hni : n = ↑i
⊢ (if False then 0 else M (inl i) (inr ())) + -M (inl i) (inr ()) / M (inr ()) (inr ()) * M (inr ()) (inr ()) =
    if n ≤ n then 0 else M (inl i) (inr ())
case pos
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : n' = i
hni : n = ↑i
⊢ (transvection (inl { val := n, isLt := hn }) (inr ())
          (-M (inl { val := n, isLt := hn }) (inr ()) / M (inr ()) (inr ())) ⬝
        (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M))
      (inl i) (inr ()) =
    if n ≤ ↑i then 0 else M (inl i) (inr ())
simp only [h, transvection_mul_apply_same, IH, ← hni, add_le_iff_nonpos_right,
    listTransvecCol_mul_last_row_drop _ _ hn]
no goals
case pos
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : n' = i
hni : n = ↑i
⊢ (if False then 0 else M (inl i) (inr ())) + -M (inl i) (inr ()) / M (inr ()) (inr ()) * M (inr ()) (inr ()) =
    if n ≤ n then 0 else M (inl i) (inr ())
field_simp [hM]
case mk
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
val✝ : ℕ
isLt✝ : val✝ < r
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl { val := val✝, isLt := isLt✝ }) (inr ()) =
    if n + 1 ≤ ↑{ val := val✝, isLt := isLt✝ } then 0 else M (inl { val := val✝, isLt := isLt✝ }) (inr ())
h : n' = { val := val✝, isLt := isLt✝ }
⊢ n = ↑{ val := val✝, isLt := isLt✝ }
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : n' = i
⊢ n = ↑i
cases i
case mk
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
val✝ : ℕ
isLt✝ : val✝ < r
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl { val := val✝, isLt := isLt✝ }) (inr ()) =
    if n + 1 ≤ ↑{ val := val✝, isLt := isLt✝ } then 0 else M (inl { val := val✝, isLt := isLt✝ }) (inr ())
h : n = val✝
⊢ n = ↑{ val := val✝, isLt := isLt✝ }
case mk
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
val✝ : ℕ
isLt✝ : val✝ < r
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl { val := val✝, isLt := isLt✝ }) (inr ()) =
    if n + 1 ≤ ↑{ val := val✝, isLt := isLt✝ } then 0 else M (inl { val := val✝, isLt := isLt✝ }) (inr ())
h : n' = { val := val✝, isLt := isLt✝ }
⊢ n = ↑{ val := val✝, isLt := isLt✝ }
simp only [Fin.mk_eq_mk] at h
no goals
case mk
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
val✝ : ℕ
isLt✝ : val✝ < r
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl { val := val✝, isLt := isLt✝ }) (inr ()) =
    if n + 1 ≤ ↑{ val := val✝, isLt := isLt✝ } then 0 else M (inl { val := val✝, isLt := isLt✝ }) (inr ())
h : n = val✝
⊢ n = ↑{ val := val✝, isLt := isLt✝ }
simp [h]
case neg
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ ↑i
⊢ (transvection (inl { val := n, isLt := hn }) (inr ())
          (-M (inl { val := n, isLt := hn }) (inr ()) / M (inr ()) (inr ())) ⬝
        (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M))
      (inl i) (inr ()) =
    if n ≤ ↑i then 0 else M (inl i) (inr ())
case neg
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
⊢ (transvection (inl { val := n, isLt := hn }) (inr ())
          (-M (inl { val := n, isLt := hn }) (inr ()) / M (inr ()) (inr ())) ⬝
        (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M))
      (inl i) (inr ()) =
    if n ≤ ↑i then 0 else M (inl i) (inr ())
have hni : n ≠ i := by
  rintro rfl
  cases i
  simp at h
case neg
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ ↑i
⊢ (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) = if n ≤ ↑i then 0 else M (inl i) (inr ())
case neg
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ ↑i
⊢ (transvection (inl { val := n, isLt := hn }) (inr ())
          (-M (inl { val := n, isLt := hn }) (inr ()) / M (inr ()) (inr ())) ⬝
        (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M))
      (inl i) (inr ()) =
    if n ≤ ↑i then 0 else M (inl i) (inr ())
simp only [ne_eq, inl.injEq, Ne.symm h, not_false_eq_true, transvection_mul_apply_of_ne]
case neg
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ ↑i
⊢ (if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())) = if n ≤ ↑i then 0 else M (inl i) (inr ())
case neg
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ ↑i
⊢ (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) = if n ≤ ↑i then 0 else M (inl i) (inr ())
rw [IH]
case neg.inl
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ ↑i
hi : n + 1 ≤ ↑i
⊢ (if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())) = if n ≤ ↑i then 0 else M (inl i) (inr ())

case neg.inr
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ ↑i
hi : ↑i < n + 1
⊢ (if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())) = if n ≤ ↑i then 0 else M (inl i) (inr ())
case neg
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ ↑i
⊢ (if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())) = if n ≤ ↑i then 0 else M (inl i) (inr ())
rcases le_or_lt (n + 1) i with (hi | hi)
n : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
hn : ↑i < r
hk : k ≤ ↑i
IH :
  (List.prod (List.drop (↑i + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if ↑i + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : ↑i < List.length (listTransvecCol M)
n' : Fin r := { val := ↑i, isLt := hn }
A :
  List.get (listTransvecCol M) { val := ↑i, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
⊢ False
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
⊢ n ≠ ↑i
rintro rfl
case mk
n : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
k : ℕ
hk✝ : k ≤ r
val✝ : ℕ
isLt✝ : val✝ < r
hn : ↑{ val := val✝, isLt := isLt✝ } < r
hk : k ≤ ↑{ val := val✝, isLt := isLt✝ }
IH :
  (List.prod (List.drop (↑{ val := val✝, isLt := isLt✝ } + 1) (listTransvecCol M)) ⬝ M)
      (inl { val := val✝, isLt := isLt✝ }) (inr ()) =
    if ↑{ val := val✝, isLt := isLt✝ } + 1 ≤ ↑{ val := val✝, isLt := isLt✝ } then 0
    else M (inl { val := val✝, isLt := isLt✝ }) (inr ())
hn' : ↑{ val := val✝, isLt := isLt✝ } < List.length (listTransvecCol M)
n' : Fin r := { val := ↑{ val := val✝, isLt := isLt✝ }, isLt := hn }
A :
  List.get (listTransvecCol M) { val := ↑{ val := val✝, isLt := isLt✝ }, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = { val := val✝, isLt := isLt✝ }
⊢ False
n : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
hn : ↑i < r
hk : k ≤ ↑i
IH :
  (List.prod (List.drop (↑i + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if ↑i + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : ↑i < List.length (listTransvecCol M)
n' : Fin r := { val := ↑i, isLt := hn }
A :
  List.get (listTransvecCol M) { val := ↑i, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
⊢ False
cases i
no goals
case mk
n : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
k : ℕ
hk✝ : k ≤ r
val✝ : ℕ
isLt✝ : val✝ < r
hn : ↑{ val := val✝, isLt := isLt✝ } < r
hk : k ≤ ↑{ val := val✝, isLt := isLt✝ }
IH :
  (List.prod (List.drop (↑{ val := val✝, isLt := isLt✝ } + 1) (listTransvecCol M)) ⬝ M)
      (inl { val := val✝, isLt := isLt✝ }) (inr ()) =
    if ↑{ val := val✝, isLt := isLt✝ } + 1 ≤ ↑{ val := val✝, isLt := isLt✝ } then 0
    else M (inl { val := val✝, isLt := isLt✝ }) (inr ())
hn' : ↑{ val := val✝, isLt := isLt✝ } < List.length (listTransvecCol M)
n' : Fin r := { val := ↑{ val := val✝, isLt := isLt✝ }, isLt := hn }
A :
  List.get (listTransvecCol M) { val := ↑{ val := val✝, isLt := isLt✝ }, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = { val := val✝, isLt := isLt✝ }
⊢ False
simp at h
no goals
case neg.inl
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ ↑i
hi : n + 1 ≤ ↑i
⊢ (if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())) = if n ≤ ↑i then 0 else M (inl i) (inr ())
simp only [hi, n.le_succ.trans hi, if_true]
case neg.inr.hnc
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ ↑i
hi : ↑i < n + 1
⊢ ¬n ≤ ↑i

case neg.inr.hnc
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ ↑i
hi : ↑i < n + 1
⊢ ¬n + 1 ≤ ↑i
case neg.inr
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ ↑i
hi : ↑i < n + 1
⊢ (if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())) = if n ≤ ↑i then 0 else M (inl i) (inr ())
rw [if_neg, if_neg]
no goals
case neg.inr.hnc
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ ↑i
hi : ↑i < n + 1
⊢ ¬n ≤ ↑i
simpa only [hni.symm, not_le, or_false_iff] using Nat.lt_succ_iff_lt_or_eq.1 hi
no goals
case neg.inr.hnc
n✝ : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk✝ : k ≤ r
n : ℕ
hn : n < r
hk : k ≤ n
IH :
  (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inl i) (inr ()) =
    if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < List.length (listTransvecCol M)
n' : Fin r := { val := n, isLt := hn }
A :
  List.get (listTransvecCol M) { val := n, isLt := hn' } =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ ↑i
hi : ↑i < n + 1
⊢ ¬n + 1 ≤ ↑i
simpa only [not_le] using hi
case H.refine'_2
n : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk : k ≤ r
⊢ M (inl i) (inr ()) = if r ≤ ↑i then 0 else M (inl i) (inr ())
case H.refine'_2
n : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk : k ≤ r
⊢ (List.prod (List.drop r (listTransvecCol M)) ⬝ M) (inl i) (inr ()) = if r ≤ ↑i then 0 else M (inl i) (inr ())
simp only [listTransvecCol, List.length_ofFn, le_refl, List.drop_eq_nil_of_le, List.prod_nil,
  Matrix.one_mul]
case H.refine'_2.hnc
n : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk : k ≤ r
⊢ ¬r ≤ ↑i
case H.refine'_2
n : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk : k ≤ r
⊢ M (inl i) (inr ()) = if r ≤ ↑i then 0 else M (inl i) (inr ())
rw [if_neg]
no goals
case H.refine'_2.hnc
n : Type ?u.156728
p : Type ?u.156731
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk : k ≤ r
⊢ ¬r ≤ ↑i
simpa only [not_le] using i.2