Log right inverse

@[simp]lemma log_right_inverse' {ω : D} {x : ω} :  ω (log ω x) = x := by  have h_log : ∃ i : Fin (2 ^ n), ω i = x := by    exact Finset.mem_image.mp x.2 |> fun ⟨i, _, hi⟩ ↦ ⟨i, hi⟩  obtain ⟨i, hi⟩ := h_log  have h_log_aux :    ∀ (fuel : ℕ) (i : Fin (2 ^ n)),      i.val < fuel → ω i = x → ω (logAux ω x fuel) = x := by    intro fuel i hi hx    induction fuel generalizing i with    | zero => simp_all    | succ fuel ih =>      by_cases hfuel : fuel < 2 ^ n      · by_cases hfound : ω (⟨fuel, hfuel⟩ : Fin (2 ^ n)) = x        · simp [logAux, hfuel, hfound]        · rw [show logAux ω x (fuel + 1) = logAux ω x fuel by simp [logAux, hfuel, hfound]]          apply ih i          · have hi_ne : i.val ≠ fuel := by              intro hval              apply hfound              have hfin : i = (⟨fuel, hfuel⟩ : Fin (2 ^ n)) := Fin.ext hval              rw [← hfin]              exact hx            omega          · exact hx      · rw [show logAux ω x (fuel + 1) = logAux ω x fuel by simp [logAux, hfuel]]        apply ih i        · exact lt_of_lt_of_le i.isLt (Nat.le_of_not_gt hfuel)        · exact hx  exact h_log_aux _ _ (Fin.is_lt i) hi