How can I get rid of `[Inhabited X]` please?

Stream: mathlib4

[Martin Dvořák]

import Mathlib

lemma Matrix.isTotallyUnimodular_iff_adjoin_zero_row {X Y X' : Type*} (A : Matrix X Y ℚ) [Inhabited X] :
    (Matrix.fromRows A (Matrix.row X' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular := by
  rw [Matrix.isTotallyUnimodular_iff, Matrix.isTotallyUnimodular_iff]
  constructor <;> intro hA k f g
  · exact hA k (Sum.inl ∘ f) g
  · if zerow : ∃ i, ∃ i', f i = Sum.inr i' then
      obtain ⟨i, i', hii'⟩ := zerow
      left
      apply Matrix.det_eq_zero_of_row_eq_zero i
      intro
      simp_all
    else
      obtain ⟨f', rfl⟩ : ∃ f₀ : Fin k → X, f = Sum.inl ∘ f₀
      · use (fun i => (f i).elim id default) -- I'd need something in place of `.elim` ?
        ext i
        cases hfi : f i with
        | inl => simp [hfi]
        | inr => exfalso; exact zerow ⟨i, _, hfi⟩
      apply hA

[Johan Commelin]

import Mathlib

lemma Matrix.isTotallyUnimodular_iff_adjoin_zero_row {X Y X' : Type*} (A : Matrix X Y ℚ) :
    (Matrix.fromRows A (Matrix.row X' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular := by
  rw [Matrix.isTotallyUnimodular_iff, Matrix.isTotallyUnimodular_iff]
  constructor <;> intro hA k f g
  · exact hA k (Sum.inl ∘ f) g
  · if zerow : ∃ i, ∃ x', f i = Sum.inr x' then
      obtain ⟨i, x', hii'⟩ := zerow
      left
      apply Matrix.det_eq_zero_of_row_eq_zero i
      intro
      simp_all
    else
      obtain ⟨f', rfl⟩ : ∃ f₀ : Fin k → X, f = Sum.inl ∘ f₀
      · push_neg at zerow
        suffices ∀ i, ∃ x, f i = Sum.inl x by
          choose f₀ hf₀ using this
          use f₀
          ext
          apply hf₀
        intro i
        specialize zerow i
        match hfi : f i with
        | .inl x => use x
        | .inr x => exact (zerow x hfi).elim
      apply hA

[Martin Dvořák]

Thanks! Can I PR your proof to Mathlib?

[Johan Commelin]

Certainly

[Johan Commelin]

Maybe you can still golf it as well

[Johan Commelin]

Because the obtain + suffices suggest that might be possible