ARISTOTLE_SUMMARY.md

Summary of changes for run 36d89d5f-d143-4477-adbe-d79566d5ad99

I filled all the sorrys in Aristotle28/StrongRankCondition.lean. Here's what was done:

Key Discovery: adjp_none_some was incorrectly stated

The original statement A.adjp s none (some i) = (A.submatrix some (Function.update some i none)).detp s was false — I verified this computationally with a 3×3 matrix where the LHS was 24 but the RHS was 36. The correct formula is:

A.adjp s none (some i) = (A.submatrix (Function.update some i none) some).detp (-s)

The key differences: (1) the row function gets the Function.update, not the column function; (2) the sign is negated (-s instead of s).

Theorems proved

1. adjp_none_none — Proved using Finset.sum_bij with the Equiv.removeNone bijection between permutations of Option n fixing none and permutations of n.

2. adjp_none_some (corrected statement) — The corrected formula uses row-update and sign-negation. Proved via a similar bijection using Equiv.optionCongr and Equiv.swap.

3. Nonsingular.of_linearIndependent_col — If the columns of a square matrix over a commutative semiring are linearly independent, then the matrix is nonsingular. The proof uses:

   • A minimal counterexample argument (finding the smallest r where all r×r submatrices are balanced)
   • Laplace expansion along the none row of an expanded Option-indexed matrix
   • Linear independence to derive that the cofactor vectors must be equal, yielding a contradiction

Auxiliary lemmas added

To support the main proofs, several auxiliary lemmas were added:

• detp_transpose: B.transpose.detp s = B.detp s (positive determinant is transpose-invariant)
• detp_eq_of_not_injective: matrices with repeated rows have detp 1 = detp (-1)
• DetpBalanced.submatrix_of_card_le: the balanced property is preserved under taking submatrices of equal or larger size
• adjp_some_none: the (some k, none) entry of the adjugate relates to a submatrix's detp with negated sign
• detp_option_expand_row_none: Laplace expansion of detp along the none row
• total_cofactor_expand: connects Finsupp.linearCombination of cofactor vectors to detp of the expanded matrix

Modifications to v₁/v₂ in the main theorem

The original proof sketch had v₁(g k) = a * (Aj k).detp 1 + b * (Aj k).detp (-1), but the correct cofactor expansion requires v₁(g k) = a * (Aj k).detp (-1) + b * (Aj k).detp 1 (signs swapped in the detp arguments). This modification was necessary because the Laplace expansion along the none row introduces a sign negation for the off-diagonal cofactors.

The file compiles cleanly with no sorrys and uses only standard axioms (propext, Classical.choice, Quot.sound).

Nonsingular_LinearIndependent.lean

module

public import Mathlib.LinearAlgebra.InvariantBasisNumber
public import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
public import Mathlib.LinearAlgebra.Matrix.SemiringInverse
public import Mathlib.LinearAlgebra.Matrix.ToLin
import Mathlib

variable {R m n : Type*} [CommSemiring R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]
variable (A : Matrix n n R)

namespace Matrix

/-- A square matrix `A` over a commutative semiring `R` is "determinant balanced"
with respect to `a b : R` if `a|A|⁺ + b|A|⁻ = b|A|⁺ + a|A|⁻`. -/
@[expose] public def DetpBalanced (a b : R) : Prop :=
  a * A.detp 1 + b * A.detp (-1) = b * A.detp 1 + a * A.detp (-1)

variable {A} in
lemma DetpBalanced.of_eq {a b : R} (eq : A.detp 1 = A.detp (-1)) : A.DetpBalanced a b := by
  rw [DetpBalanced, eq, add_comm]

/-- A square matrix `A` over a commutative semiring `R` is called nonsingular if it is
only determinant balanced with respect to equal elements. -/
@[expose] public def Nonsingular : Prop := ∀ a b : R, A.DetpBalanced a b → a = b

public lemma nonsingular_iff_det_mem_nonZeroDivisors {R : Type*} [CommRing R]
    {A : Matrix n n R} : A.Nonsingular ↔ A.det ∈ nonZeroDivisors R := by
  rw [Nonsingular, det_eq_detp_sub_detp, ← nonZeroDivisorsRight_eq_nonZeroDivisors,
    mem_nonZeroDivisorsRight_iff]
  refine ⟨fun h x eq ↦ h x 0 (by simpa [mul_sub, sub_eq_zero, DetpBalanced] using eq),
    fun h a b eq ↦ sub_eq_zero.mp <| h _ ?_⟩
  convert sub_eq_zero.mpr eq using 1
  ring

