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
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)
refine .trans ⟨fun ⟨f, eq⟩ => eq ▸ ?_, fun ⟨f, h⟩ => ?_⟩ Classical.skolem.symm
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
              | ({ val := a, property := h }, s') => { val := (a, s'), property := h }) <$>
            f s)
        s =
    (Subtype.val <$> f) s
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
refine ⟨fun s => (fun ⟨⟨a, h⟩, s'⟩ => ⟨⟨a, s'⟩, h⟩) <$> f s, fun s => ?_⟩
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
              | ({ val := a, property := h }, s') => { val := (a, s'), property := h })
            a)) =
    (Subtype.val <$> f) s
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
              | ({ val := a, property := h }, s') => { val := (a, s'), property := h }) <$>
            f s)
        s =
    (Subtype.val <$> f) s
rw [← comp_map, map_eq_pure_bind]
no goals
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
              | ({ val := a, property := h }, s') => { val := (a, s'), property := h })
            a)) =
    (Subtype.val <$> f) s
rfl
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
            | { val := (a, s'), property := h } => ({ val := a, property := h }, s')) <$>
          f s)
      s =
    x s
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
refine ⟨fun s => (fun ⟨⟨a, s'⟩, h⟩ => ⟨⟨a, h⟩, s'⟩) <$> f s, funext fun s => ?_⟩
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
                  | { val := (a, s'), property := h } => ({ val := a, property := h }, s')) <$>
                f s)
            s
      match __discr with
        | (a, s) => pure (a.val, s)) =
    x s
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
            | { val := (a, s'), property := h } => ({ val := a, property := h }, s')) <$>
          f s)
      s =
    x s
show _ >>= _ = _
no goals
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
                  | { val := (a, s'), property := h } => ({ val := a, property := h }, s')) <$>
                f s)
            s
      match __discr with
        | (a, s) => pure (a.val, s)) =
    x s
simp [map_eq_pure_bind, ← h]