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

Proof state:
case neg.mpr
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
h : ∀ {x y : α}, f x = f y → x = y
x y : m α
hempty : ¬Nonempty α
h' : x = y
⊢ f <$> x = f <$> y

Tactic:
rw [h']

Result:
no goals

Proof state:
case neg.mp
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
h : ∀ {x y : α}, f x = f y → x = y
x y : m α
hempty : ¬Nonempty α
h' : f <$> x = f <$> y
⊢ x = y

Tactic:
have (z : m α) : z = (do let a ← z; let b ← pure (f a); x) := by
  conv => lhs; rw [← bind_pure z]
  congr; funext a
  exact (hempty ⟨a⟩).elim

Result:
case neg.mp
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
h : ∀ {x y : α}, f x = f y → x = y
x y : m α
hempty : ¬Nonempty α
h' : f <$> x = f <$> y
this :
  ∀ (z : m α),
    z = do
      let a ← z
      let _ ← pure (f a)
      x
⊢ x = y

Proof state:
case neg.mp
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
h : ∀ {x y : α}, f x = f y → x = y
x y : m α
hempty : ¬Nonempty α
⊢ f <$> x = f <$> y → x = y

Tactic:
intro h'

Result:
case neg.mp
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
h : ∀ {x y : α}, f x = f y → x = y
x y : m α
hempty : ¬Nonempty α
h' : f <$> x = f <$> y
⊢ x = y

Proof state:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
h : ∀ {x y : α}, f x = f y → x = y
x y : m α
⊢ f <$> x = f <$> y ↔ x = y

Tactic:
by_cases hempty : Nonempty α

Result:
case pos
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
h : ∀ {x y : α}, f x = f y → x = y
x y : m α
hempty : Nonempty α
⊢ f <$> x = f <$> y ↔ x = y

case neg
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
h : ∀ {x y : α}, f x = f y → x = y
x y : m α
hempty : ¬Nonempty α
⊢ f <$> x = f <$> y ↔ x = y

Proof state:
case pos
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
h : ∀ {x y : α}, f x = f y → x = y
x y : m α
hempty : Nonempty α
⊢ f <$> x = f <$> y ↔ x = y

Tactic:
exact LawfulFunctor.map_inj_right_of_nonempty h

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
h : ∀ {x y : α}, f x = f y → x = y
x y : m α
hempty : ¬Nonempty α
h' : f <$> x = f <$> y
z : m α
⊢ z >>= pure = do
    let a ← z
    let _ ← pure (f a)
    x

Tactic:
congr

Result:
case e_a
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
h : ∀ {x y : α}, f x = f y → x = y
x y : m α
hempty : ¬Nonempty α
h' : f <$> x = f <$> y
z : m α
⊢ pure = fun a => do
    let _ ← pure (f a)
    x

Proof state:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
h : ∀ {x y : α}, f x = f y → x = y
x y : m α
hempty : ¬Nonempty α
h' : f <$> x = f <$> y
z : m α
⊢ z = do
    let a ← z
    let _ ← pure (f a)
    x

Tactic:
conv => lhs; rw [← bind_pure z]

Result:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
h : ∀ {x y : α}, f x = f y → x = y
x y : m α
hempty : ¬Nonempty α
h' : f <$> x = f <$> y
z : m α
⊢ z >>= pure = do
    let a ← z
    let _ ← pure (f a)
    x

Proof state:
case neg
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
h : ∀ {x y : α}, f x = f y → x = y
x y : m α
hempty : ¬Nonempty α
⊢ f <$> x = f <$> y ↔ x = y

Tactic:
constructor

Result:
case neg.mp
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
h : ∀ {x y : α}, f x = f y → x = y
x y : m α
hempty : ¬Nonempty α
⊢ f <$> x = f <$> y → x = y

case neg.mpr
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
h : ∀ {x y : α}, f x = f y → x = y
x y : m α
hempty : ¬Nonempty α
⊢ x = y → f <$> x = f <$> y

Proof state:
case e_a
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
h : ∀ {x y : α}, f x = f y → x = y
x y : m α
hempty : ¬Nonempty α
h' : f <$> x = f <$> y
z : m α
⊢ pure = fun a => do
    let _ ← pure (f a)
    x

Tactic:
funext a

Result:
case e_a.h
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
h : ∀ {x y : α}, f x = f y → x = y
x y : m α
hempty : ¬Nonempty α
h' : f <$> x = f <$> y
z : m α
a : α
⊢ pure a = do
    let _ ← pure (f a)
    x

Proof state:
case neg.mp
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
h : ∀ {x y : α}, f x = f y → x = y
x y : m α
hempty : ¬Nonempty α
h' : f <$> x = f <$> y
this :
  ∀ (z : m α),
    z = do
      let a ← z
      let _ ← pure (f a)
      x
⊢ x = y

Tactic:
rw [this x, this y]

Result:
case neg.mp
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
h : ∀ {x y : α}, f x = f y → x = y
x y : m α
hempty : ¬Nonempty α
h' : f <$> x = f <$> y
this :
  ∀ (z : m α),
    z = do
      let a ← z
      let _ ← pure (f a)
      x
⊢ (do
      let a ← x
      let _ ← pure (f a)
      x) =
    do
    let a ← y
    let _ ← pure (f a)
    x

Proof state:
case neg.mpr
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
h : ∀ {x y : α}, f x = f y → x = y
x y : m α
hempty : ¬Nonempty α
⊢ x = y → f <$> x = f <$> y

Tactic:
intro h'

Result:
case neg.mpr
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
h : ∀ {x y : α}, f x = f y → x = y
x y : m α
hempty : ¬Nonempty α
h' : x = y
⊢ f <$> x = f <$> y

Proof state:
case e_a.h
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
h : ∀ {x y : α}, f x = f y → x = y
x y : m α
hempty : ¬Nonempty α
h' : f <$> x = f <$> y
z : m α
a : α
⊢ pure a = do
    let _ ← pure (f a)
    x

Tactic:
exact (hempty ⟨a⟩).elim

Result:
no goals

Proof state:
case neg.mp
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
h : ∀ {x y : α}, f x = f y → x = y
x y : m α
hempty : ¬Nonempty α
h' : f <$> x = f <$> y
this :
  ∀ (z : m α),
    z = do
      let a ← z
      let _ ← pure (f a)
      x
⊢ (do
      let a ← x
      let _ ← pure (f a)
      x) =
    do
    let a ← y
    let _ ← pure (f a)
    x

Tactic:
rw [← bind_assoc, ← map_eq_pure_bind, h', map_eq_pure_bind, bind_assoc]

Result:
no goals