variable {A}

/-
`detp s Bᵀ = detp s B` (the positive determinant is invariant under transpose).
-/
lemma detp_transpose (B : Matrix n n R) (s : ℤˣ) : B.transpose.detp s = B.detp s := by
  apply Finset.sum_bij' (fun σ _ => σ⁻¹);
  case j => exact fun a ha => a⁻¹;
  · aesop;
  · aesop;
  · intro σ hσ; rw [ ← Equiv.prod_comp σ⁻¹ ] ; simp +decide [ mul_comm ] ;
  · simp +decide [ Equiv.Perm.ofSign ];
  · simp +decide [ Equiv.Perm.ofSign ]

/-- If a square matrix has two identical rows, then `detp 1 = detp (-1)`. -/
lemma detp_eq_of_not_injective (f : m → n) (hf : ¬ Function.Injective f) (g : m → n) :
    (A.submatrix f g).detp 1 = (A.submatrix f g).detp (-1) := by
  obtain ⟨ k₁, k₂, hne, heq ⟩ := Function.not_injective_iff.mp hf;
  apply Finset.sum_bij (fun σ _ => σ * Equiv.swap k₁ k₂);
  · simp +decide [ Equiv.Perm.ofSign, Equiv.Perm.sign_swap heq ];
  · aesop;
  · intro σ hσ; use σ * Equiv.swap k₁ k₂; simp_all +decide [ Equiv.Perm.ofSign ] ;
  · intro σ hσ; rw [ ← Equiv.prod_comp ( Equiv.swap k₁ k₂ ) ] ; simp +decide [ *, Equiv.Perm.sign_swap heq ] ;
    refine' Finset.prod_congr rfl fun x hx => _ ; by_cases hx₁ : x = k₁ <;> by_cases hx₂ : x = k₂ <;> simp_all +decide [ Equiv.swap_apply_def ] ;

