-- Mathlib/.lake/packages/batteries/Batteries/Classes/SatisfiesM.lean
theorem bind [Monad m] [LawfulMonad m] {f : α → m β}
    (hx : SatisfiesM p x) (hf : ∀ a, p a → SatisfiesM q (f a)) :
    SatisfiesM q (x >>= f)

Proof state:
m : Type u_1 → Type u_2
α β : Type u_1
p : α → Prop
x✝ : m α
q : β → Prop
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
hx : SatisfiesM p x✝
hf : ∀ (a : α), p a → SatisfiesM q (f a)
x : m { a // p a }
g : (a : α) → p a → { x // Subtype.val <$> x = f a }
⊢ SatisfiesM q (Subtype.val <$> x >>= f)

Tactic:
refine ⟨x >>= fun ⟨a, h⟩ => g a h, ?_⟩

Result:
m : Type u_1 → Type u_2
α β : Type u_1
p : α → Prop
x✝ : m α
q : β → Prop
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
hx : SatisfiesM p x✝
hf : ∀ (a : α), p a → SatisfiesM q (f a)
x : m { a // p a }
g : (a : α) → p a → { x // Subtype.val <$> x = f a }
⊢ (Subtype.val <$> do
      let x ← x
      match x with
        | ⟨a, h⟩ => (g a h).val) =
    Subtype.val <$> x >>= f

Proof state:
case e_a.h
m : Type u_1 → Type u_2
α β : Type u_1
p : α → Prop
x✝ : m α
q : β → Prop
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
hx : SatisfiesM p x✝
hf : ∀ (a : α), p a → SatisfiesM q (f a)
x : m { a // p a }
g : (a : α) → p a → { x // Subtype.val <$> x = f a }
a : α
h : p a
⊢ (do
      let a ← (g ⟨a, h⟩.val ⋯).val
      pure a.val) =
    f ⟨a, h⟩.val

Tactic:
simp [← (g a h).2, ← bind_pure_comp]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α β : Type u_1
p : α → Prop
x✝ : m α
q : β → Prop
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
hx : SatisfiesM p x✝
hf : ∀ (a : α), p a → SatisfiesM q (f a)
x : m { a // p a }
g : (a : α) → p a → { x // Subtype.val <$> x = f a }
⊢ (do
      let x ← x
      let a ← (g x.val ⋯).val
      pure a.val) =
    do
    let x ← x
    f x.val

Tactic:
congr

Result:
case e_a
m : Type u_1 → Type u_2
α β : Type u_1
p : α → Prop
x✝ : m α
q : β → Prop
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
hx : SatisfiesM p x✝
hf : ∀ (a : α), p a → SatisfiesM q (f a)
x : m { a // p a }
g : (a : α) → p a → { x // Subtype.val <$> x = f a }
⊢ (fun x => do
      let a ← (g x.val ⋯).val
      pure a.val) =
    fun x => f x.val

Proof state:
m : Type u_1 → Type u_2
α β : Type u_1
p : α → Prop
x : m α
q : β → Prop
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
hx : SatisfiesM p x
hf : ∀ (a : α), p a → SatisfiesM q (f a)
⊢ SatisfiesM q (x >>= f)

Tactic:
match x, hx with | _, ⟨x, rfl⟩ => ?_

Result:
m : Type u_1 → Type u_2
α β : Type u_1
p : α → Prop
x✝ : m α
q : β → Prop
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
hx : SatisfiesM p x✝
hf : ∀ (a : α), p a → SatisfiesM q (f a)
x : m { a // p a }
⊢ SatisfiesM q (Subtype.val <$> x >>= f)

Proof state:
m : Type u_1 → Type u_2
α β : Type u_1
p : α → Prop
x✝ : m α
q : β → Prop
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
hx : SatisfiesM p x✝
hf : ∀ (a : α), p a → SatisfiesM q (f a)
x : m { a // p a }
⊢ SatisfiesM q (Subtype.val <$> x >>= f)

Tactic:
have g a ha := Classical.indefiniteDescription _ (hf a ha)

Result:
m : Type u_1 → Type u_2
α β : Type u_1
p : α → Prop
x✝ : m α
q : β → Prop
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
hx : SatisfiesM p x✝
hf : ∀ (a : α), p a → SatisfiesM q (f a)
x : m { a // p a }
g : (a : α) → p a → { x // Subtype.val <$> x = f a }
⊢ SatisfiesM q (Subtype.val <$> x >>= f)

Proof state:
case e_a
m : Type u_1 → Type u_2
α β : Type u_1
p : α → Prop
x✝ : m α
q : β → Prop
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
hx : SatisfiesM p x✝
hf : ∀ (a : α), p a → SatisfiesM q (f a)
x : m { a // p a }
g : (a : α) → p a → { x // Subtype.val <$> x = f a }
⊢ (fun x => do
      let a ← (g x.val ⋯).val
      pure a.val) =
    fun x => f x.val

Tactic:
funext ⟨a, h⟩

Result:
case e_a.h
m : Type u_1 → Type u_2
α β : Type u_1
p : α → Prop
x✝ : m α
q : β → Prop
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
hx : SatisfiesM p x✝
hf : ∀ (a : α), p a → SatisfiesM q (f a)
x : m { a // p a }
g : (a : α) → p a → { x // Subtype.val <$> x = f a }
a : α
h : p a
⊢ (do
      let a ← (g ⟨a, h⟩.val ⋯).val
      pure a.val) =
    f ⟨a, h⟩.val

Proof state:
m : Type u_1 → Type u_2
α β : Type u_1
p : α → Prop
x✝ : m α
q : β → Prop
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
hx : SatisfiesM p x✝
hf : ∀ (a : α), p a → SatisfiesM q (f a)
x : m { a // p a }
g : (a : α) → p a → { x // Subtype.val <$> x = f a }
⊢ (Subtype.val <$> do
      let x ← x
      match x with
        | ⟨a, h⟩ => (g a h).val) =
    Subtype.val <$> x >>= f

Tactic:
simp [← bind_pure_comp]

Result:
m : Type u_1 → Type u_2
α β : Type u_1
p : α → Prop
x✝ : m α
q : β → Prop
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
hx : SatisfiesM p x✝
hf : ∀ (a : α), p a → SatisfiesM q (f a)
x : m { a // p a }
g : (a : α) → p a → { x // Subtype.val <$> x = f a }
⊢ (do
      let x ← x
      let a ← (g x.val ⋯).val
      pure a.val) =
    do
    let x ← x
    f x.val