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)
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
refine ⟨fun ⟨f, eq⟩ => eq ▸ ?_, fun ⟨f, eq⟩ => eq ▸ ?_⟩
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 { val := a, property := h } =>
            { val := Except.ok a, property := (_ : ∀ (x : α), Except.ok a = Except.ok x → p x) }
          | Except.error e =>
            { val := Except.error e, property := (_ : ∀ (a : α), Except.error e = Except.ok a → p a) }) <$>
        f =
    Subtype.val <$> f
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)
exists (fun | .ok ⟨a, h⟩ => ⟨.ok a, fun | _, rfl => h⟩ | .error e => ⟨.error e, fun.⟩) <$> f
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 { val := a, property := h } =>
            { val := Except.ok a, property := (_ : ∀ (x : α), Except.ok a = Except.ok x → p x) }
          | Except.error e =>
            { val := Except.error e, property := (_ : ∀ (a : α), Except.error e = Except.ok a → p a) }) <$>
        f =
    do
    let a ← f
    match a with
      | Except.ok a => pure (Except.ok a.val)
      | Except.error e => pure (Except.error e)
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 { val := a, property := h } =>
            { val := Except.ok a, property := (_ : ∀ (x : α), Except.ok a = Except.ok x → p x) }
          | Except.error e =>
            { val := Except.error e, property := (_ : ∀ (a : α), Except.error e = Except.ok a → p a) }) <$>
        f =
    Subtype.val <$> f
show _ = _ >>= _
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 { val := a, property := h } =>
                { val := Except.ok a, property := (_ : ∀ (x : α), Except.ok a = Except.ok x → p x) }
              | Except.error e =>
                { val := Except.error e, property := (_ : ∀ (a : α), Except.error e = Except.ok a → p a) })
            a)) =
    do
    let a ← f
    match a with
      | Except.ok a => pure (Except.ok a.val)
      | Except.error e => pure (Except.error e)
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 { val := a, property := h } =>
            { val := Except.ok a, property := (_ : ∀ (x : α), Except.ok a = Except.ok x → p x) }
          | Except.error e =>
            { val := Except.error e, property := (_ : ∀ (a : α), Except.error e = Except.ok a → p a) }) <$>
        f =
    do
    let a ← f
    match a with
      | Except.ok a => pure (Except.ok a.val)
      | Except.error e => pure (Except.error e)
rw [← comp_map, map_eq_pure_bind]
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 { val := a, property := h } =>
              { val := Except.ok a, property := (_ : ∀ (x : α), Except.ok a = Except.ok x → p x) }
            | Except.error e =>
              { val := Except.error e, property := (_ : ∀ (a : α), Except.error e = Except.ok a → p a) })
          a)) =
    fun a =>
    match a with
    | Except.ok a => pure (Except.ok a.val)
    | Except.error e => pure (Except.error e)
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 { val := a, property := h } =>
                { val := Except.ok a, property := (_ : ∀ (x : α), Except.ok a = Except.ok x → p x) }
              | Except.error e =>
                { val := Except.error e, property := (_ : ∀ (a : α), Except.error e = Except.ok a → p a) })
            a)) =
    do
    let a ← f
    match a with
      | Except.ok a => pure (Except.ok a.val)
      | Except.error e => pure (Except.error e)
congr
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 { val := a, property := h } =>
            { val := Except.ok a, property := (_ : ∀ (x : α), Except.ok a = Except.ok x → p x) }
          | Except.error e =>
            { val := Except.error e, property := (_ : ∀ (a : α), Except.error e = Except.ok a → p a) })
        a) =
    match a with
    | Except.ok a => pure (Except.ok a.val)
    | Except.error e => pure (Except.error e)
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 { val := a, property := h } =>
              { val := Except.ok a, property := (_ : ∀ (x : α), Except.ok a = Except.ok x → p x) }
            | Except.error e =>
              { val := Except.error e, property := (_ : ∀ (a : α), Except.error e = Except.ok a → p a) })
          a)) =
    fun a =>
    match a with
    | Except.ok a => pure (Except.ok a.val)
    | Except.error e => pure (Except.error e)
funext a
no goals
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 { val := a, property := h } =>
            { val := Except.ok a, property := (_ : ∀ (x : α), Except.ok a = Except.ok x → p x) }
          | Except.error e =>
            { val := Except.error e, property := (_ : ∀ (a : α), Except.error e = Except.ok a → p a) })
        a) =
    match a with
    | Except.ok a => pure (Except.ok a.val)
    | Except.error e => pure (Except.error e)
cases a <;> rfl
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
          | { val := Except.ok a, property := h } => Except.ok { val := a, property := (_ : p a) }
          | { val := Except.error e, property := property } => Except.error e) <$>
        f =
    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)
exists ((fun | ⟨.ok a, h⟩ => .ok ⟨a, h _ rfl⟩ | ⟨.error e, _⟩ => .error e) <$> f : m _)
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
              | { val := Except.ok a, property := h } => Except.ok { val := a, property := (_ : p a) }
              | { val := Except.error e, property := 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
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
          | { val := Except.ok a, property := h } => Except.ok { val := a, property := (_ : p a) }
          | { val := Except.error e, property := property } => Except.error e) <$>
        f =
    Subtype.val <$> f
show _ >>= _ = _
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
          | { val := Except.ok a, property := h } => Except.ok { val := a, property := (_ : p a) }
          | { val := Except.error e, property := 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
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
              | { val := Except.ok a, property := h } => Except.ok { val := a, property := (_ : p a) }
              | { val := Except.error e, property := 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
simp [← comp_map, map_eq_pure_bind]
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
        | { val := Except.ok a, property := h } => Except.ok { val := a, property := (_ : p a) }
        | { val := Except.error e, property := 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
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
          | { val := Except.ok a, property := h } => Except.ok { val := a, property := (_ : p a) }
          | { val := Except.error e, property := 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
congr
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 { val := a, property := h } with
      | { val := Except.ok a, property := h } => Except.ok { val := a, property := (_ : p a) }
      | { val := Except.error e, property := property } => Except.error e with
    | Except.ok a => pure (Except.ok a.val)
    | Except.error e => pure (Except.error e)) =
    pure { val := a, property := h }.val
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
        | { val := Except.ok a, property := h } => Except.ok { val := a, property := (_ : p a) }
        | { val := Except.error e, property := 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
funext ⟨a, h⟩
no goals
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 { val := a, property := h } with
      | { val := Except.ok a, property := h } => Except.ok { val := a, property := (_ : p a) }
      | { val := Except.error e, property := property } => Except.error e with
    | Except.ok a => pure (Except.ok a.val)
    | Except.error e => pure (Except.error e)) =
    pure { val := a, property := h }.val
cases a <;> rfl