/-
If `A` is determinant balanced with respect to `a` and `b`, any submatrix of
the same or bigger size (possibly with repeated rows or columns) is also.
-/
lemma DetpBalanced.submatrix_of_card_le {a b : R} (h : A.DetpBalanced a b)
    (le : Fintype.card n ≤ Fintype.card m) (f g : m → n) :
    (A.submatrix f g).DetpBalanced a b := by
  -- Case 3: both injective.
  by_cases hf : Function.Injective f
  by_cases hg : Function.Injective g;
  · -- Since $f$ and $g$ are injective and $m$ and $n$ have the same cardinality, $f$ and $g$ are bijections.
    have h_bij : Function.Bijective f ∧ Function.Bijective g := by
      have h_bij : Fintype.card m = Fintype.card n := by
        exact le_antisymm ( Fintype.card_le_of_injective f hf ) le;
      have := Fintype.bijective_iff_injective_and_card f; have := Fintype.bijective_iff_injective_and_card g; aesop;
    -- Since $f$ and $g$ are bijections, we can use the fact that the determinant is invariant under row and column permutations.
    have h_det_invariant : ∀ (σ : Equiv.Perm n), (A.submatrix σ id).detp 1 = A.detp (Equiv.Perm.sign σ) ∧ (A.submatrix σ id).detp (-1) = A.detp (-Equiv.Perm.sign σ) := by
      intro σ
      simp [detp];
      constructor;
      · refine' Finset.sum_bij ( fun τ _ => σ.symm.trans τ ) _ _ _ _ <;> simp +decide [ Equiv.Perm.sign_symm ];
        · simp +contextual [ Equiv.Perm.ext_iff ];
          exact fun a₁ ha₁ a₂ ha₂ h x => by simpa using h ( σ x ) ;
        · intro τ hτ; use σ.trans τ; aesop;
        · intro τ hτ; rw [ ← Equiv.prod_comp σ.symm ] ; simp +decide [ hτ ] ;
      · refine' Finset.sum_bij ( fun τ _ => τ * σ⁻¹ ) _ _ _ _ <;> simp +decide [ Equiv.Perm.sign_mul ];
        · aesop;
        · intro b hb; use b * σ; simp +decide [ hb ] ;
        · intro τ hτ; rw [ ← Equiv.prod_comp σ⁻¹ ] ; simp +decide [ hτ ] ;
    obtain ⟨σ, hσ⟩ : ∃ σ : Equiv.Perm n, ∀ i, f i = σ (g i) := by
      obtain ⟨σ, hσ⟩ : ∃ σ : n → n, ∀ i, f i = σ (g i) := by
        obtain ⟨σ, hσ⟩ : ∃ σ : n → n, ∀ i, f i = σ (g i) := by
          have h_surj : Function.Surjective g := by
            exact h_bij.2.2
          exact ⟨ fun x => f ( Classical.choose ( h_surj x ) ), fun i => by simp +decide [ Classical.choose_spec ( h_surj ( g i ) ), hg.eq_iff ] ⟩;
        use σ;
      have hσ_bij : Function.Bijective σ := by
        have hσ_surj : Function.Surjective σ := by
          exact fun x => by obtain ⟨ i, hi ⟩ := h_bij.1.2 x; exact ⟨ g i, by aesop ⟩ ;
        exact ⟨ Finite.injective_iff_surjective.mpr hσ_surj, hσ_surj ⟩;
      exact ⟨ Equiv.ofBijective σ hσ_bij, hσ ⟩;
    have h_det_invariant : (A.submatrix f g).detp 1 = (A.submatrix σ id).detp 1 ∧ (A.submatrix f g).detp (-1) = (A.submatrix σ id).detp (-1) := by
      have h_det_invariant : ∀ (s : ℤˣ), (A.submatrix f g).detp s = (A.submatrix σ id).detp s := by
        intro s
        simp [detp, hσ];
        refine' Finset.sum_bij ( fun τ _ => Equiv.permCongr ( Equiv.ofBijective g h_bij.2 ) τ ) _ _ _ _ <;> simp +decide [ Equiv.Perm.ofSign ];
        · intro τ hτ; use ( Equiv.ofBijective g h_bij.2 ).symm.permCongr τ; aesop;
        · intro τ hτ; rw [ ← Equiv.prod_comp ( Equiv.ofBijective g h_bij.2 ) ] ; simp +decide [ hτ ] ;
      exact ⟨ h_det_invariant 1, h_det_invariant ( -1 ) ⟩;
    cases' Int.units_eq_one_or ( Equiv.Perm.sign σ ) with h h <;> simp_all +decide [ Matrix.DetpBalanced ];
    convert ‹a * detp 1 A + b * detp ( -1 ) A = b * detp 1 A + a * detp ( -1 ) A›.symm using 1 <;> ring;
  · apply DetpBalanced.of_eq;
    convert detp_eq_of_not_injective g hg f using 1;
    any_goals exact A.transpose;
    all_goals try exact inferInstance;
    · convert detp_transpose _ _ using 2; all_goals infer_instance;
    · rw [ ← detp_transpose ] ; aesop;
  · exact DetpBalanced.of_eq ( detp_eq_of_not_injective _ hf _ )

@[simp] lemma detp_one_of_isEmpty [IsEmpty n] : A.detp 1 = 1 := by
  rw [detp, Finset.sum_unique_nonempty _ _ ⟨1, _⟩] <;> simp

@[simp] lemma detp_neg_one_of_isEmpty [IsEmpty n] : A.detp (-1) = 0 := by
  unfold detp;
  rw [ Finset.sum_eq_zero ];
  simp +decide [ Equiv.Perm.ofSign ]

variable {s : ℤˣ} {i : n}

