Get M option eq some iff

lemma getM_option_eq_some_iff {n : ℕ} {β : Type*} {f : Fin n → Option β} {v : Fin n → β} :    Matrix.getM f = some v ↔ ∀ i, f i = some (v i) := by  induction n with  | zero =>    refine ⟨fun _ i ↦ i.elim0, fun _ ↦ ?_⟩    rw [Matrix.getM]    exact congrArg some (funext fun i ↦ i.elim0)  | succ n ih =>    rw [getM_option_succ]    constructor    · intro h      rw [Option.bind_eq_some_iff] at h      obtain ⟨a, ha, hm⟩ := h      rw [Option.map_eq_some_iff] at hm      obtain ⟨w, hw, rfl⟩ := hm      intro i      exact i.cases (by simpa using ha) (by simpa using ih.mp hw)    · intro h      refine Option.bind_eq_some_iff.mpr ⟨v 0, by simpa using h 0, ?_⟩      refine Option.map_eq_some_iff.mpr        ⟨fun j ↦ v j.succ, ih.mpr fun j ↦ by simpa using h j.succ, ?_⟩      exact funext fun i ↦ i.cases (by simp) (by simp)