case refine'_1
n : Type ?u.140137
p : Type ?u.140140
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_1 : ℕ),
    k_1 < r →
      k ≤ k_1 →
        (List.prod (List.drop (k_1 + 1) (listTransvecCol M)) ⬝ M) (inr ()) i = M (inr ()) i →
          (List.prod (List.drop k_1 (listTransvecCol M)) ⬝ M) (inr ()) i = M (inr ()) i

case refine'_2
n : Type ?u.140137
p : Type ?u.140140
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
⊢ (List.prod (List.drop r (listTransvecCol M)) ⬝ M) (inr ()) i = M (inr ()) i
n : Type ?u.140137
p : Type ?u.140140
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
⊢ (List.prod (List.drop k (listTransvecCol M)) ⬝ M) (inr ()) i = M (inr ()) i
refine' Nat.decreasingInduction' _ hk _
case refine'_1
n✝ : Type ?u.140137
p : Type ?u.140140
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
n : ℕ
hn : n < r
a✝ : k ≤ n
IH : (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inr ()) i = M (inr ()) i
⊢ (List.prod (List.drop n (listTransvecCol M)) ⬝ M) (inr ()) i = M (inr ()) i
case refine'_1
n : Type ?u.140137
p : Type ?u.140140
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_1 : ℕ),
    k_1 < r →
      k ≤ k_1 →
        (List.prod (List.drop (k_1 + 1) (listTransvecCol M)) ⬝ M) (inr ()) i = M (inr ()) i →
          (List.prod (List.drop k_1 (listTransvecCol M)) ⬝ M) (inr ()) i = M (inr ()) i
intro n hn _ IH
case refine'_1
n✝ : Type ?u.140137
p : Type ?u.140140
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
n : ℕ
hn : n < r
a✝ : k ≤ n
IH : (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inr ()) i = M (inr ()) i
hn' : n < List.length (listTransvecCol M)
⊢ (List.prod (List.drop n (listTransvecCol M)) ⬝ M) (inr ()) i = M (inr ()) i
case refine'_1
n✝ : Type ?u.140137
p : Type ?u.140140
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
n : ℕ
hn : n < r
a✝ : k ≤ n
IH : (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inr ()) i = M (inr ()) i
⊢ (List.prod (List.drop n (listTransvecCol M)) ⬝ M) (inr ()) i = M (inr ()) i
have hn' : n < (listTransvecCol M).length := by simpa [listTransvecCol] using hn
case refine'_1
n✝ : Type ?u.140137
p : Type ?u.140140
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
n : ℕ
hn : n < r
a✝ : k ≤ n
IH : (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inr ()) i = M (inr ()) i
hn' : n < List.length (listTransvecCol M)
⊢ (List.prod
          (List.get (listTransvecCol M) { val := n, isLt := hn' } ::
            List.drop (↑{ val := n, isLt := hn' } + 1) (listTransvecCol M)) ⬝
        M)
      (inr ()) i =
    M (inr ()) i
case refine'_1
n✝ : Type ?u.140137
p : Type ?u.140140
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
n : ℕ
hn : n < r
a✝ : k ≤ n
IH : (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inr ()) i = M (inr ()) i
hn' : n < List.length (listTransvecCol M)
⊢ (List.prod (List.drop n (listTransvecCol M)) ⬝ M) (inr ()) i = M (inr ()) i
rw [← @List.cons_get_drop_succ _ _ ⟨n, hn'⟩]
no goals
case refine'_1
n✝ : Type ?u.140137
p : Type ?u.140140
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
n : ℕ
hn : n < r
a✝ : k ≤ n
IH : (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inr ()) i = M (inr ()) i
hn' : n < List.length (listTransvecCol M)
⊢ (List.prod
          (List.get (listTransvecCol M) { val := n, isLt := hn' } ::
            List.drop (↑{ val := n, isLt := hn' } + 1) (listTransvecCol M)) ⬝
        M)
      (inr ()) i =
    M (inr ()) i
simpa [listTransvecCol, Matrix.mul_assoc]
no goals
n✝ : Type ?u.140137
p : Type ?u.140140
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
n : ℕ
hn : n < r
a✝ : k ≤ n
IH : (List.prod (List.drop (n + 1) (listTransvecCol M)) ⬝ M) (inr ()) i = M (inr ()) i
⊢ n < List.length (listTransvecCol M)
simpa [listTransvecCol] using hn
no goals
case refine'_2
n : Type ?u.140137
p : Type ?u.140140
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
⊢ (List.prod (List.drop r (listTransvecCol M)) ⬝ M) (inr ()) i = M (inr ()) i
simp only [listTransvecCol, List.length_ofFn, le_refl, List.drop_eq_nil_of_le, List.prod_nil,
  Matrix.one_mul]