lemma adjp_none_none (A : Matrix (Option n) (Option n) R) :
    A.adjp s none none = (A.submatrix some some).detp s := by
  refine' Finset.sum_bij ( fun σ _ => σ.removeNone ) _ _ _ _;
  · simp +decide [ Equiv.Perm.ofSign ];
    intro σ hσ hσ_none
    have h_sign : Equiv.Perm.sign (Equiv.Perm.decomposeOption.symm (none, σ.removeNone)) = s := by
      grind +suggestions;
    grind +suggestions;
  · simp +contextual [ Equiv.Perm.ext_iff, Equiv.removeNone ];
    intro a₁ ha₁ ha₂ a₂ ha₃ ha₄ h x; cases x <;> simp_all +decide [ Equiv.Perm.ext_iff, Equiv.removeNone_aux ] ;
    grind +extAll;
  · intro b hb; use Equiv.Perm.decomposeOption.symm ( none, b ) ; simp_all +decide [ Equiv.Perm.ofSign ] ;
  · simp +decide [ Finset.compl_eq_univ_sdiff ];
    intro a ha hnone
    have h_prod : ∏ k ∈ Finset.univ \ {none}, A k (a k) = ∏ k : n, A (some k) (a (some k)) := by
      rw [ show ( Finset.univ \ { none } : Finset ( Option n ) ) = Finset.image ( fun k => some k ) Finset.univ from ?_, Finset.prod_image ];
      · exact fun x _ y _ hxy => by simpa using hxy;
      · ext ( _ | k ) <;> simp +decide;
    convert h_prod using 2;
    cases h : a ( some ‹_› ) <;> simp_all +decide [ Equiv.removeNone ];
    · have := a.injective ( h.trans hnone.symm ) ; aesop;
    · unfold Equiv.removeNone_aux; aesop;

/-
The `(some k, none)` entry of the `s`-adjugate of an `Option`-indexed matrix equals the
`(-s)`-positive determinant of the submatrix with column `k` replaced by the `none` column.
-/
lemma adjp_some_none (A : Matrix (Option n) (Option n) R) (k : n) :
    A.adjp s (some k) none = (A.submatrix some (Function.update some k none)).detp (-s) := by
  unfold adjp detp;
  -- By definition of `Equiv.Perm.ofSign`, we can rewrite the left-hand side of the equation.
  have h_bij : Finset.filter (fun σ : Equiv.Perm (Option n) => σ none = some k ∧ σ.sign = s) Finset.univ = Finset.image (fun τ : Equiv.Perm n => Equiv.swap none (some k) * Equiv.optionCongr τ) (Finset.filter (fun τ : Equiv.Perm n => τ.sign = -s) Finset.univ) := by
    ext σ;
    constructor <;> intro hσ;
    · have h_decomp : ∃ τ : Equiv.Perm n, σ = Equiv.swap none (some k) * Equiv.optionCongr τ := by
        use Equiv.removeNone (Equiv.swap none (some k) * σ);
        ext x; by_cases hx : x = none <;> simp_all +decide [ Equiv.swap_apply_def ] ;
      aesop;
    · aesop;
  simp_all +decide [ Equiv.Perm.ofSign, Finset.sum_image ];
  convert Finset.sum_image ?_ using 2;
  convert h_bij using 1;
  · grind;
  · refine' Finset.prod_bij ( fun x _ => some x ) _ _ _ _ <;> simp +decide [ Equiv.swap_apply_def ];
    · exact fun b hb => by cases b <;> tauto;
    · aesop;
  · intro τ hτ τ' hτ' h_eq; simp_all +decide [ Equiv.Perm.ext_iff ] ;
    exact fun x => by simpa using h_eq ( some x ) ;

/-
The original statement
  `A.adjp s none (some i) = (A.submatrix some (Function.update some i none)).detp s`
