-- 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
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

Tactic:
congr

Result:
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

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
⊢ SatisfiesM (fun x => ∀ (a : α), x = Except.ok a → p a) (Subtype.val <$> f)

Tactic:
exists (fun | .ok ⟨a, h⟩ => ⟨.ok a, fun | _, rfl => h⟩ | .error e => ⟨.error e, nofun⟩) <$> f

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
⊢ Subtype.val <$>
      (fun x =>
          match x with
          | Except.ok ⟨a, h⟩ => ⟨Except.ok a, ⋯⟩
          | Except.error e => ⟨Except.error e, ⋯⟩) <$>
        f =
    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
⊢ (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)

Tactic:
congr

Result:
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)

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 =
    Subtype.val <$> f

Tactic:
show _ = _ >>= _

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
⊢ 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)

Proof state:
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)

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
⊢ SatisfiesM p (Subtype.val <$> f)

Tactic:
exists ((fun | ⟨.ok a, h⟩ => .ok ⟨a, h _ rfl⟩ | ⟨.error e, _⟩ => .error e) <$> f : m _)

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
⊢ 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