[GOAL]
α β : Type u
m : Type u → Type v
x : OptionT m α
inst✝¹ : Monad m
f : α → β
inst✝ : LawfulMonad m
⊢ run (f <$> x) = Option.map f <$> run x
[PROOFSTEP]
rw [← bind_pure_comp _ x.run]
[GOAL]
α β : Type u
m : Type u → Type v
x : OptionT m α
inst✝¹ : Monad m
f : α → β
inst✝ : LawfulMonad m
⊢ run (f <$> x) = do
    let a ← run x
    pure (Option.map f a)
[PROOFSTEP]
change
  x.run >>=
      (fun
        | some a => OptionT.run (pure (f a))
        | none => pure none) =
    _
[GOAL]
α β : Type u
m : Type u → Type v
x : OptionT m α
inst✝¹ : Monad m
f : α → β
inst✝ : LawfulMonad m
⊢ (do
      let x ← run x
      match x with
        | some a => run (pure (f a))
        | none => pure none) =
    do
    let a ← run x
    pure (Option.map f a)
[PROOFSTEP]
apply bind_congr
[GOAL]
case h
α β : Type u
m : Type u → Type v
x : OptionT m α
inst✝¹ : Monad m
f : α → β
inst✝ : LawfulMonad m
⊢ ∀ (a : Option α),
    (match a with
      | some a => run (pure (f a))
      | none => pure none) =
      pure (Option.map f a)
[PROOFSTEP]
intro a
[GOAL]
case h
α β : Type u
m : Type u → Type v
x : OptionT m α
inst✝¹ : Monad m
f : α → β
inst✝ : LawfulMonad m
a : Option α
⊢ (match a with
    | some a => run (pure (f a))
    | none => pure none) =
    pure (Option.map f a)
[PROOFSTEP]
cases a
[GOAL]
case h.none
α β : Type u
m : Type u → Type v
x : OptionT m α
inst✝¹ : Monad m
f : α → β
inst✝ : LawfulMonad m
⊢ (match none with
    | some a => run (pure (f a))
    | none => pure none) =
    pure (Option.map f none)
[PROOFSTEP]
simp [Option.map, Option.bind]
[GOAL]
case h.some
α β : Type u
m : Type u → Type v
x : OptionT m α
inst✝¹ : Monad m
f : α → β
inst✝ : LawfulMonad m
val✝ : α
⊢ (match some val✝ with
    | some a => run (pure (f a))
    | none => pure none) =
    pure (Option.map f (some val✝))
[PROOFSTEP]
simp [Option.map, Option.bind]
[GOAL]
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ ∀ {α : Type u} (x : OptionT m α), id <$> x = x
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ : Type u
x✝ : OptionT m α✝
⊢ id <$> x✝ = x✝
[PROOFSTEP]
apply OptionT.ext
[GOAL]
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ : Type u
x✝ : OptionT m α✝
⊢ OptionT.run (id <$> x✝) = OptionT.run x✝
[PROOFSTEP]
simp only [OptionT.run_map]
[GOAL]
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ : Type u
x✝ : OptionT m α✝
⊢ Option.map id <$> OptionT.run x✝ = OptionT.run x✝
[PROOFSTEP]
rw [map_congr, id_map]
[GOAL]
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ : Type u
x✝ : OptionT m α✝
⊢ ∀ (a : Option α✝), Option.map id a = id a
[PROOFSTEP]
intro a
[GOAL]
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ : Type u
x✝ : OptionT m α✝
a : Option α✝
⊢ Option.map id a = id a
[PROOFSTEP]
cases a
[GOAL]
case h.none
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ : Type u
x✝ : OptionT m α✝
⊢ Option.map id none = id none
[PROOFSTEP]
rfl
[GOAL]
case h.some
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ : Type u
x✝ : OptionT m α✝
val✝ : α✝
⊢ Option.map id (some val✝) = id (some val✝)
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ ∀ {α β : Type u} (x : α) (f : α → OptionT m β), pure x >>= f = f x
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ β✝ : Type u
x✝ : α✝
f✝ : α✝ → OptionT m β✝
⊢ pure x✝ >>= f✝ = f✝ x✝
[PROOFSTEP]
apply OptionT.ext
[GOAL]
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ β✝ : Type u
x✝ : α✝
f✝ : α✝ → OptionT m β✝
⊢ OptionT.run (pure x✝ >>= f✝) = OptionT.run (f✝ x✝)
[PROOFSTEP]
simp
[GOAL]
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ ∀ {α β γ : Type u} (x : OptionT m α) (f : α → OptionT m β) (g : β → OptionT m γ),
    x >>= f >>= g = x >>= fun x => f x >>= g
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ β✝ γ✝ : Type u
x✝ : OptionT m α✝
f✝ : α✝ → OptionT m β✝
g✝ : β✝ → OptionT m γ✝
⊢ x✝ >>= f✝ >>= g✝ = x✝ >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
apply OptionT.ext
[GOAL]
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ β✝ γ✝ : Type u
x✝ : OptionT m α✝
f✝ : α✝ → OptionT m β✝
g✝ : β✝ → OptionT m γ✝
⊢ OptionT.run (x✝ >>= f✝ >>= g✝) = OptionT.run (x✝ >>= fun x => f✝ x >>= g✝)
[PROOFSTEP]
simp only [OptionT.run_bind, bind_assoc]
[GOAL]
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ β✝ γ✝ : Type u
x✝ : OptionT m α✝
f✝ : α✝ → OptionT m β✝
g✝ : β✝ → OptionT m γ✝
⊢ (do
      let x ← OptionT.run x✝
      let x ←
        match x with
          | some a => OptionT.run (f✝ a)
          | none => pure none
      match x with
        | some a => OptionT.run (g✝ a)
        | none => pure none) =
    do
    let x ← OptionT.run x✝
    match x with
      | some a => do
        let x ← OptionT.run (f✝ a)
        match x with
          | some a => OptionT.run (g✝ a)
          | none => pure none
      | none => pure none