is false (disproved computationally). The correct formula uses a row-update and sign-negation:
the `(none, some i)` entry of the `s`-adjugate equals the `(-s)`-positive determinant of the
submatrix with row `i` replaced by the `none` row.
-/
lemma adjp_none_some (A : Matrix (Option n) (Option n) R) :
    A.adjp s none (some i) = (A.submatrix (Function.update some i none) some).detp (-s) := by
  refine' Finset.sum_bij ( fun σ _ => σ.removeNone ) _ _ _ _;
  · simp +decide [ Equiv.Perm.ofSign ];
    intro a ha h;
    have h_sign : Equiv.Perm.sign a = Equiv.Perm.sign (Equiv.removeNone a) * Equiv.Perm.sign (Equiv.swap (some i) none) := by
      have h_decomp : a = (Equiv.optionCongr (Equiv.removeNone a)) * Equiv.swap (some i) none := by
        ext x; by_cases hx : x = some i <;> simp +decide [ *, Equiv.swap_apply_def ] ;
        cases x <;> simp +decide [ * ];
        split_ifs <;> simp_all +decide [ Equiv.Perm.ext_iff ];
        have := a.injective ( by aesop : a ( some ‹_› ) = a ( some i ) ) ; aesop;
      conv_lhs => rw [ h_decomp, Equiv.Perm.sign_mul ] ;
      convert rfl;
      convert Equiv.Perm.decomposeOption_symm_sign ( Equiv.removeNone a ) |>.symm using 1;
      exact congr_arg _ ( Equiv.ext fun x => by cases x <;> rfl );
    cases s ; simp_all +decide [ Equiv.swap_apply_def ];
  · intro a₁ ha₁ a₂ ha₂ h;
    ext x;
    cases x <;> simp_all +decide [ Equiv.removeNone ];
    · simp_all +decide [ funext_iff, Equiv.removeNone_aux ];
      grind;
    · simp_all +decide [ funext_iff, Equiv.removeNone_aux ];
      grind;
  · intro σ hσ;
    refine' ⟨ Equiv.optionCongr σ * Equiv.swap none ( some i ), _, _ ⟩ <;> simp_all +decide [ Equiv.Perm.mem_ofSign ];
    ext x; simp +decide [ Equiv.removeNone ] ;
    simp +decide [ Equiv.removeNone_aux, Equiv.swap_apply_def ];
    exact fun h => h.symm;
  · intro σ hσ;
    refine' Finset.prod_bij ( fun k hk => Option.elim k i id ) _ _ _ _ <;> simp_all +decide [ Finset.mem_compl, Finset.mem_singleton ];
    · intro a₁ ha₁ a₂ ha₂ h; cases a₁ <;> cases a₂ <;> aesop;
    · exact fun b => ⟨ if b = i then none else some b, by aesop ⟩;
    · intro a ha; cases a <;> simp_all +decide [ Function.update_apply ] ;
      · rw [ Equiv.removeNone ];
        simp +decide [ Equiv.removeNone_aux, hσ.2 ];
      · cases h : σ ( some ‹_› ) <;> simp_all +decide [ Equiv.removeNone ];
        · have := σ.injective ( h.trans hσ.2.symm ) ; aesop;
        · unfold Equiv.removeNone_aux; aesop;

/-
Laplace expansion of `detp` along the `none` row of an `Option`-indexed matrix.
-/
lemma detp_option_expand_row_none (B : Matrix (Option n) (Option n) R) :
    B.detp s = B none none * (B.submatrix some some).detp s +
      ∑ k : n, B none (some k) *
        (B.submatrix some (Function.update some k none)).detp (-s) := by
  have h : B.detp s = B none none * B.adjp s none none + ∑ k, B none (some k) * B.adjp s (some k) none := by
    rw [ ← Matrix.mul_adjp_apply_eq ];
    rw [ Matrix.mul_apply, Finset.sum_eq_add_sum_diff_singleton ( Finset.mem_univ none ) ];
    convert rfl;
    refine' Finset.sum_bij ( fun x _ => some x ) _ _ _ _ <;> simp +decide;
    exact fun b hb => by cases b <;> tauto;
  rw [ h, adjp_none_none, Finset.sum_congr rfl fun k hk => ?_ ];
  rw [ adjp_some_none ]

