m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
y : m β
⊢ (Seq.seq (const β <$> x) fun x => y) = do
    let a ← x
    let _ ← y
    pure a
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
y : m β
⊢ (SeqLeft.seqLeft x fun x => y) = do
    let a ← x
    let _ ← y
    pure a
rw [seqLeft_eq]
no goals
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
y : m β
⊢ (Seq.seq (const β <$> x) fun x => y) = do
    let a ← x
    let _ ← y
    pure a
simp [map_eq_pure_bind, seq_eq_bind_map]