[PROOFSTEP]
rw [bind_congr]
[GOAL]
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ β✝ γ✝ : Type u
x✝ : OptionT m α✝
f✝ : α✝ → OptionT m β✝
g✝ : β✝ → OptionT m γ✝
⊢ ∀ (a : Option α✝),
    (do
        let x ←
          match a with
            | some a => OptionT.run (f✝ a)
            | none => pure none
        match x with
          | some a => OptionT.run (g✝ a)
          | none => pure none) =
      match a with
      | some a => do
        let x ← OptionT.run (f✝ a)
        match x with
          | some a => OptionT.run (g✝ a)
          | none => pure none
      | none => pure none
[PROOFSTEP]
intro a
[GOAL]
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ β✝ γ✝ : Type u
x✝ : OptionT m α✝
f✝ : α✝ → OptionT m β✝
g✝ : β✝ → OptionT m γ✝
a : Option α✝
⊢ (do
      let x ←
        match a with
          | some a => OptionT.run (f✝ a)
          | none => pure none
      match x with
        | some a => OptionT.run (g✝ a)
        | none => pure none) =
    match a with
    | some a => do
      let x ← OptionT.run (f✝ a)
      match x with
        | some a => OptionT.run (g✝ a)
        | none => pure none
    | none => pure none
[PROOFSTEP]
cases a
[GOAL]
case h.none
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ β✝ γ✝ : Type u
x✝ : OptionT m α✝
f✝ : α✝ → OptionT m β✝
g✝ : β✝ → OptionT m γ✝
⊢ (do
      let x ←
        match none with
          | some a => OptionT.run (f✝ a)
          | none => pure none
      match x with
        | some a => OptionT.run (g✝ a)
        | none => pure none) =
    match none with
    | some a => do
      let x ← OptionT.run (f✝ a)
      match x with
        | some a => OptionT.run (g✝ a)
        | none => pure none
    | none => pure none
[PROOFSTEP]
simp
[GOAL]
case h.some
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ β✝ γ✝ : Type u
x✝ : OptionT m α✝
f✝ : α✝ → OptionT m β✝
g✝ : β✝ → OptionT m γ✝
val✝ : α✝
⊢ (do
      let x ←
        match some val✝ with
          | some a => OptionT.run (f✝ a)
          | none => pure none
      match x with
        | some a => OptionT.run (g✝ a)
        | none => pure none) =
    match some val✝ with
    | some a => do
      let x ← OptionT.run (f✝ a)
      match x with
        | some a => OptionT.run (g✝ a)
        | none => pure none
    | none => pure none
[PROOFSTEP]
simp