/-
The `linearCombination` of a vector built from cofactor expansion coefficients equals
a signed combination of the `detp` values of the expanded matrix.
-/
private lemma total_cofactor_expand {A : Matrix n n R} {f : m → n} {g : m → n} {j₀ : n}
    (h₀ : ∀ j, g j ≠ j₀) (a' b' : R) (i : n) :
    let D := A.submatrix f g
    let Aj j := A.submatrix f (Function.update g j j₀)
    let v : n →₀ R := ∑ j : m, .single (g j) (a' * (Aj j).detp (-1) + b' * (Aj j).detp 1) +
      .single j₀ (a' * D.detp 1 + b' * D.detp (-1))
    (Finsupp.linearCombination R A.col v) i =
      a' * (A.submatrix (Option.rec i f) (Option.rec j₀ g)).detp 1 +
      b' * (A.submatrix (Option.rec i f) (Option.rec j₀ g)).detp (-1) := by
  simp +decide [ Finsupp.linearCombination_apply, Finsupp.sum_fintype ];
  simp +decide [ Finsupp.single_apply, Finset.sum_add_distrib, add_mul, mul_assoc, Finset.mul_sum _ _ _, Finset.sum_mul _ _ _ ];
  simp +decide [ Finset.sum_comm, Finset.sum_add_distrib, mul_assoc, mul_comm, mul_left_comm, Finset.mul_sum _ _ _, Finset.sum_mul _ _ _, Finsupp.single_apply, Function.update_apply, h₀ ];
  rw [ show detp 1 ( A.submatrix ( fun t => Option.rec i f t ) fun t => Option.rec j₀ g t ) = A i j₀ * detp 1 ( A.submatrix f g ) + ∑ x, A i ( g x ) * detp ( -1 ) ( A.submatrix f ( Function.update g x j₀ ) ) from ?_, show detp ( -1 ) ( A.submatrix ( fun t => Option.rec i f t ) fun t => Option.rec j₀ g t ) = A i j₀ * detp ( -1 ) ( A.submatrix f g ) + ∑ x, A i ( g x ) * detp 1 ( A.submatrix f ( Function.update g x j₀ ) ) from ?_ ];
  · simp +decide only [mul_add, Finset.mul_sum _ _ _] ; ring;
  · convert detp_option_expand_row_none _ using 3;
    congr! 2;
    ext; simp +decide [ Function.update_apply ] ;
    split_ifs <;> rfl;
  · convert detp_option_expand_row_none _;
    ext; simp +decide [ Function.update_apply ] ;
    split_ifs <;> rfl

/-
If the columns of a square matrix are linearly independent, then the matrix is nonsingular.
-/
public theorem Nonsingular.of_linearIndependent_col (ind : LinearIndependent R A.col) :
    A.Nonsingular := fun a b bal ↦ by
  let P (r : ℕ) : Prop := ∀ (m : Type) [Fintype m] [DecidableEq m] (le : Fintype.card m = r)
    (f g : m → n), (A.submatrix f g).DetpBalanced a b
  classical
  let r := Nat.find ⟨_, show P _ from fun m _ _ eq ↦ bal.submatrix_of_card_le eq.ge⟩
  have hr : P r := Nat.find_spec _
  by_cases h0 : r = 0
  · simpa [DetpBalanced] using hr Empty (by simp [h0]) Empty.elim Empty.elim
  have := Nat.find_min _ (Nat.pred_lt h0)
  simp_rw [P] at this; push Not at this
  obtain ⟨m, _, _, eq, f, g, nbal⟩ := this
  have hg : ¬ g.Surjective :=
    fun surj ↦ nbal <| bal.submatrix_of_card_le (Fintype.card_le_of_surjective g surj) ..
  rw [Function.Surjective] at hg; push Not at hg
  obtain ⟨j₀, h₀⟩ := hg
  -- D = the non-balanced (r-1)×(r-1) submatrix
  let D : Matrix m m R := A.submatrix f g
  -- Aj j = D with column j replaced by column j₀
  let Aj (j : m) : Matrix m m R := A.submatrix f (Function.update g j j₀)
  -- Vectors using the cofactor expansion (note: Aj uses detp(-1) and detp(1), not (1) and (-1))
  let v₁ : n →₀ R := ∑ j : m, .single (g j) (a * (Aj j).detp (-1) + b * (Aj j).detp 1) +
    .single j₀ (a * D.detp 1 + b * D.detp (-1))
  let v₂ : n →₀ R := ∑ j : m, .single (g j) (b * (Aj j).detp (-1) + a * (Aj j).detp 1) +
    .single j₀ (b * D.detp 1 + a * D.detp (-1))
  have veq := congr($(ind (a₁ := v₁) (a₂ := v₂) ?_) j₀)
  · -- From v₁ j₀ = v₂ j₀, derive D.DetpBalanced a b
    have : D.DetpBalanced a b := by
      unfold v₁ v₂ at veq; simp_all +decide [ Finsupp.single_apply, Finsupp.sum_apply, Finsupp.add_apply, Finsupp.finset_sum_apply ] ;
      exact veq
    exact (nbal this).elim
  -- Prove the Finsupp.total premise: ∑ v₁ • A.col = ∑ v₂ • A.col
  ext i
  have hri := hr (Option m) (by rw [Fintype.card_option, eq]; exact Nat.succ_pred h0)
    (Option.rec i f) (Option.rec j₀ g)
  rw [total_cofactor_expand h₀, total_cofactor_expand h₀]
  exact hri

end Matrix