-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Lemmas.lean
theorem map_inj_of_inj [Applicative m] [LawfulApplicative m] [Nonempty α] {f : α → β}
    (w : ∀ x y, f x = f y → x = y) {x y : m α}
    (h : f <$> x = f <$> y) : x = y

Proof state:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Applicative m
inst✝¹ : LawfulApplicative m
inst✝ : Nonempty α
f : α → β
w : ∀ (x y : α), f x = f y → x = y
x y : m α
h : f <$> x = f <$> y
⊢ x = y

Tactic:
apply map_inj_of_left_inverse ?_ h

Result:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Applicative m
inst✝¹ : LawfulApplicative m
inst✝ : Nonempty α
f : α → β
w : ∀ (x y : α), f x = f y → x = y
x y : m α
h : f <$> x = f <$> y
⊢ ∃ g, ∀ (x : α), g (f x) = x

Proof state:
case refine_1
m : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Applicative m
inst✝¹ : LawfulApplicative m
inst✝ : Nonempty α
f : α → β
w : ∀ (x y : α), f x = f y → x = y
x y : m α
h : f <$> x = f <$> y
a : α
⊢ β → α

Tactic:
intro b

Result:
case refine_1
m : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Applicative m
inst✝¹ : LawfulApplicative m
inst✝ : Nonempty α
f : α → β
w : ∀ (x y : α), f x = f y → x = y
x y : m α
h : f <$> x = f <$> y
a : α
b : β
⊢ α

Proof state:
case refine_2
m : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Applicative m
inst✝¹ : LawfulApplicative m
inst✝ : Nonempty α
f : α → β
w : ∀ (x y : α), f x = f y → x = y
x y : m α
h : f <$> x = f <$> y
a : α
⊢ ∀ (x : α), (fun b => if p : ∃ a, f a = b then p.choose else a) (f x) = x

Tactic:
intro b

Result:
case refine_2
m : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Applicative m
inst✝¹ : LawfulApplicative m
inst✝ : Nonempty α
f : α → β
w : ∀ (x y : α), f x = f y → x = y
x y : m α
h : f <$> x = f <$> y
a b : α
⊢ (fun b => if p : ∃ a, f a = b then p.choose else a) (f b) = b

Proof state:
case pos
m : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Applicative m
inst✝¹ : LawfulApplicative m
inst✝ : Nonempty α
f : α → β
w : ∀ (x y : α), f x = f y → x = y
x y : m α
h : f <$> x = f <$> y
a : α
b : β
p : ∃ a, f a = b
⊢ α

Tactic:
exact Exists.choose p

Result:
no goals

Proof state:
case refine_2.a
m : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Applicative m
inst✝¹ : LawfulApplicative m
inst✝ : Nonempty α
f : α → β
w : ∀ (x y : α), f x = f y → x = y
x y : m α
h : f <$> x = f <$> y
a b : α
⊢ f ⋯.choose = f b

Tactic:
apply Exists.choose_spec (p := fun a => f a = f b)

Result:
no goals

Proof state:
case neg
m : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Applicative m
inst✝¹ : LawfulApplicative m
inst✝ : Nonempty α
f : α → β
w : ∀ (x y : α), f x = f y → x = y
x y : m α
h : f <$> x = f <$> y
a : α
b : β
p : ¬∃ a, f a = b
⊢ α

Tactic:
exact a

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Applicative m
inst✝¹ : LawfulApplicative m
inst✝ : Nonempty α
f : α → β
w : ∀ (x y : α), f x = f y → x = y
x y : m α
h : f <$> x = f <$> y
a : α
⊢ ∃ g, ∀ (x : α), g (f x) = x

Tactic:
refine ⟨?_, ?_⟩

Result:
case refine_1
m : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Applicative m
inst✝¹ : LawfulApplicative m
inst✝ : Nonempty α
f : α → β
w : ∀ (x y : α), f x = f y → x = y
x y : m α
h : f <$> x = f <$> y
a : α
⊢ β → α

case refine_2
m : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Applicative m
inst✝¹ : LawfulApplicative m
inst✝ : Nonempty α
f : α → β
w : ∀ (x y : α), f x = f y → x = y
x y : m α
h : f <$> x = f <$> y
a : α
⊢ ∀ (x : α), ?refine_1 (f x) = x

Proof state:
case refine_1
m : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Applicative m
inst✝¹ : LawfulApplicative m
inst✝ : Nonempty α
f : α → β
w : ∀ (x y : α), f x = f y → x = y
x y : m α
h : f <$> x = f <$> y
a : α
b : β
⊢ α

Tactic:
by_cases p : ∃ a, f a = b

Result:
case pos
m : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Applicative m
inst✝¹ : LawfulApplicative m
inst✝ : Nonempty α
f : α → β
w : ∀ (x y : α), f x = f y → x = y
x y : m α
h : f <$> x = f <$> y
a : α
b : β
p : ∃ a, f a = b
⊢ α

case neg
m : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Applicative m
inst✝¹ : LawfulApplicative m
inst✝ : Nonempty α
f : α → β
w : ∀ (x y : α), f x = f y → x = y
x y : m α
h : f <$> x = f <$> y
a : α
b : β
p : ¬∃ a, f a = b
⊢ α

Proof state:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Applicative m
inst✝¹ : LawfulApplicative m
inst✝ : Nonempty α
f : α → β
w : ∀ (x y : α), f x = f y → x = y
x y : m α
h : f <$> x = f <$> y
⊢ ∃ g, ∀ (x : α), g (f x) = x

Tactic:
let ⟨a⟩ := ‹Nonempty α›

Result:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Applicative m
inst✝¹ : LawfulApplicative m
inst✝ : Nonempty α
f : α → β
w : ∀ (x y : α), f x = f y → x = y
x y : m α
h : f <$> x = f <$> y
a : α
⊢ ∃ g, ∀ (x : α), g (f x) = x

Proof state:
case refine_2
m : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Applicative m
inst✝¹ : LawfulApplicative m
inst✝ : Nonempty α
f : α → β
w : ∀ (x y : α), f x = f y → x = y
x y : m α
h : f <$> x = f <$> y
a b : α
⊢ ⋯.choose = b

Tactic:
apply w

Result:
case refine_2.a
m : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Applicative m
inst✝¹ : LawfulApplicative m
inst✝ : Nonempty α
f : α → β
w : ∀ (x y : α), f x = f y → x = y
x y : m α
h : f <$> x = f <$> y
a b : α
⊢ f ⋯.choose = f b

Proof state:
case refine_2
m : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Applicative m
inst✝¹ : LawfulApplicative m
inst✝ : Nonempty α
f : α → β
w : ∀ (x y : α), f x = f y → x = y
x y : m α
h : f <$> x = f <$> y
a b : α
⊢ (fun b => if p : ∃ a, f a = b then p.choose else a) (f b) = b

Tactic:
simp only [exists_apply_eq_apply, ↓reduceDIte]

Result:
case refine_2
m : Type u_1 → Type u_2
α β : Type u_1
inst✝² : Applicative m
inst✝¹ : LawfulApplicative m
inst✝ : Nonempty α
f : α → β
w : ∀ (x y : α), f x = f y → x = y
x y : m α
h : f <$> x = f <$> y
a b : α
⊢ ⋯.choose = b