help with small proof involving Axiom of Choice

Stream: new members

[Mike]

I'm going through Mathematics in Lean, and thought of a lemma I would like to know how to prove:

lemma inv_eq_default_or (y : β) (x : α) : inverse f y = x →
  (x = default ∨ f x = y)

What I've got so far is:

import MIL.Common
import Mathlib.Data.Set.Lattice
import Mathlib.Data.Set.Function
import Mathlib.Analysis.SpecialFunctions.Log.Basic

variable {α β : Type*} [Inhabited α]
variable (f : α → β)

#check Classical.choose_spec

open Function

lemma inv_eq_default_or (y : β) (x : α) : inverse f y = x →
  (x = default ∨ f x = y) := by
  intro h'
  rw [inverse] at h'
  by_cases h : ∃ x₀, f x₀ = y
  case pos =>
    right
    rw [dif_pos h] at h'

The Lean Infoview shows that I have:

h: ∃ x₀, f x₀ = y
h': choose h = x

Does anyone know how to use h and h' to prove that f x = y to finish the positive direction.

Thanks!

Edit!

Answered it myself by reading https://lean-lang.org/theorem_proving_in_lean4/axioms_and_computation.html?highlight=choose#choice

Solution is:

lemma inv_eq_default_or (y : β) (x : α) : inverse f y = x →
  (x = default ∨ f x = y) := by
  intro h'
  rw [inverse] at h'
  by_cases h : ∃ x₀, f x₀ = y
  case neg =>
    left
    rw [dif_neg h] at h'
    rw [h']
  case pos =>
    right
    rw [dif_pos h] at h'
    have : f (choose h) = y := by apply choose_spec h
    rw [h'] at this
    exact this

I wasn't applying choose_spec correctly.