-- Mathlib/.lake/packages/batteries/Batteries/Control/Monad.lean
theorem _root_.LawfulFunctor.map_inj_right_of_nonempty [Functor f] [LawfulFunctor f] [Nonempty α]
    {g : α → β} (h : ∀ {x y : α}, g x = g y → x = y) {x y : f α} :
    g <$> x = g <$> y ↔ x = y

Proof state:
case mp
f : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Functor f
inst✝¹ : LawfulFunctor f
inst✝ : Nonempty α
g : α → β
h : ∀ {x y : α}, g x = g y → x = y
x y : f α
⊢ g <$> x = g <$> y → x = y

Tactic:
let g' a := if h : ∃ b, g b = a then h.choose else Classical.ofNonempty

Result:
case mp
f : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Functor f
inst✝¹ : LawfulFunctor f
inst✝ : Nonempty α
g : α → β
h : ∀ {x y : α}, g x = g y → x = y
x y : f α
g' : β → α := fun a => if h : ∃ b, g b = a then h.choose else Classical.ofNonempty
⊢ g <$> x = g <$> y → x = y

Proof state:
case mpr
f : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Functor f
inst✝¹ : LawfulFunctor f
inst✝ : Nonempty α
g : α → β
h : ∀ {x y : α}, g x = g y → x = y
x y : f α
⊢ x = y → g <$> x = g <$> y

Tactic:
intro h'

Result:
case mpr
f : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Functor f
inst✝¹ : LawfulFunctor f
inst✝ : Nonempty α
g : α → β
h : ∀ {x y : α}, g x = g y → x = y
x y : f α
h' : x = y
⊢ g <$> x = g <$> y

Proof state:
f : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Functor f
inst✝¹ : LawfulFunctor f
inst✝ : Nonempty α
g : α → β
h : ∀ {x y : α}, g x = g y → x = y
x y : f α
g' : β → α := fun a => if h : ∃ b, g b = a then h.choose else Classical.ofNonempty
a : α
⊢ ⋯.choose = a

Tactic:
exact h (_ : ∃ b, g b = g a).choose_spec

Result:
no goals

Proof state:
f : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Functor f
inst✝¹ : LawfulFunctor f
inst✝ : Nonempty α
g : α → β
h : ∀ {x y : α}, g x = g y → x = y
x y : f α
⊢ g <$> x = g <$> y ↔ x = y

Tactic:
constructor

Result:
case mp
f : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Functor f
inst✝¹ : LawfulFunctor f
inst✝ : Nonempty α
g : α → β
h : ∀ {x y : α}, g x = g y → x = y
x y : f α
⊢ g <$> x = g <$> y → x = y

case mpr
f : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Functor f
inst✝¹ : LawfulFunctor f
inst✝ : Nonempty α
g : α → β
h : ∀ {x y : α}, g x = g y → x = y
x y : f α
⊢ x = y → g <$> x = g <$> y

Proof state:
f : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Functor f
inst✝¹ : LawfulFunctor f
inst✝ : Nonempty α
g : α → β
h : ∀ {x y : α}, g x = g y → x = y
x y : f α
g' : β → α := fun a => if h : ∃ b, g b = a then h.choose else Classical.ofNonempty
a : α
⊢ g' (g a) = a

Tactic:
simp only [exists_apply_eq_apply, ↓reduceDIte, g']

Result:
f : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Functor f
inst✝¹ : LawfulFunctor f
inst✝ : Nonempty α
g : α → β
h : ∀ {x y : α}, g x = g y → x = y
x y : f α
g' : β → α := fun a => if h : ∃ b, g b = a then h.choose else Classical.ofNonempty
a : α
⊢ ⋯.choose = a

Proof state:
case mp
f : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Functor f
inst✝¹ : LawfulFunctor f
inst✝ : Nonempty α
g : α → β
h : ∀ {x y : α}, g x = g y → x = y
x y : f α
g' : β → α := fun a => if h : ∃ b, g b = a then h.choose else Classical.ofNonempty
g'g : ∀ (a : α), g' (g a) = a
⊢ g <$> x = g <$> y → x = y

Tactic:
intro h'

Result:
case mp
f : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Functor f
inst✝¹ : LawfulFunctor f
inst✝ : Nonempty α
g : α → β
h : ∀ {x y : α}, g x = g y → x = y
x y : f α
g' : β → α := fun a => if h : ∃ b, g b = a then h.choose else Classical.ofNonempty
g'g : ∀ (a : α), g' (g a) = a
h' : g <$> x = g <$> y
⊢ x = y

Proof state:
case mpr
f : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Functor f
inst✝¹ : LawfulFunctor f
inst✝ : Nonempty α
g : α → β
h : ∀ {x y : α}, g x = g y → x = y
x y : f α
h' : x = y
⊢ g <$> x = g <$> y

Tactic:
rw [h']

Result:
no goals

Proof state:
case mp
f : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Functor f
inst✝¹ : LawfulFunctor f
inst✝ : Nonempty α
g : α → β
h : ∀ {x y : α}, g x = g y → x = y
x y : f α
g' : β → α := fun a => if h : ∃ b, g b = a then h.choose else Classical.ofNonempty
⊢ g <$> x = g <$> y → x = y

Tactic:
have g'g a : g' (g a) = a := by
  simp only [exists_apply_eq_apply, ↓reduceDIte, g']
  exact h (_ : ∃ b, g b = g a).choose_spec

Result:
case mp
f : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Functor f
inst✝¹ : LawfulFunctor f
inst✝ : Nonempty α
g : α → β
h : ∀ {x y : α}, g x = g y → x = y
x y : f α
g' : β → α := fun a => if h : ∃ b, g b = a then h.choose else Classical.ofNonempty
g'g : ∀ (a : α), g' (g a) = a
⊢ g <$> x = g <$> y → x = y