-- Mathlib/.lake/packages/batteries/Batteries/Classes/SatisfiesM.lean
theorem SatisfiesM_StateT_eq [Monad m] [LawfulMonad m] :
    SatisfiesM (m := StateT ρ m) (α := α) p x ↔ ∀ s, SatisfiesM (m := m) (p ·.1) (x.run s)

Proof state:
case refine_1
m : Type u_1 → Type u_2
α ρ : Type u_1
p : α → Prop
x : StateT ρ m α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x✝ : SatisfiesM p x
f : StateT ρ m { a // p a }
eq : Subtype.val <$> f = x
⊢ ∃ f_1, ∀ (x : ρ), Subtype.val <$> f_1 x = (Subtype.val <$> f) x

Tactic:
refine ⟨fun s => (fun ⟨⟨a, h⟩, s'⟩ => ⟨⟨a, s'⟩, h⟩) <$> f s, fun s => ?_⟩

Result:
case refine_1
m : Type u_1 → Type u_2
α ρ : Type u_1
p : α → Prop
x : StateT ρ m α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x✝ : SatisfiesM p x
f : StateT ρ m { a // p a }
eq : Subtype.val <$> f = x
s : ρ
⊢ Subtype.val <$>
      (fun s =>
          (fun x =>
              match x with
              | (⟨a, h⟩, s') => ⟨(a, s'), h⟩) <$>
            f s)
        s =
    (Subtype.val <$> f) s

Proof state:
case refine_2
m : Type u_1 → Type u_2
α ρ : Type u_1
p : α → Prop
x : StateT ρ m α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x✝ : ∃ f, ∀ (x_1 : ρ), Subtype.val <$> f x_1 = x x_1
f : ρ → m { a // (fun x => p x.fst) a }
h : ∀ (x_1 : ρ), Subtype.val <$> f x_1 = x x_1
⊢ SatisfiesM p x

Tactic:
refine ⟨fun s => (fun ⟨⟨a, s'⟩, h⟩ => ⟨⟨a, h⟩, s'⟩) <$> f s, funext fun s => ?_⟩

Result:
case refine_2
m : Type u_1 → Type u_2
α ρ : Type u_1
p : α → Prop
x : StateT ρ m α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x✝ : ∃ f, ∀ (x_1 : ρ), Subtype.val <$> f x_1 = x x_1
f : ρ → m { a // (fun x => p x.fst) a }
h : ∀ (x_1 : ρ), Subtype.val <$> f x_1 = x x_1
s : ρ
⊢ (Subtype.val <$> fun s =>
        (fun x =>
            match x with
            | ⟨(a, s'), h⟩ => (⟨a, h⟩, s')) <$>
          f s)
      s =
    x s

Proof state:
case refine_2
m : Type u_1 → Type u_2
α ρ : Type u_1
p : α → Prop
x : StateT ρ m α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x✝ : ∃ f, ∀ (x_1 : ρ), Subtype.val <$> f x_1 = x x_1
f : ρ → m { a // (fun x => p x.fst) a }
h : ∀ (x_1 : ρ), Subtype.val <$> f x_1 = x x_1
s : ρ
⊢ (Subtype.val <$> fun s =>
        (fun x =>
            match x with
            | ⟨(a, s'), h⟩ => (⟨a, h⟩, s')) <$>
          f s)
      s =
    x s

Tactic:
show _ >>= _ = _

Result:
case refine_2
m : Type u_1 → Type u_2
α ρ : Type u_1
p : α → Prop
x : StateT ρ m α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x✝ : ∃ f, ∀ (x_1 : ρ), Subtype.val <$> f x_1 = x x_1
f : ρ → m { a // (fun x => p x.fst) a }
h : ∀ (x_1 : ρ), Subtype.val <$> f x_1 = x x_1
s : ρ
⊢ (do
      let __discr ←
        (fun s =>
              (fun x =>
                  match x with
                  | ⟨(a, s'), h⟩ => (⟨a, h⟩, s')) <$>
                f s)
            s
      match __discr with
        | (a, s) => pure (a.val, s)) =
    x s

Proof state:
case refine_1
m : Type u_1 → Type u_2
α ρ : Type u_1
p : α → Prop
x : StateT ρ m α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x✝ : SatisfiesM p x
f : StateT ρ m { a // p a }
eq : Subtype.val <$> f = x
s : ρ
⊢ Subtype.val <$>
      (fun s =>
          (fun x =>
              match x with
              | (⟨a, h⟩, s') => ⟨(a, s'), h⟩) <$>
            f s)
        s =
    (Subtype.val <$> f) s

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 : StateT ρ m α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x✝ : SatisfiesM p x
f : StateT ρ m { a // p a }
eq : Subtype.val <$> f = x
s : ρ
⊢ (do
      let a ← f s
      pure
          ((Subtype.val ∘ fun x =>
              match x with
              | (⟨a, h⟩, s') => ⟨(a, s'), h⟩)
            a)) =
    (Subtype.val <$> f) s

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

Tactic:
rfl

Result:
no goals

Proof state:
case refine_2
m : Type u_1 → Type u_2
α ρ : Type u_1
p : α → Prop
x : StateT ρ m α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x✝ : ∃ f, ∀ (x_1 : ρ), Subtype.val <$> f x_1 = x x_1
f : ρ → m { a // (fun x => p x.fst) a }
h : ∀ (x_1 : ρ), Subtype.val <$> f x_1 = x x_1
s : ρ
⊢ (do
      let __discr ←
        (fun s =>
              (fun x =>
                  match x with
                  | ⟨(a, s'), h⟩ => (⟨a, h⟩, s')) <$>
                f s)
            s
      match __discr with
        | (a, s) => pure (a.val, s)) =
    x s

Tactic:
simp [← h]

Result:
no goals

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

Tactic:
refine .trans ⟨fun ⟨f, eq⟩ => eq ▸ ?_, fun ⟨f, h⟩ => ?_⟩ Classical.skolem.symm

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

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