-- Mathlib/.lake/packages/batteries/Batteries/Classes/SatisfiesM.lean
theorem SatisfiesM_ExceptT_eq [Monad m] [LawfulMonad m] :
    SatisfiesM (m := ExceptT ρ m) (α := α) p x ↔
      SatisfiesM (m := m) (∀ a, · = .ok a → p a) x.run

Proof state:
case refine_2.e_a
m : Type u_1 → Type u_2
α ρ : Type u_1
p : α → Prop
x : ExceptT ρ m α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x✝ : SatisfiesM (fun x => ∀ (a : α), x = Except.ok a → p a) x
f : m { a // (fun x => ∀ (a : α), x = Except.ok a → p a) a }
eq : Subtype.val <$> f = x
⊢ (fun x =>
      match
        match x with
        | ⟨Except.ok a, h⟩ => Except.ok ⟨a, ⋯⟩
        | ⟨Except.error e, property⟩ => Except.error e with
      | Except.ok a => pure (Except.ok a.val)
      | Except.error e => pure (Except.error e)) =
    fun a => pure a.val

Tactic:
funext ⟨a, h⟩

Result:
case refine_2.e_a.h
m : Type u_1 → Type u_2
α ρ : Type u_1
p : α → Prop
x : ExceptT ρ m α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x✝ : SatisfiesM (fun x => ∀ (a : α), x = Except.ok a → p a) x
f : m { a // (fun x => ∀ (a : α), x = Except.ok a → p a) a }
eq : Subtype.val <$> f = x
a : Except ρ α
h : ∀ (a_1 : α), a = Except.ok a_1 → p a_1
⊢ (match
      match ⟨a, h⟩ with
      | ⟨Except.ok a, h⟩ => Except.ok ⟨a, ⋯⟩
      | ⟨Except.error e, property⟩ => Except.error e with
    | Except.ok a => pure (Except.ok a.val)
    | Except.error e => pure (Except.error e)) =
    pure ⟨a, h⟩.val

Proof state:
case refine_2
m : Type u_1 → Type u_2
α ρ : Type u_1
p : α → Prop
x : ExceptT ρ m α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x✝ : SatisfiesM (fun x => ∀ (a : α), x = Except.ok a → p a) x
f : m { a // (fun x => ∀ (a : α), x = Except.ok a → p a) a }
eq : Subtype.val <$> f = x
⊢ (do
      let a ←
        (fun x =>
              match x with
              | ⟨Except.ok a, h⟩ => Except.ok ⟨a, ⋯⟩
              | ⟨Except.error e, property⟩ => Except.error e) <$>
            f
      match a with
        | Except.ok a => pure (Except.ok a.val)
        | Except.error e => pure (Except.error e)) =
    Subtype.val <$> f

Tactic:
simp [← comp_map, ← bind_pure_comp]

Result:
case refine_2
m : Type u_1 → Type u_2
α ρ : Type u_1
p : α → Prop
x : ExceptT ρ m α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x✝ : SatisfiesM (fun x => ∀ (a : α), x = Except.ok a → p a) x
f : m { a // (fun x => ∀ (a : α), x = Except.ok a → p a) a }
eq : Subtype.val <$> f = x
⊢ (do
      let x ← f
      match
          match x with
          | ⟨Except.ok a, h⟩ => Except.ok ⟨a, ⋯⟩
          | ⟨Except.error e, property⟩ => Except.error e with
        | Except.ok a => pure (Except.ok a.val)
        | Except.error e => pure (Except.error e)) =
    do
    let a ← f
    pure a.val

Proof state:
case refine_2.e_a.h
m : Type u_1 → Type u_2
α ρ : Type u_1
p : α → Prop
x : ExceptT ρ m α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x✝ : SatisfiesM (fun x => ∀ (a : α), x = Except.ok a → p a) x
f : m { a // (fun x => ∀ (a : α), x = Except.ok a → p a) a }
eq : Subtype.val <$> f = x
a : Except ρ α
h : ∀ (a_1 : α), a = Except.ok a_1 → p a_1
⊢ (match
      match ⟨a, h⟩ with
      | ⟨Except.ok a, h⟩ => Except.ok ⟨a, ⋯⟩
      | ⟨Except.error e, property⟩ => Except.error e with
    | Except.ok a => pure (Except.ok a.val)
    | Except.error e => pure (Except.error e)) =
    pure ⟨a, h⟩.val

Tactic:
cases a <;> rfl

Result:
no goals

Proof state:
case refine_2
m : Type u_1 → Type u_2
α ρ : Type u_1
p : α → Prop
x : ExceptT ρ m α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x✝ : SatisfiesM (fun x => ∀ (a : α), x = Except.ok a → p a) x
f : m { a // (fun x => ∀ (a : α), x = Except.ok a → p a) a }
eq : Subtype.val <$> f = x
⊢ Subtype.val <$>
      (fun x =>
          match x with
          | ⟨Except.ok a, h⟩ => Except.ok ⟨a, ⋯⟩
          | ⟨Except.error e, property⟩ => Except.error e) <$>
        f =
    Subtype.val <$> f

Tactic:
show _ >>= _ = _

Result:
case refine_2
m : Type u_1 → Type u_2
α ρ : Type u_1
p : α → Prop
x : ExceptT ρ m α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x✝ : SatisfiesM (fun x => ∀ (a : α), x = Except.ok a → p a) x
f : m { a // (fun x => ∀ (a : α), x = Except.ok a → p a) a }
eq : Subtype.val <$> f = x
⊢ (do
      let a ←
        (fun x =>
              match x with
              | ⟨Except.ok a, h⟩ => Except.ok ⟨a, ⋯⟩
              | ⟨Except.error e, property⟩ => Except.error e) <$>
            f
      match a with
        | Except.ok a => pure (Except.ok a.val)
        | Except.error e => pure (Except.error e)) =
    Subtype.val <$> f

Proof state:
case refine_1.e_a
m : Type u_1 → Type u_2
α ρ : Type u_1
p : α → Prop
x : ExceptT ρ m α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x✝ : SatisfiesM p x
f : ExceptT ρ m { a // p a }
eq : Subtype.val <$> f = x
⊢ (fun a =>
      pure
        ((Subtype.val ∘ fun x =>
            match x with
            | Except.ok ⟨a, h⟩ => ⟨Except.ok a, ⋯⟩
            | Except.error e => ⟨Except.error e, ⋯⟩)
          a)) =
    fun a =>
    match a with
    | Except.ok a => pure (Except.ok a.val)
    | Except.error e => pure (Except.error e)

Tactic:
funext a

Result:
case refine_1.e_a.h
m : Type u_1 → Type u_2
α ρ : Type u_1
p : α → Prop
x : ExceptT ρ m α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x✝ : SatisfiesM p x
f : ExceptT ρ m { a // p a }
eq : Subtype.val <$> f = x
a : Except ρ { a // p a }
⊢ pure
      ((Subtype.val ∘ fun x =>
          match x with
          | Except.ok ⟨a, h⟩ => ⟨Except.ok a, ⋯⟩
          | Except.error e => ⟨Except.error e, ⋯⟩)
        a) =
    match a with
    | Except.ok a => pure (Except.ok a.val)
    | Except.error e => pure (Except.error e)

Proof state:
m : Type u_1 → Type u_2
α ρ : Type u_1
p : α → Prop
x : ExceptT ρ m α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ SatisfiesM p x ↔ SatisfiesM (fun x => ∀ (a : α), x = Except.ok a → p a) x

Tactic:
refine ⟨fun ⟨f, eq⟩ => eq ▸ ?_, fun ⟨f, eq⟩ => eq ▸ ?_⟩

Result:
case refine_1
m : Type u_1 → Type u_2
α ρ : Type u_1
p : α → Prop
x : ExceptT ρ m α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x✝ : SatisfiesM p x
f : ExceptT ρ m { a // p a }
eq : Subtype.val <$> f = x
⊢ SatisfiesM (fun x => ∀ (a : α), x = Except.ok a → p a) (Subtype.val <$> f)

case refine_2
m : Type u_1 → Type u_2
α ρ : Type u_1
p : α → Prop
x : ExceptT ρ m α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x✝ : SatisfiesM (fun x => ∀ (a : α), x = Except.ok a → p a) x
f : m { a // (fun x => ∀ (a : α), x = Except.ok a → p a) a }
eq : Subtype.val <$> f = x
⊢ SatisfiesM p (Subtype.val <$> f)

Proof state:
case refine_1
m : Type u_1 → Type u_2
α ρ : Type u_1
p : α → Prop
x : ExceptT ρ m α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x✝ : SatisfiesM p x
f : ExceptT ρ m { a // p a }
eq : Subtype.val <$> f = x
⊢ Subtype.val <$>
      (fun x =>
          match x with
          | Except.ok ⟨a, h⟩ => ⟨Except.ok a, ⋯⟩
          | Except.error e => ⟨Except.error e, ⋯⟩) <$>
        f =
    do
    let a ← f
    match a with
      | Except.ok a => pure (Except.ok a.val)
      | Except.error e => pure (Except.error e)

Tactic:
rw [← comp_map, map_eq_pure_bind]

Result:
case refine_1
m : Type u_1 → Type u_2
α ρ : Type u_1
p : α → Prop
x : ExceptT ρ m α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x✝ : SatisfiesM p x
f : ExceptT ρ m { a // p a }
eq : Subtype.val <$> f = x
⊢ (do
      let a ← f
      pure
          ((Subtype.val ∘ fun x =>
              match x with
              | Except.ok ⟨a, h⟩ => ⟨Except.ok a, ⋯⟩
              | Except.error e => ⟨Except.error e, ⋯⟩)
            a)) =
    do
    let a ← f
    match a with
      | Except.ok a => pure (Except.ok a.val)
      | Except.error e => pure (Except.error e)